diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 32 |
1 files changed, 24 insertions, 8 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index df9af97f..790a6624 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -367,8 +367,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = | P.E_for(id,e1,e2,e3,atyp,e4) -> E_for(to_ast_id id,to_ast_exp ctx e1, to_ast_exp ctx e2, to_ast_exp ctx e3,to_ast_order ctx atyp, to_ast_exp ctx e4) - | P.E_loop (P.While, e1, e2) -> E_loop (While, to_ast_exp ctx e1, to_ast_exp ctx e2) - | P.E_loop (P.Until, e1, e2) -> E_loop (Until, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_loop (P.While, m, e1, e2) -> E_loop (While, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2) + | P.E_loop (P.Until, m, e1, e2) -> E_loop (Until, to_ast_measure ctx m, to_ast_exp ctx e1, to_ast_exp ctx e2) | P.E_vector(exps) -> E_vector(List.map (to_ast_exp ctx) exps) | P.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp ctx vexp, to_ast_exp ctx exp) | P.E_vector_subrange(vex,exp1,exp2) -> @@ -414,6 +414,16 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) = | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp") ), (l,())) +and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure = + let m = match m with + | P.Measure_none -> Measure_none + | P.Measure_some exp -> + if !opt_magic_hash then + Measure_some (to_ast_exp ctx exp) + else + raise (Reporting.err_general l "Internal loop termination measure found without -dmagic_hash") + in Measure_aux (m,l) + and to_ast_lexp ctx (P.E_aux(exp,l) : P.exp) : unit lexp = let lexp = match exp with | P.E_id id -> LEXP_id (to_ast_id id) @@ -762,6 +772,10 @@ let to_ast_prec = function | P.InfixL -> InfixL | P.InfixR -> InfixR +let to_ast_loop_measure ctx = function + | P.Loop (P.While, exp) -> Loop (While, to_ast_exp ctx exp) + | P.Loop (P.Until, exp) -> Loop (Until, to_ast_exp ctx exp) + let to_ast_def ctx def : unit def list ctx_out = match def with | P.DEF_overload (id, ids) -> @@ -800,6 +814,8 @@ let to_ast_def ctx def : unit def list ctx_out = [DEF_scattered sdef], ctx | P.DEF_measure (id, pat, exp) -> [DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp)], ctx + | P.DEF_loop_measures (id, measures) -> + [DEF_loop_measures (to_ast_id id, List.map (to_ast_loop_measure ctx) measures)], ctx let rec remove_mutrec = function | [] -> [] @@ -856,8 +872,8 @@ let constraint_of_string str = let atyp = Parser.typ_eof Lexer.token (Lexing.from_string str) in to_ast_constraint initial_ctx atyp -let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> Some (string_of_id id)), false)) -let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, (fun _ -> None), false)) +let extern_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [("_", string_of_id id)], false)) +let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, [], false)) let quant_item_param = function | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))] @@ -921,7 +937,7 @@ let generate_undefineds vs_ids (Defs defs) = let undefined_td = function | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let typschm = typschm_of_string ("unit -> " ^ string_of_id id ^ " effect {undef}") in - [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) (mk_pat (P_lit (mk_lit L_unit))) (if !opt_fast_undefined && List.length ids > 0 then @@ -931,7 +947,7 @@ let generate_undefineds vs_ids (Defs defs) = [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]] | TD_record (id, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]] @@ -979,7 +995,7 @@ let generate_undefineds vs_ids (Defs defs) = (mk_exp (E_app (mk_id "internal_pick", [mk_exp (E_list (List.map (make_constr typ_to_var) constr_args))]))) letbinds in - [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false)); + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, [], false)); mk_fundef [mk_funcl (prepend_id "undefined_" id) pat body]] @@ -1015,7 +1031,7 @@ let generate_enum_functions vs_ids (Defs defs) = let rec gen_enums = function | DEF_type (TD_aux (TD_enum (id, elems, _), _)) as enum :: defs -> let enum_val_spec name quants typ = - mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, (fun _ -> None), !opt_enum_casts)) + mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, [], !opt_enum_casts)) in let range_constraint kid = nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1))) in |