%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Machinery for typing rules % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% embed {{ lem let rec remove_one i l = match l with | [] -> [] | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) end let rec remove_from l l2 = match l2 with | [] -> l | i::l2' -> remove_from (remove_one i l) l2' end let disjoint s1 s2 = Set.null (s1 inter s2) let rec disjoint_all sets = match sets with | [] -> true | s1::[] -> true | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) end }} grammar k :: 'Ki_' ::= {{ com Internal kinds }} | K_Typ :: :: typ | K_Nat :: :: nat | K_Ord :: :: ord | K_Efct :: :: efct | K_Lam ( k0 .. kn -> k' ) :: :: ctor | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} t , u :: 'T_' ::= {{ com Internal types }} | x :: :: id | ' x :: :: var | t1 -> t2 effect :: :: fn | ( t1 , .... , tn ) :: :: tup | x < t_args > :: :: app | t |-> t1 :: :: abbrev | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} | atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }} | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }} | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }} | bit :: S :: bit_typ {{ ichlo T_id "bit" }} | string :: S :: string_typ {{ ichlo T_id "string" }} | unit :: S :: unit_typ {{ ichlo T_id "unit" }} | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} | x :: :: optx_x {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }} | :: :: optx_none {{ lem Nothing }} {{ ocaml None }} tag :: 'Tag_' ::= {{ com Data indicating where the identifier arises and thus information necessary in compilation }} | None :: :: empty | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} | Ctor :: :: ctor {{ com Data constructor from a type union }} | Extern optx :: :: extern {{ com External function, specied only with a val statement }} | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} | Spec :: :: spec | Enum :: :: enum | Alias :: :: alias ne :: 'Ne_' ::= {{ com internal numeric expressions }} | ' x :: :: var | num :: :: const | infinity :: :: inf | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add | 2 ** ne :: :: exp | ( - ne ) :: :: unary | zero :: S :: zero {{ lem (Ne_const 0) }} | one :: S :: one {{ lem (Ne_const 1) }} | bitlength ( bin ) :: M :: cbin {{ ocaml (asssert false) }} {{ hol ARB }} {{ lem (blength [[bin]]) }} | bitlength ( hex ) :: M :: chex {{ ocaml (assert false) }} {{ hol ARB }} {{ lem (hlength [[hex]]) }} | count ( num0 ... numi ) :: M :: length {{ichlo "todo" }} | length ( pat1 ... patn ) :: M :: cpat {{ ocaml (assert false) }} {{ hol ARB }} {{ lem (Ne_const (List.length [[pat1...patn]])) }} | length ( exp1 ... expn ) :: M :: cexp {{ hol ARB }} {{ ocaml (assert false) }} {{ lem (Ne_const (List.length [[exp1...expn]])) }} t_arg :: 't_arg_' ::= {{ com Argument to type constructors }} | t :: :: typ | ne :: :: nexp | effect :: :: effect | order :: :: order | fresh :: M :: freshvar {{ lem T_arg (T_var "fresh") }} t_args :: '' ::= {{ lem list t_arg }} {{ com Arguments to type constructors }} | t_arg1 ... t_argn :: :: T_args nec :: 'Nec_' ::= {{ com Numeric expression constraints }} | ne <= ne' :: :: lteq | ne = ne' :: :: eq | ne >= ne' :: :: gteq | ' x 'IN' { num1 , ... , numn } :: :: in | nec0 .. necn -> nec'0 ... nec'm :: :: cond | nec0 ... necn :: :: branch S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} {{ hol nec list }} {{ lem list nec }} {{ com nexp constraint lists }} | { nec1 , .. , necn } :: :: Sn_concrete {{ hol [[nec1 .. necn]] }} {{ lem [[nec1 .. necn]] }} | S_N1 u+ .. u+ S_Nn :: M :: SN_union {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }} {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }} {{ ocaml (assert false) }} | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }} {{ ocaml (assert false) }} {{ ichl todo }} | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }} {{ ocaml assert false }} {{ ichl todo }} | resolve ( S_N ) :: :: resolution {{ lem [[S_N]] (* Write constraint solver *) }} E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} {{ lem definition_env }} {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }} | < E_k , E_a , E_r , E_e > :: :: base {{ hol arb }} {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} | empty :: :: empty {{ hol arb }} {{ lem DenvEmp }} | E_d u+ E_d' :: :: union {{ hol arb }} {{ lem (denv_union [[E_d]] [[E_d']]) }} kinf :: 'kinf_' ::= {{ com Whether a kind is default or from a local binding }} | k :: :: k | k default :: :: def tid :: 'tid_' ::= {{ com A type identifier or type variable }} | id :: :: id | kid :: :: var E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} {{ hol (tid-> kinf) }} {{ lem (map tid kinf) }} {{ com Kind environments }} | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} | E_k1 u+ .. u+ E_kn :: M :: union {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }} {{ ocaml (assert false) }} | E_k u- E_k1 .. E_kn :: M :: multi_set_minus {{ hol arb }} {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} {{ ocaml assert false }} tinf :: 'tinf_' ::= {{ com Type variables, type, and constraints, bound to an identifier }} | t :: :: typ | E_k , S_N , tag , t :: :: quant_typ tinflist :: 'tinfs_' ::= {{ com In place so that a list of tinfs can be referred to without the dot form }} | tinf1 ... tinfn :: :: ls E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::= {{ phantom }} {{ hol tid |-> tinf}} {{ lem map tid tinf }} | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete | E_a1 u+ .. u+ E_an :: :: union field_typs :: 'FT_' ::= {{ phantom }} {{ lem list (id * t) }} {{ com Record fields }} | id1 : t1 , .. , idn : tn :: :: fields {{ lem [[id1 t1..idn tn]] }} E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} {{ hol (id*t) |-> tinf) }} {{ lem map (list (id*t)) tinf }} {{ com Record environments }} | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} | E_r1 u+ .. u+ E_rn :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} {{ ocaml (assert false) }} enumerate_map :: '' ::= {{ phantom }} {{ lem (list (nat*id)) }} | { num1 |-> id1 ... numn |-> idn } :: :: enum_map {{ lem [[num1 id1...numn idn]] }} E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} {{ lem (map t (list (nat*id))) }} {{ com Enumeration environments }} | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} | E_e1 u+ .. u+ E_en :: :: union {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} embed {{ lem type definition_env = | DenvEmp | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) }} grammar E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} {{ hol (id |-> tinf) }} {{ lem map id tinf }} {{ com Type environments }} | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} | { id |-> overload tinf : tinf1 , ... , tinfn } :: :: overload | ( E_t1 u+ .... u+ E_tn ) :: M :: union {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} {{ ocaml (assert false) }} | u+ E_t1 .. E_tn :: M :: multi_union {{ hol arb }} {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} {{ ocaml assert false }} | E_t u- E_t1 .. E_tn :: M :: multi_set_minus {{ hol arb }} {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} {{ ocaml assert false }} | ( E_t1 inter .... inter E_tn ) :: M :: intersect {{ hol arb }} {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} {{ ocaml (assert false) }} | inter E_t1 .. E_tn :: M :: multi_inter {{ hol arb }} {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} {{ ocaml assert false }} ts :: ts_ ::= {{ phantom }} {{ lem list t }} | t1 , .. , tn :: :: lst embed {{ lem let blength (bit) = Ne_const 8 let hlength (bit) = Ne_const 8 type env = | EnvEmp | Env of (map id tinf) * definition_env type inf = | Iemp | Inf of (list nec) * effect val denv_union : definition_env -> definition_env -> definition_env let denv_union de1 de2 = match (de1,de2) with | (DenvEmp,de2) -> de2 | (de1,DenvEmp) -> de1 | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) end val env_union : env -> env -> env let env_union e1 e2 = match (e1,e2) with | (EnvEmp,e2) -> e2 | (e1,EnvEmp) -> e1 | ((Env te1 de1),(Env te2 de2)) -> Env (te1 union te2) (denv_union de1 de2) end let inf_union i1 i2 = match (i1,i2) with | (Iemp,i2) -> i2 | (i1,Iemp) -> i1 | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) end let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) }} grammar E :: '' ::= {{ hol ((string,env_body) fmaptree) }} {{ lem env }} {{ com Definition environment and lexical environment }} | < E_t , E_d > :: :: E {{ hol arb }} {{ lem (Env [[E_t]] [[E_d]]) }} | empty :: M :: E_empty {{ hol arb }} {{ lem EnvEmp }} {{ ocaml assert false }} | E u+ E' :: :: E_union {{ lem (env_union [[E]] [[E']]) }} I :: '' ::= {{ lem inf }} {{ com Information given by type checking an expression }} | < S_N , effect > :: :: I {{ lem (Inf [[S_N]] [[effect]]) }} | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} {{ lem Iemp }} | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }} | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}