# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1267095094 -3600
# Node ID b0a120469041eaa830c09732c340be2ab466caa5
# Parent  fc8f5897b00a591d13df379e00f196fda3d86cfd
a few simplifications

diff -r fc8f5897b00a -r b0a120469041 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Feb 25 11:30:00 2010 +0100
+++ b/Nominal/Parser.thy	Thu Feb 25 11:51:34 2010 +0100
@@ -11,24 +11,21 @@
 
 Nominal-Datatype-part:
 
-1st Arg: string list  
-         ^^^^^^^^^^^
-         strings of the types to be defined
 
-2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
+1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
                type(s) to be defined             constructors list
                (ty args, name, syn)              (name, typs, syn)
 
 Binder-Function-part:
 
-3rd Arg: (binding * typ option * mixfix) list 
+2rd Arg: (binding * typ option * mixfix) list 
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^    
             binding function(s)           
               to be defined               
             (name, type, syn)             
 
-4th Arg:  term list 
+3th Arg:  term list 
           ^^^^^^^^^
           the equations of the binding functions
           (Trueprop equations)
@@ -39,13 +36,15 @@
 (* nominal datatype parser *)
 local
   structure P = OuterParse
+
+  fun tuple ((x, y, z), u) = (x, y, z, u)
 in
 
 val _ = OuterKeyword.keyword "bind"
 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
 
 (* binding specification *)
-(* should use and_list *)
+(* maybe use and_list *)
 val bind_parser = 
   P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
 
@@ -54,8 +53,8 @@
 
 (* 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))
+  (P.type_args -- P.binding -- P.opt_infix >> P.triple1) -- 
+    (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple
 
 (* function equation parser *)
 val fun_parser = 
@@ -63,7 +62,7 @@
 
 (* main parser *)
 val main_parser =
-  (P.and_list1 dt_parser) -- fun_parser
+  (P.and_list1 dt_parser) -- fun_parser >> P.triple2
 
 end
 *}
@@ -141,20 +140,22 @@
   val dt_names' = add_raws dt_names
   val dt_full_names = map (Sign.full_bname thy) dt_names 
   val dt_full_names' = map (Sign.full_bname thy) dt_names' 
+  val dt_env = dt_full_names ~~ dt_full_names'
   
   val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts)
   val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y))) 
     (get_typed_constrs dts)
+  val ctrs_env = ctrs_names ~~ ctrs_names'
 
   val bn_fun_strs = get_bn_fun_strs bn_funs
   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_eqs' = map (fn trm => 
-    (Attrib.empty_binding, 
-      (replace_term ((ctrs_names ~~ ctrs_names') @ (bn_fun_strs ~~ bn_fun_strs')) (dt_full_names ~~ dt_full_names') trm))) bn_eqs
+    (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
 in
   if null bn_eqs 
   then (([], []), lthy)
@@ -174,12 +175,12 @@
 *}
 
 ML {*
-(* 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 get_constrs2 thy dts =
 let
+  (* 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)
+
   val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
 in
   flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
@@ -187,11 +188,11 @@
 *}
 
 ML {*
-fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
+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);
+  fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
 
   (* adding the types for parsing datatypes *)
   val lthy_tmp = lthy
@@ -200,7 +201,7 @@
   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) = 
+  fun prep_dt lthy (tvs, tname, mx, cnstrs) = 
     (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
 
   (* parsing the datatypes *)