
diff -r 6a133abb7633 -r 212f3ab40cc2 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Feb 26 18:38:25 2010 +0100
+++ b/Nominal/Parser.thy	Sat Feb 27 11:54:59 2010 +0100
@@ -137,8 +137,6 @@
 end 
 *}
 
-ML {* Primrec.add_primrec *}
-
 ML {*
 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
@@ -161,7 +159,7 @@
   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 => 
+  val bn_eqs' = map (fn (_, trm) => 
     (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
 in
   if null bn_eqs 
@@ -171,7 +169,7 @@
 *}
 
 ML {* 
-fun nominal_datatype2 dts bn_funs bn_eqs lthy =
+fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
 in
@@ -181,30 +179,70 @@
 end
 *}
 
-ML {*
-fun get_constrs2 lthy dts =
+
+ML {* 
+(* parsing the datatypes and declaring *)
+(* constructors in the local theory    *)
+fun prepare_dts dt_strs lthy = 
 let
   val thy = ProofContext.theory_of lthy
+  
+  fun mk_type full_tname tvrs =
+    Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)
 
-  (* 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)
+  fun prep_cnstr lthy full_tname tvs (cname, anno_tys, mx, _) =
+  let
+    val tys = map (Syntax.read_typ lthy o snd) anno_tys
+    val ty = mk_type full_tname tvs
+  in
+    ((cname, tys ---> ty, mx), (cname, tys, mx))
+  end
+  
+  fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
+  let
+    val full_tname = Sign.full_name thy tname
+    val (cnstrs', cnstrs'') = 
+      split_list (map (prep_cnstr lthy full_tname tvs) cnstrs)
+  in
+    (cnstrs', (tvs, tname, mx, cnstrs''))
+  end 
 
-  val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
+  val (cnstrs, dts) = 
+    split_list (map (prep_dt lthy) dt_strs)
 in
-  flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
+  lthy
+  |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+  |> pair dts
 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 {*
+(* parsing the function specification and *)
+(* declaring the functions in the local theory *)
+fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
+let
+  fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
+
+  val ((bn_funs, bn_eqs), _) = 
+    Specification.read_spec bn_fun_strs bn_eq_strs lthy
+
+  val bn_funs' = map prep_bn_fun bn_funs
+in
+  lthy
+  |> Local_Theory.theory (Sign.add_consts_i bn_funs')
+  |> pair (bn_funs', bn_eqs) 
+end 
 *}
 
 ML {*
+fun forth (_, _, _, x) = x
+
+fun find_all eq [] _ = []
+  | find_all eq ((key, value)::xs) key' = 
+      let
+        val values = find_all eq xs key'
+      in if eq (key', key) then value :: values else values end;
+
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
@@ -221,79 +259,55 @@
 *}
 
 ML {*
-fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+fun prepare_binds dt_strs lthy = 
 let
-  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
-
-  (* adding the types for parsing datatypes *)
-  val lthy_tmp1 = lthy
-    |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
-
-  (* parsing the datatypes *)
-  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_tmp1
-    |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep))
-
-  (* 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 
-
-  (* adding functions for parsing binders *)
-  val lthy_tmp3 = lthy_tmp2
-    |> Local_Theory.theory (Sign.add_consts_i bn_fun_prep)
-
-  (* parsing the binding structure *)
-  val binds = 
-    let
-      fun prep_bn env str =
-        (case Syntax.read_term lthy_tmp3 str of
+  fun prep_bn env str =
+        (case Syntax.read_term lthy 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."))   
+         | x => error (str ^ " not allowed as binding specification."))   
  
-      fun prep_typ env (opt_name, _) = 
+  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)
+  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
-  nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd 
+  map ((map prep_binds) o forth) dt_strs
 end
 *}
 
+ML {*
+fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+let
+  val t = start_timing ()
+
+  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
+
+  val ((dts, (bn_fun, bn_eq)), binds) = 
+    lthy 
+    |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
+    |> prepare_dts dt_strs
+    ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
+    ||> prepare_binds dt_strs
+  
+  val _ = tracing (PolyML.makestring binds)
+  val _ = tracing (#message (end_timing t))
+in
+  nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
+end
+*}
+
+
 (* Command Keyword *)
 
-
 ML {*
 let
    val kind = OuterKeyword.thy_decl




