diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 31 |
1 files changed, 18 insertions, 13 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 689df577..7ec0154e 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -51,7 +51,7 @@ open Ast open Util open Ast_util -open Big_int +module Big_int = Nat_big_num let opt_undefined_gen = ref false let opt_magic_hash = ref false @@ -131,7 +131,7 @@ let string_of_parse_id_aux = function | Parse_ast.DeIid v -> v let string_contains str char = - try (String.index str char; true) with + try (ignore (String.index str char); true) with | Not_found -> false let to_ast_id (Parse_ast.Id_aux(id, l)) = @@ -185,12 +185,12 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let make_r bot top = match bot,top with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (add_big_int (sub_big_int t b) unit_big_int),l) + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) | bot,(Parse_ast.ATyp_aux(_,l) as top) -> Parse_ast.ATyp_aux((Parse_ast.ATyp_sum ((Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant unit_big_int,Parse_ast.Unknown)), + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), Parse_ast.Unknown)), (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in let base = to_ast_nexp k_env b in @@ -206,9 +206,9 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> let make_sub_one t = match t with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (sub_big_int t unit_big_int),l) + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) | t -> (Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (minus_big_int unit_big_int),Parse_ast.Unknown)), + (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with | Ord_aux(Ord_inc,dl) -> (to_ast_nexp k_env b), (to_ast_nexp k_env r) @@ -291,10 +291,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with - | Some(k) -> (match k.k with - | K_Efct -> Effect_var v - | K_infer -> k.k <- K_Efct; Effect_var v - | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k)) + | Some k -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_set(effects) -> Effect_set( List.map @@ -522,6 +519,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp) | Parse_ast.E_return exp -> E_return(to_ast_exp k_env def_ord exp) | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg) + | _ -> raise (Reporting_basic.err_unreachable l "Unparsable construct in to_ast_exp") ), (l,())) and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit lexp = @@ -750,7 +748,7 @@ let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.funde (*let _ = Printf.eprintf "to_ast_fundef\n" in*) let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) - + type def_progress = No_def | Def_place_holder of id * Parse_ast.l @@ -826,6 +824,9 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_reg_dec(dec) -> let d = to_ast_dec envs dec in ((Finished(DEF_reg_dec(d))),envs),partial_defs + | Parse_ast.DEF_internal_mutrec _ -> + (* Should never occur because of remove_mutrec *) + typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> (match sd with | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> @@ -890,8 +891,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out ((Finished def), envs),partial_defs | _, true -> typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) - + | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) + let rec to_ast_defs_helper envs partial_defs = function | [] -> ([],envs,partial_defs) | d::ds -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in @@ -951,6 +952,10 @@ let initial_kind_env = ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ] +let exp_of_string order str = + let exp = Parser2.exp_eof Lexer2.token (Lexing.from_string str) in + to_ast_exp initial_kind_env order exp + let typschm_of_string order str = let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in |