diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser.mly | 4 | ||||
| -rw-r--r-- | src/type_internal.ml | 9 |
2 files changed, 13 insertions, 0 deletions
diff --git a/src/parser.mly b/src/parser.mly index 7027d7a6..fb7ffa44 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -585,6 +585,10 @@ atomic_exp: { eloc (E_vector_update($2,$4,$6)) } | Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare { eloc (E_vector_update_subrange($2,$4,$6,$8)) } + | SquareBarBar BarBarSquare + { eloc (E_list []) } + | SquareBarBar exp BarBarSquare + { eloc (E_list [$2]) } | SquareBarBar comma_exps BarBarSquare { eloc (E_list($2)) } | Switch exp Lcurly case_exps Rcurly diff --git a/src/type_internal.ml b/src/type_internal.ml index 85e6b15e..51b03883 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2268,6 +2268,15 @@ let initial_typ_env = mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")]) (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))), (External (Some "mod_signed_vec")),[],pure_e,pure_e,nob)])); + ("div", + Base(((mk_nat_params["n";"m";"o";]), + (mk_pure_fun (mk_tup [mk_atom (mk_nv "n");mk_atom (mk_nv "m")]) + (mk_atom (mk_nv "o")))), + (*This should really be != to 0, as negative is just fine*) + (External (Some "quot")),[(*GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "m"),n_one);*) + LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee, + (mk_mult (mk_nv "n") (mk_nv "o")),(mk_nv "m"))], + pure_e,pure_e,nob)); ("quot", Overload( Base(((mk_typ_params ["a";"b";"c"]), |