TypedEnv = Env + Types +

(* 'a stands for the type of linear types. 'b stands for the type of
nonlinear types. *)

types

('a,'b) env = ('a,'b) vty list

(* Addition of a type to an environment. *)

constdefs canaddtypetoenv :: "('a,'b) env => nat => ('a,'b) vty => bool"
"canaddtypetoenv G n t == ((n < length G) & (canaddt (typeof n G) t))"

consts addtypetoenv :: "('a,'b) env => nat => ('a,'b) vty => ('a,'b) env"
primrec
"addtypetoenv G 0       t = (addt (hd G) t) # (tl G)"
"addtypetoenv G (Suc n) t = (hd G) # (addtypetoenv (tl G) n t)"

(* Addition of a list of types (with positions) to an environment. *)

(* Types are added in reverse order, so that addtoenv matches
mAPP. The order doesn't matter anyway, as addition of types is
commutative. *)

consts addtoenv :: "('a,'b) env => nat list => ('a,'b) vty list => ('a,'b) env"
primrec
"addtoenv G [] ts     = G"
addtoenv_Cons 
"addtoenv G (n#ns) ts = \ 
\ addtypetoenv (addtoenv G ns (tl ts)) n (hd ts)"

consts canaddtoenv :: "('a,'b) env => nat list => ('a,'b) vty list => bool"
primrec
"canaddtoenv G [] ts     = (ts = [])"
"canaddtoenv G (n#ns) ts = \ 
\ (case ts of [] => False | v#vs => \ 
\   ((canaddtypetoenv (addtoenv G ns vs) n v) & \ 
\    (canaddtoenv G ns vs)))"

(* Addition of environments. *)

consts addenv :: "('a,'b) env => ('a,'b) env => ('a,'b) env"
primrec
"addenv []     us = []"
"addenv (t#ts) us = \ 
\ (case us of [] => [] | v#vs => (addt t v) # (addenv ts vs))"

consts canaddenv :: "('a,'b) env => ('a,'b) env => bool"
primrec
"canaddenv [] us     = (us = [])"
"canaddenv (t#ts) us = \ 
\ (case us of [] => False | v#vs => \ 
\   ((canaddt t v) & (canaddenv ts vs)))"

consts canaddenvfrom :: "nat => ('a,'b) env => ('a,'b) env => bool"
primrec
"canaddenvfrom 0       ts us = canaddenv ts us"
"canaddenvfrom (Suc n) ts us = canaddenvfrom n (tl ts) (tl us)" 

(* Unlimited environments. *)

consts unlimited :: "('a,'b) env => bool"
primrec
"unlimited []     = True"
"unlimited (t#ts) = ((unlim t) & (unlimited ts))"

(* Skeleton of an environment. *)

constdefs skeleton :: "('a,'b) env => ('a,'b) env"
"skeleton G == map skel G"

(* Balanced environment. *)

consts balanced :: "('a,'b) env => bool"
primrec
"balanced []     = True"
"balanced (t#ts) = ((bal t) & (balanced ts))"

(* Using the capability of a type in an environment.

usetype x G  is the environment obtained by subtracting typeof x G
from G. If x >= length G then usetype x G = G. *)

consts usetype :: "nat => ('a,'b) env => ('a,'b) env"
primrec
"usetype x []     = []"
"usetype x (t#ts) = (case x of 0 => ((skel t) # ts) \ 
\                            | (Suc y) => (t # (usetype y ts)))" 

end
