--- a/src/Pure/Isar/isar_thy.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML Sun May 21 14:35:27 2000 +0200
@@ -28,14 +28,14 @@
val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory
val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
val add_classrel_i: (class * class) * Comment.text -> theory -> theory
- val add_defsort: xsort * Comment.text -> theory -> theory
+ val add_defsort: string * Comment.text -> theory -> theory
val add_defsort_i: sort * Comment.text -> theory -> theory
val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
-> theory -> theory
val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
-> theory -> theory
- val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory
+ val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
--- a/src/Pure/Isar/outer_parse.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML Sun May 21 14:35:27 2000 +0200
@@ -42,9 +42,9 @@
val comment: token list -> Comment.text * token list
val marg_comment: token list -> Comment.text * token list
val interest: token list -> Comment.interest * token list
- val sort: token list -> xsort * token list
- val arity: token list -> (xsort list * xsort) * token list
- val simple_arity: token list -> (xsort list * xclass) * token list
+ val sort: token list -> string * token list
+ val arity: token list -> (string list * string) * token list
+ val simple_arity: token list -> (string list * xclass) * token list
val type_args: token list -> string list * token list
val typ: token list -> string * token list
val opt_infix: token list -> Syntax.mixfix * token list
@@ -175,14 +175,13 @@
(* sorts and arities *)
-val sort =
- xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
+val sort = group "sort" xname;
fun gen_arity cod =
Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
val arity = gen_arity sort;
-val simple_arity = gen_arity name;
+val simple_arity = gen_arity xname;
(* types *)
@@ -266,7 +265,6 @@
((Scan.repeat1
(Scan.repeat1 (atom_arg is_symid blk) ||
paren_args "(" ")" (args is_symid) ||
- paren_args "{" "}" (args is_symid) ||
paren_args "[" "]" (args is_symid))) >> flat) x;
--- a/src/Pure/Thy/thy_parse.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/Thy/thy_parse.ML Sun May 21 14:35:27 2000 +0200
@@ -201,13 +201,9 @@
(* arities *)
-val sort =
- name >> brackets ||
- "{" $$-- name_list --$$ "}";
-
+val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
val sort_list1 = list1 sort >> mk_list;
-
val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
val arity_decls = repeat1 (names1 --$$ "::" -- !! arity)
--- a/src/Pure/axclass.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/axclass.ML Sun May 21 14:35:27 2000 +0200
@@ -19,9 +19,9 @@
-> tactic option -> theory -> theory
val add_inst_subclass_i: class * class -> string list -> thm list
-> tactic option -> theory -> theory
- val add_inst_arity: xstring * xsort list * xclass list -> string list
+ val add_inst_arity: xstring * string list * string -> string list
-> thm list -> tactic option -> theory -> theory
- val add_inst_arity_i: string * sort list * class list -> string list
+ val add_inst_arity_i: string * sort list * sort -> string list
-> thm list -> tactic option -> theory -> theory
val axclass_tac: thm list -> tactic
val prove_subclass: theory -> class * class -> thm list
@@ -29,10 +29,10 @@
val prove_arity: theory -> string * sort list * class -> thm list
-> tactic option -> thm
val goal_subclass: theory -> xclass * xclass -> thm list
- val goal_arity: theory -> xstring * xsort list * xclass -> thm list
+ val goal_arity: theory -> xstring * string list * xclass -> thm list
val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
- val instance_arity_proof: (xstring * xsort list * xclass) * Comment.text
+ val instance_arity_proof: (xstring * string list * xclass) * Comment.text
-> bool -> theory -> ProofHistory.T
val instance_arity_proof_i: (string * sort list * class) * Comment.text
-> bool -> theory -> ProofHistory.T
@@ -146,7 +146,7 @@
val (c1, c2) = dest_classrel prop handle TERM _ =>
raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
in (c1, c2) end;
- in Theory.add_classrel (map prep_thm thms) thy end;
+ in Theory.add_classrel_i (map prep_thm thms) thy end;
(*theorems expressing arities*)
fun add_arity_thms thms thy =
@@ -157,7 +157,7 @@
val (t, ss, c) = dest_arity prop handle TERM _ =>
raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
in (t, ss, [c]) end;
- in Theory.add_arities (map prep_thm thms) thy end;
+ in Theory.add_arities_i (map prep_thm thms) thy end;
@@ -357,15 +357,32 @@
(** add proved subclass relations and arities **)
-fun intrn_classrel sg c1_c2 =
- pairself (Sign.intern_class sg) c1_c2;
+(* prepare classes and arities *)
+
+fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
+
+fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc;
+fun read_classrel sg cc = Library.pairself (read_class sg) cc;
-fun intrn_arity intrn sg (raw_t, Ss, x) =
- let val t = Sign.intern_tycon sg raw_t in
- if Sign.is_type_abbr sg t then error ("Illegal type abbreviation: " ^ quote t)
- else (t, map (Sign.intern_sort sg) Ss, intrn sg x)
+fun check_tycon sg t =
+ let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in
+ if is_some (Symtab.lookup (abbrs, t)) then
+ error ("Illegal type abbreviation: " ^ quote t)
+ else if is_none (Symtab.lookup (tycons, t)) then
+ error ("Undeclared type constructor: " ^ quote t)
+ else t
end;
+fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
+ (check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x);
+
+val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
+val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
+val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
+val cert_simple_arity = prep_arity (K I) Sign.certify_sort (K I);
+
+
+(* old-style instance declarations *)
fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in
@@ -386,10 +403,10 @@
in add_arity_thms (map prove cs) thy end;
-val add_inst_subclass = ext_inst_subclass intrn_classrel;
-val add_inst_subclass_i = ext_inst_subclass (K I);
-val add_inst_arity = ext_inst_arity (intrn_arity Sign.intern_sort);
-val add_inst_arity_i = ext_inst_arity (K I);
+val add_inst_subclass = ext_inst_subclass read_classrel;
+val add_inst_subclass_i = ext_inst_subclass cert_classrel;
+val add_inst_arity = ext_inst_arity read_arity;
+val add_inst_arity_i = ext_inst_arity cert_arity;
(* make old-style interactive goals *)
@@ -397,8 +414,8 @@
fun mk_goal mk_prop thy sig_prop =
Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop));
-val goal_subclass = mk_goal (mk_classrel oo intrn_classrel);
-val goal_arity = mk_goal (mk_arity oo intrn_arity Sign.intern_class);
+val goal_subclass = mk_goal (mk_classrel oo read_classrel);
+val goal_arity = mk_goal (mk_arity oo read_simple_arity);
@@ -411,10 +428,10 @@
|> IsarThy.theorem_i (("", [inst_attribute add_thms],
(mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
-val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
-val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;
-val instance_arity_proof = inst_proof (mk_arity oo intrn_arity Sign.intern_class) add_arity_thms;
-val instance_arity_proof_i = inst_proof (K mk_arity) add_arity_thms;
+val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
+val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
+val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
+val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
--- a/src/Pure/theory.ML Sun May 21 14:33:46 2000 +0200
+++ b/src/Pure/theory.ML Sun May 21 14:35:27 2000 +0200
@@ -40,7 +40,7 @@
val add_classes_i: (bclass * class list) list -> theory -> theory
val add_classrel: (xclass * xclass) list -> theory -> theory
val add_classrel_i: (class * class) list -> theory -> theory
- val add_defsort: xsort -> theory -> theory
+ val add_defsort: string -> theory -> theory
val add_defsort_i: sort -> theory -> theory
val add_types: (bstring * int * mixfix) list -> theory -> theory
val add_nonterminals: bstring list -> theory -> theory
@@ -48,7 +48,7 @@
-> theory -> theory
val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
-> theory -> theory
- val add_arities: (xstring * xsort list * xsort) list -> theory -> theory
+ val add_arities: (xstring * string list * string) list -> theory -> theory
val add_arities_i: (string * sort list * sort) list -> theory -> theory
val add_consts: (bstring * string * mixfix) list -> theory -> theory
val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory