share more code between definitional and axiomatic domain packages
authorhuffman
Mon, 12 Apr 2010 16:04:32 -0700
changeset 36118 413d6d1f0f6e
parent 36117 01a9db7382f5
child 36119 ff605b8fdfdb
share more code between definitional and axiomatic domain packages
src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 15:05:42 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 16:04:32 2010 -0700
@@ -125,84 +125,12 @@
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
+type info =
+     Domain_Take_Proofs.iso_info list * Domain_Take_Proofs.take_induct_info;
+
 fun gen_add_domain
     (prep_typ : theory -> 'a -> typ)
-    (comp_dbind : binding)
-    (eqs''' : ((string * string option) list * binding * mixfix *
-               (binding * (bool * binding option * 'a) list * mixfix) list) list)
-    (thy : theory) =
-  let
-    val dtnvs : (binding * typ list * mixfix) list =
-      let
-        fun readS (SOME s) = Syntax.read_sort_global thy s
-          | readS NONE = Sign.defaultS thy;
-        fun readTFree (a, s) = TFree (a, readS s);
-      in
-        map (fn (vs,dname:binding,mx,_) =>
-                (dname, map readTFree vs, mx)) eqs'''
-      end;
-
-    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
-    fun thy_arity (dname,tvars,mx) =
-      (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep});
-
-    (* this theory is used just for parsing and error checking *)
-    val tmp_thy = thy
-      |> Theory.copy
-      |> Sign.add_types (map thy_type dtnvs)
-      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
-
-    val dbinds : binding list =
-        map (fn (_,dbind,_,_) => dbind) eqs''';
-    val cons''' :
-        (binding * (bool * binding option * 'a) list * mixfix) list list =
-        map (fn (_,_,_,cons) => cons) eqs''';
-    val cons'' :
-        (binding * (bool * binding option * typ) list * mixfix) list list =
-        map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
-    val dtnvs' : (string * typ list) list =
-      map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
-    val eqs' : ((string * typ list) *
-        (binding * (bool * binding option * typ) list * mixfix) list) list =
-        check_and_sort_domain false dtnvs' cons'' tmp_thy;
-    val dts : typ list = map (Type o fst) eqs';
-    val new_dts : (string * string list) list =
-        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun one_con (con,args,mx) : cons =
-        (Binding.name_of con,  (* FIXME preverse binding (!?) *)
-         ListPair.map (fn ((lazy,sel,tp),vn) =>
-           mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
-                      (args, Datatype_Prop.make_tnames (map third args)));
-    val eqs : eq list =
-        map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-
-    fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
-    fun mk_con_typ (bind, args, mx) =
-        if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
-    fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
-    val repTs : typ list = map mk_eq_typ eqs';
-
-    val ((iso_infos, take_info), thy) = thy |>
-        Domain_Axioms.add_axioms
-          (map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
-            (dtnvs ~~ (dts ~~ repTs)));
-
-    val ((rewss, take_rews), theorems_thy) =
-        thy
-          |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
-                Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
-             (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
-          ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
-  in
-    theorems_thy
-      |> PureThy.add_thmss
-           [((Binding.qualified true "rews" comp_dbind,
-              flat rewss @ take_rews), [])]
-      |> snd
-  end;
-
-fun gen_add_new_domain
-    (prep_typ : theory -> 'a -> typ)
+    (add_isos : (binding * mixfix * (typ * typ)) list -> theory -> info * theory)
     (comp_dbind : binding)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
@@ -241,33 +169,34 @@
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
         check_and_sort_domain true dtnvs' cons'' tmp_thy;
+    val dts : typ list = map (Type o fst) eqs';
 
     fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
     fun mk_con_typ (bind, args, mx) =
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
-    
-    val ((iso_infos, take_info), thy) = thy |>
-      Domain_Isomorphism.domain_isomorphism
-        (map (fn ((vs, dname, mx, _), eq) =>
-                 (map fst vs, dname, mx, mk_eq_typ eq, NONE))
-             (eqs''' ~~ eqs'))
+    val repTs : typ list = map mk_eq_typ eqs';
 
-    val dts : typ list = map (Type o fst) eqs';
+    val iso_spec : (binding * mixfix * (typ * typ)) list =
+        map (fn ((dbind, _, mx), eq) => (dbind, mx, eq))
+          (dtnvs ~~ (dts ~~ repTs));
+
+    val ((iso_infos, take_info), thy) = add_isos iso_spec thy;
+
     val new_dts : (string * string list) list =
         map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun one_con (con,args,mx) : cons =
-        (Binding.name_of con,   (* FIXME preverse binding (!?) *)
+        (Binding.name_of con,  (* FIXME preverse binding (!?) *)
          ListPair.map (fn ((lazy,sel,tp),vn) =>
            mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
-                      (args, Datatype_Prop.make_tnames (map third args))
-        );
+                      (args, Datatype_Prop.make_tnames (map third args)));
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
+
     val ((rewss, take_rews), theorems_thy) =
         thy
-          |> fold_map (fn (((dbind, eq), (x,cs)), info) =>
-               Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
+          |> fold_map (fn (((dbind, eq), (_,cs)), info) =>
+                Domain_Theorems.theorems (eq, eqs) dbind cs info take_info)
              (dbinds ~~ eqs ~~ eqs' ~~ iso_infos)
           ||>> Domain_Theorems.comp_theorems (comp_dbind, eqs) take_info;
   in
@@ -278,11 +207,26 @@
       |> snd
   end;
 
-val add_domain = gen_add_domain Sign.certify_typ;
-val add_domain_cmd = gen_add_domain Syntax.read_typ_global;
+fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
+  let
+    fun prep (dbind, mx, (lhsT, rhsT)) =
+      let val (dname, vs) = dest_Type lhsT;
+      in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end;
+  in
+    Domain_Isomorphism.domain_isomorphism (map prep spec)
+  end;
 
-val add_new_domain = gen_add_new_domain Sign.certify_typ;
-val add_new_domain_cmd = gen_add_new_domain Syntax.read_typ_global;
+val add_domain =
+    gen_add_domain Sign.certify_typ Domain_Axioms.add_axioms;
+
+val add_new_domain =
+    gen_add_domain Sign.certify_typ define_isos;
+
+val add_domain_cmd =
+    gen_add_domain Syntax.read_typ_global Domain_Axioms.add_axioms;
+
+val add_new_domain_cmd =
+    gen_add_domain Syntax.read_typ_global define_isos;
 
 
 (** outer syntax **)