# HG changeset patch # User wenzelm # Date 1129751568 -7200 # Node ID c6f1442ce949f415a10a7e97d546f572139d8952 # Parent ab08250b80dfbd076dfb3b145ec818f07cd1b4e9 removed obsolete thy_syntax.ML; diff -r ab08250b80df -r c6f1442ce949 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed Oct 19 21:52:47 2005 +0200 +++ b/src/ZF/IsaMakefile Wed Oct 19 21:52:48 2005 +0200 @@ -45,8 +45,7 @@ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ Trancl.thy Univ.thy \ WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy \ - ind_syntax.ML pair.thy simpdata.ML \ - thy_syntax.ML upair.thy + ind_syntax.ML pair.thy simpdata.ML upair.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF diff -r ab08250b80df -r c6f1442ce949 src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Wed Oct 19 21:52:47 2005 +0200 +++ b/src/ZF/ROOT.ML Wed Oct 19 21:52:48 2005 +0200 @@ -13,9 +13,6 @@ reset eta_contract; -(*syntax for old-style theory sections*) -use "thy_syntax"; - with_path "Integ" use_thy "Main_ZFC"; Goal "True"; (*leave subgoal package empty*) diff -r ab08250b80df -r c6f1442ce949 src/ZF/thy_syntax.ML --- a/src/ZF/thy_syntax.ML Wed Oct 19 21:52:47 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,184 +0,0 @@ -(* Title: ZF/thy_syntax.ML - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1994 University of Cambridge - -Additional sections for *old-style* theory files in ZF. -*) - -local - -open ThyParse; - -fun mk_bind suffix s = - if ThmDatabase.is_ml_identifier s then - "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)) - "[]"; - -(*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) -fun scan_to_id s = - s |> Symbol.explode - |> Scan.error (Scan.finite Symbol.stopper - (Scan.!! (fn _ => "Expected to find an identifier in " ^ s) - (Scan.any Symbol.is_blank |-- Syntax.scan_id))) - |> #1; - - -(* (Co)Inductive definitions *) - -fun inductive_decl coind = - let - fun mk_params ((((((recs, sdom_sum), ipairs), - monos), con_defs), type_intrs), type_elims) = - 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 (Library.quote x, y), "[]")) 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" - end - val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string - val ipairs = "intrs" $$-- repeat1 (ident -- !! string) - in domains -- ipairs -- optlist "monos" -- optlist "con_defs" - -- optlist "type_intrs" -- optlist "type_elims" - >> mk_params - end; - - -(* Datatype definitions *) - -fun datatype_decl coind = - let - 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 = List.concat (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\ - \ {defs, intrs, elim, mk_cases, \ - \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_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; - in optional ("<=" $$-- string) "\"\"" -- - enum1 "and" (name --$$ "=" -- enum1 "|" construct) -- - optlist "monos" -- optlist "type_intrs" -- optlist "type_elims" - >> mk_params -end; - - - -(** rep_datatype **) - -fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) = - "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n " ^ - mk_list case_eqns ^ " " ^ mk_list recursor_eqns; - -val rep_datatype_decl = - (("elim" $$-- ident) -- - ("induct" $$-- ident) -- - ("case_eqns" $$-- list1 ident) -- - optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string; - - - -(** primrec **) - -fun mk_primrec_decl eqns = - 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 Library.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; - - - -(** augment thy syntax **) - -in - -val _ = ThySyn.add_syntax - ["inductive", "coinductive", "datatype", "codatatype", "and", "|", - "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims", - (*rep_datatype*) - "elim", "induct", "case_eqns", "recursor_eqns"] - [section "inductive" "" (inductive_decl false), - section "coinductive" "" (inductive_decl true), - section "datatype" "" (datatype_decl false), - section "codatatype" "" (datatype_decl true), - section "rep_datatype" "" rep_datatype_decl, - section "primrec" "" primrec_decl]; - -end;