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