diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/thy_syntax.ML --- a/src/ZF/thy_syntax.ML Wed Nov 14 18:46:07 2001 +0100 +++ b/src/ZF/thy_syntax.ML Wed Nov 14 18:46:30 2001 +0100 @@ -10,19 +10,18 @@ open ThyParse; -(*ML identifiers for introduction rules.*) -fun mk_intr_name suffix s = +fun mk_bind suffix s = if ThmDatabase.is_ml_identifier s then - "op " ^ s ^ suffix (*the "op" cancels any infix status*) + "op " ^ s ^ suffix (*the "op" cancels any infix status*) else "_"; (*bad name, don't try to bind*) (*For lists of theorems. Either a string (an ML list expression) or else a list of identifiers.*) -fun optlist s = - optional (s $$-- - (string >> unenclose - || list1 (name>>unenclose) >> mk_list)) +fun optlist s = + optional (s $$-- + (string >> unenclose + || list1 (name>>unenclose) >> mk_list)) "[]"; (*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) @@ -33,42 +32,43 @@ (Scan.any Symbol.is_blank |-- Syntax.scan_id))) |> #1; -(*(Co)Inductive definitions theory section."*) + +(* (Co)Inductive definitions *) + fun inductive_decl coind = - let - fun mk_params ((((((recs, sdom_sum), ipairs), + let + fun mk_params ((((((recs, sdom_sum), ipairs), monos), con_defs), type_intrs), type_elims) = - let val big_rec_name = space_implode "_" + let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs) and srec_tms = mk_list recs and sintrs = mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs) - and inames = mk_list (map (mk_intr_name "" o fst) ipairs) + and inames = mk_list (map (mk_bind "" o fst) ipairs) in - ";\n\n\ - \local\n\ - \val (thy, {defs, intrs, elim, mk_cases, \ - \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\ - \ " ^ - (if coind then "Co" else "") ^ - "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ - sintrs ^ " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ - type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ - \in\n\ - \structure " ^ big_rec_name ^ " =\n\ - \struct\n\ - \ val defs = defs\n\ - \ val bnd_mono = bnd_mono\n\ - \ val dom_subset = dom_subset\n\ - \ val intrs = intrs\n\ - \ val elim = elim\n\ - \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ - \ val mutual_induct = mutual_induct\n\ - \ val mk_cases = mk_cases\n\ - \ val " ^ inames ^ " = intrs\n\ - \end;\n\ - \val thy = thy;\nend;\n\ - \val thy = thy\n" + ";\n\n\ + \local\n\ + \val (thy, {defs, intrs, elim, mk_cases, \ + \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\ + \ " ^ + (if coind then "Co" else "") ^ + "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^ + " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ + \in\n\ + \structure " ^ big_rec_name ^ " =\n\ + \struct\n\ + \ val defs = defs\n\ + \ val bnd_mono = bnd_mono\n\ + \ val dom_subset = dom_subset\n\ + \ val intrs = intrs\n\ + \ val elim = elim\n\ + \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ + \ val mutual_induct = mutual_induct\n\ + \ val mk_cases = mk_cases\n\ + \ val " ^ inames ^ " = intrs\n\ + \end;\n\ + \val thy = thy;\nend;\n\ + \val thy = thy\n" end val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string val ipairs = "intrs" $$-- repeat1 (ident -- !! string) @@ -78,54 +78,53 @@ end; -(*Datatype definitions theory section. co is true for codatatypes*) +(* Datatype definitions *) + fun datatype_decl coind = let - (*generate strings*) fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); val mk_data = mk_list o map mk_const o snd val mk_scons = mk_big_list o map mk_data fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) = let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs - val big_rec_name = space_implode "_" rec_names - and srec_tms = mk_list (map fst rec_pairs) - and scons = mk_scons rec_pairs - val con_names = flat (map (map (unenclose o #1 o #1) o snd) - rec_pairs) - val inames = mk_list (map (mk_intr_name "_I") con_names) + val big_rec_name = space_implode "_" rec_names + and srec_tms = mk_list (map fst rec_pairs) + and scons = mk_scons rec_pairs + val con_names = flat (map (map (unenclose o #1 o #1) o snd) + rec_pairs) + val inames = mk_list (map (mk_bind "_I") con_names) in - ";\n\n\ - \local\n\ - \val (thy,\n\ + ";\n\n\ + \local\n\ + \val (thy,\n\ \ {defs, intrs, elim, mk_cases, \ - \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\ + \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\ \ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\ - \ " ^ - (if coind then "Co" else "") ^ - "Data_Package.add_datatype (" ^ sdom ^ ", " ^ srec_tms ^ ", " ^ - scons ^ ", " ^ monos ^ ", " ^ - type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ - \in\n\ - \structure " ^ big_rec_name ^ " =\n\ - \struct\n\ - \ val defs = defs\n\ - \ val bnd_mono = bnd_mono\n\ - \ val dom_subset = dom_subset\n\ - \ val intrs = intrs\n\ - \ val elim = elim\n\ - \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ - \ val mutual_induct = mutual_induct\n\ - \ val mk_cases = mk_cases\n\ - \ val con_defs = con_defs\n\ - \ val case_eqns = case_eqns\n\ - \ val recursor_eqns = recursor_eqns\n\ - \ val free_iffs = free_iffs\n\ - \ val free_SEs = free_SEs\n\ - \ val mk_free = mk_free\n\ - \ val " ^ inames ^ " = intrs;\n\ - \end;\n\ - \val thy = thy;\nend;\n\ - \val thy = thy\n" + \ " ^ + (if coind then "Co" else "") ^ + "Data_Package.add_datatype_x (" ^ sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^ + " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\ + \in\n\ + \structure " ^ big_rec_name ^ " =\n\ + \struct\n\ + \ val defs = defs\n\ + \ val bnd_mono = bnd_mono\n\ + \ val dom_subset = dom_subset\n\ + \ val intrs = intrs\n\ + \ val elim = elim\n\ + \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\ + \ val mutual_induct = mutual_induct\n\ + \ val mk_cases = mk_cases\n\ + \ val con_defs = con_defs\n\ + \ val case_eqns = case_eqns\n\ + \ val recursor_eqns = recursor_eqns\n\ + \ val free_iffs = free_iffs\n\ + \ val free_SEs = free_SEs\n\ + \ val mk_free = mk_free\n\ + \ val " ^ inames ^ " = intrs;\n\ + \end;\n\ + \val thy = thy;\nend;\n\ + \val thy = thy\n" end val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty; val construct = name -- string_list -- opt_mixfix; @@ -136,6 +135,7 @@ end; + (** rep_datatype **) fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) = @@ -143,27 +143,25 @@ mk_list case_eqns ^ " " ^ mk_list recursor_eqns; val rep_datatype_decl = - (("elim" $$-- ident) -- + (("elim" $$-- ident) -- ("induct" $$-- ident) -- - ("case_eqns" $$-- list1 ident) -- + ("case_eqns" $$-- list1 ident) -- optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string; + (** primrec **) fun mk_primrec_decl eqns = - let val names = map fst eqns - in - ";\nval (thy, " ^ mk_list names ^ - ") = PrimrecPackage.add_primrec " ^ - mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ + let val binds = map (mk_bind "" o fst) eqns in + ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^ + mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\ \val thy = thy\n" end; (* either names and axioms or just axioms *) -val primrec_decl = - ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl; - +val primrec_decl = + ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;