removed obsolete thy_syntax.ML;
authorwenzelm
Wed Oct 19 21:52:48 2005 +0200 (2005-10-19)
changeset 17935c6f1442ce949
parent 17934 ab08250b80df
child 17936 308b19d78764
removed obsolete thy_syntax.ML;
src/ZF/IsaMakefile
src/ZF/ROOT.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/ZF/IsaMakefile	Wed Oct 19 21:52:47 2005 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Oct 19 21:52:48 2005 +0200
     1.3 @@ -45,8 +45,7 @@
     1.4    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     1.5    Trancl.thy Univ.thy \
     1.6    WF.thy ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
     1.7 -  ind_syntax.ML pair.thy simpdata.ML		\
     1.8 -  thy_syntax.ML upair.thy
     1.9 +  ind_syntax.ML pair.thy simpdata.ML upair.thy
    1.10  	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
    1.11  
    1.12  
     2.1 --- a/src/ZF/ROOT.ML	Wed Oct 19 21:52:47 2005 +0200
     2.2 +++ b/src/ZF/ROOT.ML	Wed Oct 19 21:52:48 2005 +0200
     2.3 @@ -13,9 +13,6 @@
     2.4  
     2.5  reset eta_contract;
     2.6  
     2.7 -(*syntax for old-style theory sections*)
     2.8 -use "thy_syntax";
     2.9 -
    2.10  with_path "Integ" use_thy "Main_ZFC";
    2.11  
    2.12  Goal "True";  (*leave subgoal package empty*)
     3.1 --- a/src/ZF/thy_syntax.ML	Wed Oct 19 21:52:47 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,184 +0,0 @@
     3.4 -(*  Title:      ZF/thy_syntax.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson
     3.7 -    Copyright   1994  University of Cambridge
     3.8 -
     3.9 -Additional sections for *old-style* theory files in ZF.
    3.10 -*)
    3.11 -
    3.12 -local
    3.13 -
    3.14 -open ThyParse;
    3.15 -
    3.16 -fun mk_bind suffix s =
    3.17 -    if ThmDatabase.is_ml_identifier s then
    3.18 -        "op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    3.19 -    else "_";               (*bad name, don't try to bind*)
    3.20 -
    3.21 -
    3.22 -(*For lists of theorems.  Either a string (an ML list expression) or else
    3.23 -  a list of identifiers.*)
    3.24 -fun optlist s =
    3.25 -    optional (s $$--
    3.26 -              (string >> unenclose
    3.27 -               || list1 (name>>unenclose) >> mk_list))
    3.28 -    "[]";
    3.29 -
    3.30 -(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
    3.31 -fun scan_to_id s =
    3.32 -    s |> Symbol.explode
    3.33 -    |> Scan.error (Scan.finite Symbol.stopper
    3.34 -      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
    3.35 -        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    3.36 -    |> #1;
    3.37 -
    3.38 -
    3.39 -(* (Co)Inductive definitions *)
    3.40 -
    3.41 -fun inductive_decl coind =
    3.42 -  let
    3.43 -    fun mk_params ((((((recs, sdom_sum), ipairs),
    3.44 -                      monos), con_defs), type_intrs), type_elims) =
    3.45 -      let val big_rec_name = space_implode "_"
    3.46 -                           (map (scan_to_id o unenclose) recs)
    3.47 -          and srec_tms = mk_list recs
    3.48 -          and sintrs   =
    3.49 -            mk_big_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) ipairs)
    3.50 -          and inames   = mk_list (map (mk_bind "" o fst) ipairs)
    3.51 -      in
    3.52 -         ";\n\n\
    3.53 -         \local\n\
    3.54 -         \val (thy, {defs, intrs, elim, mk_cases, \
    3.55 -                    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
    3.56 -         \  " ^
    3.57 -         (if coind then "Co" else "") ^
    3.58 -         "Ind_Package.add_inductive_x (" ^  srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^
    3.59 -           " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
    3.60 -         \in\n\
    3.61 -         \structure " ^ big_rec_name ^ " =\n\
    3.62 -         \struct\n\
    3.63 -         \  val defs = defs\n\
    3.64 -         \  val bnd_mono = bnd_mono\n\
    3.65 -         \  val dom_subset = dom_subset\n\
    3.66 -         \  val intrs = intrs\n\
    3.67 -         \  val elim = elim\n\
    3.68 -         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
    3.69 -         \  val mutual_induct = mutual_induct\n\
    3.70 -         \  val mk_cases = mk_cases\n\
    3.71 -         \  val " ^ inames ^ " = intrs\n\
    3.72 -         \end;\n\
    3.73 -         \val thy = thy;\nend;\n\
    3.74 -         \val thy = thy\n"
    3.75 -      end
    3.76 -    val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
    3.77 -    val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
    3.78 -  in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
    3.79 -             -- optlist "type_intrs" -- optlist "type_elims"
    3.80 -     >> mk_params
    3.81 -  end;
    3.82 -
    3.83 -
    3.84 -(* Datatype definitions *)
    3.85 -
    3.86 -fun datatype_decl coind =
    3.87 -  let
    3.88 -    fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
    3.89 -    val mk_data = mk_list o map mk_const o snd
    3.90 -    val mk_scons = mk_big_list o map mk_data
    3.91 -    fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
    3.92 -      let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
    3.93 -          val big_rec_name = space_implode "_" rec_names
    3.94 -          and srec_tms = mk_list (map fst rec_pairs)
    3.95 -          and scons    = mk_scons rec_pairs
    3.96 -          val con_names = List.concat (map (map (unenclose o #1 o #1) o snd)
    3.97 -                                rec_pairs)
    3.98 -          val inames = mk_list (map (mk_bind "_I") con_names)
    3.99 -      in
   3.100 -         ";\n\n\
   3.101 -         \local\n\
   3.102 -         \val (thy,\n\
   3.103 -         \     {defs, intrs, elim, mk_cases, \
   3.104 -                    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
   3.105 -         \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
   3.106 -         \  " ^
   3.107 -         (if coind then "Co" else "") ^
   3.108 -         "Data_Package.add_datatype_x (" ^  sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^
   3.109 -           " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   3.110 -         \in\n\
   3.111 -         \structure " ^ big_rec_name ^ " =\n\
   3.112 -         \struct\n\
   3.113 -         \  val defs = defs\n\
   3.114 -         \  val bnd_mono = bnd_mono\n\
   3.115 -         \  val dom_subset = dom_subset\n\
   3.116 -         \  val intrs = intrs\n\
   3.117 -         \  val elim = elim\n\
   3.118 -         \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   3.119 -         \  val mutual_induct = mutual_induct\n\
   3.120 -         \  val mk_cases = mk_cases\n\
   3.121 -         \  val con_defs = con_defs\n\
   3.122 -         \  val case_eqns = case_eqns\n\
   3.123 -         \  val recursor_eqns = recursor_eqns\n\
   3.124 -         \  val free_iffs = free_iffs\n\
   3.125 -         \  val free_SEs = free_SEs\n\
   3.126 -         \  val mk_free = mk_free\n\
   3.127 -         \  val " ^ inames ^ " = intrs;\n\
   3.128 -         \end;\n\
   3.129 -         \val thy = thy;\nend;\n\
   3.130 -         \val thy = thy\n"
   3.131 -      end
   3.132 -    val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   3.133 -    val construct = name -- string_list -- opt_mixfix;
   3.134 -  in optional ("<=" $$-- string) "\"\"" --
   3.135 -     enum1 "and" (name --$$ "=" -- enum1 "|" construct) --
   3.136 -     optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
   3.137 -     >> mk_params
   3.138 -end;
   3.139 -
   3.140 -
   3.141 -
   3.142 -(** rep_datatype **)
   3.143 -
   3.144 -fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
   3.145 -  "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n    " ^
   3.146 -  mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
   3.147 -
   3.148 -val rep_datatype_decl =
   3.149 -  (("elim" $$-- ident) --
   3.150 -   ("induct" $$-- ident) --
   3.151 -   ("case_eqns" $$-- list1 ident) --
   3.152 -   optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
   3.153 -
   3.154 -
   3.155 -
   3.156 -(** primrec **)
   3.157 -
   3.158 -fun mk_primrec_decl eqns =
   3.159 -  let val binds = map (mk_bind "" o fst) eqns in
   3.160 -    ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
   3.161 -      mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst Library.quote) eqns)) ^ " " ^ " thy;\n\
   3.162 -    \val thy = thy\n"
   3.163 -  end;
   3.164 -
   3.165 -(* either names and axioms or just axioms *)
   3.166 -val primrec_decl =
   3.167 -    ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
   3.168 -
   3.169 -
   3.170 -
   3.171 -(** augment thy syntax **)
   3.172 -
   3.173 -in
   3.174 -
   3.175 -val _ = ThySyn.add_syntax
   3.176 - ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
   3.177 -  "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims",
   3.178 -  (*rep_datatype*)
   3.179 -  "elim", "induct", "case_eqns", "recursor_eqns"]
   3.180 - [section "inductive"    "" (inductive_decl false),
   3.181 -  section "coinductive"  "" (inductive_decl true),
   3.182 -  section "datatype"     "" (datatype_decl false),
   3.183 -  section "codatatype"   "" (datatype_decl true),
   3.184 -  section "rep_datatype" "" rep_datatype_decl,
   3.185 -  section "primrec"      "" primrec_decl];
   3.186 -
   3.187 -end;