diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/test/vectors.sail | 1 | ||||
| -rw-r--r-- | src/type_internal.ml | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/test/vectors.sail b/src/test/vectors.sail index da5a525b..910ca329 100644 --- a/src/test/vectors.sail +++ b/src/test/vectors.sail @@ -76,6 +76,7 @@ function bit main _ = { (* constraints checking *) BA := 12; + CR := 0b00000000000000000000000000000000; CR[32 + BA] := CR[32 + BA]; (* slice access of literal *) diff --git a/src/type_internal.ml b/src/type_internal.ml index 45b89f3b..c5654bf5 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -489,10 +489,13 @@ let initial_kind_env = ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ) ] +let mk_range n = {t=Tapp("range",[TA_nexp {nexp=n};TA_nexp {nexp=Nconst 0}])} 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 None,[],pure_e)); - ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "add"),[],pure_e)); + ("+",Some(([("n",{k=K_Nat});("m",{k=K_Nat})],{t= Tfn({t=Ttup([mk_range (Nvar "n");mk_range (Nvar "m")])}, + (mk_range (Nadd({nexp=Nvar "n"},{nexp=Nvar "m"}))), + pure_e)}),External (Some "add"),[],pure_e)); ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e)); ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e)); ("mod",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "mod"),[],pure_e)); |