summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKathy Gray2014-12-11 18:25:48 +0000
committerKathy Gray2014-12-11 18:25:48 +0000
commit86a94bfcdedcb1824d7869f8d3a0e595d7015fc3 (patch)
tree39cfca72941273d23fe6082cb0688fd40629850f /src
parent4e1f3c7012ad9bae2771b88eaca3fa6791582b55 (diff)
Add 2 ** n function; support providing type variables to other files when lexing
Diffstat (limited to 'src')
-rw-r--r--src/process_file.ml2
-rw-r--r--src/type_internal.ml6
2 files changed, 7 insertions, 1 deletions
diff --git a/src/process_file.ml b/src/process_file.ml
index b38ec0c5..deca5d53 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -73,7 +73,7 @@ let parse_file (f : string) : Parse_ast.defs =
raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
| Lexer.LexError(s,p) ->
raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
- let () = Lexer.custom_type_names := type_names in
+ let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in
let lexbuf = get_lexbuf f in
try
Parser.file Lexer.token lexbuf
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f592df02..d771ee4a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1080,6 +1080,12 @@ let initial_typ_env =
External (Some "mult_overflow_vec_signed"), [],pure_e);
]));
+ ("**",
+ Base(((mk_nat_params ["o";"p"]),
+ (mk_pure_fun (mk_tup [(mk_range {nexp = Nconst two} {nexp = Nconst two});
+ (mk_range (mk_nv "o") (mk_nv "p"))])
+ (mk_range {nexp =N2n ((mk_nv "o"), None)} {nexp = N2n ((mk_nv "p"), None)}))),
+ External (Some "power"), [],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"})),