diff options
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 51 |
1 files changed, 19 insertions, 32 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 909556b1..198e057e 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -15,7 +15,7 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in + let ctx1 = List.rev (EConstr.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in let rec share l1 l2 accu = match l1, l2 with | d1 :: l1, d2 :: l2 -> @@ -29,47 +29,34 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = EConstr.of_constr (NamedDecl.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 (EConstr.of_constr body) t + let t = NamedDecl.get_type decl in + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t in - (!evdref, Environ.push_named decl env) + (sigma, EConstr.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 env = Environ.reset_with_named_context (EConstr.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 (EConstr.of_constr (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 sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in + sigma let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () (* 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 +let add_if_undefined env eff = + let open Entries in + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body 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 add_side_effects env eff = + List.fold_left add_if_undefined env eff let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in @@ -93,7 +80,7 @@ let generic_refine ~typecheck f gl = let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in + let sigma = if typecheck then Typing.check env sigma c concl else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = @@ -106,7 +93,6 @@ let generic_refine ~typecheck f gl = let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) - let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with | None -> (** Nothing to do, the goal has been solved by side-effect *) @@ -124,7 +110,8 @@ let generic_refine ~typecheck f gl = (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in - let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ + Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> |