diff options
| -rw-r--r-- | language/l2.lem | 14 | ||||
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 14 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 |
5 files changed, 26 insertions, 10 deletions
diff --git a/language/l2.lem b/language/l2.lem index c8eacad3..64838e88 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -33,7 +33,7 @@ type base_kind = (* base kind *) type nexp = (* expression of kind Nat, for vector sizes and origins *) | Nexp_var of kid (* variable *) - | Nexp_constant of nat (* constant *) + | Nexp_constant of natural (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) @@ -78,7 +78,7 @@ type n_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of kid * list nat + | NC_nat_set_bounded of kid * list natural type kinded_id = (* optionally kind-annotated identifier *) @@ -97,7 +97,7 @@ type lit = (* Literal constant *) | L_one (* $bitone : bit$ *) | L_true (* $true : bool$ *) | L_false (* $false : bool$ *) - | L_num of nat (* natural number constant *) + | L_num of natural (* natural number constant *) | L_hex of string (* bit vector constant, C-style *) | L_bin of string (* bit vector constant, C-style *) | L_undef (* constant representing undefined values *) @@ -133,7 +133,7 @@ type pat = (* Pattern *) | P_app of id * list pat (* union constructor pattern *) | P_record of list fpat * bool (* struct pattern *) | P_vector of list pat (* vector pattern *) - | P_vector_indexed of list (nat * pat) (* vector pattern (with explicit indices) *) + | P_vector_indexed of list (natural * pat) (* vector pattern (with explicit indices) *) | P_vector_concat of list pat (* concatenated vector pattern *) | P_tup of list pat (* tuple pattern *) | P_list of list pat (* list pattern *) @@ -157,7 +157,7 @@ type exp = (* Expression *) | E_if of exp * exp * exp (* conditional *) | E_for of id * exp * exp * exp * exp (* loop *) | E_vector of list exp (* vector (indexed from 0) *) - | E_vector_indexed of list (nat * exp) (* vector (indexed consecutively) *) + | E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *) | E_vector_access of exp * exp (* vector access *) | E_vector_subrange of exp * exp * exp (* subvector extraction *) | E_vector_update of exp * exp * exp (* vector functional update *) @@ -221,8 +221,8 @@ type tannot_opt = (* Optional type annotation for functions *) type index_range = (* index specification, for bitfields in register types *) - | BF_single of nat (* single index *) - | BF_range of nat * nat (* index range *) + | BF_single of natural (* single index *) + | BF_range of natural * natural (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) diff --git a/language/l2.ott b/language/l2.ott index 2224eb32..d7f03240 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -7,7 +7,7 @@ metavar num ::= {{ lex numeric }} {{ ocaml int }} {{ hol num }} - {{ lem nat }} + {{ lem natural }} {{ com Numeric literals }} metavar hex ::= diff --git a/language/l2_parse.ott b/language/l2_parse.ott index af90abaa..b617dc6c 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -7,7 +7,7 @@ metavar num ::= {{ lex numeric }} {{ ocaml int }} {{ hol num }} - {{ lem nat }} + {{ lem natural }} {{ com Numeric literals }} metavar hex ::= diff --git a/src/type_check.ml b/src/type_check.ml index 9be7a323..a253126a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -766,6 +766,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (lb',t_env',cs,ef) = (check_lbind envs lbind) in let (e,t,_,cs',_) = check_exp (Env(d_env,Envmap.union t_env t_env')) expect_t body in (E_aux(E_let(lb',e),(l,Some(([],t),Emp,cs@cs',pure_e))),t,t_env,cs@cs',pure_e) + | E_assign(lexp,exp) -> + let (lexp',t',t_env',tag,ef) = check_lexp envs lexp in + let (exp',t'',_,cs,ef) = check_exp envs t' exp in + let (t',c') = type_consistent l d_env unit_t expect_t in + (E_aux(E_assign(lexp',exp'),(l,(Some(([],unit_t),tag,cs,ef)))),unit_t,t_env',cs,ef) | _ -> (E_aux(e,(l,annot)),expect_t,t_env,[],pure_e) and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tannot emap * nexp_range list * t * effect) = @@ -796,6 +801,15 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r t'', csl@cs_p@cs_p'@cs2,union_effects efl ef2) +and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *effect) = + let (Env(d_env,t_env)) = envs in + match lexp with + | LEXP_id id -> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + | LEXP_memory(id,exps) -> (LEXP_aux(lexp,(l,annot)),new_t(),t_env,Emp,pure_e) + | LEXP_vector(vec,acc) -> (LEXP_aux(lexp,(l,annot)),new_t(),t_env,Emp,pure_e) + | LEXP_vector_range(vec,base,range)-> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + | LEXP_field(vec,id)-> (LEXP_aux(lexp,(l,annot))),new_t(),t_env,Emp,pure_e + and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect = let Env(d_env,t_env) = envs in match lbind with diff --git a/src/type_internal.ml b/src/type_internal.ml index bb9801a3..5b196e8b 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -200,7 +200,9 @@ let initial_typ_env = Envmap.from_list [ ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External,[],pure_e)); ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); - ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e)); + ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External,[],pure_e)); ] let initial_abbrev_env = |