Changed syntax of rep_datatype and inductive: Theorems
authorberghofe
Wed Oct 21 17:46:00 1998 +0200 (1998-10-21)
changeset 5716a3d2a6b6693e
parent 5715 5fc697ad232b
child 5717 0d28dbe484b6
Changed syntax of rep_datatype and inductive: Theorems
are no longer specified by a string of ML type "thm list" but
by a comma-separated list of identifiers, which are looked
up in the theory.
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Oct 21 17:40:35 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Oct 21 17:46:00 1998 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
     1.5          \  InductivePackage.add_inductive true " ^
     1.6          (if coind then "true " else "false ") ^ srec_tms ^ " " ^
     1.7 -         sintrs ^ " " ^ monos ^ " " ^ con_defs ^ " thy;\n\
     1.8 +         sintrs ^ " " ^ mk_list monos ^ " " ^ mk_list con_defs ^ " thy;\n\
     1.9          \in\n\
    1.10          \structure " ^ big_rec_name ^ " =\n\
    1.11          \struct\n\
    1.12 @@ -72,9 +72,9 @@
    1.13          \val thy = thy\n"
    1.14        end
    1.15      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    1.16 -    fun optstring s = optional (s $$-- string >> trim) "[]"
    1.17 +    fun optlist s = optional (s $$-- list1 name) []
    1.18    in
    1.19 -    repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
    1.20 +    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
    1.21        >> mk_params
    1.22    end;
    1.23  
    1.24 @@ -143,13 +143,13 @@
    1.25      ";\nlocal\n\
    1.26      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
    1.27      \  case_thms, split_thms, induction, size, simps}) =\n\
    1.28 -    \  DatatypePackage.add_rep_datatype " ^
    1.29 +    \  DatatypePackage.rep_datatype " ^
    1.30      (case names of
    1.31 -        Some names => "(Some [" ^ commas (map quote names) ^ "]) (" ^
    1.32 -          distinct ^ ") (" ^ inject ^ ") (" ^ induct ^ ") thy;\nin\n" ^
    1.33 -            mk_bind_thms_string names
    1.34 -      | None => "None (" ^ distinct ^ ") (" ^ inject ^ ") (" ^ induct ^
    1.35 -          ") thy;\nin\n") ^
    1.36 +        Some names => "(Some [" ^ commas_quote names ^ "]) " ^
    1.37 +          mk_list (map mk_list distinct) ^ " " ^ mk_list (map mk_list inject) ^
    1.38 +            " " ^ induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
    1.39 +      | None => "None " ^ mk_list (map mk_list distinct) ^ " " ^
    1.40 +          mk_list (map mk_list inject) ^ " " ^ induct ^ " thy;\nin\n") ^
    1.41      "val thy = thy;\nend;\nval thy = thy\n";
    1.42  
    1.43    (*** parsers ***)
    1.44 @@ -168,33 +168,37 @@
    1.45    val opt_typs = repeat ((string >> strip_quotes) ||
    1.46      simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.47    val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
    1.48 -    parens (n ^ ", " ^ brackets (commas (map quote Ts)) ^ ", " ^ mx));
    1.49 +    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
    1.50    val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
    1.51  
    1.52 +  fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
    1.53 +
    1.54  in
    1.55    val datatype_decl =
    1.56      enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
    1.57        enum1 "|" constructor) >> mk_dt_string;
    1.58    val rep_datatype_decl =
    1.59      ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
    1.60 -      ("distinct" $$-- (name >> strip_quotes)) -- ("inject" $$--
    1.61 -        (name >> strip_quotes)) -- ("induct" $$-- (name >> strip_quotes))) >>
    1.62 -          mk_rep_dt_string;
    1.63 +      optlistlist "distinct" -- optlistlist "inject" --
    1.64 +        ("induct" $$-- name)) >> mk_rep_dt_string;
    1.65  end;
    1.66  
    1.67  
    1.68  (** primrec **)
    1.69  
    1.70 -fun mk_primrec_decl (alt_name, (names, eqns)) =
    1.71 -  ";\nval (thy, " ^ (if null names then "_" else brackets (commas names)) ^
    1.72 -  ") = PrimrecPackage.add_primrec (" ^ alt_name ^ ") " ^
    1.73 -    brackets (commas_quote names) ^ " " ^ brackets (commas eqns) ^ " thy;\n\
    1.74 -  \val thy = thy\n";
    1.75 +fun mk_primrec_decl (alt_name, eqns) =
    1.76 +  let
    1.77 +    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
    1.78 +  in
    1.79 +    ";\nval (thy, " ^ mk_list names ^
    1.80 +    ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
    1.81 +      mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
    1.82 +    \val thy = thy\n"
    1.83 +  end;
    1.84  
    1.85  (* either names and axioms or just axioms *)
    1.86 -val primrec_decl = (optional ("(" $$-- name --$$ ")" >> (cat "Some")) "None" --
    1.87 -  ((repeat1 (ident -- string) >> ListPair.unzip) ||
    1.88 -   (repeat1 string >> (pair [])))) >> mk_primrec_decl;
    1.89 +val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
    1.90 +  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
    1.91  
    1.92  
    1.93  (** rec: interface to Slind's TFL **)