typ_no_norm;
authorwenzelm
Thu Aug 03 00:41:07 2000 +0200 (2000-08-03)
changeset 95048168600e88a5
parent 9503 3324cbbecef8
child 9505 09c75c801dde
typ_no_norm;
src/Pure/Isar/args.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Isar/args.ML	Thu Aug 03 00:34:22 2000 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Thu Aug 03 00:41:07 2000 +0200
     1.3 @@ -30,9 +30,11 @@
     1.4    val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
     1.5    val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
     1.6    val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
     1.7 +  val global_typ_no_norm: theory * T list -> typ * (theory * T list)
     1.8    val global_typ: theory * T list -> typ * (theory * T list)
     1.9    val global_term: theory * T list -> term * (theory * T list)
    1.10    val global_prop: theory * T list -> term * (theory * T list)
    1.11 +  val local_typ_no_norm: Proof.context * T list -> typ * (Proof.context * T list)
    1.12    val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
    1.13    val local_term: Proof.context * T list -> term * (Proof.context * T list)
    1.14    val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    1.15 @@ -137,10 +139,12 @@
    1.16  
    1.17  fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
    1.18  
    1.19 +val global_typ_no_norm = gen_item (ProofContext.read_typ_no_norm o ProofContext.init);
    1.20  val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
    1.21  val global_term = gen_item (ProofContext.read_term o ProofContext.init);
    1.22  val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
    1.23  
    1.24 +val local_typ_no_norm = gen_item ProofContext.read_typ_no_norm;
    1.25  val local_typ = gen_item ProofContext.read_typ;
    1.26  val local_term = gen_item ProofContext.read_term;
    1.27  val local_prop = gen_item ProofContext.read_prop;
     2.1 --- a/src/Pure/Isar/isar_output.ML	Thu Aug 03 00:34:22 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_output.ML	Thu Aug 03 00:41:07 2000 +0200
     2.3 @@ -288,7 +288,7 @@
     2.4   [("thm", args Attrib.local_thms (string_of oo pretty_thm)),
     2.5    ("prop", args Args.local_prop (string_of oo pretty_term)),
     2.6    ("term", args Args.local_term (string_of oo pretty_term)),
     2.7 -  ("typ", args Args.local_typ (string_of oo pretty_typ))];
     2.8 +  ("typ", args Args.local_typ_no_norm (string_of oo pretty_typ))];
     2.9  
    2.10  end;
    2.11  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Aug 03 00:34:22 2000 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Aug 03 00:41:07 2000 +0200
     3.3 @@ -27,7 +27,9 @@
     3.4    val assumptions: context -> (cterm list * exporter) list
     3.5    val fixed_names: context -> string list
     3.6    val read_typ: context -> string -> typ
     3.7 +  val read_typ_no_norm: context -> string -> typ
     3.8    val cert_typ: context -> typ -> typ
     3.9 +  val cert_typ_no_norm: context -> typ -> typ
    3.10    val intern_skolem: context -> term -> term
    3.11    val extern_skolem: context -> term -> term
    3.12    val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
    3.13 @@ -377,13 +379,24 @@
    3.14  
    3.15  (** prepare types **)
    3.16  
    3.17 -fun read_typ ctxt s =
    3.18 -  transform_error (Sign.read_typ (sign_of ctxt, def_sort ctxt)) s
    3.19 +local
    3.20 +
    3.21 +fun read_typ_aux read ctxt s =
    3.22 +  transform_error (read (sign_of ctxt, def_sort ctxt)) s
    3.23      handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
    3.24  
    3.25 -fun cert_typ ctxt raw_T =
    3.26 -  Sign.certify_typ (sign_of ctxt) raw_T
    3.27 -    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
    3.28 +fun cert_typ_aux cert ctxt raw_T = cert (sign_of ctxt) raw_T
    3.29 +  handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
    3.30 +
    3.31 +in
    3.32 +
    3.33 +val read_typ         = read_typ_aux Sign.read_typ;
    3.34 +val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm;
    3.35 +val cert_typ         = cert_typ_aux Sign.certify_typ;
    3.36 +val cert_typ_no_norm = cert_typ_aux Sign.certify_typ_no_norm;
    3.37 +
    3.38 +end;
    3.39 +
    3.40  
    3.41  
    3.42  (* internalize Skolem constants *)
     4.1 --- a/src/Pure/sign.ML	Thu Aug 03 00:34:22 2000 +0200
     4.2 +++ b/src/Pure/sign.ML	Thu Aug 03 00:41:07 2000 +0200
     4.3 @@ -84,10 +84,12 @@
     4.4    val certify_class: sg -> class -> class
     4.5    val certify_sort: sg -> sort -> sort
     4.6    val certify_typ: sg -> typ -> typ
     4.7 +  val certify_typ_no_norm: sg -> typ -> typ
     4.8    val certify_term: sg -> term -> term * typ * int
     4.9    val read_sort: sg -> string -> sort
    4.10    val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
    4.11    val read_typ: sg * (indexname -> sort option) -> string -> typ
    4.12 +  val read_typ_no_norm: sg * (indexname -> sort option) -> string -> typ
    4.13    val infer_types: sg -> (indexname -> typ option) ->
    4.14      (indexname -> sort option) -> string list -> bool
    4.15      -> xterm list * typ -> term * (indexname * typ) list
    4.16 @@ -576,9 +578,14 @@
    4.17    (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
    4.18  
    4.19  (*read and certify typ wrt a signature*)
    4.20 -fun read_typ (sg, def_sort) str =
    4.21 -  (Type.cert_typ (tsig_of sg) (read_raw_typ (sg, def_sort) str)
    4.22 -      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
    4.23 +local
    4.24 +  fun read_typ_aux cert (sg, def_sort) str =
    4.25 +    (cert (tsig_of sg) (read_raw_typ (sg, def_sort) str)
    4.26 +        handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
    4.27 +in
    4.28 +  val read_typ = read_typ_aux Type.cert_typ;
    4.29 +  val read_typ_no_norm = read_typ_aux Type.cert_typ_no_norm;
    4.30 +end;
    4.31  
    4.32  
    4.33  
    4.34 @@ -587,6 +594,7 @@
    4.35  val certify_class = Type.cert_class o tsig_of;
    4.36  val certify_sort = Type.cert_sort o tsig_of;
    4.37  val certify_typ = Type.cert_typ o tsig_of;
    4.38 +val certify_typ_no_norm = Type.cert_typ_no_norm o tsig_of;
    4.39  
    4.40  
    4.41  (* certify_term *)
     5.1 --- a/src/Pure/type.ML	Thu Aug 03 00:34:22 2000 +0200
     5.2 +++ b/src/Pure/type.ML	Thu Aug 03 00:41:07 2000 +0200
     5.3 @@ -46,6 +46,7 @@
     5.4    val merge_tsigs: type_sig * type_sig -> type_sig
     5.5    val typ_errors: type_sig -> typ * string list -> string list
     5.6    val cert_typ: type_sig -> typ -> typ
     5.7 +  val cert_typ_no_norm: type_sig -> typ -> typ
     5.8    val norm_typ: type_sig -> typ -> typ
     5.9    val norm_term: type_sig -> term -> term
    5.10    val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    5.11 @@ -352,12 +353,13 @@
    5.12  
    5.13  (* cert_typ *)           (*exception TYPE*)
    5.14  
    5.15 -(*check and normalize type wrt tsig*)
    5.16 -fun cert_typ tsig T =
    5.17 +fun cert_typ_no_norm tsig T =
    5.18    (case typ_errors tsig (T, []) of
    5.19 -    [] => norm_typ tsig T
    5.20 +    [] => T
    5.21    | errs => raise TYPE (cat_lines errs, [T], []));
    5.22  
    5.23 +fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
    5.24 +
    5.25  
    5.26  
    5.27  (** merge type signatures **)