diff options
| author | Kathy Gray | 2014-06-06 13:42:43 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-06-07 11:32:38 +0100 |
| commit | 956b5dcc550251ff05ff46d38ff77f4d4d245e2d (patch) | |
| tree | 4eb4536f5978493600c2cd82e8bb48ad04cb5515 /src | |
| parent | 0573e2f5e578be7e67dff6a68aa1f36225b9a3cc (diff) | |
Adding type abbreviations for uint8 to uint64 to make for easier casts
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 0c3efcab..f8799d37 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -691,6 +691,11 @@ let rec fresh_evar bindings e = | _ -> None let nat_t = {t = Tapp("range",[TA_nexp{nexp= Nconst zero};TA_nexp{nexp = Npos_inf};])} +let uint8_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 8)},Some (big_int_of_int 256))}])} +let uint16_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 16)},Some (big_int_of_int 65536))}])} +let uint32_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 32)},Some (big_int_of_int 4294967296))}])} +let uint64_t = {t = Tapp("range",[TA_nexp{nexp = Nconst zero}; TA_nexp{nexp = N2n({nexp = Nconst (big_int_of_int 64)},Some (big_int_of_string "18446744073709551616"))}])} + let unit_t = { t = Tid "unit" } let bit_t = {t = Tid "bit" } let bool_t = {t = Tid "bool" } @@ -708,6 +713,10 @@ let initial_kind_env = Envmap.from_list [ ("bool", {k = K_Typ}); ("nat", {k = K_Typ}); + ("uint8", {k = K_Typ}); + ("uint16", {k= K_Typ}); + ("uint32", {k=K_Typ}); + ("uint64", {k=K_Typ}); ("unit", {k = K_Typ}); ("bit", {k = K_Typ}); ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); @@ -717,6 +726,16 @@ let initial_kind_env = ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ) ] +let initial_abbrev_env = + Envmap.from_list [ + ("nat",Base(([],nat_t),Emp_global,[],pure_e)); + ("uint8",Base(([],uint8_t),Emp_global,[],pure_e)); + ("uint16",Base(([],uint16_t),Emp_global,[],pure_e)); + ("uint32",Base(([],uint32_t),Emp_global,[],pure_e)); + ("uint64",Base(([],uint64_t),Emp_global,[],pure_e)); + ] + + let mk_nat_params l = List.map (fun i -> (i,{k=K_Nat})) l let mk_typ_params l = List.map (fun i -> (i,{k=K_Typ})) l let mk_ord_params l = List.map (fun i -> (i,{k=K_Ord})) l @@ -883,10 +902,6 @@ let initial_typ_env = ("<<<",Base((["a",{k=K_Typ}],{t= Tfn ({t=Ttup([{t=Tvar "a"};nat_typ])},{t=Tvar "a"},pure_e)}),External (Some "bitwise_leftshift"),[],pure_e)); ] -let initial_abbrev_env = - Envmap.from_list [ - ("nat",Base(([],nat_t),Emp_global,[],pure_e)); - ] let rec t_subst s_env t = match t.t with |