src/ZF/thy_syntax.ML
changeset 6053 8a1059aa01f0
parent 3925 90f499226ab9
child 6070 032babd0120b
     1.1 --- a/src/ZF/thy_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/thy_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -9,134 +9,144 @@
     1.4  
     1.5  local
     1.6  
     1.7 -(*Inductive definitions theory section.   co is either "" or "Co"*)
     1.8 -fun inductive_decl co =
     1.9 -  let open ThyParse 
    1.10 -    fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
    1.11 -        if Syntax.is_identifier s then "op " ^ s  else "_"
    1.12 -    fun mk_params ((((((rec_tms, sdom_sum), ipairs), 
    1.13 +
    1.14 +open ThyParse;
    1.15 +
    1.16 +(*ML identifiers for introduction rules.*)
    1.17 +fun mk_intr_name suffix s =  
    1.18 +    if Syntax.is_identifier s then
    1.19 +	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    1.20 +    else "_";               (*bad name, don't try to bind*)
    1.21 +
    1.22 +
    1.23 +(*For lists of theorems.  Either a string (an ML list expression) or else
    1.24 +  a list of identifiers.*)
    1.25 +fun optlist s = 
    1.26 +    optional (s $$-- 
    1.27 +	      (string >> strip_quotes
    1.28 +	       || list1 (name>>strip_quotes) >> mk_list)) 
    1.29 +    "[]";
    1.30 +
    1.31 +
    1.32 +(*(Co)Inductive definitions theory section."*)
    1.33 +fun inductive_decl coind =
    1.34 +  let  
    1.35 +    fun mk_params ((((((recs, sdom_sum), ipairs), 
    1.36                        monos), con_defs), type_intrs), type_elims) =
    1.37        let val big_rec_name = space_implode "_" 
    1.38 -                           (map (scan_to_id o trim) rec_tms)
    1.39 -          and srec_tms = mk_list rec_tms
    1.40 +                           (map (scan_to_id o strip_quotes) recs)
    1.41 +          and srec_tms = mk_list recs
    1.42            and sintrs   = mk_big_list (map snd ipairs)
    1.43 -          val stri_name = big_rec_name ^ "_Intrnl"
    1.44 +          and inames   = mk_list (map (mk_intr_name "" o fst) ipairs)
    1.45        in
    1.46 -         (";\n\n\
    1.47 -          \structure " ^ stri_name ^ " =\n\
    1.48 -          \  struct\n\
    1.49 -          \  val _ = writeln \"" ^ co ^ 
    1.50 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.51 -          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) "
    1.52 -                           ^ srec_tms ^ "\n\
    1.53 -          \  and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\
    1.54 -          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
    1.55 -                           ^ sintrs ^ "\n\
    1.56 -          \  end;\n\n\
    1.57 -          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
    1.58 -             stri_name ^ ".rec_tms, " ^
    1.59 -             stri_name ^ ".dom_sum, " ^
    1.60 -             stri_name ^ ".intr_tms)"
    1.61 -         ,
    1.62 -          "structure " ^ big_rec_name ^ " =\n\
    1.63 -          \ let\n\
    1.64 -          \  val _ = writeln \"Proofs for " ^ co ^ 
    1.65 -                     "Inductive definition " ^ big_rec_name ^ "\"\n\
    1.66 -          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
    1.67 -          \\t  (open " ^ stri_name ^ "\n\
    1.68 -          \\t   val thy\t\t= thy\n\
    1.69 -          \\t   val monos\t\t= " ^ monos ^ "\n\
    1.70 -          \\t   val con_defs\t\t= " ^ con_defs ^ "\n\
    1.71 -          \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
    1.72 -          \\t   val type_elims\t= " ^ type_elims ^ ")\n\
    1.73 -          \ in\n\
    1.74 -          \  struct\n\
    1.75 -          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
    1.76 -          \  open Result\n\
    1.77 -          \  end\n\
    1.78 -          \ end;\n\n\
    1.79 -          \structure " ^ stri_name ^ " = struct end;\n\n"
    1.80 -         )
    1.81 +	 ";\n\n\
    1.82 +	 \local\n\
    1.83 +	 \val (thy, {defs, intrs, elim, mk_cases, \
    1.84 +		    \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
    1.85 +	 \  " ^
    1.86 +	 (if coind then "Co" else "") ^ 
    1.87 +	 "Ind_Package.add_inductive (" ^  srec_tms ^ ", " ^ sdom_sum ^ ", " ^
    1.88 +	  sintrs ^ ", " ^ monos ^ ", " ^ con_defs ^ ", " ^ 
    1.89 +	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
    1.90 +	 \in\n\
    1.91 +	 \structure " ^ big_rec_name ^ " =\n\
    1.92 +	 \struct\n\
    1.93 +	 \  val defs = defs\n\
    1.94 +	 \  val bnd_mono = bnd_mono\n\
    1.95 +	 \  val dom_subset = dom_subset\n\
    1.96 +	 \  val intrs = intrs\n\
    1.97 +	 \  val elim = elim\n\
    1.98 +	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
    1.99 +	 \  val mutual_induct = mutual_induct\n\
   1.100 +	 \  val mk_cases = mk_cases\n\
   1.101 +	 \  val " ^ inames ^ " = intrs\n\
   1.102 +	 \end;\n\
   1.103 +	 \val thy = thy;\nend;\n\
   1.104 +	 \val thy = thy\n"
   1.105        end
   1.106      val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
   1.107      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
   1.108 -    fun optstring s = optional (s $$-- string >> trim) "[]"
   1.109 -  in domains -- ipairs -- optstring "monos" -- optstring "con_defs"
   1.110 -             -- optstring "type_intrs" -- optstring "type_elims"
   1.111 +  in domains -- ipairs -- optlist "monos" -- optlist "con_defs"
   1.112 +             -- optlist "type_intrs" -- optlist "type_elims"
   1.113       >> mk_params
   1.114    end;
   1.115  
   1.116  
   1.117 -(*Datatype definitions theory section.   co is either "" or "Co"*)
   1.118 -fun datatype_decl co =
   1.119 -  let open ThyParse 
   1.120 -      (*generate strings*)
   1.121 -      fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
   1.122 -      val mk_data = mk_list o map mk_const o snd
   1.123 -      val mk_scons = mk_big_list o map mk_data
   1.124 -      fun mk_intr_name s =  (*the "op" cancels any infix status*)
   1.125 -          if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_"
   1.126 -      fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) =
   1.127 -        let val rec_names = map (scan_to_id o trim o fst) rec_pairs
   1.128 -            val big_rec_name = space_implode "_" rec_names
   1.129 -            and srec_tms = mk_list (map fst rec_pairs)
   1.130 -            and scons    = mk_scons rec_pairs
   1.131 -            and sdom_sum = 
   1.132 -                if dom = "" then  (*default domain: univ or quniv*)
   1.133 -                    "Ind_Syntax." ^ co ^ "data_domain rec_tms"
   1.134 -                else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom
   1.135 -            val stri_name = big_rec_name ^ "_Intrnl"
   1.136 -            val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs)
   1.137 -        in
   1.138 -           (";\n\n\
   1.139 -            \structure " ^ stri_name ^ " =\n\
   1.140 -            \  struct\n\
   1.141 -            \  val _ = writeln \"" ^ co ^ 
   1.142 -                       "Datatype definition " ^ big_rec_name ^ "\"\n\
   1.143 -            \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\
   1.144 -            \  val dom_sum\t= " ^ sdom_sum ^ "\n\
   1.145 -            \  and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
   1.146 -                   ^ scons ^ "\n\
   1.147 -            \  val intr_tms\t= Ind_Syntax.mk_all_intr_tms (sign_of thy) (rec_tms, con_ty_lists)\n\
   1.148 -            \  end;\n\n\
   1.149 -            \val thy = thy |> " ^ co ^ "Ind.add_constructs_def(" ^ 
   1.150 -                 mk_list (map quote rec_names) ^ ", " ^ 
   1.151 -                 stri_name ^ ".con_ty_lists) \n\
   1.152 -            \              |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
   1.153 -               stri_name ^ ".rec_tms, " ^
   1.154 -               stri_name ^ ".dom_sum, " ^
   1.155 -               stri_name ^ ".intr_tms)"
   1.156 -           ,
   1.157 -            "structure " ^ big_rec_name ^ " =\n\
   1.158 -            \ let\n\
   1.159 -            \  val _ = writeln \"Proofs for " ^ co ^ 
   1.160 -                       "Datatype definition " ^ big_rec_name ^ "\"\n\
   1.161 -            \  structure Result = " ^ co ^ "Data_section_Fun\n\
   1.162 -            \\t  (open " ^ stri_name ^ "\n\
   1.163 -            \\t   val thy\t\t= thy\n\
   1.164 -            \\t   val big_rec_name\t= Sign.intern_const (sign_of thy) \"" ^ big_rec_name ^ "\"\n\
   1.165 -            \\t   val monos\t\t= " ^ monos ^ "\n\
   1.166 -            \\t   val type_intrs\t= " ^ type_intrs ^ "\n\
   1.167 -            \\t   val type_elims\t= " ^ type_elims ^ ");\n\
   1.168 -            \ in\n\
   1.169 -            \  struct\n\
   1.170 -            \  val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\
   1.171 -            \  open Result\n\
   1.172 -            \  end\n\
   1.173 -            \ end;\n\n\
   1.174 -            \structure " ^ stri_name ^ " = struct end;\n\n"
   1.175 -           )
   1.176 -        end
   1.177 -      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
   1.178 -      val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   1.179 -      val construct = name -- string_list -- opt_mixfix;
   1.180 -  in optional ("<=" $$-- string) "" --
   1.181 +(*Datatype definitions theory section.   co is true for codatatypes*)
   1.182 +fun datatype_decl coind =
   1.183 +  let
   1.184 +    (*generate strings*)
   1.185 +    fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
   1.186 +    val mk_data = mk_list o map mk_const o snd
   1.187 +    val mk_scons = mk_big_list o map mk_data
   1.188 +    fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
   1.189 +      let val rec_names = map (scan_to_id o strip_quotes o fst) rec_pairs
   1.190 +	  val big_rec_name = space_implode "_" rec_names
   1.191 +	  and srec_tms = mk_list (map fst rec_pairs)
   1.192 +	  and scons    = mk_scons rec_pairs
   1.193 +	  val con_names = flat (map (map (strip_quotes o #1 o #1) o snd)
   1.194 +				rec_pairs)
   1.195 +          val inames = mk_list (map (mk_intr_name "_I") con_names)
   1.196 +      in
   1.197 +	 ";\n\n\
   1.198 +	 \local\n\
   1.199 +	 \val (thy,\n\
   1.200 +         \     {defs, intrs, elim, mk_cases, \
   1.201 +		    \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
   1.202 +         \     {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
   1.203 +	 \  " ^
   1.204 +	 (if coind then "Co" else "") ^ 
   1.205 +	 "Data_Package.add_datatype (" ^  sdom ^ ", " ^ srec_tms ^ ", " ^
   1.206 +	  scons ^ ", " ^ monos ^ ", " ^ 
   1.207 +	  type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
   1.208 +	 \in\n\
   1.209 +	 \structure " ^ big_rec_name ^ " =\n\
   1.210 +	 \struct\n\
   1.211 +	 \  val defs = defs\n\
   1.212 +	 \  val bnd_mono = bnd_mono\n\
   1.213 +	 \  val dom_subset = dom_subset\n\
   1.214 +	 \  val intrs = intrs\n\
   1.215 +	 \  val elim = elim\n\
   1.216 +	 \  val " ^ (if coind then "co" else "") ^ "induct = induct\n\
   1.217 +	 \  val mutual_induct = mutual_induct\n\
   1.218 +	 \  val mk_cases = mk_cases\n\
   1.219 +	 \  val con_defs = con_defs\n\
   1.220 +	 \  val case_eqns = case_eqns\n\
   1.221 +	 \  val recursor_eqns = recursor_eqns\n\
   1.222 +	 \  val free_iffs = free_iffs\n\
   1.223 +	 \  val free_SEs = free_SEs\n\
   1.224 +	 \  val mk_free = mk_free\n\
   1.225 +	 \  val " ^ inames ^ " = intrs;\n\
   1.226 +	 \end;\n\
   1.227 +	 \val thy = thy;\nend;\n\
   1.228 +	 \val thy = thy\n"
   1.229 +      end
   1.230 +    val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
   1.231 +    val construct = name -- string_list -- opt_mixfix;
   1.232 +  in optional ("<=" $$-- string) "\"\"" --
   1.233       enum1 "and" (string --$$ "=" -- enum1 "|" construct) --
   1.234 -     optstring "monos" -- optstring "type_intrs" -- optstring "type_elims"
   1.235 +     optlist "monos" -- optlist "type_intrs" -- optlist "type_elims"
   1.236       >> mk_params
   1.237  end;
   1.238  
   1.239  
   1.240 +(** primrec **)
   1.241 +
   1.242 +fun mk_primrec_decl eqns =
   1.243 +  let val names = map fst eqns
   1.244 +  in
   1.245 +    ";\nval (thy, " ^ mk_list names ^
   1.246 +    ") = PrimrecPackage.add_primrec " ^
   1.247 +      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   1.248 +    \val thy = thy\n"
   1.249 +  end;
   1.250 +
   1.251 +(* either names and axioms or just axioms *)
   1.252 +val primrec_decl = 
   1.253 +    ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
   1.254 +
   1.255 +
   1.256 +
   1.257  
   1.258  (** augment thy syntax **)
   1.259  
   1.260 @@ -146,9 +156,10 @@
   1.261   ["inductive", "coinductive", "datatype", "codatatype", "and", "|",
   1.262    "<=", "domains", "intrs", "monos", "con_defs", "type_intrs",
   1.263    "type_elims"]
   1.264 - [("inductive", inductive_decl ""),
   1.265 -  ("coinductive", inductive_decl "Co"),
   1.266 -  ("datatype", datatype_decl ""),
   1.267 -  ("codatatype", datatype_decl "Co")];
   1.268 + [section "inductive"   "" (inductive_decl false),
   1.269 +  section "coinductive" "" (inductive_decl true),
   1.270 +  section "datatype"    "" (datatype_decl false),
   1.271 +  section "codatatype"  "" (datatype_decl true),
   1.272 +  section "primrec"     "" primrec_decl];
   1.273  
   1.274  end;