Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

588 lines (501 sloc) 20.975 kb
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Term
(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
evar is defined in the current evar_map, should not be accessed. *)
(* type of the goals *)
type goal = {
content : Evd.evar; (* Corresponding evar. Allows to retrieve
logical information once put together
with an evar_map. *)
tags : string list (* Heriditary? tags to be displayed *)
}
(* spiwack: I don't deal with the tags, yet. It is a worthy discussion
whether we do want some tags displayed besides the goal or not. *)
let pr_goal {content = e} = str "GOAL:" ++ Pp.int e
(* access primitive *)
(* invariant : [e] must exist in [em] *)
let content evars { content = e } = Evd.find evars e
(* Builds a new (empty) goal with evar [e] *)
let build e =
{ content = e ;
tags = []
}
let uid {content = e} = string_of_int e
let get_by_uid u =
(* this necessarily forget about tags.
when tags are to be implemented, they
should be done another way.
We could use the store in evar_extra,
for instance. *)
build (int_of_string u)
(* Builds a new goal with content evar [e] and
inheriting from goal [gl]*)
let descendent gl e =
{ gl with content = e}
(* [advance sigma g] returns [Some g'] if [g'] is undefined and
is the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially) solved. *)
open Store.Field
let rec advance sigma g =
let evi = Evd.find sigma g.content in
if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
let v =
match evi.Evd.evar_body with
| Evd.Evar_defined c -> c
| _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
in
let (e,_) = Term.destEvar v in
let g' = { g with content = e } in
advance sigma g'
else
match evi.Evd.evar_body with
| Evd.Evar_defined _ -> None
| _ -> Some g
(*** Goal tactics ***)
(* Goal tactics are [subgoal sensitive]-s *)
type subgoals = { subgoals: goal list }
(* type of the base elements of the goal API.*)
(* it has an extra evar_info with respect to what would be expected,
it is supposed to be the evar_info of the goal in the evar_map.
The idea is that it is computed by the [run] function as an
optimisation, since it will generaly not change during the
evaluation. *)
type 'a sensitive =
Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a
(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
(* the evar_info corresponding to the goal is computed at once
as an optimisation (it shouldn't change during the evaluation). *)
let eval t env defs gl =
let info = content defs gl in
let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
let rdefs = ref defs in
let r = t env rdefs gl info in
( r , !rdefs )
(* monadic bind on sensitive expressions *)
let bind e f env rdefs goal info =
f (e env rdefs goal info) env rdefs goal info
(* monadic return on sensitive expressions *)
let return v _ _ _ _ = v
(* interpretation of "open" constr *)
(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
In an ideal world, this could/should be the other way round.
As of now, though, it seems at least quite useful to build tactics. *)
let interp_constr cexpr env rdefs _ _ =
let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in
rdefs := defs ;
c
(* Type of constr with holes used by refine. *)
(* The list of evars doesn't necessarily contain all the evars in the constr,
only those the constr has introduced. *)
(* The variables in [myevars] are supposed to be stored
in decreasing order. Breaking this invariant might cause
many things to go wrong. *)
type refinable = {
me: constr;
my_evars: Evd.evar list
}
module Refinable = struct
type t = refinable
type handle = Evd.evar list ref
let make t env rdefs gl info =
let r = ref [] in
let me = t r env rdefs gl info in
{ me = me;
my_evars = !r }
let make_with t env rdefs gl info =
let r = ref [] in
let (me,side) = t r env rdefs gl info in
{ me = me ; my_evars = !r } , side
let mkEvar handle env typ _ rdefs _ _ =
let ev = Evarutil.e_new_evar rdefs env typ in
let (e,_) = Term.destEvar ev in
handle := e::!handle;
ev
(* [with_type c typ] constrains term [c] to have type [typ]. *)
let with_type t typ env rdefs _ _ =
(* spiwack: this function assumes that no evars can be created during
this sort of coercion.
If it is not the case it could produce bugs. We would need to add a handle
and add the new evars to it. *)
let my_type = Retyping.get_type_of env !rdefs t in
let j = Environ.make_judge t my_type in
let (new_defs,j') =
Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
in
rdefs := new_defs;
j'.Environ.uj_val
(* spiwack: it is not very fine grain since it solves all typeclasses holes,
not only those containing the current goal, or a given term. But it
seems to fit our needs so far. *)
let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
()
(* a pessimistic (i.e : there won't be many positive answers) filter
over evar_maps, acting only on undefined evars *)
let evar_map_filter_undefined f evm =
Evd.fold_undefined
(fun ev evi r -> if f ev evi then Evd.add r ev evi else r)
evm
Evd.empty
(* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
let rec fusion l1 l2 = match l1 , l2 with
| [] , _ -> l2
| _ , [] -> l1
| a::l1 , b::_ when a>b -> a::(fusion l1 l2)
| a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
| _ , b::l2 -> b::(fusion l1 l2)
let update_handle handle init_defs post_defs =
(* [delta_evars] holds the evars that have been introduced by this
refinement (but not immediatly solved) *)
(* spiwack: this is the hackish part, don't know how to do any better though. *)
let delta_evars = evar_map_filter_undefined
(fun ev _ -> not (Evd.mem init_defs ev))
post_defs
in
(* [delta_evars] in the shape of a list of [evar]-s*)
let delta_list = List.map fst (Evd.to_list delta_evars) in
(* The variables in [myevars] are supposed to be stored
in decreasing order. Breaking this invariant might cause
many things to go wrong. *)
handle := fusion delta_list !handle;
delta_evars
(* [constr_of_raw] is a pretyping function. The [check_type] argument
asks whether the term should have the same type as the conclusion.
[resolve_classes] is a flag on pretyping functions which, if set to true,
calls the typeclass resolver.
The principal argument is a [glob_constr] which is then pretyped in the
context of a term, the remaining evars are registered to the handle.
It is the main component of the toplevel refine tactic.*)
(* spiwack: it is not entirely satisfactory to have this function here. Plus it is
a bit hackish. However it does not seem possible to move it out until
pretyping is defined as some proof procedure. *)
let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info =
(* We need to keep trace of what [rdefs] was originally*)
let init_defs = !rdefs in
(* if [check_type] is true, then creates a type constraint for the
proof-to-be *)
let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
(* call to [understand_tcc_evars] returns a constr with undefined evars
these evars will be our new goals *)
let open_constr =
Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
in
ignore(update_handle handle init_defs !rdefs);
open_constr
let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
let delta = update_handle handle !rdefs evars in
rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
else c
end
(* [refine t] takes a refinable term and use it as a partial proof for current
goal. *)
let refine step env rdefs gl info =
(* subgoals to return *)
(* The evars in [my_evars] are stored in reverse order.
It is expectingly better however to display the goal
in increasing order. *)
rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ;
let subgoals = List.map (descendent gl) (List.rev step.my_evars) in
(* creates the new [evar_map] by defining the evar of the current goal
as being [refine_step]. *)
let new_defs = Evd.define gl.content (step.me) !rdefs in
rdefs := new_defs;
(* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
let subgoals =
Option.List.flatten (List.map (advance !rdefs) subgoals)
in
{ subgoals = subgoals }
(*** Cleaning goals ***)
let clear ids env rdefs gl info =
let hyps = Evd.evar_hyps info in
let concl = Evd.evar_concl info in
let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
let cleared_env = Environ.reset_with_named_context hyps env in
let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
let (cleared_evar,_) = Term.destEvar cleared_concl in
let cleared_goal = descendent gl cleared_evar in
rdefs := Evd.define gl.content cleared_concl !rdefs;
{ subgoals = [cleared_goal] }
let wrap_apply_to_hyp_and_dependent_on sign id f g =
try Environ.apply_to_hyp_and_dependent_on sign id f g
with Environ.Hyp_not_found ->
Errors.error "No such assumption"
let check_typability env sigma c =
let _ = Typing.type_of env sigma c in ()
let recheck_typability (what,id) env sigma t =
try check_typability env sigma t
with _ ->
let s = match what with
| None -> "the conclusion"
| Some id -> "hypothesis "^(Names.string_of_id id) in
Errors.error
("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))
let remove_hyp_body env sigma id =
let sign =
wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
(fun (_,c,t) _ ->
match c with
| None -> Errors.error ((Names.string_of_id id)^" is not a local definition")
| Some c ->(id,None,t))
(fun (id',c,t as d) sign ->
(
begin
let env = Environ.reset_with_named_context sign env in
match c with
| None -> recheck_typability (Some id',id) env sigma t
| Some b ->
let b' = mkCast (b,DEFAULTcast, t) in
recheck_typability (Some id',id) env sigma b'
end;d))
in
Environ.reset_with_named_context sign env
let clear_body idents env rdefs gl info =
let info = content !rdefs gl in
let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
let aux env id =
let env' = remove_hyp_body env !rdefs id in
recheck_typability (None,id) env' !rdefs (Evd.evar_concl info);
env'
in
let new_env =
List.fold_left aux full_env idents
in
let concl = Evd.evar_concl info in
let (defs',new_constr) = Evarutil.new_evar !rdefs new_env concl in
let (new_evar,_) = destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr defs';
{ subgoals = [new_goal] }
(*** Sensitive primitives ***)
(* [concl] is the conclusion of the current goal *)
let concl _ _ _ info =
Evd.evar_concl info
(* [hyps] is the [named_context_val] representing the hypotheses
of the current goal *)
let hyps _ _ _ info =
Evd.evar_hyps info
(* [env] is the current [Environ.env] containing both the
environment in which the proof is ran, and the goal hypotheses *)
let env env _ _ _ = env
(* [defs] is the [Evd.evar_map] at the current evaluation point *)
let defs _ rdefs _ _ =
!rdefs
(* Cf mli for more detailed comment.
[null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
to communicate whether or not the value is defined in the particular context. *)
exception UndefinedHere
(* no handler: this should never be allowed to reach toplevel *)
let null _ _ _ _ = raise UndefinedHere
let plus s1 s2 env rdefs goal info =
try s1 env rdefs goal info
with UndefinedHere -> s2 env rdefs goal info
(* Equality of two goals *)
let equal { content = e1 } { content = e2 } = e1 = e2
let here goal value _ _ goal' _ =
if equal goal goal' then
value
else
raise UndefinedHere
(* arnaud: voir à la passer dans Util ? *)
let rec list_mem_with eq x = function
| y::_ when eq x y -> true
| _::l -> list_mem_with eq x l
| [] -> false
let here_list goals value _ _ goal' _ =
if list_mem_with equal goal' goals then
value
else
raise UndefinedHere
(*** Conversion in goals ***)
let convert_hyp check (id,b,bt as d) env rdefs gl info =
let sigma = !rdefs in
(* This function substitutes the new type and body definitions
in the appropriate variable when used with {!Environ.apply_hyps}. *)
let replace_function =
(fun _ (_,c,ct) _ ->
if check && not (Reductionops.is_conv env sigma bt ct) then
Errors.error ("Incorrect change of the type of "^(Names.string_of_id id));
if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
Errors.error ("Incorrect change of the body of "^(Names.string_of_id id));
d)
in
(* Modified named context. *)
let new_hyps =
Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
in
let new_env = Environ.reset_with_named_context new_hyps env in
let new_constr =
Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
in
let (new_evar,_) = Term.destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr !rdefs;
{ subgoals = [new_goal] }
let convert_concl check cl' env rdefs gl info =
let sigma = !rdefs in
let cl = concl env rdefs gl info in
check_typability env sigma cl';
if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
let new_constr =
Evarutil.e_new_evar rdefs env cl'
in
let (new_evar,_) = Term.destEvar new_constr in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_constr !rdefs;
{ subgoals = [new_goal] }
else
Errors.error "convert-concl rule passed non-converting term"
(*** Bureaucracy in hypotheses ***)
(* Renames a hypothesis. *)
let rename_hyp_sign id1 id2 sign =
Environ.apply_to_hyp_and_dependent_on sign id1
(fun (_,b,t) _ -> (id2,b,t))
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
let rename_hyp id1 id2 env rdefs gl info =
let hyps = hyps env rdefs gl info in
if id1 <> id2 &&
List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
Errors.error ((Names.string_of_id id2)^" is already used.");
let new_hyps = rename_hyp_sign id1 id2 hyps in
let new_env = Environ.reset_with_named_context new_hyps env in
let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
let (new_evar,_) = Term.destEvar new_subproof in
let new_goal = descendent gl new_evar in
rdefs := Evd.define gl.content new_subproof !rdefs;
{ subgoals = [new_goal] }
(*** Additional functions ***)
(* emulates List.map for functions of type
[Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
new evar_map to next definition. *)
(*This sort of construction actually works with any monad (here the State monade
in Haskell). There is a generic construction in Haskell called mapM.
*)
let rec list_map f l s =
match l with
| [] -> ([],s)
| a::l -> let (a,s) = f s a in
let (l,s) = list_map f l s in
(a::l,s)
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
internal types. *)
module V82 = struct
(* Old style env primitive *)
let env evars gl =
let evi = content evars gl in
Evd.evar_env evi
(* For printing *)
let unfiltered_env evars gl =
let evi = content evars gl in
Evd.evar_unfiltered_env evi
(* Old style hyps primitive *)
let hyps evars gl =
let evi = content evars gl in
evi.Evd.evar_hyps
(* Access to ".evar_concl" *)
let concl evars gl =
let evi = content evars gl in
evi.Evd.evar_concl
(* Access to ".evar_extra" *)
let extra evars gl =
let evi = content evars gl in
evi.Evd.evar_extra
(* Old style filtered_context primitive *)
let filtered_context evars gl =
let evi = content evars gl in
Evd.evar_filtered_context evi
(* Old style mk_goal primitive *)
let mk_goal evars hyps concl extra =
let evk = Evarutil.new_untyped_evar () in
let evi = { Evd.evar_hyps = hyps;
Evd.evar_concl = concl;
Evd.evar_filter = List.map (fun _ -> true)
(Environ.named_context_of_val hyps);
Evd.evar_body = Evd.Evar_empty;
Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
Evd.evar_candidates = None;
Evd.evar_extra = extra }
in
let evi = Typeclasses.mark_unresolvable evi in
let evars = Evd.add evars evk evi in
let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in
let inst = Array.of_list (List.map mkVar ids) in
let ev = Term.mkEvar (evk,inst) in
(build evk, ev, evars)
(* Equality function on goals *)
let equal evars gl1 gl2 =
let evi1 = content evars gl1 in
let evi2 = content evars gl2 in
Evd.eq_evar_info evi1 evi2
(* Creates a dummy [goal sigma] for use in auto *)
let dummy_goal =
(* This goal seems to be marshalled somewhere. Therefore it cannot be
marked unresolvable for typeclasses, as non-empty Store.t-s happen
to have functional content. *)
let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
let evk = Evarutil.new_untyped_evar () in
let sigma = Evd.add Evd.empty evk evi in
{ Evd.it = build evk ; Evd.sigma = sigma }
(* Makes a goal out of an evar *)
let build = build
(* Instantiates a goal with an open term *)
let partial_solution sigma { content=evk } c =
Evd.define evk c sigma
(* Parts of the progress tactical *)
let same_goal evars1 gl1 evars2 gl2 =
let evi1 = content evars1 gl1 in
let evi2 = content evars2 gl2 in
Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
let weak_progress glss gls =
match glss.Evd.it with
| [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
| _ -> true
let progress glss gls =
weak_progress glss gls
(* spiwack: progress normally goes like this:
(Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
This is immensly slow in the current implementation. Maybe we could
reimplement progress_evar_map with restricted folds like "fold_undefined",
with a good implementation of them.
*)
(* Used for congruence closure *)
let new_goal_with sigma gl new_hyps =
let evi = content sigma gl in
let new_evi = { evi with Evd.evar_hyps = new_hyps } in
let new_evi = Typeclasses.mark_unresolvable new_evi in
let evk = Evarutil.new_untyped_evar () in
let new_sigma = Evd.add Evd.empty evk new_evi in
{ Evd.it = build evk ; sigma = new_sigma }
(* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
let evi = content sigma gl in
let evi = Evarutil.nf_evar_info sigma evi in
let sigma = Evd.add sigma gl.content evi in
(gl,sigma)
(* Goal represented as a type, doesn't take into account section variables *)
let abstract_type sigma gl =
let (gl,sigma) = nf_evar sigma gl in
let env = env sigma gl in
let genv = Global.env () in
let is_proof_var decl =
try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
with Not_found -> true in
Environ.fold_named_context_reverse (fun t decl ->
if is_proof_var decl then
mkNamedProd_or_LetIn decl t
else
t
) ~init:(concl sigma gl) env
end
Jump to Line
Something went wrong with that request. Please try again.