
diff -r ea46a354f382 -r 6a133abb7633 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Feb 26 18:21:39 2010 +0100
+++ b/Nominal/Parser.thy	Fri Feb 26 18:38:25 2010 +0100
@@ -31,6 +31,10 @@
           (Trueprop equations)
 *}
 
+ML {*
+
+*}
+
 text {*****************************************************}
 ML {* 
 (* nominal datatype parser *)
@@ -38,6 +42,7 @@
   structure P = OuterParse
 
   fun tuple ((x, y, z), u) = (x, y, z, u)
+  fun tswap (((x, y), z), u) = (x, y, u, z)
 in
 
 val _ = OuterKeyword.keyword "bind"
@@ -46,15 +51,15 @@
 (* binding specification *)
 (* maybe use and_list *)
 val bind_parser = 
-  P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
+  P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap)
 
 val constr_parser =
   P.binding -- Scan.repeat anno_typ
 
 (* datatype parser *)
 val dt_parser =
-  (P.type_args -- P.binding -- P.opt_infix >> P.triple1) -- 
-    (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple
+  (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) -- 
+    (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple
 
 (* function equation parser *)
 val fun_parser = 
@@ -132,6 +137,8 @@
 end 
 *}
 
+ML {* Primrec.add_primrec *}
+
 ML {*
 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
@@ -151,8 +158,8 @@
   val bn_fun_strs' = add_raws bn_fun_strs
   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
   
-  val bn_funs' = map (fn (bn, opt_ty, mx) => 
-    (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs
+  val bn_funs' = map (fn (bn, ty, mx) => 
+    (raw_bind bn, SOME (replace_typ dt_env ty), mx)) bn_funs
   
   val bn_eqs' = map (fn trm => 
     (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
@@ -175,8 +182,10 @@
 *}
 
 ML {*
-fun get_constrs2 thy dts =
+fun get_constrs2 lthy dts =
 let
+  val thy = ProofContext.theory_of lthy
+
   (* makes a full named type out of a binding with tvars applied to it *)
   fun mk_type thy bind tvrs =
     Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs)
@@ -187,44 +196,104 @@
 end
 *}
 
+ML {* 
+fun find_all _ [] _ = []
+  | find_all eq ((y, z)::xs) x = 
+      if eq (x, y) 
+      then z::find_all eq xs x 
+      else find_all eq xs x 
+*}
+
+ML {*
+fun mk_env xs =
+  let
+    fun mapp (_: int) [] = []
+      | mapp i ((a, _) :: xs) = 
+         case a of
+           NONE => mapp (i + 1) xs
+         | SOME x => (x, i) :: mapp (i + 1) xs
+  in mapp 0 xs end
+
+fun env_lookup xs x =
+  case AList.lookup (op =) xs x of
+    SOME x => x
+  | NONE => error ("cannot find " ^ x ^ " in the binding specification.")  
+*}
+
 ML {*
 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
 let
-  val thy = ProofContext.theory_of lthy
-
   fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
 
   (* adding the types for parsing datatypes *)
-  val lthy_tmp = lthy
+  val lthy_tmp1 = lthy
     |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
 
-  fun prep_cnstr lthy (((cname, atys), mx), binders) =
-    (cname, map (Syntax.read_typ lthy o snd) atys, mx)
-  
-  fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
-    (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
-
   (* parsing the datatypes *)
-  val dts_prep = map (prep_dt lthy_tmp) dt_strs
-
+  val dts_prep = 
+    let
+      fun prep_cnstr lthy (cname, anno_tys, mx, _) =
+        (cname, map (Syntax.read_typ lthy o snd) anno_tys, mx)
+  
+      fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
+        (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
+    in
+      map (prep_dt lthy_tmp1) dt_strs
+    end
+ 
   (* adding constructors for parsing functions *)
-  val lthy_tmp2 = lthy_tmp
-    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep))
+  val lthy_tmp2 = lthy_tmp1
+    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep))
 
-  val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
+  (* parsing the function specification *)
+  val (bn_fun_prep, bn_eq_prep) =
+    let 
+      val ((bn_fun_aux, bn_eq_aux), _) = Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2
+
+      fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
+      fun prep_bn_eq (attr, t) = t
+    in
+      (map prep_bn_fun bn_fun_aux, map prep_bn_eq bn_eq_aux)
+    end 
 
-  fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) 
-
-  fun prep_bn_eq (attr, t) = t
+  (* adding functions for parsing binders *)
+  val lthy_tmp3 = lthy_tmp2
+    |> Local_Theory.theory (Sign.add_consts_i bn_fun_prep)
 
-  val bn_fun_prep = map prep_bn_fun bn_fun_aux
-  val bn_eq_prep = map prep_bn_eq bn_eq_aux 
+  (* parsing the binding structure *)
+  val binds = 
+    let
+      fun prep_bn env str =
+        (case Syntax.read_term lthy_tmp3 str of
+           Free (x, _) => (env_lookup env x, NONE)
+         | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
+         | _ => error (str ^ " not allowed as binding specification."))   
+ 
+      fun prep_typ env (opt_name, _) = 
+        (case opt_name of
+           NONE => []
+         | SOME x => find_all (op=) env x)
+        
+      fun prep_binds (_, anno_tys, _, bind_strs) = 
+      let
+        val env = mk_env anno_tys
+        val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
+      in
+        map (prep_typ binds) anno_tys
+      end
+    in
+      map ((map prep_binds) o #4) dt_strs
+    end
+
+    val _ = tracing (PolyML.makestring binds)
 in
-  nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
+  nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd 
 end
 *}
 
 (* Command Keyword *)
+
+
 ML {*
 let
    val kind = OuterKeyword.thy_decl




