src/ZF/thy_syntax.ML
author wenzelm
Wed May 12 17:26:56 1999 +0200 (1999-05-12)
changeset 6642 732af87c0650
parent 6112 5e4871c5136b
child 8127 68c6159440f1
permissions -rw-r--r--
strip_quotes replaced by unenclose;
     1 (*  Title:      ZF/thy_syntax.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1994  University of Cambridge
     5 
     6 Additional theory file sections for ZF.
     7 *)
     8 
     9 
    10 local
    11 
    12 
    13 open ThyParse;
    14 
    15 (*ML identifiers for introduction rules.*)
    16 fun mk_intr_name suffix s =  
    17     if ThmDatabase.is_ml_identifier s then
    18 	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    19     else "_";               (*bad name, don't try to bind*)
    20 
    21 
    22 (*For lists of theorems.  Either a string (an ML list expression) or else
    23   a list of identifiers.*)
    24 fun optlist s = 
    25     optional (s $$-- 
    26 	      (string >> unenclose
    27 	       || list1 (name>>unenclose) >> mk_list)) 
    28     "[]";
    29 
    30 
    31 (*(Co)Inductive definitions theory section."*)
    32 fun inductive_decl coind =
    33   let  
    34     fun mk_params ((((((recs, sdom_sum), ipairs), 
    35                       monos), con_defs), type_intrs), type_elims) =
    36       let val big_rec_name = space_implode "_" 
    37                            (map (scan_to_id o unenclose) recs)
    38           and srec_tms = mk_list recs
    39           and sintrs   = mk_big_list (map snd ipairs)
    40           and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
    41       in
    42 	 ";\n\n\
    43 	 \local\n\
    44 	 \val (thy, {defs, intrs, elim, mk_cases, \
    45 		    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
    46 	 \  " ^
    47 	 (if coind then "Co" else "") ^ 
    48 	 "Ind_Package.add_inductive (" ^  srec_tms ^ ", " ^ sdom_sum ^ ", " ^
    49 	  sintrs ^ ", " ^ monos ^ ", " ^ con_defs ^ ", " ^ 
    50 	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
    51 	 \in\n\
    52 	 \structure " ^ big_rec_name ^ " =\n\
    53 	 \struct\n\
    54 	 \  val defs = defs\n\
    55 	 \  val bnd_mono = bnd_mono\n\
    56 	 \  val dom_subset = dom_subset\n\
    57 	 \  val intrs = intrs\n\
    58 	 \  val elim = elim\n\
    59 	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
    60 	 \  val mutual_induct = mutual_induct\n\
    61 	 \  val mk_cases = mk_cases\n\
    62 	 \  val " ^ inames ^ " = intrs\n\
    63 	 \end;\n\
    64 	 \val thy = thy;\nend;\n\
    65 	 \val thy = thy\n"
    66       end
    67     val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
    68     val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
    69   in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
    70              -- optlist "type_intrs" -- optlist "type_elims"
    71      >> mk_params
    72   end;
    73 
    74 
    75 (*Datatype definitions theory section.   co is true for codatatypes*)
    76 fun datatype_decl coind =
    77   let
    78     (*generate strings*)
    79     fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
    80     val mk_data = mk_list o map mk_const o snd
    81     val mk_scons = mk_big_list o map mk_data
    82     fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
    83       let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
    84 	  val big_rec_name = space_implode "_" rec_names
    85 	  and srec_tms = mk_list (map fst rec_pairs)
    86 	  and scons    = mk_scons rec_pairs
    87 	  val con_names = flat (map (map (unenclose o #1 o #1) o snd)
    88 				rec_pairs)
    89           val inames = mk_list (map (mk_intr_name "_I") con_names)
    90       in
    91 	 ";\n\n\
    92 	 \local\n\
    93 	 \val (thy,\n\
    94          \     {defs, intrs, elim, mk_cases, \
    95 		    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
    96          \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
    97 	 \  " ^
    98 	 (if coind then "Co" else "") ^ 
    99 	 "Data_Package.add_datatype (" ^  sdom ^ ", " ^ srec_tms ^ ", " ^
   100 	  scons ^ ", " ^ monos ^ ", " ^ 
   101 	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   102 	 \in\n\
   103 	 \structure " ^ big_rec_name ^ " =\n\
   104 	 \struct\n\
   105 	 \  val defs = defs\n\
   106 	 \  val bnd_mono = bnd_mono\n\
   107 	 \  val dom_subset = dom_subset\n\
   108 	 \  val intrs = intrs\n\
   109 	 \  val elim = elim\n\
   110 	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   111 	 \  val mutual_induct = mutual_induct\n\
   112 	 \  val mk_cases = mk_cases\n\
   113 	 \  val con_defs = con_defs\n\
   114 	 \  val case_eqns = case_eqns\n\
   115 	 \  val recursor_eqns = recursor_eqns\n\
   116 	 \  val free_iffs = free_iffs\n\
   117 	 \  val free_SEs = free_SEs\n\
   118 	 \  val mk_free = mk_free\n\
   119 	 \  val " ^ inames ^ " = intrs;\n\
   120 	 \end;\n\
   121 	 \val thy = thy;\nend;\n\
   122 	 \val thy = thy\n"
   123       end
   124     val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   125     val construct = name -- string_list -- opt_mixfix;
   126   in optional ("<=" $$-- string) "\"\"" --
   127      enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
   128      optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
   129      >> mk_params
   130 end;
   131 
   132 
   133 (** rep_datatype **)
   134 
   135 fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
   136   "|> DatatypeTactics.rep_datatype_i " ^ elim ^ " " ^ induct ^ "\n    " ^
   137   mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
   138 
   139 val rep_datatype_decl =
   140   (("elim" $$-- ident) -- 
   141    ("induct" $$-- ident) --
   142    ("case_eqns" $$-- list1 ident) -- 
   143    optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
   144 
   145 
   146 (** primrec **)
   147 
   148 fun mk_primrec_decl eqns =
   149   let val names = map fst eqns
   150   in
   151     ";\nval (thy, " ^ mk_list names ^
   152     ") = PrimrecPackage.add_primrec " ^
   153       mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   154     \val thy = thy\n"
   155   end;
   156 
   157 (* either names and axioms or just axioms *)
   158 val primrec_decl = 
   159     ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
   160 
   161 
   162 
   163 
   164 (** augment thy syntax **)
   165 
   166 in
   167 
   168 val _ = ThySyn.add_syntax
   169  ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
   170   "<=", "domains", "intrs", "monos", "con_defs", "type_intrs", "type_elims",
   171   (*rep_datatype*)
   172   "elim", "induct", "case_eqns", "recursor_eqns"]
   173  [section "inductive"    "" (inductive_decl false),
   174   section "coinductive"  "" (inductive_decl true),
   175   section "datatype"     "" (datatype_decl false),
   176   section "codatatype"   "" (datatype_decl true),
   177   section "rep_datatype" "" rep_datatype_decl,
   178   section "primrec"      "" primrec_decl];
   179 
   180 end;