summaryrefslogtreecommitdiff
path: root/language/l2_typ.ott
diff options
context:
space:
mode:
Diffstat (limited to 'language/l2_typ.ott')
-rw-r--r--language/l2_typ.ott326
1 files changed, 326 insertions, 0 deletions
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
new file mode 100644
index 00000000..43a3ea17
--- /dev/null
+++ b/language/l2_typ.ott
@@ -0,0 +1,326 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% 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 }}
+ | id :: :: id
+ | kid :: :: var
+ | t1 -> t2 effect :: :: fn
+ | ( t1 * .... * tn ) :: :: tup
+ | id t_args :: :: app
+ | register t_args :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }}
+ | t [ t1 / id1 ... tn / idn ] :: 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
+ | 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
+
+ne :: 'Ne_' ::=
+ {{ com internal numeric expressions }}
+ | kid :: :: var
+ | num :: :: const
+ | ne1 * ne2 :: :: mult
+ | ne1 + ... + nen :: :: add
+ | 2 ** ne :: :: exp
+ | ( - ne ) :: :: unary
+ | zero :: S :: zero
+ {{ lem (Ne_const 0) }}
+ | bitlength ( bin ) :: M :: cbin
+ {{ ocaml (asssert false) }}
+ {{ hol ARB }}
+ {{ lem (blength [[bin]]) }}
+ | bitlength ( hex ) :: M :: chex
+ {{ ocaml (assert false) }}
+ {{ hol ARB }}
+ {{ lem (hlength [[hex]]) }}
+ | 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
+
+ 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
+ | kid 'IN' { num1 , ... , numn } :: :: in
+
+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 records, enumerations, and kinds }}
+ | < E_k , 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
+
+ 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]]) }}
+ | ( 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+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }}
+ {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:49:15 +0000