Theory TypeSystem

chapter ‹Generated by Lem from ‹semantics/typeSystem.lem›.›

theory "TypeSystem" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives_extra"
  "Lib"
  "Namespace"
  "Ast"
  "SemanticPrimitives"

begin 

― ‹‹open import Pervasives_extra››
― ‹‹open import Lib››
― ‹‹open import Ast››
― ‹‹open import Namespace››
― ‹‹open import SemanticPrimitives››

― ‹‹ Check that the free type variables are in the given list. Every deBruijn
 * variable must be smaller than the first argument. So if it is 0, no deBruijn
 * indices are permitted. ››
― ‹‹val check_freevars : nat -> list tvarN -> t -> bool››
function (sequential,domintros) 
check_freevars  :: " nat ⇒(string)list ⇒ t ⇒ bool "  where 
     "
check_freevars dbmax tvs (Tvar tv) = (
  Set.member tv (set tvs))"
|"
check_freevars dbmax tvs (Tapp ts tn) = (
  ((∀ x ∈ (set ts).  (check_freevars dbmax tvs) x)))"
|"
check_freevars dbmax tvs (Tvar_db n) = ( n < dbmax )" 
by pat_completeness auto


― ‹‹ Simultaneous substitution of types for type variables in a type ››
― ‹‹val type_subst : Map.map tvarN t -> t -> t››
function (sequential,domintros) 
type_subst  :: "((string),(t))Map.map ⇒ t ⇒ t "  where 
     "
type_subst s (Tvar tv) = (
  (case   s tv of
      None => Tvar tv
    | Some(t1) => t1
  ))"
|"
type_subst s (Tapp ts tn) = (
  Tapp (List.map (type_subst s) ts) tn )"
|"
type_subst s (Tvar_db n) = ( Tvar_db n )" 
by pat_completeness auto


― ‹‹ Increment the deBruijn indices in a type by n levels, skipping all levels
 * less than skip. ››
― ‹‹val deBruijn_inc : nat -> nat -> t -> t››
function (sequential,domintros) 
deBruijn_inc  :: " nat ⇒ nat ⇒ t ⇒ t "  where 
     "
deBruijn_inc skip n (Tvar tv) = ( Tvar tv )"
|"
deBruijn_inc skip n (Tvar_db m) = (
  if m < skip then
    Tvar_db m
  else
    Tvar_db (m + n))"
|"
deBruijn_inc skip n (Tapp ts tn) = ( Tapp (List.map (deBruijn_inc skip n) ts) tn )" 
by pat_completeness auto


― ‹‹ skip the lowest given indices and replace the next (LENGTH ts) with the given types and reduce all the higher ones ››
― ‹‹val deBruijn_subst : nat -> list t -> t -> t››
function (sequential,domintros) 
deBruijn_subst  :: " nat ⇒(t)list ⇒ t ⇒ t "  where 
     "
deBruijn_subst skip ts (Tvar tv) = ( Tvar tv )"
|"
deBruijn_subst skip ts (Tvar_db n) = (
  if ¬ (n < skip) ∧ (n < (List.length ts + skip)) then
    List.nth ts (n - skip)
  else if ¬ (n < skip) then
    Tvar_db (n - List.length ts)
  else
    Tvar_db n )"
|"
deBruijn_subst skip ts (Tapp ts' tn) = (
  Tapp (List.map (deBruijn_subst skip ts) ts') tn )" 
by pat_completeness auto


― ‹‹ Type environments ››
datatype tenv_val_exp =
    Empty
  ― ‹‹ Binds several de Bruijn type variables ››
  | Bind_tvar " nat " " tenv_val_exp "
  ― ‹‹ The number is how many de Bruijn type variables the typescheme binds ››
  | Bind_name " varN " " nat " " t " " tenv_val_exp "

― ‹‹val bind_tvar : nat -> tenv_val_exp -> tenv_val_exp››
definition bind_tvar  :: " nat ⇒ tenv_val_exp ⇒ tenv_val_exp "  where 
     " bind_tvar tvs tenvE = ( if tvs =( 0 :: nat) then tenvE else Bind_tvar tvs tenvE )"


― ‹‹val opt_bind_name : maybe varN -> nat -> t -> tenv_val_exp -> tenv_val_exp››
fun opt_bind_name  :: "(string)option ⇒ nat ⇒ t ⇒ tenv_val_exp ⇒ tenv_val_exp "  where 
     " opt_bind_name None tvs t1 tenvE = ( tenvE )"
|" opt_bind_name (Some n') tvs t1 tenvE = ( Bind_name n' tvs t1 tenvE )"


― ‹‹val tveLookup : varN -> nat -> tenv_val_exp -> maybe (nat * t)››
fun 
tveLookup  :: " string ⇒ nat ⇒ tenv_val_exp ⇒(nat*t)option "  where 
     "
tveLookup n inc Empty = ( None )"
|"
tveLookup n inc (Bind_tvar tvs tenvE) = ( tveLookup n (inc + tvs) tenvE )"
|"
tveLookup n inc (Bind_name n' tvs t1 tenvE) = (
  if n' = n then
    Some (tvs, deBruijn_inc tvs inc t1)
  else
    tveLookup n inc tenvE )"


type_synonym tenv_abbrev =" (modN, typeN, ( tvarN list * t)) namespace "
type_synonym tenv_ctor =" (modN, conN, ( tvarN list * t list * tid_or_exn)) namespace "
type_synonym tenv_val =" (modN, varN, (nat * t)) namespace "

datatype_record type_env =
  
 v0 ::" tenv_val "
   
 c0 ::" tenv_ctor "
   
 t ::" tenv_abbrev "
   


― ‹‹val extend_dec_tenv : type_env -> type_env -> type_env››
definition extend_dec_tenv  :: " type_env ⇒ type_env ⇒ type_env "  where 
     " extend_dec_tenv tenv' tenv = (
  (| v0 = (nsAppend(v0   tenv')(v0   tenv)),
     c0 = (nsAppend(c0   tenv')(c0   tenv)),
     t = (nsAppend(t   tenv')(t   tenv)) |) )"


― ‹‹val lookup_varE : id modN varN -> tenv_val_exp -> maybe (nat * t)››
fun lookup_varE  :: "((string),(string))id0 ⇒ tenv_val_exp ⇒(nat*t)option "  where 
     " lookup_varE (Short x) tenvE = ( tveLookup x(( 0 :: nat)) tenvE )"
|" lookup_varE _ tenvE = ( None )"


― ‹‹val lookup_var : id modN varN -> tenv_val_exp -> type_env -> maybe (nat * t)››
definition lookup_var  :: "((modN),(varN))id0 ⇒ tenv_val_exp ⇒ type_env ⇒(nat*t)option "  where 
     " lookup_var id1 tenvE tenv = (
  (case  lookup_varE id1 tenvE of
    Some x => Some x
  | None => nsLookup(v0   tenv) id1
  ))"


― ‹‹val num_tvs : tenv_val_exp -> nat››
fun 
num_tvs  :: " tenv_val_exp ⇒ nat "  where 
     "
num_tvs Empty = (( 0 :: nat))"
|"
num_tvs (Bind_tvar tvs tenvE) = ( tvs + num_tvs tenvE )"
|"
num_tvs (Bind_name n tvs t1 tenvE) = ( num_tvs tenvE )"


― ‹‹val bind_var_list : nat -> list (varN * t) -> tenv_val_exp -> tenv_val_exp››
fun 
bind_var_list  :: " nat ⇒(string*t)list ⇒ tenv_val_exp ⇒ tenv_val_exp "  where 
     "
bind_var_list tvs [] tenvE = ( tenvE )"
|"
bind_var_list tvs ((n,t1)# binds) tenvE = (
  Bind_name n tvs t1 (bind_var_list tvs binds tenvE))"


― ‹‹ A pattern matches values of a certain type and extends the type environment
 * with the pattern's binders. The number is the maximum deBruijn type variable
 * allowed. ››
― ‹‹val type_p : nat -> type_env -> pat -> t -> list (varN * t) -> bool››

― ‹‹ An expression has a type ››
― ‹‹val type_e : type_env -> tenv_val_exp -> exp -> t -> bool››

― ‹‹ A list of expressions has a list of types ››
― ‹‹val type_es : type_env -> tenv_val_exp -> list exp -> list t -> bool››

― ‹‹ Type a mutually recursive bundle of functions.  Unlike pattern typing, the
 * resulting environment does not extend the input environment, but just
 * represents the functions ››
― ‹‹val type_funs : type_env -> tenv_val_exp -> list (varN * varN * exp) -> list (varN * t) -> bool››

datatype_record decls =
  
 defined_mods0 ::" ( modN list) set " 

     defined_types0 ::" ( (modN, typeN)id0) set " 

     defined_exns ::" ( (modN, conN)id0) set " 


― ‹‹val empty_decls : decls››
definition empty_decls  :: " decls "  where 
     " empty_decls = ( (| defined_mods0 = ({}), defined_types0 = ({}), defined_exns = ({})|) )"


― ‹‹val union_decls : decls -> decls -> decls››
definition union_decls  :: " decls ⇒ decls ⇒ decls "  where 
     " union_decls d1 d2 = (
  (| defined_mods0 = ((defined_mods0   d1) ∪(defined_mods0   d2)),
     defined_types0 = ((defined_types0   d1) ∪(defined_types0   d2)),
     defined_exns = ((defined_exns   d1) ∪(defined_exns   d2)) |) )"


― ‹‹ Check a declaration and update the top-level environments
 * The arguments are in order:
 * - the module that the declaration is in
 * - the set of all modules, and types, and exceptions that have been previously declared
 * - the type environment
 * - the declaration
 * - the set of all modules, and types, and exceptions that are declared here
 * - the environment of new stuff declared here ››

― ‹‹val type_d : bool -> list modN -> decls -> type_env -> dec -> decls -> type_env -> bool››

― ‹‹val type_ds : bool -> list modN -> decls -> type_env -> list dec -> decls -> type_env -> bool››
― ‹‹val check_signature : list modN -> tenv_abbrev -> decls -> type_env -> maybe specs -> decls -> type_env -> bool››
― ‹‹val type_specs : list modN -> tenv_abbrev -> specs -> decls -> type_env -> bool››
― ‹‹val type_prog : bool -> decls -> type_env -> list top -> decls -> type_env -> bool››

― ‹‹ Check that the operator can have type (t1 -> ... -> tn -> t) ››
― ‹‹val type_op : op -> list t -> t -> bool››
fun type_op  :: " op0 ⇒(t)list ⇒ t ⇒ bool "  where 
     " type_op (Opn o0) ts t1 = ( 
  (case (o0,ts) of
      ( _, [Tapp [] TC_int, Tapp [] TC_int]) => (t1 = Tint)
    | (_,_) => False
  ) )"
|" type_op (Opb o1) ts t1 = ( 
  (case (o1,ts) of
      ( _, [Tapp [] TC_int, Tapp [] TC_int]) => (t1 =
                                                   Tapp []
                                                     (TC_name
                                                        (Short (''bool''))))
    | (_,_) => False
  ) )"
|" type_op (Opw w o2) ts t1 = ( 
  (case (w,o2,ts) of
      ( W8, _, [Tapp [] TC_word8, Tapp [] TC_word8]) => (t1 =
                                                           Tapp [] TC_word8)
    | ( W64, _, [Tapp [] TC_word64, Tapp [] TC_word64]) => (t1 =
                                                              Tapp []
                                                                TC_word64)
    | (_,_,_) => False
  ) )"
|" type_op (Shift w0 s n0) ts t1 = ( 
  (case (w0,s,n0,ts) of
      ( W8, _, _, [Tapp [] TC_word8]) => (t1 = Tapp [] TC_word8)
    | ( W64, _, _, [Tapp [] TC_word64]) => (t1 = Tapp [] TC_word64)
    | (_,_,_,_) => False
  ) )"
|" type_op Equality ts t1 = ( 
  (case  ts of
      [t11, t2] => (t11 = t2) ∧
                     (t1 = Tapp [] (TC_name (Short (''bool''))))
    | _ => False
  ) )"
|" type_op (FP_cmp f) ts t1 = ( 
  (case (f,ts) of
      ( _, [Tapp [] TC_word64, Tapp [] TC_word64]) => (t1 =
                                                         Tapp []
                                                           (TC_name
                                                              (Short
                                                                 (''bool''))))
    | (_,_) => False
  ) )"
|" type_op (FP_uop f0) ts t1 = ( 
  (case (f0,ts) of
      ( _, [Tapp [] TC_word64]) => (t1 = Tapp [] TC_word64)
    | (_,_) => False
  ) )"
|" type_op (FP_bop f1) ts t1 = ( 
  (case (f1,ts) of
      ( _, [Tapp [] TC_word64, Tapp [] TC_word64]) => (t1 = Tapp [] TC_word64)
    | (_,_) => False
  ) )"
|" type_op Opapp ts t1 = ( 
  (case  ts of
      [Tapp [t2', t3'] TC_fn, t2] => (t2 = t2') ∧ (t1 = t3')
    | _ => False
  ) )"
|" type_op Opassign ts t1 = ( 
  (case  ts of
      [Tapp [t11] TC_ref, t2] => (t11 = t2) ∧ (t1 = Tapp [] TC_tup)
    | _ => False
  ) )"
|" type_op Opref ts t1 = ( 
  (case  ts of [t11] => (t1 = Tapp [t11] TC_ref) | _ => False ) )"
|" type_op Opderef ts t1 = ( 
  (case  ts of [Tapp [t11] TC_ref] => (t1 = t11) | _ => False ) )"
|" type_op Aw8alloc ts t1 = ( 
  (case  ts of
      [Tapp [] TC_int, Tapp [] TC_word8] => (t1 = Tapp [] TC_word8array)
    | _ => False
  ) )"
|" type_op Aw8sub ts t1 = ( 
  (case  ts of
      [Tapp [] TC_word8array, Tapp [] TC_int] => (t1 = Tapp [] TC_word8)
    | _ => False
  ) )"
|" type_op Aw8length ts t1 = ( 
  (case  ts of [Tapp [] TC_word8array] => (t1 = Tapp [] TC_int) | _ => False ) )"
|" type_op Aw8update ts t1 = ( 
  (case  ts of
      [Tapp [] TC_word8array, Tapp [] TC_int, Tapp [] TC_word8] => t1 =
                                                                    Tapp 
                                                                    [] 
                                                                    TC_tup
    | _ => False
  ) )"
|" type_op (WordFromInt w1) ts t1 = ( 
  (case (w1,ts) of
      ( W8, [Tapp [] TC_int]) => t1 = Tapp [] TC_word8
    | ( W64, [Tapp [] TC_int]) => t1 = Tapp [] TC_word64
    | (_,_) => False
  ) )"
|" type_op (WordToInt w2) ts t1 = ( 
  (case (w2,ts) of
      ( W8, [Tapp [] TC_word8]) => t1 = Tapp [] TC_int
    | ( W64, [Tapp [] TC_word64]) => t1 = Tapp [] TC_int
    | (_,_) => False
  ) )"
|" type_op CopyStrStr ts t1 = ( 
  (case  ts of
      [Tapp [] TC_string, Tapp [] TC_int, Tapp [] TC_int] => t1 =
                                                               Tapp []
                                                                 TC_string
    | _ => False
  ) )"
|" type_op CopyStrAw8 ts t1 = ( 
  (case  ts of
      [Tapp [] TC_string, Tapp [] TC_int, Tapp [] TC_int, Tapp [] TC_word8array, Tapp [] TC_int] => 
  t1 = Tapp [] TC_tup
    | _ => False
  ) )"
|" type_op CopyAw8Str ts t1 = ( 
  (case  ts of
      [Tapp [] TC_word8array, Tapp [] TC_int, Tapp [] TC_int] => t1 =
                                                                   Tapp 
                                                                   []
                                                                    TC_string
    | _ => False
  ) )"
|" type_op CopyAw8Aw8 ts t1 = ( 
  (case  ts of
      [Tapp [] TC_word8array, Tapp [] TC_int, Tapp [] TC_int, Tapp [] TC_word8array, Tapp [] TC_int] => 
  t1 = Tapp [] TC_tup
    | _ => False
  ) )"
|" type_op Ord ts t1 = ( 
  (case  ts of [Tapp [] TC_char] => (t1 = Tint) | _ => False ) )"
|" type_op Chr ts t1 = ( 
  (case  ts of [Tapp [] TC_int] => (t1 = Tchar) | _ => False ) )"
|" type_op (Chopb o3) ts t1 = ( 
  (case (o3,ts) of
      ( _, [Tapp [] TC_char, Tapp [] TC_char]) => (t1 =
                                                     Tapp []
                                                       (TC_name
                                                          (Short (''bool''))))
    | (_,_) => False
  ) )"
|" type_op Implode ts t1 = ( 
  (case  ts of
      [] => False
    | t0 # l0 => (case  t0 of
                     Tvar _ => False
                   | Tvar_db _ => False
                   | Tapp l1 t4 => (case  l1 of
                                       [] => False
                                     | t5 # l2 => (case  t5 of
                                                      Tvar _ => False
                                                    | Tvar_db _ => False
                                                    | Tapp l3 t7 => (case  l3 of
                                                                    [] => 
                                                                    (case  t7 of
                                                                    TC_name _ => 
                                                                    False
                                                                    | TC_int => 
                                                                    False
                                                                    | TC_char => 
                                                                    (case  l2 of
                                                                    [] => 
                                                                    (case  t4 of
                                                                    TC_name i0 => 
                                                                    (case  i0 of
                                                                    Short s1 =>
                                                                    if
                                                                    (
                                                                    s1 =
                                                                    (''list'')) then
                                                                    (
                                                                    (case  l0 of
                                                                    [] => 
                                                                    t1 =
                                                                    Tapp 
                                                                    []
                                                                    TC_string
                                                                    | _ => 
                                                                    False
                                                                    )) else
                                                                    False
                                                                    | Long _ _ => 
                                                                    False
                                                                    )
                                                                    | TC_int => 
                                                                    False
                                                                    | TC_char => 
                                                                    False
                                                                    | TC_string => 
                                                                    False
                                                                    | TC_ref => 
                                                                    False
                                                                    | TC_word8 => 
                                                                    False
                                                                    | TC_word64 => 
                                                                    False
                                                                    | TC_word8array => 
                                                                    False
                                                                    | TC_fn => 
                                                                    False
                                                                    | TC_tup => 
                                                                    False
                                                                    | TC_exn => 
                                                                    False
                                                                    | TC_vector => 
                                                                    False
                                                                    | TC_array => 
                                                                    False
                                                                    )
                                                                    | _ # _ => 
                                                                    False
                                                                    )
                                                                    | TC_string => 
                                                                    False
                                                                    | TC_ref => 
                                                                    False
                                                                    | TC_word8 => 
                                                                    False
                                                                    | TC_word64 => 
                                                                    False
                                                                    | TC_word8array => 
                                                                    False
                                                                    | TC_fn => 
                                                                    False
                                                                    | TC_tup => 
                                                                    False
                                                                    | TC_exn => 
                                                                    False
                                                                    | TC_vector => 
                                                                    False
                                                                    | TC_array => 
                                                                    False
                                                                    )
                                                                    | _ # _ => 
                                                                    False
                                                                    )
                                                  )
                                   )
                 )
  ) )"
|" type_op Strsub ts t1 = ( 
  (case  ts of
      [Tapp [] TC_string, Tapp [] TC_int] => t1 = Tchar
    | _ => False
  ) )"
|" type_op Strlen ts t1 = ( 
  (case  ts of [Tapp [] TC_string] => t1 = Tint | _ => False ) )"
|" type_op Strcat ts t1 = ( 
  (case  ts of
      [] => False
    | t10 # l6 => (case  t10 of
                      Tvar _ => False
                    | Tvar_db _ => False
                    | Tapp l7 t12 => (case  l7 of
                                         [] => False
                                       | t13 # l8 => (case  t13 of
                                                         Tvar _ => False
                                                       | Tvar_db _ => 
                                                     False
                                                       | Tapp l9 t15 => 
                                                     (case  l9 of
                                                         [] => (case  t15 of
                                                                   TC_name _ => 
                                                               False
                                                                 | TC_int => 
                                                               False
                                                                 | TC_char => 
                                                               False
                                                                 | TC_string => 
                                                               (case  l8 of
                                                                   [] => 
                                                               (case  t12 of
                                                                   TC_name i3 => 
                                                               (case  i3 of
                                                                   Short s3 =>
                                                               if(s3 =
                                                                    (''list'')) then
                                                                 ((case  l6 of
                                                                    [] => 
                                                                  t1 =
                                                                    Tapp 
                                                                    []
                                                                    TC_string
                                                                    | _ => 
                                                                  False
                                                                  )) else
                                                                 False
                                                                 | Long _ _ => 
                                                               False
                                                               )
                                                                 | TC_int => 
                                                               False
                                                                 | TC_char => 
                                                               False
                                                                 | TC_string => 
                                                               False
                                                                 | TC_ref => 
                                                               False
                                                                 | TC_word8 => 
                                                               False
                                                                 | TC_word64 => 
                                                               False
                                                                 | TC_word8array => 
                                                               False
                                                                 | TC_fn => 
                                                               False
                                                                 | TC_tup => 
                                                               False
                                                                 | TC_exn => 
                                                               False
                                                                 | TC_vector => 
                                                               False
                                                                 | TC_array => 
                                                               False
                                                               )
                                                                 | _ # _ => 
                                                               False
                                                               )
                                                                 | TC_ref => 
                                                               False
                                                                 | TC_word8 => 
                                                               False
                                                                 | TC_word64 => 
                                                               False
                                                                 | TC_word8array => 
                                                               False
                                                                 | TC_fn => 
                                                               False
                                                                 | TC_tup => 
                                                               False
                                                                 | TC_exn => 
                                                               False
                                                                 | TC_vector => 
                                                               False
                                                                 | TC_array => 
                                                               False
                                                               )
                                                       | _ # _ => False
                                                     )
                                                     )
                                     )
                  )
  ) )"
|" type_op VfromList ts t1 = ( 
  (case  ts of
      [] => False
    | t18 # l12 => (case  t18 of
                       Tvar _ => False
                     | Tvar_db _ => False
                     | Tapp l13 t20 => (case  l13 of
                                           [] => False
                                         | t21 # l14 => (case  l14 of
                                                            [] => (case  t20 of
                                                                    TC_name i5 => 
                                                                  (case  i5 of
                                                                    Short s5 =>
                                                                  if(
                                                                    s5 =
                                                                    (''list'')) then
                                                                    (
                                                                    (case 
                                                                    (t21,l12) of
                                                                    (_,[]) => 
                                                                    t1 =
                                                                    Tapp
                                                                    [t21]
                                                                    TC_vector
                                                                    | (_,_) => 
                                                                    False
                                                                    )) else
                                                                    False
                                                                    | Long _ _ => 
                                                                  False
                                                                  )
                                                                    | TC_int => 
                                                                  False
                                                                    | TC_char => 
                                                                  False
                                                                    | TC_string => 
                                                                  False
                                                                    | TC_ref => 
                                                                  False
                                                                    | TC_word8 => 
                                                                  False
                                                                    | TC_word64 => 
                                                                  False
                                                                    | TC_word8array => 
                                                                  False
                                                                    | TC_fn => 
                                                                  False
                                                                    | TC_tup => 
                                                                  False
                                                                    | TC_exn => 
                                                                  False
                                                                    | TC_vector => 
                                                                  False
                                                                    | TC_array => 
                                                                  False
                                                                  )
                                                          | _ # _ => 
                                                        False
                                                        )
                                       )
                   )
  ) )"
|" type_op Vsub ts t1 = ( 
  (case  ts of
      [Tapp [t11] TC_vector, Tapp [] TC_int] => t1 = t11
    | _ => False
  ) )"
|" type_op Vlength ts t1 = ( 
  (case  ts of [Tapp [t11] TC_vector] => (t1 = Tapp [] TC_int) | _ => False ) )"
|" type_op Aalloc ts t1 = ( 
  (case  ts of
      [Tapp [] TC_int, t11] => t1 = Tapp [t11] TC_array
    | _ => False
  ) )"
|" type_op AallocEmpty ts t1 = ( 
  (case  ts of
      [Tapp [] TC_tup] =>( ∃ t10. t1 = Tapp [t10] TC_array)
    | _ => False
  ) )"
|" type_op Asub ts t1 = ( 
  (case  ts of
      [Tapp [t11] TC_array, Tapp [] TC_int] => t1 = t11
    | _ => False
  ) )"
|" type_op Alength ts t1 = ( 
  (case  ts of [Tapp [t11] TC_array] => t1 = Tapp [] TC_int | _ => False ) )"
|" type_op Aupdate ts t1 = ( 
  (case  ts of
      [Tapp [t11] TC_array, Tapp [] TC_int, t2] => (t11 = t2) ∧
                                                     (t1 = Tapp [] TC_tup)
    | _ => False
  ) )"
|" type_op ConfigGC ts t1 = ( 
  (case  ts of
      [Tapp [] TC_int, Tapp [] TC_int] => t1 = Tapp [] TC_tup
    | _ => False
  ) )"
|" type_op (FFI s0) ts t1 = ( 
  (case (s0,ts) of
      (_, [Tapp [] TC_string, Tapp [] TC_word8array]) => t1 = Tapp [] TC_tup
    | (_,_) => False
  ) )"


― ‹‹val check_type_names : tenv_abbrev -> t -> bool››
function (sequential,domintros) 
check_type_names  :: "((string),(string),((string)list*t))namespace ⇒ t ⇒ bool "  where 
     "
check_type_names tenvT (Tvar tv) = (
  True )"
|"
check_type_names tenvT (Tapp ts tn) = (
  (case  tn of
     TC_name tn =>
       (case  nsLookup tenvT tn of
           Some (tvs, t1) => List.length tvs = List.length ts
         | None => False
       )
   | _ => True
  ) ∧
  ((∀ x ∈ (set ts).  (check_type_names tenvT) x)))"
|"
check_type_names tenvT (Tvar_db n) = (
  True )" 
by pat_completeness auto


― ‹‹ Substitution of type names for the type they abbreviate ››
― ‹‹val type_name_subst : tenv_abbrev -> t -> t››
function (sequential,domintros) 
type_name_subst  :: "((string),(string),((string)list*t))namespace ⇒ t ⇒ t "  where 
     "
type_name_subst tenvT (Tvar tv) = ( Tvar tv )"
|"
type_name_subst tenvT (Tapp ts tc) = (
  (let args = (List.map (type_name_subst tenvT) ts) in
    (case  tc of
        TC_name tn =>
          (case  nsLookup tenvT tn of
              Some (tvs, t1) => type_subst (map_of (Lem_list_extra.zipSameLength tvs args)) t1
            | None => Tapp args tc
          )
      | _ => Tapp args tc
    )))"
|"
type_name_subst tenvT (Tvar_db n) = ( Tvar_db n )" 
by pat_completeness auto


― ‹‹ Check that a type definition defines no already defined types or duplicate
 * constructors, and that the free type variables of each constructor argument
 * type are included in the type's type parameters. Also check that all of the
 * types mentioned are in scope. ››
― ‹‹val check_ctor_tenv : tenv_abbrev -> list (list tvarN * typeN * list (conN * list t)) -> bool››
definition check_ctor_tenv  :: "((modN),(typeN),((tvarN)list*t))namespace ⇒((tvarN)list*typeN*(conN*(t)list)list)list ⇒ bool "  where 
     " check_ctor_tenv tenvT tds = (
  check_dup_ctors tds ∧
  (((∀ x ∈ (set tds).  ( λx .  
  (case  x of
      (tvs,tn,ctors) =>
  Lem_list.allDistinct tvs ∧
    ((∀ x ∈ (set ctors).
       ( λx .  (case  x of
                           (cn,ts) => ((∀ x ∈ (set ts).
                                         (check_freevars (( 0 :: nat)) tvs) x))
                                        ∧
                                        ((∀ x ∈ (set ts).
                                           (check_type_names tenvT) x))
                       )) x))
  )) x)) ∧
  Lem_list.allDistinct (List.map ( λx .  
  (case  x of (_,tn,_) => tn )) tds)))"


― ‹‹val build_ctor_tenv : list modN -> tenv_abbrev -> list (list tvarN * typeN * list (conN * list t)) -> tenv_ctor››
definition build_ctor_tenv  :: "(string)list ⇒((modN),(typeN),((tvarN)list*t))namespace ⇒((tvarN)list*string*(string*(t)list)list)list ⇒((string),(string),((tvarN)list*(t)list*tid_or_exn))namespace "  where 
     " build_ctor_tenv mn tenvT tds = (
  alist_to_ns
    (List.rev
      (List.concat
        (List.map
           ( λx .  
  (case  x of
      (tvs,tn,ctors) =>
  List.map
    ( λx .  (case  x of
                        (cn,ts) => (cn,(tvs,List.map (type_name_subst tenvT)
                                              ts, TypeId (mk_id mn tn)))
                    )) ctors
  ))
           tds))))"


― ‹‹ Check that an exception definition defines no already defined (or duplicate)
 * constructors, and that the arguments have no free type variables. ››
― ‹‹val check_exn_tenv : list modN -> conN -> list t -> bool››
definition check_exn_tenv  :: "(modN)list ⇒ string ⇒(t)list ⇒ bool "  where 
     " check_exn_tenv mn cn ts = (
  ((∀ x ∈ (set ts).  (check_freevars(( 0 :: nat)) []) x)))"


― ‹‹ For the value restriction on let-based polymorphism ››
― ‹‹val is_value : exp -> bool››
function (sequential,domintros) 
is_value  :: " exp0 ⇒ bool "  where 
     "
is_value (Lit _) = ( True )"
|"
is_value (Con _ es) = ( ((∀ x ∈ (set es).  is_value x)))"
|"
is_value (Var _) = ( True )"
|"
is_value (Fun _ _) = ( True )"
|"
is_value (Tannot e _) = ( is_value e )"
|"
is_value (Lannot e _) = ( is_value e )"
|"
is_value _ = ( False )" 
by pat_completeness auto


― ‹‹val tid_exn_to_tc : tid_or_exn -> tctor››
fun tid_exn_to_tc  :: " tid_or_exn ⇒ tctor "  where 
     " tid_exn_to_tc (TypeId tid) = ( TC_name tid )"
|" tid_exn_to_tc (TypeExn _) = ( TC_exn )"


inductive
type_ps  :: " nat ⇒ type_env ⇒(pat)list ⇒(t)list ⇒(varN*t)list ⇒ bool "  
      and
type_p  :: " nat ⇒ type_env ⇒ pat ⇒ t ⇒(varN*t)list ⇒ bool "  where

"pany" : " ⋀ tvs tenv t0.
check_freevars tvs [] t0
==>
type_p tvs tenv Pany t0 []"

|

"pvar" : " ⋀ tvs tenv n t0.
check_freevars tvs [] t0
==>
type_p tvs tenv (Pvar n) t0 [(n,t0)]"

|

"plit_int" : " ⋀ tvs tenv n.

type_p tvs tenv (Plit (IntLit n)) Tint []"

|

"plit_char" : " ⋀ tvs tenv c1.

type_p tvs tenv (Plit (Char c1)) Tchar []"

|

"plit_string" : " ⋀ tvs tenv s.

type_p tvs tenv (Plit (StrLit s)) Tstring []"

|

"plit_word8" : " ⋀ tvs tenv w.

type_p tvs tenv (Plit (Word8 w)) Tword8 []"

|

"plit_word64" : " ⋀ tvs tenv w.

type_p tvs tenv (Plit (Word64 w)) Tword64 []"

|

"pcon_some" : " ⋀ tvs tenv cn ps ts tvs' tn ts' bindings.
((∀ x ∈ (set ts').  (check_freevars tvs []) x)) ∧
((List.length ts' = List.length tvs') ∧
(type_ps tvs tenv ps (List.map (type_subst (map_of (Lem_list_extra.zipSameLength tvs' ts'))) ts) bindings ∧
(nsLookup(c0   tenv) cn = Some (tvs', ts, tn))))
==>
type_p tvs tenv (Pcon (Some cn) ps) (Tapp ts' (tid_exn_to_tc tn)) bindings "

|

"pcon_none" : " ⋀ tvs tenv ps ts bindings.
type_ps tvs tenv ps ts bindings
==>
type_p tvs tenv (Pcon None ps) (Tapp ts TC_tup) bindings "

|

"pref" : " ⋀ tvs tenv p t0 bindings.
type_p tvs tenv p t0 bindings
==>
type_p tvs tenv (Pref p) (Tref t0) bindings "

|

"ptypeannot" : " ⋀ tvs tenv p t0 bindings.
check_freevars(( 0 :: nat)) [] t0 ∧
(check_type_names(t   tenv) t0 ∧
type_p tvs tenv p (type_name_subst(t   tenv) t0) bindings)
==>
type_p tvs tenv (Ptannot p t0) (type_name_subst(t   tenv) t0) bindings "

|

"empty" : " ⋀ tvs tenv.

type_ps tvs tenv [] [] []"

|

"cons" : " ⋀ tvs tenv p ps t0 ts bindings bindings'.
type_p tvs tenv p t0 bindings ∧
type_ps tvs tenv ps ts bindings'
==>
type_ps tvs tenv (p # ps) (t0 # ts) (bindings'@bindings)"

inductive
type_funs  :: " type_env ⇒ tenv_val_exp ⇒(varN*varN*exp0)list ⇒(varN*t)list ⇒ bool "  
      and
type_es  :: " type_env ⇒ tenv_val_exp ⇒(exp0)list ⇒(t)list ⇒ bool "  
      and
type_e  :: " type_env ⇒ tenv_val_exp ⇒ exp0 ⇒ t ⇒ bool "  where

"lit_int" : " ⋀ tenv tenvE n.

type_e tenv tenvE (Lit (IntLit n)) Tint "

|

"lit_char" : " ⋀ tenv tenvE c1.

type_e tenv tenvE (Lit (Char c1)) Tchar "

|

"lit_string" : " ⋀ tenv tenvE s.

type_e tenv tenvE (Lit (StrLit s)) Tstring "

|

"lit_word8" : " ⋀ tenv tenvE w.

type_e tenv tenvE (Lit (Word8 w)) Tword8 "

|

"lit_word64" : " ⋀ tenv tenvE w.

type_e tenv tenvE (Lit (Word64 w)) Tword64 "

|

"raise" : " ⋀ tenv tenvE e t0.
check_freevars (num_tvs tenvE) [] t0 ∧
type_e tenv tenvE e Texn
==>
type_e tenv tenvE (Raise e) t0 "


|

"handle" : " ⋀ tenv tenvE e pes t0.
type_e tenv tenvE e t0 ∧ (¬ (pes = []) ∧
((∀ (p,e) ∈  
  List.set pes. ( ∃ bindings. 
   Lem_list.allDistinct (pat_bindings p []) ∧
   (type_p (num_tvs tenvE) tenv p Texn bindings ∧
   type_e tenv (bind_var_list(( 0 :: nat)) bindings tenvE) e t0)))))
==>
type_e tenv tenvE (Handle e pes) t0 "

|

"con_some" : " ⋀ tenv tenvE cn es tvs tn ts' ts.
((∀ x ∈ (set ts').  (check_freevars (num_tvs tenvE) []) x)) ∧
((List.length tvs = List.length ts') ∧
(type_es tenv tenvE es (List.map (type_subst (map_of (Lem_list_extra.zipSameLength tvs ts'))) ts) ∧
(nsLookup(c0   tenv) cn = Some (tvs, ts, tn))))
==>
type_e tenv tenvE (Con (Some cn) es) (Tapp ts' (tid_exn_to_tc tn))"

|

"con_none" : " ⋀ tenv tenvE es ts.
type_es tenv tenvE es ts
==>
type_e tenv tenvE (Con None es) (Tapp ts TC_tup)"

|

"var" : " ⋀ tenv tenvE n t0 targs tvs.
(tvs = List.length targs) ∧
(((∀ x ∈ (set targs).  (check_freevars (num_tvs tenvE) []) x)) ∧
(lookup_var n tenvE tenv = Some (tvs,t0)))
==>
type_e tenv tenvE (Var n) (deBruijn_subst(( 0 :: nat)) targs t0)"

|

"fn" : " ⋀ tenv tenvE n e t1 t2.
check_freevars (num_tvs tenvE) [] t1 ∧
type_e tenv (Bind_name n(( 0 :: nat)) t1 tenvE) e t2
==>
type_e tenv tenvE (Fun n e) (Tfn t1 t2)"

|

"app" : " ⋀ tenv tenvE op0 es ts t0.
type_es tenv tenvE es ts ∧
(type_op op0 ts t0 ∧
check_freevars (num_tvs tenvE) [] t0)
==>
type_e tenv tenvE (App op0 es) t0 "

|

"log" : " ⋀ tenv tenvE l e1 e2.
type_e tenv tenvE e1 (Tapp [] (TC_name (Short (''bool'')))) ∧
type_e tenv tenvE e2 (Tapp [] (TC_name (Short (''bool''))))
==>
type_e tenv tenvE (Log l e1 e2) (Tapp [] (TC_name (Short (''bool''))))"

|

"if'" : " ⋀ tenv tenvE e1 e2 e3 t0.
type_e tenv tenvE e1 (Tapp [] (TC_name (Short (''bool'')))) ∧
(type_e tenv tenvE e2 t0 ∧
type_e tenv tenvE e3 t0)
==>
type_e tenv tenvE (If e1 e2 e3) t0 "

|

"mat" : " ⋀ tenv tenvE e pes t1 t2.
type_e tenv tenvE e t1 ∧ (¬ (pes = []) ∧
((∀ (p,e) ∈  
  List.set pes.  ( ∃ bindings. 
   Lem_list.allDistinct (pat_bindings p []) ∧
   (type_p (num_tvs tenvE) tenv p t1 bindings ∧
   type_e tenv (bind_var_list(( 0 :: nat)) bindings tenvE) e t2)))))
==>
type_e tenv tenvE (Mat e pes) t2 "

|

― ‹‹
let_poly : forall tenv tenvE n e1 e2 t1 t2 tvs.
is_value e1 &&
type_e tenv (bind_tvar tvs tenvE) e1 t1 &&
type_e tenv (opt_bind_name n tvs t1 tenvE) e2 t2
==>
type_e tenv tenvE (Let n e1 e2) t2

and
››

"let_mono" : " ⋀ tenv tenvE n e1 e2 t1 t2.
type_e tenv tenvE e1 t1 ∧
type_e tenv (opt_bind_name n(( 0 :: nat)) t1 tenvE) e2 t2
==>
type_e tenv tenvE (Let n e1 e2) t2 "

― ‹‹
and

letrec : forall tenv tenvE funs e t tenv' tvs.
type_funs tenv (bind_var_list 0 tenv' (bind_tvar tvs tenvE)) funs tenv' &&
type_e tenv (bind_var_list tvs tenv' tenvE) e t
==>
type_e tenv tenvE (Letrec funs e) t
››

|

"letrec" : " ⋀ tenv tenvE funs e t0 bindings.
type_funs tenv (bind_var_list(( 0 :: nat)) bindings tenvE) funs bindings ∧
type_e tenv (bind_var_list(( 0 :: nat)) bindings tenvE) e t0
==>
type_e tenv tenvE (Letrec funs e) t0 "

|

"typeannot": " ⋀ tenv tenvE e t0.
check_freevars(( 0 :: nat)) [] t0 ∧
(check_type_names(t   tenv) t0 ∧
type_e tenv tenvE e (type_name_subst(t   tenv) t0))
==>
type_e tenv tenvE (Tannot e t0) (type_name_subst(t   tenv) t0)"

|

"locannot": " ⋀ tenv tenvE e l t0.
type_e tenv tenvE e t0
==>
type_e tenv tenvE (Lannot e l) t0 "

|

"empty" : " ⋀ tenv tenvE.

type_es tenv tenvE [] []"

|

"cons" : " ⋀ tenv tenvE e es t0 ts.
type_e tenv tenvE e t0 ∧
type_es tenv tenvE es ts
==>
type_es tenv tenvE (e # es) (t0 # ts)"

|

"no_funs" : " ⋀ tenv tenvE.

type_funs tenv tenvE [] []"

|

"funs" : " ⋀ tenv tenvE fn n e funs bindings t1 t2.
check_freevars (num_tvs tenvE) [] (Tfn t1 t2) ∧
(type_e tenv (Bind_name n(( 0 :: nat)) t1 tenvE) e t2 ∧
(type_funs tenv tenvE funs bindings ∧
(Map.map_of bindings fn = None)))
==>
type_funs tenv tenvE ((fn, n, e)# funs) ((fn, Tfn t1 t2)# bindings)"

― ‹‹val tenv_add_tvs : nat -> alist varN t -> alist varN (nat * t)››
definition tenv_add_tvs  :: " nat ⇒(string*t)list ⇒(string*(nat*t))list "  where 
     " tenv_add_tvs tvs bindings = (
  List.map ( λx .  
  (case  x of (n,t1) => (n,(tvs,t1)) )) bindings )"


― ‹‹val type_pe_determ : type_env -> tenv_val_exp -> pat -> exp -> bool››
definition type_pe_determ  :: " type_env ⇒ tenv_val_exp ⇒ pat ⇒ exp0 ⇒ bool "  where 
     " type_pe_determ tenv tenvE p e = ((
  ∀ t1. 
  ∀ tenv1. 
  ∀ t2. 
  ∀ tenv2. 
    (type_p(( 0 :: nat)) tenv p t1 tenv1 ∧ (type_e tenv tenvE e t1 ∧
    (type_p(( 0 :: nat)) tenv p t2 tenv2 ∧ type_e tenv tenvE e t2)))
    ⟶
    (tenv1 = tenv2)))"


― ‹‹val tscheme_inst : (nat * t) -> (nat * t) -> bool››
fun tscheme_inst  :: " nat*t ⇒ nat*t ⇒ bool "  where 
     " tscheme_inst (tvs_spec, t_spec) (tvs_impl, t_impl) = ((
  ∃ subst. 
    (List.length subst = tvs_impl) ∧
    (check_freevars tvs_impl [] t_impl ∧
    (((∀ x ∈ (set subst).  (check_freevars tvs_spec []) x)) ∧
    (deBruijn_subst(( 0 :: nat)) subst t_impl = t_spec)))))"


inductive
type_d  :: " bool ⇒(modN)list ⇒ decls ⇒ type_env ⇒ dec ⇒ decls ⇒ type_env ⇒ bool "  where

"dlet_poly" : " ⋀ extra_checks tvs mn tenv p e t0 bindings decls locs.
is_value e ∧
(Lem_list.allDistinct (pat_bindings p []) ∧
(type_p tvs tenv p t0 bindings ∧
(type_e tenv (bind_tvar tvs Empty) e t0 ∧
(extra_checks ⟶
  ((∀ tvs'. ∀ bindings'. ∀ t'. 
    (type_p tvs' tenv p t' bindings' ∧
    type_e tenv (bind_tvar tvs' Empty) e t') ⟶
      list_all2 tscheme_inst (List.map snd (tenv_add_tvs tvs' bindings')) (List.map snd (tenv_add_tvs tvs bindings))))))))
==>
type_d extra_checks mn decls tenv (Dlet locs p e)
  empty_decls (| v0 = (alist_to_ns (tenv_add_tvs tvs bindings)), c0 = nsEmpty, t = nsEmpty |) "

|

"dlet_mono" : " ⋀ extra_checks mn tenv p e t0 bindings decls locs.
― ‹‹ The following line makes sure that when the value restriction prohibits
   generalisation, a type error is given rather than picking an arbitrary
   instantiation. However, we should only do the check when the extra_checks
   argument tells us to. ››
(extra_checks ⟶ (¬ (is_value e) ∧ type_pe_determ tenv Empty p e)) ∧
(Lem_list.allDistinct (pat_bindings p []) ∧
(type_p(( 0 :: nat)) tenv p t0 bindings ∧
type_e tenv Empty e t0))
==>
type_d extra_checks mn decls tenv (Dlet locs p e)
  empty_decls (| v0 = (alist_to_ns (tenv_add_tvs(( 0 :: nat)) bindings)), c0 = nsEmpty, t = nsEmpty |) "

|

"dletrec" : " ⋀ extra_checks mn tenv funs bindings tvs decls locs.
type_funs tenv (bind_var_list(( 0 :: nat)) bindings (bind_tvar tvs Empty)) funs bindings ∧
(extra_checks ⟶
  ((∀ tvs'. ∀ bindings'. 
    type_funs tenv (bind_var_list(( 0 :: nat)) bindings' (bind_tvar tvs' Empty)) funs bindings' ⟶
      list_all2 tscheme_inst (List.map snd (tenv_add_tvs tvs' bindings')) (List.map snd (tenv_add_tvs tvs bindings)))))
==>
type_d extra_checks mn decls tenv (Dletrec locs funs)
  empty_decls (| v0 = (alist_to_ns (tenv_add_tvs tvs bindings)), c0 = nsEmpty, t = nsEmpty |) "

|

"dtype" : " ⋀ extra_checks mn tenv tdefs decls defined_types' decls' tenvT locs.
check_ctor_tenv (nsAppend tenvT(t   tenv)) tdefs ∧
((defined_types' = List.set (List.map ( λx .  
  (case  x of (tvs,tn,ctors) => (mk_id mn tn) )) tdefs)) ∧
(disjnt defined_types'(defined_types0   decls) ∧
((tenvT = alist_to_ns (List.map ( λx .  
  (case  x of
      (tvs,tn,ctors) => (tn, (tvs, Tapp (List.map Tvar tvs)
                                     (TC_name (mk_id mn tn))))
  )) tdefs)) ∧
(decls' = (| defined_mods0 = ({}), defined_types0 = defined_types', defined_exns = ({}) |)))))
==>
type_d extra_checks mn decls tenv (Dtype locs tdefs)
  decls' (| v0 = nsEmpty, c0 = (build_ctor_tenv mn (nsAppend tenvT(t   tenv)) tdefs), t = tenvT |) "

|

"dtabbrev" : " ⋀ extra_checks mn decls tenv tvs tn t0 locs.
check_freevars(( 0 :: nat)) tvs t0 ∧
(check_type_names(t   tenv) t0 ∧
Lem_list.allDistinct tvs)
==>
type_d extra_checks mn decls tenv (Dtabbrev locs tvs tn t0)
  empty_decls (| v0 = nsEmpty, c0 = nsEmpty,
                 t = (nsSing tn (tvs,type_name_subst(t   tenv) t0)) |) "

|

"dexn" : " ⋀ extra_checks mn tenv cn ts decls decls' locs.
check_exn_tenv mn cn ts ∧
(¬ (mk_id mn cn ∈(defined_exns   decls)) ∧
(((∀ x ∈ (set ts).  (check_type_names(t   tenv)) x)) ∧
(decls' = (| defined_mods0 = ({}), defined_types0 = ({}), defined_exns = ({mk_id mn cn}) |))))
==>
type_d extra_checks mn decls tenv (Dexn locs cn ts)
  decls' (| v0 = nsEmpty,
            c0 = (nsSing cn ([], List.map (type_name_subst(t   tenv)) ts, TypeExn (mk_id mn cn))),
            t = nsEmpty |) "

inductive
type_ds  :: " bool ⇒(modN)list ⇒ decls ⇒ type_env ⇒(dec)list ⇒ decls ⇒ type_env ⇒ bool "  where

"empty" : " ⋀ extra_checks mn tenv decls.

type_ds extra_checks mn decls tenv []
  empty_decls (| v0 = nsEmpty, c0 = nsEmpty, t = nsEmpty |) "

|

"cons" : " ⋀ extra_checks mn tenv d ds tenv1 tenv2 decls decls1 decls2.
type_d extra_checks mn decls tenv d decls1 tenv1 ∧
type_ds extra_checks mn (union_decls decls1 decls) (extend_dec_tenv tenv1 tenv) ds decls2 tenv2
==>
type_ds extra_checks mn decls tenv (d # ds)
  (union_decls decls2 decls1) (extend_dec_tenv tenv2 tenv1)"

inductive
type_specs  :: "(modN)list ⇒ tenv_abbrev ⇒ specs ⇒ decls ⇒ type_env ⇒ bool "  where

"empty" : " ⋀ mn tenvT.

type_specs mn tenvT []
  empty_decls (| v0 = nsEmpty, c0 = nsEmpty, t = nsEmpty |) "

|

"sval" : " ⋀ mn tenvT x t0 specs tenv fvs decls subst.
check_freevars(( 0 :: nat)) fvs t0 ∧
(check_type_names tenvT t0 ∧
(type_specs mn tenvT specs decls tenv ∧
(subst = map_of (Lem_list_extra.zipSameLength fvs (List.map Tvar_db (genlist (λ x .  x) (List.length fvs)))))))
==>
type_specs mn tenvT (Sval x t0 # specs)
  decls
  (extend_dec_tenv tenv
    (| v0 = (nsSing x (List.length fvs, type_subst subst (type_name_subst tenvT t0))),
       c0 = nsEmpty,
       t = nsEmpty |))"

|

"stype" : " ⋀ mn tenvT tenv td specs decls' decls tenvT'.
(tenvT' = alist_to_ns (List.map ( λx .  
  (case  x of
      (tvs,tn,ctors) => (tn, (tvs, Tapp (List.map Tvar tvs)
                                     (TC_name (mk_id mn tn))))
  )) td)) ∧
(check_ctor_tenv (nsAppend tenvT' tenvT) td ∧
(type_specs mn (nsAppend tenvT' tenvT) specs decls tenv ∧
(decls' = (| defined_mods0 = ({}),
            defined_types0 = (List.set (List.map ( λx .  
  (case  x of (tvs,tn,ctors) => (mk_id mn tn) )) td)),
            defined_exns = ({}) |))))
==>
type_specs mn tenvT (Stype td # specs)
  (union_decls decls decls')
  (extend_dec_tenv tenv
   (| v0 = nsEmpty,
      c0 = (build_ctor_tenv mn (nsAppend tenvT' tenvT) td),
      t = tenvT' |))"

|

"stabbrev" : " ⋀ mn tenvT tenvT' tvs tn t0 specs decls tenv.
Lem_list.allDistinct tvs ∧
(check_freevars(( 0 :: nat)) tvs t0 ∧
(check_type_names tenvT t0 ∧
((tenvT' = nsSing tn (tvs,type_name_subst tenvT t0)) ∧
type_specs mn (nsAppend tenvT' tenvT) specs decls tenv)))
==>
type_specs mn tenvT (Stabbrev tvs tn t0 # specs)
  decls (extend_dec_tenv tenv (| v0 = nsEmpty, c0 = nsEmpty, t = tenvT' |))"

|

"sexn" : " ⋀ mn tenvT tenv cn ts specs decls.
check_exn_tenv mn cn ts ∧
(type_specs mn tenvT specs decls tenv ∧
((∀ x ∈ (set ts).  (check_type_names tenvT) x)))
==>
type_specs mn tenvT (Sexn cn ts # specs)
  (union_decls decls (| defined_mods0 = ({}), defined_types0 = ({}), defined_exns = ({mk_id mn cn}) |))
  (extend_dec_tenv tenv
   (| v0 = nsEmpty,
      c0 = (nsSing cn ([], List.map (type_name_subst tenvT) ts, TypeExn (mk_id mn cn))),
      t = nsEmpty |))"

|

"stype_opq" : " ⋀ mn tenvT tenv tn specs tvs decls tenvT'.
Lem_list.allDistinct tvs ∧
((tenvT' = nsSing tn (tvs, Tapp (List.map Tvar tvs) (TC_name (mk_id mn tn)))) ∧
type_specs mn (nsAppend tenvT' tenvT) specs decls tenv)
==>
type_specs mn tenvT (Stype_opq tvs tn # specs)
  (union_decls decls (| defined_mods0 = ({}), defined_types0 = ({mk_id mn tn}), defined_exns = ({}) |))
  (extend_dec_tenv tenv (| v0 = nsEmpty, c0 = nsEmpty, t = tenvT' |))"

― ‹‹val weak_decls : decls -> decls -> bool››
definition weak_decls  :: " decls ⇒ decls ⇒ bool "  where 
     " weak_decls decls_impl decls_spec = (
  ((defined_mods0   decls_impl) =(defined_mods0   decls_spec)) ∧
  (((defined_types0   decls_spec) ⊆(defined_types0   decls_impl)) ∧
  ((defined_exns   decls_spec) ⊆(defined_exns   decls_impl))))"


― ‹‹val weak_tenvT : id modN typeN -> (list tvarN * t) -> (list tvarN * t) -> bool››
fun weak_tenvT  :: "((modN),(typeN))id0 ⇒(string)list*t ⇒(string)list*t ⇒ bool "  where 
     " weak_tenvT n (tvs_spec, t_spec) (tvs_impl, t_impl) = (
  (
  ― ‹‹ For simplicity, we reject matches that differ only by renaming of bound type variables ››tvs_spec = tvs_impl) ∧
  ((t_spec = t_impl) ∨
   (
   ― ‹‹ The specified type is opaque ››t_spec = Tapp (List.map Tvar tvs_spec) (TC_name n))))"


definition tscheme_inst2  :: " 'a ⇒ nat*t ⇒ nat*t ⇒ bool "  where 
     " tscheme_inst2 _ ts1 ts2 = ( tscheme_inst ts1 ts2 )"


― ‹‹val weak_tenv : type_env -> type_env -> bool››
definition weak_tenv  :: " type_env ⇒ type_env ⇒ bool "  where 
     " weak_tenv tenv_impl tenv_spec = (
  nsSub tscheme_inst2(v0   tenv_spec)(v0   tenv_impl) ∧
  (nsSub ( λx .  
  (case  x of _ => λ x y .  x = y ))(c0   tenv_spec)(c0   tenv_impl) ∧
  nsSub weak_tenvT(t   tenv_spec)(t   tenv_impl)))"


inductive
check_signature  :: "(modN)list ⇒ tenv_abbrev ⇒ decls ⇒ type_env ⇒(specs)option ⇒ decls ⇒ type_env ⇒ bool "  where

"none" : " ⋀ mn tenvT decls tenv.

check_signature mn tenvT decls tenv None decls tenv "

|

"some" : " ⋀ mn specs tenv_impl tenv_spec decls_impl decls_spec tenvT.
weak_tenv tenv_impl tenv_spec ∧
(weak_decls decls_impl decls_spec ∧
type_specs mn tenvT specs decls_spec tenv_spec)
==>
check_signature mn tenvT decls_impl tenv_impl (Some specs) decls_spec tenv_spec "

definition tenvLift  :: " string ⇒ type_env ⇒ type_env "  where 
     " tenvLift mn tenv = (
  (| v0 = (nsLift mn(v0   tenv)), c0 = (nsLift mn(c0   tenv)), t = (nsLift mn(t   tenv))  |) )"


inductive
type_top  :: " bool ⇒ decls ⇒ type_env ⇒ top0 ⇒ decls ⇒ type_env ⇒ bool "  where

"tdec" : " ⋀ extra_checks tenv d tenv' decls decls'.
type_d extra_checks [] decls tenv d decls' tenv'
==>
type_top extra_checks decls tenv (Tdec d) decls' tenv' "

|

"tmod" : " ⋀ extra_checks tenv mn spec ds tenv_impl tenv_spec decls decls_impl decls_spec.
¬ ([mn] ∈(defined_mods0   decls)) ∧
(type_ds extra_checks [mn] decls tenv ds decls_impl tenv_impl ∧
check_signature [mn](t   tenv) decls_impl tenv_impl spec decls_spec tenv_spec)
==>
type_top extra_checks decls tenv (Tmod mn spec ds)
  (union_decls (| defined_mods0 = ({[mn]}), defined_types0 = ({}), defined_exns = ({}) |) decls_spec)
  (tenvLift mn tenv_spec)"

inductive
type_prog  :: " bool ⇒ decls ⇒ type_env ⇒(top0)list ⇒ decls ⇒ type_env ⇒ bool "  where

"empty" : " ⋀ extra_checks tenv decls.

type_prog extra_checks decls tenv [] empty_decls (| v0 = nsEmpty, c0 = nsEmpty, t = nsEmpty |) "

|

"cons" : " ⋀ extra_checks tenv top0 tops tenv1 tenv2 decls decls1 decls2.
type_top extra_checks decls tenv top0 decls1 tenv1 ∧
type_prog extra_checks (union_decls decls1 decls) (extend_dec_tenv tenv1 tenv) tops decls2 tenv2
==>
type_prog extra_checks decls tenv (top0 # tops)
  (union_decls decls2 decls1) (extend_dec_tenv tenv2 tenv1)"
end