From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- proofs/refine.ml | 162 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 162 insertions(+) create mode 100644 proofs/refine.ml (limited to 'proofs/refine.ml') diff --git a/proofs/refine.ml b/proofs/refine.ml new file mode 100644 index 00000000..3f552706 --- /dev/null +++ b/proofs/refine.ml @@ -0,0 +1,162 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + +let typecheck_evar ev env sigma = + let info = Evd.find sigma ev in + (** Typecheck the hypotheses. *) + let type_hyp (sigma, env) decl = + let t = get_type decl in + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref t in + let () = match decl with + | LocalAssum _ -> () + | LocalDef (_,body,_) -> Typing.e_check env evdref body t + in + (!evdref, Environ.push_named decl env) + in + let (common, changed) = extract_prefix env info in + let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in + (** Typecheck the conclusion *) + let evdref = ref sigma in + let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + !evdref + +let typecheck_proof c concl env sigma = + let evdref = ref sigma in + let () = Typing.e_check env evdref c concl in + !evdref + +let (pr_constrv,pr_constr) = + Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () + +(* Get the side-effect's constant declarations to update the monad's + * environmnent *) +let add_if_undefined kn cb env = + try ignore(Environ.lookup_constant kn env); env + with Not_found -> Environ.add_constant kn cb env + +(* Add the side effects to the monad's environment, if not already done. *) +let add_side_effect env = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + add_if_undefined kn cb env + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.fold_left (fun env (_,kn,cb,eff_env) -> + add_if_undefined kn cb env) env l + +let add_side_effects env effects = + List.fold_left (fun env eff -> add_side_effect env eff) env effects + +let make_refine_enter ?(unsafe = true) f = + { enter = fun gl -> + let gl = Proofview.Goal.assume gl in + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + (** Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.future_goals sigma in + let prev_principal_goal = Evd.principal_future_goal sigma in + (** Create the refinement term *) + let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in + let evs = Evd.future_goals sigma in + let evkmain = Evd.principal_future_goal sigma in + (** Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in + (** Check that the introduced evars are well-typed *) + let fold accu ev = typecheck_evar ev env accu in + let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + (** Check that the refined term is typesafe *) + let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + (** Check that the goal itself does not appear in the refined term *) + let self = Proofview.Goal.goal gl in + let _ = + if not (Evarutil.occur_evar_upto sigma self c) then () + else Pretype_errors.error_occur_check env sigma self c + in + (** Proceed to the refinement *) + let sigma = match evkmain with + | None -> Evd.define self c sigma + | Some evk -> + let id = Evd.evar_ident self sigma in + let sigma = Evd.define self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma + in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in + (** Select the goals *) + let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> + Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.tclUNIT v + } + +let refine_one ?(unsafe = true) f = + Proofview.Goal.enter_one (make_refine_enter ~unsafe f) + +let refine ?(unsafe = true) f = + let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in + Proofview.Goal.enter (make_refine_enter ~unsafe f) + +(** Useful definitions *) + +let with_type env evd c t = + let my_type = Retyping.get_type_of env evd c in + let j = Environ.make_judge c my_type in + let (evd,j') = + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + in + evd , j'.Environ.uj_val + +let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in + refine ?unsafe f +end } + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e -- cgit v1.2.3