Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 588 insertions, 0 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
new file mode 100644
index 00000000..1542267e
--- /dev/null
+++ b/proofs/goal.ml
@@ -0,0 +1,588 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \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
+      | _ -> Util.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 tycon = Evarutil.mk_tycon_type typ in
+    let (new_defs,j') = 
+      Coercion.Default.inh_conv_coerce_to (Util.dummy_loc) env !rdefs j tycon 
+    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 ?onlyargs ?split ?(fail=false) () env rdefs _ _ =
+    rdefs:=Typeclasses.resolve_typeclasses ?onlyargs ?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.Default.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 -> 
+    Util.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
+    Util.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 -> Util.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
+	 Util.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
+	 Util.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
+    Util.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
+       Util.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 = (Util.dummy_loc,Evd.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 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