adapted to inner syntax of sorts;
authorwenzelm
Sun May 21 14:35:27 2000 +0200 (2000-05-21)
changeset 8897fb1436ca3b2e
parent 8896 c80aba8c1d5e
child 8898 a1ee54500516
adapted to inner syntax of sorts;
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Sun May 21 14:33:46 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Sun May 21 14:35:27 2000 +0200
     1.3 @@ -28,14 +28,14 @@
     1.4    val add_classes_i: (bclass * class list) list * Comment.text  -> theory -> theory
     1.5    val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory
     1.6    val add_classrel_i: (class * class) * Comment.text -> theory -> theory
     1.7 -  val add_defsort: xsort * Comment.text -> theory -> theory
     1.8 +  val add_defsort: string * Comment.text -> theory -> theory
     1.9    val add_defsort_i: sort * Comment.text -> theory -> theory
    1.10    val add_nonterminals: (bstring * Comment.text) list -> theory -> theory
    1.11    val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list
    1.12      -> theory -> theory
    1.13    val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list
    1.14      -> theory -> theory
    1.15 -  val add_arities: ((xstring * xsort list * xsort) * Comment.text) list -> theory -> theory
    1.16 +  val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory
    1.17    val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory
    1.18    val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory
    1.19    val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Sun May 21 14:33:46 2000 +0200
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun May 21 14:35:27 2000 +0200
     2.3 @@ -42,9 +42,9 @@
     2.4    val comment: token list -> Comment.text * token list
     2.5    val marg_comment: token list -> Comment.text * token list
     2.6    val interest: token list -> Comment.interest * token list
     2.7 -  val sort: token list -> xsort * token list
     2.8 -  val arity: token list -> (xsort list * xsort) * token list
     2.9 -  val simple_arity: token list -> (xsort list * xclass) * token list
    2.10 +  val sort: token list -> string * token list
    2.11 +  val arity: token list -> (string list * string) * token list
    2.12 +  val simple_arity: token list -> (string list * xclass) * token list
    2.13    val type_args: token list -> string list * token list
    2.14    val typ: token list -> string * token list
    2.15    val opt_infix: token list -> Syntax.mixfix * token list
    2.16 @@ -175,14 +175,13 @@
    2.17  
    2.18  (* sorts and arities *)
    2.19  
    2.20 -val sort =
    2.21 -  xname >> single || $$$ "{" |-- !!! (list xname --| $$$ "}");
    2.22 +val sort = group "sort" xname;
    2.23  
    2.24  fun gen_arity cod =
    2.25    Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
    2.26  
    2.27  val arity = gen_arity sort;
    2.28 -val simple_arity = gen_arity name;
    2.29 +val simple_arity = gen_arity xname;
    2.30  
    2.31  
    2.32  (* types *)
    2.33 @@ -266,7 +265,6 @@
    2.34    ((Scan.repeat1
    2.35      (Scan.repeat1 (atom_arg is_symid blk) ||
    2.36        paren_args "(" ")" (args is_symid) ||
    2.37 -      paren_args "{" "}" (args is_symid) ||
    2.38        paren_args "[" "]" (args is_symid))) >> flat) x;
    2.39  
    2.40  
     3.1 --- a/src/Pure/Thy/thy_parse.ML	Sun May 21 14:33:46 2000 +0200
     3.2 +++ b/src/Pure/Thy/thy_parse.ML	Sun May 21 14:35:27 2000 +0200
     3.3 @@ -201,13 +201,9 @@
     3.4  
     3.5  (* arities *)
     3.6  
     3.7 -val sort =
     3.8 -  name >> brackets ||
     3.9 -  "{" $$-- name_list --$$ "}";
    3.10 -
    3.11 +val sort = name || "{" $$-- list ident --$$ "}" >> (quote o enclose "{" "}" o commas);
    3.12  val sort_list1 = list1 sort >> mk_list;
    3.13  
    3.14 -
    3.15  val arity = optional ("(" $$-- !! (sort_list1 --$$")")) "[]" -- sort;
    3.16  
    3.17  val arity_decls = repeat1 (names1 --$$ "::" -- !! arity)
     4.1 --- a/src/Pure/axclass.ML	Sun May 21 14:33:46 2000 +0200
     4.2 +++ b/src/Pure/axclass.ML	Sun May 21 14:35:27 2000 +0200
     4.3 @@ -19,9 +19,9 @@
     4.4      -> tactic option -> theory -> theory
     4.5    val add_inst_subclass_i: class * class -> string list -> thm list
     4.6      -> tactic option -> theory -> theory
     4.7 -  val add_inst_arity: xstring * xsort list * xclass list -> string list
     4.8 +  val add_inst_arity: xstring * string list * string -> string list
     4.9      -> thm list -> tactic option -> theory -> theory
    4.10 -  val add_inst_arity_i: string * sort list * class list -> string list
    4.11 +  val add_inst_arity_i: string * sort list * sort -> string list
    4.12      -> thm list -> tactic option -> theory -> theory
    4.13    val axclass_tac: thm list -> tactic
    4.14    val prove_subclass: theory -> class * class -> thm list
    4.15 @@ -29,10 +29,10 @@
    4.16    val prove_arity: theory -> string * sort list * class -> thm list
    4.17      -> tactic option -> thm
    4.18    val goal_subclass: theory -> xclass * xclass -> thm list
    4.19 -  val goal_arity: theory -> xstring * xsort list * xclass -> thm list
    4.20 +  val goal_arity: theory -> xstring * string list * xclass -> thm list
    4.21    val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
    4.22    val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
    4.23 -  val instance_arity_proof: (xstring * xsort list * xclass) * Comment.text
    4.24 +  val instance_arity_proof: (xstring * string list * xclass) * Comment.text
    4.25      -> bool -> theory -> ProofHistory.T
    4.26    val instance_arity_proof_i: (string * sort list * class) * Comment.text
    4.27      -> bool -> theory -> ProofHistory.T
    4.28 @@ -146,7 +146,7 @@
    4.29          val (c1, c2) = dest_classrel prop handle TERM _ =>
    4.30            raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
    4.31        in (c1, c2) end;
    4.32 -  in Theory.add_classrel (map prep_thm thms) thy end;
    4.33 +  in Theory.add_classrel_i (map prep_thm thms) thy end;
    4.34  
    4.35  (*theorems expressing arities*)
    4.36  fun add_arity_thms thms thy =
    4.37 @@ -157,7 +157,7 @@
    4.38          val (t, ss, c) = dest_arity prop handle TERM _ =>
    4.39            raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
    4.40        in (t, ss, [c]) end;
    4.41 -  in Theory.add_arities (map prep_thm thms) thy end;
    4.42 +  in Theory.add_arities_i (map prep_thm thms) thy end;
    4.43  
    4.44  
    4.45  
    4.46 @@ -357,15 +357,32 @@
    4.47  
    4.48  (** add proved subclass relations and arities **)
    4.49  
    4.50 -fun intrn_classrel sg c1_c2 =
    4.51 -  pairself (Sign.intern_class sg) c1_c2;
    4.52 +(* prepare classes and arities *)
    4.53 +
    4.54 +fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
    4.55 +
    4.56 +fun cert_classrel sg cc = Library.pairself (Sign.certify_class sg) cc;
    4.57 +fun read_classrel sg cc = Library.pairself (read_class sg) cc;
    4.58  
    4.59 -fun intrn_arity intrn sg (raw_t, Ss, x) =
    4.60 -  let val t = Sign.intern_tycon sg raw_t in
    4.61 -    if Sign.is_type_abbr sg t then error ("Illegal type abbreviation: " ^ quote t)
    4.62 -    else (t, map (Sign.intern_sort sg) Ss, intrn sg x)
    4.63 +fun check_tycon sg t =
    4.64 +  let val {tycons, abbrs, ...} = Type.rep_tsig (Sign.tsig_of sg) in
    4.65 +    if is_some (Symtab.lookup (abbrs, t)) then
    4.66 +      error ("Illegal type abbreviation: " ^ quote t)
    4.67 +    else if is_none (Symtab.lookup (tycons, t)) then
    4.68 +      error ("Undeclared type constructor: " ^ quote t)
    4.69 +    else t
    4.70    end;
    4.71  
    4.72 +fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
    4.73 +  (check_tycon sg (prep_tycon sg t), map (prep_sort sg) Ss, prep_x sg x);
    4.74 +
    4.75 +val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
    4.76 +val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
    4.77 +val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
    4.78 +val cert_simple_arity = prep_arity (K I) Sign.certify_sort (K I);
    4.79 +
    4.80 +
    4.81 +(* old-style instance declarations *)
    4.82  
    4.83  fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
    4.84    let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in
    4.85 @@ -386,10 +403,10 @@
    4.86    in add_arity_thms (map prove cs) thy end;
    4.87  
    4.88  
    4.89 -val add_inst_subclass = ext_inst_subclass intrn_classrel;
    4.90 -val add_inst_subclass_i = ext_inst_subclass (K I);
    4.91 -val add_inst_arity = ext_inst_arity (intrn_arity Sign.intern_sort);
    4.92 -val add_inst_arity_i = ext_inst_arity (K I);
    4.93 +val add_inst_subclass = ext_inst_subclass read_classrel;
    4.94 +val add_inst_subclass_i = ext_inst_subclass cert_classrel;
    4.95 +val add_inst_arity = ext_inst_arity read_arity;
    4.96 +val add_inst_arity_i = ext_inst_arity cert_arity;
    4.97  
    4.98  
    4.99  (* make old-style interactive goals *)
   4.100 @@ -397,8 +414,8 @@
   4.101  fun mk_goal mk_prop thy sig_prop =
   4.102    Goals.goalw_cterm [] (Thm.cterm_of (Theory.sign_of thy) (mk_prop (Theory.sign_of thy) sig_prop));
   4.103  
   4.104 -val goal_subclass = mk_goal (mk_classrel oo intrn_classrel);
   4.105 -val goal_arity = mk_goal (mk_arity oo intrn_arity Sign.intern_class);
   4.106 +val goal_subclass = mk_goal (mk_classrel oo read_classrel);
   4.107 +val goal_arity = mk_goal (mk_arity oo read_simple_arity);
   4.108  
   4.109  
   4.110  
   4.111 @@ -411,10 +428,10 @@
   4.112    |> IsarThy.theorem_i (("", [inst_attribute add_thms],
   4.113      (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
   4.114  
   4.115 -val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
   4.116 -val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;
   4.117 -val instance_arity_proof = inst_proof (mk_arity oo intrn_arity Sign.intern_class) add_arity_thms;
   4.118 -val instance_arity_proof_i = inst_proof (K mk_arity) add_arity_thms;
   4.119 +val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
   4.120 +val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
   4.121 +val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
   4.122 +val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
   4.123  
   4.124  
   4.125  
     5.1 --- a/src/Pure/theory.ML	Sun May 21 14:33:46 2000 +0200
     5.2 +++ b/src/Pure/theory.ML	Sun May 21 14:35:27 2000 +0200
     5.3 @@ -40,7 +40,7 @@
     5.4    val add_classes_i: (bclass * class list) list -> theory -> theory
     5.5    val add_classrel: (xclass * xclass) list -> theory -> theory
     5.6    val add_classrel_i: (class * class) list -> theory -> theory
     5.7 -  val add_defsort: xsort -> theory -> theory
     5.8 +  val add_defsort: string -> theory -> theory
     5.9    val add_defsort_i: sort -> theory -> theory
    5.10    val add_types: (bstring * int * mixfix) list -> theory -> theory
    5.11    val add_nonterminals: bstring list -> theory -> theory
    5.12 @@ -48,7 +48,7 @@
    5.13      -> theory -> theory
    5.14    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    5.15      -> theory -> theory
    5.16 -  val add_arities: (xstring * xsort list * xsort) list -> theory -> theory
    5.17 +  val add_arities: (xstring * string list * string) list -> theory -> theory
    5.18    val add_arities_i: (string * sort list * sort) list -> theory -> theory
    5.19    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    5.20    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory