# 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
```