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