diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 6 | ||||
| -rw-r--r-- | src/rewrites.ml | 42 | ||||
| -rw-r--r-- | src/type_check.ml | 6 |
3 files changed, 24 insertions, 30 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 1b91bb5d..822cc7b6 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -664,14 +664,12 @@ let doc_exp_lem, doc_let_lem = match args with | [exp1; exp2; exp3; ord_exp; vartuple; body] -> let loopvar, body = match body with - | E_aux (E_let (LB_aux (LB_val (_, _), _), - E_aux (E_let (LB_aux (LB_val (_, _), _), - E_aux (E_if (_, + | E_aux (E_if (_, E_aux (E_let (LB_aux (LB_val ( ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _)) | (P_aux (P_var (P_aux (P_id id, _), _), _)) | (P_aux (P_id id, _))), _), _), - body), _), _), _)), _)), _) -> id, body + body), _), _), _) -> id, body | _ -> raise (Reporting.err_unreachable l __POS__ ("Unable to find loop variable in " ^ string_of_exp body)) in let step = match ord_exp with | E_aux (E_lit (L_aux (L_false, _)), _) -> diff --git a/src/rewrites.ml b/src/rewrites.ml index 1ca39998..5fb1962e 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -3772,24 +3772,22 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = |> mk_var_exps_pats pl env in let exp4 = rewrite_var_updates (add_vars overwrite exp4 vars) in - let ord_exp, kids, constr, lower, upper, lower_exp, upper_exp = - match destruct_numeric (Env.expand_synonyms env (typ_of exp1)), destruct_numeric (Env.expand_synonyms env (typ_of exp2)) with - | None, _ | _, None -> - raise (Reporting.err_unreachable el __POS__ "Could not determine loop bounds") - | Some (kids1, constr1, n1), Some (kids2, constr2, n2) -> - let kids = kids1 @ kids2 in - let constr = nc_and constr1 constr2 in - let ord_exp, lower, upper, lower_exp, upper_exp = - if is_order_inc order - then (annot_exp (E_lit (mk_lit L_true)) el env bool_typ, n1, n2, exp1, exp2) - else (annot_exp (E_lit (mk_lit L_false)) el env bool_typ, n2, n1, exp2, exp1) - in - ord_exp, kids, constr, lower, upper, lower_exp, upper_exp - in (* Bind the loop variable in the body, annotated with constraints *) let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in - let lvar_nc = nc_and constr (nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper)) in - let lvar_typ = mk_typ (Typ_exist (List.map (mk_kopt K_int) (lvar_kid :: kids), lvar_nc, atom_typ (nvar lvar_kid))) in + let lower_id = mk_id ("loop_" ^ string_of_id id ^ "_lower") in + let upper_id = mk_id ("loop_" ^ string_of_id id ^ "_upper") in + let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in + let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in + let lower_id_exp = annot_exp (E_id lower_id) el env (atom_typ (nvar lower_kid)) in + let upper_id_exp = annot_exp (E_id upper_id) el env (atom_typ (nvar upper_kid)) in + let annot_bool_lit lit = annot_exp (E_lit lit) el env bool_typ in + let ord_exp, lower_exp, upper_exp, exp1, exp2 = + if is_order_inc order + then annot_bool_lit (mk_lit L_true), exp1, exp2, lower_id_exp, upper_id_exp + else annot_bool_lit (mk_lit L_false), exp2, exp1, upper_id_exp, lower_id_exp + in + let lvar_nc = nc_and (nc_lteq (nvar lower_kid) (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) (nvar upper_kid)) in + let lvar_typ = mk_typ (Typ_exist (List.map (mk_kopt K_int) [lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in let lvar_pat = unaux_pat (add_p_typ lvar_typ (annot_pat (P_var ( annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)), TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in @@ -3805,23 +3803,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = that would force the loop to be effectful, so we use an if-expression instead. This code assumes that the loop bounds have (possibly existential) atom types, and the loop body has type unit. *) - let lower_kid = mk_kid ("loop_" ^ string_of_id id ^ "_lower") in - let lower_pat = P_var (annot_pat P_wild el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in + let lower_pat = P_var (annot_pat (P_id lower_id) el env (typ_of lower_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var lower_kid)]))) in let lb_lower = annot_letbind (lower_pat, lower_exp) el env (typ_of lower_exp) in - let upper_kid = mk_kid ("loop_" ^ string_of_id id ^ "_upper") in - let upper_pat = P_var (annot_pat P_wild el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in + let upper_pat = P_var (annot_pat (P_id upper_id) el env (typ_of upper_exp), mk_typ_pat (TP_app (mk_id "atom", [mk_typ_pat (TP_var upper_kid)]))) in let lb_upper = annot_letbind (upper_pat, upper_exp) el env (typ_of upper_exp) in let guard = annot_exp (E_constraint (nc_lteq (nvar lower_kid) (nvar upper_kid))) el env bool_typ in let unit_exp = annot_exp (E_lit (mk_lit L_unit)) el env unit_typ in let skip_val = tuple_exp (if overwrite then vars else unit_exp :: vars) in - let guarded_body = + let guarded_body = fix_eff_exp (annot_exp (E_if (guard, body, skip_val)) el env (typ_of exp4)) in + let v = fix_eff_exp (annot_exp (E_let (lb_lower, fix_eff_exp (annot_exp (E_let (lb_upper, - fix_eff_exp (annot_exp (E_if (guard, body, skip_val)) + fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of exp4)))) el env (typ_of exp4)))) el env (typ_of exp4)) in - let v = fix_eff_exp (annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; guarded_body])) el env (typ_of body)) in Added_vars (v, tuple_pat (if overwrite then varpats else pat :: varpats)) | E_loop(loop,cond,body) -> (* Find variables that might be updated in the loop body and are used diff --git a/src/type_check.ml b/src/type_check.ml index 9ece1e25..4ac81528 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1518,11 +1518,11 @@ and unify_constraint l env goals (NC_aux (aux1, _) as nc1) (NC_aux (aux2, _) as List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2) | NC_equal (n1a, n2a), NC_equal (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) - | NC_not_equal (n1a, n2a), NC_equal (n1b, n2b) -> + | NC_not_equal (n1a, n2a), NC_not_equal (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) - | NC_bounded_ge (n1a, n2a), NC_equal (n1b, n2b) -> + | NC_bounded_ge (n1a, n2a), NC_bounded_ge (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) - | NC_bounded_le (n1a, n2a), NC_equal (n1b, n2b) -> + | NC_bounded_le (n1a, n2a), NC_bounded_le (n1b, n2b) -> merge_uvars l (unify_nexp l env goals n1a n1b) (unify_nexp l env goals n2a n2b) | NC_true, NC_true -> KBindings.empty | NC_false, NC_false -> KBindings.empty |