src/Pure/type.ML
changeset 24274 cb9236269af1
parent 23655 d2d1138e0ddc
child 24484 013b98b57b86
     1.1 --- a/src/Pure/type.ML	Tue Aug 14 23:22:55 2007 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Aug 14 23:22:58 2007 +0200
     1.3 @@ -31,9 +31,12 @@
     1.4    val cert_class: tsig -> class -> class
     1.5    val cert_sort: tsig -> sort -> sort
     1.6    val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
     1.7 +  type mode
     1.8 +  val mode_default: mode
     1.9 +  val mode_syntax: mode
    1.10 +  val mode_abbrev: mode
    1.11 +  val cert_typ_mode: mode -> tsig -> typ -> typ
    1.12    val cert_typ: tsig -> typ -> typ
    1.13 -  val cert_typ_syntax: tsig -> typ -> typ
    1.14 -  val cert_typ_abbrev: tsig -> typ -> typ
    1.15    val arity_number: tsig -> string -> int
    1.16    val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
    1.17  
    1.18 @@ -144,6 +147,15 @@
    1.19    Sorts.witness_sorts (#2 classes) log_types;
    1.20  
    1.21  
    1.22 +(* certification mode *)
    1.23 +
    1.24 +datatype mode = Mode of {normalize: bool, logical: bool};
    1.25 +
    1.26 +val mode_default = Mode {normalize = true, logical = true};
    1.27 +val mode_syntax = Mode {normalize = true, logical = false};
    1.28 +val mode_abbrev = Mode {normalize = false, logical = false};
    1.29 +
    1.30 +
    1.31  (* certified types *)
    1.32  
    1.33  fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
    1.34 @@ -155,14 +167,16 @@
    1.35    | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x)
    1.36    | inst_typ _ T = T;
    1.37  
    1.38 -fun certify_typ normalize syntax tsig ty =
    1.39 +in
    1.40 +
    1.41 +fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
    1.42    let
    1.43      val TSig {types = (_, types), ...} = tsig;
    1.44      fun err msg = raise TYPE (msg, [ty], []);
    1.45  
    1.46 -    val check_syntax =
    1.47 -      if syntax then K ()
    1.48 -      else fn c => err ("Illegal occurrence of syntactic type: " ^ quote c);
    1.49 +    val check_logical =
    1.50 +      if logical then fn c => err ("Illegal occurrence of syntactic type: " ^ quote c)
    1.51 +      else fn _ => ();
    1.52  
    1.53      fun cert (T as Type (c, Ts)) =
    1.54            let
    1.55 @@ -171,11 +185,12 @@
    1.56            in
    1.57              (case Symtab.lookup types c of
    1.58                SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
    1.59 -            | SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
    1.60 -                if syn then check_syntax c else ();
    1.61 +            | SOME (Abbreviation (vs, U, syn), _) =>
    1.62 +               (nargs (length vs);
    1.63 +                if syn then check_logical c else ();
    1.64                  if normalize then inst_typ (vs ~~ Ts') U
    1.65                  else Type (c, Ts'))
    1.66 -            | SOME (Nonterminal, _) => (nargs 0; check_syntax c; T)
    1.67 +            | SOME (Nonterminal, _) => (nargs 0; check_logical c; T)
    1.68              | NONE => err (undecl_type c))
    1.69            end
    1.70        | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
    1.71 @@ -187,11 +202,7 @@
    1.72      val ty' = cert ty;
    1.73    in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.74  
    1.75 -in
    1.76 -
    1.77 -val cert_typ        = certify_typ true false;
    1.78 -val cert_typ_syntax = certify_typ true true;
    1.79 -val cert_typ_abbrev = certify_typ false true;
    1.80 +val cert_typ = cert_typ_mode mode_default;
    1.81  
    1.82  end;
    1.83  
    1.84 @@ -547,7 +558,7 @@
    1.85  fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
    1.86    let
    1.87      fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
    1.88 -    val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
    1.89 +    val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
    1.90        handle TYPE (msg, _, _) => err msg;
    1.91    in
    1.92      (case duplicates (op =) vs of