From 86a94bfcdedcb1824d7869f8d3a0e595d7015fc3 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Thu, 11 Dec 2014 18:25:48 +0000 Subject: Add 2 ** n function; support providing type variables to other files when lexing --- src/process_file.ml | 2 +- src/type_internal.ml | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) (limited to 'src') 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"})), -- cgit v1.2.3