# HG changeset patch # User clasohm # Date 773053422 -7200 # Node ID 3ca9d49fd662f69c18f5d35a90e7357d1ab421b7 # Parent 10884e64c241e7dbc4edaff00d6bd3a61a2f3303 replaced extend_theory by new add_* functions; changed syntax of datatype declaration diff -r 10884e64c241 -r 3ca9d49fd662 src/ZF/Fin.ML --- a/src/ZF/Fin.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/Fin.ML Fri Jul 01 11:03:42 1994 +0200 @@ -16,7 +16,7 @@ *) structure Fin = Inductive_Fun - (val thy = Arith.thy addconsts [(["Fin"],"i=>i")] + (val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)] val rec_doms = [("Fin","Pow(A)")] val sintrs = ["0 : Fin(A)", "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"] diff -r 10884e64c241 -r 3ca9d49fd662 src/ZF/List.ML --- a/src/ZF/List.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/List.ML Fri Jul 01 11:03:42 1994 +0200 @@ -9,10 +9,9 @@ structure List = Datatype_Fun (val thy = Univ.thy val rec_specs = [("list", "univ(A)", - [(["Nil"], "i"), - (["Cons"], "[i,i]=>i")])] + [(["Nil"], "i", NoSyn), + (["Cons"], "[i,i]=>i", NoSyn)])] val rec_styp = "i=>i" - val ext = None val sintrs = ["Nil : list(A)", "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"] val monos = [] diff -r 10884e64c241 -r 3ca9d49fd662 src/ZF/constructor.ML --- a/src/ZF/constructor.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/constructor.ML Fri Jul 01 11:03:42 1994 +0200 @@ -22,10 +22,9 @@ signature CONSTRUCTOR = sig val thy : theory (*parent theory*) - val rec_specs : (string * string * (string list * string)list) list + val rec_specs : (string * string * (string list * string * mixfix)list) list (*recursion ops, types, domains, constructors*) val rec_styp : string (*common type of all recursion ops*) - val ext : Syntax.sext option (*syntax extension for new theory*) val sintrs : string list (*desired introduction rules*) val monos : thm list (*monotonicity of each M operator*) val type_intrs : thm list (*type-checking intro rules*) @@ -63,15 +62,21 @@ (fn a => "Name of recursive set not an identifier: " ^ a); (*Expands multiple constant declarations*) -fun pairtypes (cs,st) = map (rpair st) cs; +fun flatten_consts ((names, typ, mfix) :: cs) = + let fun mk_const name = (name, typ, mfix) + in (map mk_const names) @ (flatten_consts cs) end + | flatten_consts [] = []; (*Constructors with types and arguments*) fun mk_con_ty_list cons_pairs = - let fun mk_con_ty (a,st) = - let val T = rdty st - val args = mk_frees "xa" (binder_types T) - in (a,T,args) end - in map mk_con_ty (flat (map pairtypes cons_pairs)) end; + let fun mk_con_ty (a, st, syn) = + let val T = rdty st; + val args = mk_frees "xa" (binder_types T); + val name = const_name a syn; (* adds "op" to infix constructors*) + in (name, T, args) end; + + fun pairtypes c = flatten_consts [c]; + in map mk_con_ty (flat (map pairtypes cons_pairs)) end; val con_ty_lists = map (mk_con_ty_list o #3) rec_specs; @@ -87,8 +92,8 @@ (*Make constructor definition*) fun mk_con_defs (kpart, con_ty_list) = - let val ncon = length con_ty_list (*number of constructors*) - fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*) + let val ncon = length con_ty_list (*number of constructors*) + fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*) mk_defpair sign (list_comb (Const(a,T), args), mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args))) @@ -107,7 +112,7 @@ (*Treatment of a single constructor*) fun add_case ((a,T,args), (opno,cases)) = - if Syntax.is_identifier a + if Syntax.is_identifier a then (opno, (Free(case_name ^ "_" ^ a, T), args) :: cases) else (opno+1, @@ -142,13 +147,15 @@ val axpairs = big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists)); -val const_decs = remove_mixfixes ext - (([big_case_name], flatten_typ sign big_case_typ) :: - (big_rec_name ins rec_names, rec_styp) :: +val const_decs = flatten_consts + (([big_case_name], flatten_typ sign big_case_typ, NoSyn) :: + (big_rec_name ins rec_names, rec_styp, NoSyn) :: flat (map #3 rec_specs)); -val con_thy = extend_theory thy (big_rec_name ^ "_Constructors") - ([], [], [], [], [], const_decs, ext) axpairs; +val con_thy = thy + |> add_consts const_decs + |> add_axioms axpairs + |> add_thyname (big_rec_name ^ "_Constructors"); (*1st element is the case definition; others are the constructors*) val con_defs = map (get_axiom con_thy o #1) axpairs; diff -r 10884e64c241 -r 3ca9d49fd662 src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/ind_syntax.ML Fri Jul 01 11:03:42 1994 +0200 @@ -14,14 +14,6 @@ end; fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t); -(*Add constants to a theory*) -infix addconsts; -fun thy addconsts const_decs = - extend_theory thy (space_implode "_" (flat (map #1 const_decs)) - ^ "_Theory") - ([], [], [], [], [], const_decs, None) []; - - (*Make a definition, lhs==rhs, checking that vars on lhs contain *) fun mk_defpair sign (lhs,rhs) = let val Const(name,_) = head_of lhs diff -r 10884e64c241 -r 3ca9d49fd662 src/ZF/intr_elim.ML --- a/src/ZF/intr_elim.ML Wed Jun 29 12:13:03 1994 +0200 +++ b/src/ZF/intr_elim.ML Fri Jul 01 11:03:42 1994 +0200 @@ -207,8 +207,10 @@ | _ => rec_tms ~~ (*define the sets as Parts*) map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); -val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive") - ([], [], [], [], [], [], None) axpairs; +val thy = + Ind.thy + |> add_axioms axpairs + |> add_thyname (big_rec_name ^ "_Inductive"); val defs = map (get_axiom thy o #1) axpairs;