added type_env function;
authorwenzelm
Fri Dec 14 11:51:52 2001 +0100 (2001-12-14)
changeset 124960a9bd5034e05
parent 12495 89f97fa683f5
child 12497 ec6ba9e6eef3
added type_env function;
let norm_type_XXX work directly with type env component;
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Fri Dec 14 11:51:01 2001 +0100
     1.2 +++ b/src/Pure/envir.ML	Fri Dec 14 11:51:52 2001 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  signature ENVIR =
     1.5  sig
     1.6    datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
     1.7 +  val type_env: env -> typ Vartab.table
     1.8    exception SAME
     1.9    val genvars: string -> env * typ list -> env * term list
    1.10    val genvar: string -> env * typ -> env * term
    1.11 @@ -23,9 +24,9 @@
    1.12    val alist_of: env -> (indexname * term) list
    1.13    val norm_term: env -> term -> term
    1.14    val norm_term_same: env -> term -> term
    1.15 -  val norm_type: env -> typ -> typ
    1.16 -  val norm_type_same: env -> typ -> typ
    1.17 -  val norm_types_same: env -> typ list -> typ list
    1.18 +  val norm_type: typ Vartab.table -> typ -> typ
    1.19 +  val norm_type_same: typ Vartab.table -> typ -> typ
    1.20 +  val norm_types_same: typ Vartab.table -> typ list -> typ list
    1.21    val beta_norm: term -> term
    1.22    val head_norm: env -> term -> term
    1.23    val fastype: env -> typ list -> term -> typ
    1.24 @@ -42,6 +43,7 @@
    1.25       asol: term Vartab.table,   (*table of assignments to Vars*)
    1.26       iTs: typ Vartab.table}     (*table of assignments to TVars*)
    1.27  
    1.28 +fun type_env (Envir {iTs, ...}) = iTs;
    1.29  
    1.30  (*Generate a list of distinct variables.
    1.31    Increments index to make them distinct from ALL present variables. *)
    1.32 @@ -155,11 +157,11 @@
    1.33  
    1.34  val beta_norm = norm_term (empty 0);
    1.35  
    1.36 -fun norm_type (Envir {iTs, ...}) = normTh iTs;
    1.37 -fun norm_type_same (Envir {iTs, ...}) =
    1.38 +fun norm_type iTs = normTh iTs;
    1.39 +fun norm_type_same iTs =
    1.40    if Vartab.is_empty iTs then raise SAME else normT iTs;
    1.41  
    1.42 -fun norm_types_same (Envir {iTs, ...}) =
    1.43 +fun norm_types_same iTs =
    1.44    if Vartab.is_empty iTs then raise SAME else normTs iTs;
    1.45  
    1.46