diff options
| author | Gabriel Kerneis | 2014-06-12 17:19:29 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-06-12 17:36:03 +0100 |
| commit | 0e317b1e29182ff72143be3819efa368b0cef0e7 (patch) | |
| tree | 5cb981de2470c370f9824ecb163b823c3a6430dc | |
| parent | 89eb6678e6b2eabe5fd30f772df7587d668dff9b (diff) | |
Overloaded multiplication
Hopefully I got the constraints right again.
| -rw-r--r-- | src/type_internal.ml | 34 |
1 files changed, 30 insertions, 4 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 5444fb9e..e95f564e 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -810,10 +810,6 @@ let initial_typ_env = (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p")))), External (Some "add_bit_vec"), [], pure_e); ])); - ("*",Base(((mk_nat_params ["n";"m";"o";"p"]), - (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) - (mk_range (mk_mult (mk_nv "n") (mk_nv "o")) (mk_mult (mk_nv "m") (mk_nv "p"))))), - External (Some "multiply"),[],pure_e)); ("-",Overload(Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "minus"),[],pure_e), true, @@ -840,6 +836,36 @@ let initial_typ_env = (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "minus_range_vec"), [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})],pure_e); ])); + ("*",Overload(Base(((mk_typ_params ["a";"b";"c"]), + (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), External (Some "multiply"),[],pure_e), + true, + [Base(((mk_nat_params["n";"m";"o";"p"]), + (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); + mk_range (mk_nv "o") (mk_nv "p")]) + (mk_range (mk_mult (mk_nv "n") (mk_nv "o")) (mk_mult (mk_nv "m") (mk_nv "p"))))), + External (Some "multiply"), [],pure_e); + Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); + mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) + (* could also use 2*n instead of n+n *) + (mk_vector bit_t (Ovar "ord") (Nvar "o") (Nadd (mk_nv "n", mk_nv "n"))))), + External (Some "multiply_vec"), [],pure_e); + + Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); + mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) + (* could also use 2*m instead of m+m *) + (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), + External (Some "mult_range_vec"), + [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e); + Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), + (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); + mk_range (mk_nv "o") (mk_nv "p")]) + (* could also use 2*m instead of m+m *) + (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), + External (Some "mult_vec_range"), + [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})],pure_e); + ])); ("mod", Overload(Base(((mk_typ_params ["a";"b";"c"]), (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})), |