diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 171 | ||||
| -rw-r--r-- | src/ast_util.mli | 16 | ||||
| -rw-r--r-- | src/c_backend.ml | 6 | ||||
| -rw-r--r-- | src/rewrites.ml | 263 | ||||
| -rw-r--r-- | src/type_check.ml | 6 |
6 files changed, 456 insertions, 8 deletions
@@ -544,7 +544,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = let cond_val, wrap = to_aval (anf cond) in let then_aexp = anf then_exp in let else_aexp = anf else_exp in - wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp))) + wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp))) | E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot)) diff --git a/src/ast_util.ml b/src/ast_util.ml index a5aef418..b9ab21b2 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -985,7 +985,7 @@ let rec is_number (Typ_aux (t,_)) = | Typ_app (Id_aux (Id "atom", _),_) -> true | _ -> false -let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with +let is_ref_typ (Typ_aux (typ_aux, _)) = match typ_aux with | Typ_app (id, _) -> string_of_id id = "register" || string_of_id id = "reg" | _ -> false @@ -1298,3 +1298,172 @@ let hex_to_bin hex = |> List.concat |> List.map Sail_lib.char_of_bit |> (fun bits -> String.init (List.length bits) (List.nth bits)) + +(* Functions for working with locations *) + +let locate_id l (Id_aux (name, _)) = Id_aux (name, l) + +let locate_kid l (Kid_aux (name, _)) = Kid_aux (name, l) + +let locate_lit l (L_aux (lit, _)) = L_aux (lit, l) + +let locate_base_effect l (BE_aux (base_effect, _)) = BE_aux (base_effect, l) + +let locate_effect l (Effect_aux (Effect_set effects, _)) = + Effect_aux (Effect_set (List.map (locate_base_effect l) effects), l) + +let rec locate_nexp l (Nexp_aux (nexp_aux, _)) = + let nexp_aux = match nexp_aux with + | Nexp_id id -> Nexp_id (locate_id l id) + | Nexp_var kid -> Nexp_var (locate_kid l kid) + | Nexp_constant n -> Nexp_constant n + | Nexp_app (id, nexps) -> Nexp_app (locate_id l id, List.map (locate_nexp l) nexps) + | Nexp_times (nexp1, nexp2) -> Nexp_times (locate_nexp l nexp1, locate_nexp l nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (locate_nexp l nexp1, locate_nexp l nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (locate_nexp l nexp1, locate_nexp l nexp2) + | Nexp_exp nexp -> Nexp_exp (locate_nexp l nexp) + | Nexp_neg nexp -> Nexp_neg (locate_nexp l nexp) + in + Nexp_aux (nexp_aux, l) + +let rec locate_nc l (NC_aux (nc_aux, _)) = + let nc_aux = match nc_aux with + | NC_equal (nexp1, nexp2) -> NC_equal (locate_nexp l nexp1, locate_nexp l nexp2) + | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (locate_nexp l nexp1, locate_nexp l nexp2) + | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (locate_nexp l nexp1, locate_nexp l nexp2) + | NC_not_equal (nexp1, nexp2) -> NC_not_equal (locate_nexp l nexp1, locate_nexp l nexp2) + | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums) + | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2) + | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2) + | NC_true -> NC_true + | NC_false -> NC_false + in + NC_aux (nc_aux, l) + +let rec locate_typ l (Typ_aux (typ_aux, _)) = + let typ_aux = match typ_aux with + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id id -> Typ_id (locate_id l id) + | Typ_var kid -> Typ_var (locate_kid l kid) + | Typ_fn (arg_typ, ret_typ, effect) -> Typ_fn (locate_typ l arg_typ, locate_typ l ret_typ, locate_effect l effect) + | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ l typ1, locate_typ l typ2) + | Typ_tup typs -> Typ_tup (List.map (locate_typ l) typs) + | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid l) kids, locate_nc l constr, locate_typ l typ) + | Typ_app (id, typ_args) -> Typ_app (locate_id l id, List.map (locate_typ_arg l) typ_args) + in + Typ_aux (typ_aux, l) + +and locate_typ_arg l (Typ_arg_aux (typ_arg_aux, _)) = + let typ_arg_aux = match typ_arg_aux with + | Typ_arg_nexp nexp -> Typ_arg_nexp nexp + | Typ_arg_typ typ -> Typ_arg_typ (locate_typ l typ) + | Typ_arg_order ord -> Typ_arg_order ord + in + Typ_arg_aux (typ_arg_aux, l) + +let rec locate_typ_pat l (TP_aux (tp_aux, _)) = + let tp_aux = match tp_aux with + | TP_wild -> TP_wild + | TP_var kid -> TP_var (locate_kid l kid) + | TP_app (id, tps) -> TP_app (locate_id l id, List.map (locate_typ_pat l) tps) + in + TP_aux (tp_aux, l) + +let rec locate_pat : 'a. l -> 'a pat -> 'a pat = fun l (P_aux (p_aux, (_, annot))) -> + let p_aux = match p_aux with + | P_lit lit -> P_lit (locate_lit l lit) + | P_wild -> P_wild + | P_or (pat1, pat2) -> P_or (locate_pat l pat1, locate_pat l pat2) + | P_not pat -> P_not (locate_pat l pat) + | P_as (pat, id) -> P_as (locate_pat l pat, locate_id l id) + | P_typ (typ, pat) -> P_typ (locate_typ l typ, locate_pat l pat) + | P_id id -> P_id (locate_id l id) + | P_var (pat, typ_pat) -> P_var (locate_pat l pat, locate_typ_pat l typ_pat) + | P_app (id, pats) -> P_app (locate_id l id, List.map (locate_pat l) pats) + | P_record (fpats, semi) -> P_record (List.map (locate_fpat l) fpats, semi) + | P_vector pats -> P_vector (List.map (locate_pat l) pats) + | P_vector_concat pats -> P_vector_concat (List.map (locate_pat l) pats) + | P_tup pats -> P_tup (List.map (locate_pat l) pats) + | P_list pats -> P_list (List.map (locate_pat l) pats) + | P_cons (hd_pat, tl_pat) -> P_cons (locate_pat l hd_pat, locate_pat l tl_pat) + | P_string_append pats -> P_string_append (List.map (locate_pat l) pats) + in + P_aux (p_aux, (l, annot)) + +and locate_fpat : 'a. l -> 'a fpat -> 'a fpat = fun l (FP_aux (FP_Fpat (id, pat), (_, annot))) -> + FP_aux (FP_Fpat (locate_id l id, locate_pat l pat), (l, annot)) + +let rec locate : 'a. l -> 'a exp -> 'a exp = fun l (E_aux (e_aux, (_, annot))) -> + let e_aux = match e_aux with + | E_block exps -> E_block (List.map (locate l) exps) + | E_nondet exps -> E_nondet (List.map (locate l) exps) + | E_id id -> E_id (locate_id l id) + | E_lit lit -> E_lit (locate_lit l lit) + | E_cast (typ, exp) -> E_cast (locate_typ l typ, locate l exp) + | E_app (f, exps) -> E_app (locate_id l f, List.map (locate l) exps) + | E_app_infix (exp1, op, exp2) -> E_app_infix (locate l exp1, locate_id l op, locate l exp2) + | E_tuple exps -> E_tuple (List.map (locate l) exps) + | E_if (cond_exp, then_exp, else_exp) -> E_if (locate l cond_exp, locate l then_exp, locate l else_exp) + | E_loop (loop, cond, body) -> E_loop (loop, locate l cond, locate l body) + | E_for (id, exp1, exp2, exp3, ord, exp4) -> + E_for (locate_id l id, locate l exp1, locate l exp2, locate l exp3, ord, locate l exp4) + | E_vector exps -> E_vector (List.map (locate l) exps) + | E_vector_access (exp1, exp2) -> E_vector_access (locate l exp1, locate l exp2) + | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (locate l exp1, locate l exp2, locate l exp3) + | E_vector_update (exp1, exp2, exp3) -> E_vector_update (locate l exp1, locate l exp2, locate l exp3) + | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> + E_vector_update_subrange (locate l exp1, locate l exp2, locate l exp3, locate l exp4) + | E_vector_append (exp1, exp2) -> + E_vector_append (locate l exp1, locate l exp2) + | E_list exps -> E_list (List.map (locate l) exps) + | E_cons (exp1, exp2) -> E_cons (locate l exp1, locate l exp2) + | E_record fexps -> E_record (locate_fexps l fexps) + | E_record_update (exp, fexps) -> E_record_update (locate l exp, locate_fexps l fexps) + | E_field (exp, id) -> E_field (locate l exp, locate_id l id) + | E_case (exp, cases) -> E_case (locate l exp, List.map (locate_pexp l) cases) + | E_let (letbind, exp) -> E_let (locate_letbind l letbind, locate l exp) + | E_assign (lexp, exp) -> E_assign (locate_lexp l lexp, locate l exp) + | E_sizeof nexp -> E_sizeof (locate_nexp l nexp) + | E_return exp -> E_return (locate l exp) + | E_exit exp -> E_exit (locate l exp) + | E_ref id -> E_ref (locate_id l id) + | E_throw exp -> E_throw (locate l exp) + | E_try (exp, cases) -> E_try (locate l exp, List.map (locate_pexp l) cases) + | E_assert (exp, message) -> E_assert (locate l exp, locate l message) + | E_constraint constr -> E_constraint (locate_nc l constr) + | E_var (lexp, exp1, exp2) -> E_var (locate_lexp l lexp, locate l exp1, locate l exp2) + | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (locate_pat l pat, locate l exp1, locate l exp2) + | E_internal_return exp -> E_internal_return (locate l exp) + | E_internal_value value -> E_internal_value value + in + E_aux (e_aux, (l, annot)) + +and locate_letbind : 'a. l -> 'a letbind -> 'a letbind = fun l (LB_aux (LB_val (pat, exp), (_, annot))) -> + LB_aux (LB_val (locate_pat l pat, locate l exp), (l, annot)) + +and locate_pexp : 'a. l -> 'a pexp -> 'a pexp = fun l (Pat_aux (pexp_aux, (_, annot))) -> + let pexp_aux = match pexp_aux with + | Pat_exp (pat, exp) -> Pat_exp (locate_pat l pat, locate l exp) + | Pat_when (pat, guard, exp) -> Pat_when (locate_pat l pat, locate l guard, locate l exp) + in + Pat_aux (pexp_aux, (l, annot)) + +and locate_lexp : 'a. l -> 'a lexp -> 'a lexp = fun l (LEXP_aux (lexp_aux, (_, annot))) -> + let lexp_aux = match lexp_aux with + | LEXP_id id -> LEXP_id (locate_id l id) + | LEXP_deref exp -> LEXP_deref (locate l exp) + | LEXP_memory (id, exps) -> LEXP_memory (locate_id l id, List.map (locate l) exps) + | LEXP_cast (typ, id) -> LEXP_cast (locate_typ l typ, locate_id l id) + | LEXP_tup lexps -> LEXP_tup (List.map (locate_lexp l) lexps) + | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (locate_lexp l) lexps) + | LEXP_vector (lexp, exp) -> LEXP_vector (locate_lexp l lexp, locate l exp) + | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (locate_lexp l lexp, locate l exp1, locate l exp2) + | LEXP_field (lexp, id) -> LEXP_field (locate_lexp l lexp, locate_id l id) + in + LEXP_aux (lexp_aux, (l, annot)) + +and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fexps, semi), (_, annot))) -> + FES_aux (FES_Fexps (List.map (locate_fexp l) fexps, semi), (l, annot)) + +and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) -> + FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot)) diff --git a/src/ast_util.mli b/src/ast_util.mli index eac0d62e..9dafbcd8 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -298,7 +298,7 @@ val lexp_to_exp : 'a lexp -> 'a exp val is_unit_typ : typ -> bool val is_number : typ -> bool -val is_reftyp : typ -> bool +val is_ref_typ : typ -> bool val is_vector_typ : typ -> bool val is_bit_typ : typ -> bool val is_bitvector_typ : typ -> bool @@ -350,3 +350,17 @@ val pat_ids : 'a pat -> IdSet.t val subst : id -> 'a exp -> 'a exp -> 'a exp val hex_to_bin : string -> string + + +(** locate takes an expression and recursively sets the location in + every subexpression to the provided location. Expressions build + using mk_exp and similar do not have locations, so they can then be + annotated as e.g. locate (gen_loc l) (mk_exp ...) where l is the + location from which the code is being generated. *) +val locate : l -> 'a exp -> 'a exp + +val locate_pat : l -> 'a pat -> 'a pat + +val locate_lexp : l -> 'a lexp -> 'a lexp + +val locate_typ : l -> typ -> typ diff --git a/src/c_backend.ml b/src/c_backend.ml index e61886b7..d58094ca 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -2211,6 +2211,12 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | CT_bits _ -> "string_of_sail_bits" | _ -> assert false end + | "decimal_string_of_bits", _ -> + begin match cval_ctyp (List.nth args 0) with + | CT_bits64 _ -> "decimal_string_of_mach_bits" + | CT_bits _ -> "decimal_string_of_sail_bits" + | _ -> assert false + end | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp) | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp) | "undefined_vector", CT_bits64 _ -> "UNDEFINED(mach_bits)" diff --git a/src/rewrites.ml b/src/rewrites.ml index 9c26e69a..7a085213 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -1855,7 +1855,7 @@ let rewrite_register_ref_writes (Defs defs) = let lexp_ref_exp (LEXP_aux (_, annot) as lexp) = try let exp = infer_exp (env_of_annot annot) (strip_exp (lexp_to_exp lexp)) in - if is_reftyp (typ_of exp) then Some exp else None + if is_ref_typ (typ_of exp) then Some exp else None with | _ -> None in let e_assign (lexp, exp) = let (lhs, rhs) = rewrite_lexp_to_rhs lexp in @@ -3044,7 +3044,7 @@ let pexp_rewriters rewrite_pexp = let stringappend_counter = ref 0 let fresh_stringappend_id () = - let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in + let id = mk_id ("_s" ^ (string_of_int !stringappend_counter) ^ "#") in stringappend_counter := !stringappend_counter + 1; id @@ -3064,6 +3064,237 @@ let construct_bool_match env (match_on : tannot exp) (pexp : tannot pexp) : tann let false_pexp = Pat_aux (Pat_exp (annot_pat P_wild unk env (typ_of match_on), false_exp), unkt) in annot_exp (E_case (match_on, [true_pexp; false_pexp])) unk env bool_typ +let rec bindings_of_pat (P_aux (p_aux, p_annot) as pat) = + match p_aux with + | P_lit _ | P_wild -> [] + | P_id id -> [pat] + | P_record _ -> failwith "record patterns not yet implemented" + (* we assume the type-checker has already checked the two sides have the same bindings *) + | P_or (left, right) -> bindings_of_pat left + | P_as (p, id) -> [annot_pat (P_id id) unk (pat_env_of p) (pat_typ_of p)] + | P_cons (left, right) -> bindings_of_pat left @ bindings_of_pat right + (* todo: is this right for negated patterns? *) + | P_not p + | P_typ (_, p) + | P_var (p, _) -> bindings_of_pat p + | P_app (_, ps) + | P_vector ps + | P_vector_concat ps + | P_tup ps + | P_list ps + | P_string_append ps -> List.map bindings_of_pat ps |> List.flatten + +let rec binding_typs_of_pat (P_aux (p_aux, p_annot) as pat) = + match p_aux with + | P_lit _ | P_wild -> [] + | P_id id -> [pat_typ_of pat] + | P_record _ -> failwith "record patterns not yet implemented" + (* we assume the type-checker has already checked the two sides have the same bindings *) + | P_or (left, right) -> binding_typs_of_pat left + | P_as (p, id) -> [pat_typ_of p] + | P_cons (left, right) -> binding_typs_of_pat left @ binding_typs_of_pat right + (* todo: is this right for negated patterns? *) + | P_not p + | P_typ (_, p) + | P_var (p, _) -> binding_typs_of_pat p + | P_app (_, ps) + | P_vector ps + | P_vector_concat ps + | P_tup ps + | P_list ps + | P_string_append ps -> List.map binding_typs_of_pat ps |> List.flatten + +let construct_toplevel_string_append_call env f_id bindings binding_typs guard expr = + (* s# if match f#(s#) { Some (bindings) => guard, _ => false) } => let Some(bindings) = f#(s#) in expr *) + let s_id = fresh_stringappend_id () in + let option_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (match binding_typs with + | [] -> unit_typ + | [typ] -> typ + | typs -> tuple_typ typs + ), unk)] + in + let bindings = if bindings = [] then + [annot_pat (P_lit (mk_lit L_unit)) unk env unit_typ] + else + bindings + in + let new_pat = annot_pat (P_id s_id) unk env string_typ in + let new_guard = annot_exp ( + E_case (annot_exp (E_app (f_id, [annot_exp (E_id s_id) unk env string_typ])) unk env option_typ, + [ + Pat_aux (Pat_exp (annot_pat (P_app (mk_id "Some", bindings)) unk env option_typ, guard), unkt); + Pat_aux (Pat_exp (annot_pat P_wild unk env option_typ, annot_exp (E_lit (mk_lit L_false)) unk env bool_typ), unkt) + ] + ) + ) unk env bool_typ in + let new_letbind = annot_letbind (P_app (mk_id "Some", bindings), annot_exp (E_app (f_id, [annot_exp (E_id s_id) unk env string_typ])) unk env option_typ) unk env option_typ in + let new_expr = annot_exp (E_let (new_letbind, expr)) unk env (typ_of expr) in + (new_pat, [new_guard], new_expr) + +let construct_toplevel_string_append_func env f_id pat = + let binding_typs = binding_typs_of_pat pat in + let bindings = bindings_of_pat pat in + let bindings = if bindings = [] then + [annot_pat (P_lit (mk_lit L_unit)) unk env unit_typ] + else + bindings + in + let option_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (match binding_typs with + | [] -> unit_typ + | [typ] -> typ + | typs -> tuple_typ typs + ), unk)] + in + let fun_typ = (mk_typ (Typ_fn (string_typ, option_typ, no_effect))) in + let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in + let new_val_spec, env = Type_check.check_val_spec env new_val_spec in + let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in + let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in + let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in + let s_id = fresh_stringappend_id () in + let arg_pat = mk_pat (P_id s_id) in + (* We can ignore guards here because we've already removed them *) + let rec rewrite_pat env (pat, guards, expr) = + match pat with + (* "lit" ^ pat2 ^ ... ^ patn => Some(...) ---> s# if startswith(s#, "lit") => match string_drop(s#, strlen("lit")) { + pat2 => Some(...) + _ => None() + } + *) + | P_aux (P_string_append ( + P_aux (P_lit (L_aux (L_string s, _) as lit), _) + :: pats + ), psa_annot) -> + let s_id = fresh_stringappend_id () in + let drop_exp = annot_exp (E_app (mk_id "string_drop", [annot_exp (E_id s_id) unk env string_typ; annot_exp (E_app (mk_id "string_length", [annot_exp (E_lit lit) unk env string_typ])) unk env nat_typ])) unk env string_typ in + (* recurse into pat2 .. patn *) + let new_pat2_pexp = + match rewrite_pat env (P_aux (P_string_append pats, psa_annot), guards, expr) with + | pat, [], expr -> Pat_aux (Pat_exp (pat, expr), unkt) + | pat, gs, expr -> Pat_aux (Pat_when (pat, fold_typed_guards env gs, expr), unkt) + in + let new_guard = annot_exp (E_app (mk_id "string_startswith", [annot_exp (E_id s_id) unk env string_typ; + annot_exp (E_lit lit) unk env string_typ] + )) unk env bool_typ in + let new_wildcard = Pat_aux (Pat_exp (annot_pat P_wild unk env string_typ, annot_exp (E_app (mk_id "None", [annot_exp (E_lit (mk_lit L_unit)) unk env unit_typ])) unk env option_typ), unkt) in + let new_expr = annot_exp (E_case (drop_exp, [new_pat2_pexp; new_wildcard])) unk env (typ_of expr) in + (annot_pat (P_id s_id) unk env string_typ, [new_guard], new_expr) + (* mapping(x) ^ pat2 ^ .. ^ patn => Some(...) ---> s# => match map_matches_prefix(s#) { + Some(x, n#) => match string_drop(s#, n#) { + pat2 ^ .. ^ patn => Some(...) + _ => None() + } + } + *) + | P_aux (P_string_append ( + P_aux (P_app (mapping_id, arg_pats) , _) + :: pats + ), psa_annot) + when Env.is_mapping mapping_id env -> + (* common things *) + let mapping_prefix_func = + match mapping_id with + | Id_aux (Id id, _) + | Id_aux (DeIid id, _) -> id ^ "_matches_prefix" + in + let mapping_inner_typ = + match Env.get_val_spec (mk_id mapping_prefix_func) env with + | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [Typ_arg_aux (Typ_arg_typ typ, _)]), _), _), _)) -> typ + | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?" + in + + let s_id = fresh_stringappend_id () in + let len_id = fresh_stringappend_id () in + + (* construct drop expression -- string_drop(s#, len#) *) + let drop_exp = annot_exp (E_app (mk_id "string_drop", + [annot_exp (E_id s_id) unk env string_typ; + annot_exp (E_id len_id) unk env nat_typ])) + unk env string_typ in + (* construct func expression -- maybe_atoi s# *) + let func_exp = annot_exp (E_app (mk_id mapping_prefix_func, + [annot_exp (E_id s_id) unk env string_typ])) + unk env mapping_inner_typ in + (* construct some pattern -- Some (n#, len#) *) + let opt_typ = app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ mapping_inner_typ, unk)] in + let tup_arg_pat = match arg_pats with + | [] -> assert false + | [arg_pat] -> arg_pat + | arg_pats -> annot_pat (P_tup arg_pats) unk env (tuple_typ (List.map pat_typ_of arg_pats)) + in + + let some_pat = annot_pat (P_app (mk_id "Some", + [tup_arg_pat; + annot_pat (P_id len_id) unk env nat_typ])) + unk env opt_typ in + let some_pat, some_pat_env, _ = bind_pat env (strip_pat some_pat) opt_typ in + + (* need to add the Some(...) env to tup_arg_pats for pat_to_exp below as it calls the typechecker *) + let tup_arg_pat = map_pat_annot (fun (l, tannot) -> (l, replace_env some_pat_env tannot)) tup_arg_pat in + + let new_wildcard = Pat_aux (Pat_exp (annot_pat P_wild unk env string_typ, annot_exp (E_app (mk_id "None", [annot_exp (E_lit (mk_lit L_unit)) unk env unit_typ])) unk env option_typ), unkt) in + + (* recurse into pat2 .. patn *) + let new_pat2_pexp = + match rewrite_pat env (P_aux (P_string_append (pats), psa_annot), guards, expr) with + | pat, [], expr -> Pat_aux (Pat_exp (pat, expr), unkt) + | pat, gs, expr -> Pat_aux (Pat_when (pat, fold_typed_guards env gs, expr), unkt) + in + + let inner_match = annot_exp (E_case (drop_exp, [new_pat2_pexp; new_wildcard])) unk env option_typ in + + let outer_match = annot_exp (E_case (func_exp, [Pat_aux (Pat_exp (some_pat, inner_match), unkt); new_wildcard])) unk env option_typ in + + (annot_pat (P_id s_id) unk env string_typ, [], outer_match) + | _ -> (pat, guards, expr) + in + let new_pat, new_guards, new_expr = rewrite_pat env (pat, [], annot_exp (E_app (mk_id "Some", List.map (fun p -> pat_to_exp p) bindings)) unk env option_typ) in + let new_pexp = match new_guards with + | [] -> Pat_aux (Pat_exp (new_pat, new_expr), unkt) + | gs -> Pat_aux (Pat_when (new_pat, fold_typed_guards env gs, new_expr), unkt) + in + let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) in + let new_match = mk_exp (E_case (mk_exp (E_id s_id), [strip_pexp new_pexp; wildcard])) in + let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl f_id arg_pat new_match]), (unk,())) in + let new_fun_def, env = Type_check.check_fundef env new_fun_def in + List.flatten [new_val_spec; new_fun_def] + +let rewrite_defs_toplevel_string_append (Defs defs) = + let new_defs = ref ([] : tannot def list) in + let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) = + (* merge cases of Pat_exp and Pat_when *) + let (P_aux (p_aux, p_annot) as pat, guards, expr) = + match pexp_aux with + | Pat_exp (pat, expr) -> (pat, [], expr) + | Pat_when (pat, guard, expr) -> (pat, [guard], expr) + in + + let env = env_of_annot p_annot in + + let (new_pat, new_guards, new_expr) = + match pat with + | P_aux (P_string_append appends, psa_annot) -> + let f_id = fresh_stringappend_id () in + new_defs := (construct_toplevel_string_append_func env f_id pat) @ !new_defs; + construct_toplevel_string_append_call env f_id (bindings_of_pat pat) (binding_typs_of_pat pat) (fold_typed_guards env guards) expr + | _ -> (pat, guards, expr) + in + + (* un-merge Pat_exp and Pat_when cases *) + let new_pexp = match new_guards with + | [] -> Pat_aux (Pat_exp (new_pat, new_expr), pexp_annot) + | gs -> Pat_aux (Pat_when (new_pat, fold_typed_guards env gs, new_expr), pexp_annot) + in + new_pexp + in + let rewrite def = + new_defs := []; + let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in + let rewritten = rewrite_def { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } def in + !new_defs @ [rewritten] + in + Defs (List.map rewrite defs |> List.flatten) + let rec rewrite_defs_pat_string_append = let rec rewrite_pat env ((pat : tannot pat), (guards : tannot exp list), (expr : tannot exp)) = @@ -3090,8 +3321,7 @@ let rec rewrite_defs_pat_string_append = :: pats ), psa_annot) -> - let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in - stringappend_counter := !stringappend_counter + 1; + let id = fresh_stringappend_id () in (* construct drop expression -- string_drop(s#, strlen("lit")) *) let drop_exp = annot_exp (E_app (mk_id "string_drop", [annot_exp (E_id id) unk env string_typ; annot_exp (E_app (mk_id "string_length", [annot_exp (E_lit lit) unk env string_typ])) unk env nat_typ])) unk env string_typ in @@ -4475,6 +4705,26 @@ let rewrite_case (e,ann) = let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in E_aux (E_case (e1,cases@[Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann) end + | E_let (LB_aux (LB_val (pat,e1),lb_ann),e2) -> + begin + let env = env_of_annot ann in + let ctx = ctx_from_pattern_completeness_ctx env in + let rps = remove_clause_from_pattern ctx pat RP_any in + match rps with + | [] -> E_aux (e,ann) + | (example::_) -> + let _ = + if !opt_coq_warn_nonexhaustive + then Reporting_basic.print_err false false + (fst ann) "Non-exhaustive let" ("Example: " ^ string_of_rp example) in + let l = Parse_ast.Generated Parse_ast.Unknown in + let p = P_aux (P_wild, (l, empty_tannot)) in + let ann' = mk_tannot env (typ_of_annot ann) (mk_effect [BE_escape]) in + (* TODO: use an expression that specifically indicates a failed pattern match *) + let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in + E_aux (E_case (e1,[Pat_aux (Pat_exp(pat,e2),ann); + Pat_aux (Pat_exp (p,b),(l,empty_tannot))]),ann) + end | _ -> E_aux (e,ann) let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) = @@ -4598,6 +4848,7 @@ let if_mono f defs = let rewrite_defs_lem = [ ("realise_mappings", rewrite_defs_realise_mappings); ("remove_mapping_valspecs", remove_mapping_valspecs); + ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("mono_rewrites", mono_rewrites); @@ -4647,6 +4898,7 @@ let rewrite_defs_lem = [ let rewrite_defs_coq = [ ("realise_mappings", rewrite_defs_realise_mappings); ("remove_mapping_valspecs", remove_mapping_valspecs); + ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen true); @@ -4690,6 +4942,7 @@ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("realise_mappings", rewrite_defs_realise_mappings); + ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen false); @@ -4714,6 +4967,7 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("realise_mappings", rewrite_defs_realise_mappings); + ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen false); @@ -4736,6 +4990,7 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("realise_mappings", rewrite_defs_realise_mappings); + ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); ("rewrite_undefined", rewrite_undefined_if_gen false); diff --git a/src/type_check.ml b/src/type_check.ml index 71028f96..765c41f9 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2199,6 +2199,10 @@ let rec add_opt_constraint constr env = let rec add_constraints constrs env = List.fold_left (fun env constr -> Env.add_constraint constr env) env constrs +let solve_quant env = function + | QI_aux (QI_id _, _) -> false + | QI_aux (QI_const nc, _) -> prove env nc + (* When doing implicit type coercion, for performance reasons we want to filter out the possible casts to only those that could reasonably apply. We don't mind if we try some coercions that are @@ -2830,7 +2834,7 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) match pat_aux with | P_lit lit -> let var = fresh_var () in - let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in + let guard = locate l (mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit)))) in let (typed_pat, env, guards) = bind_pat env (mk_pat (P_id var)) typ in typed_pat, env, guard::guards | _ -> raise typ_exn |