Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 454 insertions, 0 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
new file mode 100644
index 00000000..dd40c5cc
--- /dev/null
+++ b/contrib/interface/depends.ml
@@ -0,0 +1,454 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant                                  *)
+(* <O___,, *                                                            *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *      GNU Lesser General Public License Version 2.1,        *)
+(*         *      or (at your option) any later version.                *)
+(************************************************************************)
+
+(* Copyright © 2007, Lionel Elie Mamane <lionel@mamane.lu> *)
+
+(* This is distributed in the hope that it will be useful,           *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of    *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *)
+(* Lesser General Public License for more details.                   *)
+
+(* You should have received a copy of the GNU Lesser General Public    *)
+(* License along with this library; if not, write to the Free Software *)
+(* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston,          *)
+(* MA  02110-1301, USA                                                 *)
+
+
+(* LEM TODO: a .mli file *)
+
+open Refiner
+open Proof_type
+open Rawterm
+open Term
+open Libnames
+open Util
+open Tacexpr
+open Entries
+
+(* DBG utilities, to be removed *)
+let print_bool b = print_string (string_of_bool b)
+let string_of_ppcmds p = Pp.pp_with Format.str_formatter p; Format.flush_str_formatter()
+let acc_str f = List.fold_left (fun a b -> a ^ (f b) ^ "+") "O"
+(* End utilities, to be removed *)
+
+let explore_tree pfs =
+  print_string "explore_tree called\n";
+  print_string "pfs is a top: ";
+  (* We expect yes. *)
+  print_string (if (is_top_pftreestate pfs) then "yes" else "no");
+  print_newline();
+  let rec explain_tree (pt:proof_tree) =
+    match pt.ref with
+      | None -> "none"
+      | Some (Prim p, l) -> "<Prim (" ^ (explain_prim p) ^ ") | " ^ (acc_str explain_tree l) ^ ">"
+      | Some (Nested (t,p), l) -> "<Nested (" ^ explain_compound t ^ ", " ^ (explain_tree p) ^ ") | " ^ (acc_str explain_tree l) ^ ">"
+      | Some (Decl_proof _, _) -> "Decl_proof"
+      | Some (Daimon, _) -> "Daimon"
+  and explain_compound cr =
+    match cr with
+      | Tactic (texp, b) -> "Tactic (" ^ (string_of_ppcmds (Tactic_printer.pr_tactic texp)) ^ ", " ^ (string_of_bool b) ^ ")"
+      | Proof_instr (b, instr) -> "Proof_instr (" ^ (string_of_bool b) ^ (string_of_ppcmds (Tactic_printer.pr_proof_instr instr)) ^ ")"
+  and explain_prim = function
+    | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
+    | Intro identifier -> "Intro"
+    | Intro_replacing identifier -> "Intro_replacing"
+    | Cut (bool, identifier, types) -> "Cut"
+    | FixRule (identifier, int, l) -> "FixRule"
+    | Cofix (identifier, l) -> "Cofix"
+    | Convert_concl (types, cast_kind) -> "Convert_concl"
+    | Convert_hyp named_declaration -> "Convert_hyp"
+    | Thin identifier_list -> "Thin"
+    | ThinBody identifier_list -> "ThinBody"
+    | Move (bool, identifier, identifier') -> "Move"
+    | Rename (identifier, identifier') -> "Rename"
+    | Change_evars -> "Change_evars"
+  in
+  let pt = proof_of_pftreestate pfs in
+    (* We expect 0 *)
+    print_string "Number of open subgoals: ";
+    print_int pt.open_subgoals;
+    print_newline();
+    print_string "First rule is a ";
+    print_string (explain_tree pt);
+    print_newline()
+
+
+let o f g x = f (g x)
+let fst_of_3 (x, _, _) = x
+let snd_of_3 (_, x, _) = x
+let trd_of_3 (_, _, x) = x
+
+(* TODO: These for now return a Libnames.global_reference, but a
+   prooftree will also depend on things like tactic declarations, etc
+   so we may need a new type for that. *)
+let rec depends_of_hole_kind hk acc = match hk with
+  | Evd.ImplicitArg (gr,_)            -> gr::acc
+  | Evd.TomatchTypeParameter (ind, _) -> (IndRef ind)::acc
+  | Evd.BinderType _
+  | Evd.QuestionMark _
+  | Evd.CasesType
+  | Evd.InternalHole
+  | Evd.GoalEvar
+  | Evd.ImpossibleCase  -> acc
+
+let depends_of_'a_cast_type depends_of_'a act acc = match act with
+  | CastConv (ck, a) -> depends_of_'a a acc
+  | CastCoerce       -> acc
+
+let depends_of_'a_bindings depends_of_'a ab acc = match ab with
+  | ImplicitBindings al  -> list_union_map depends_of_'a al acc
+  | ExplicitBindings apl -> list_union_map (fun x y -> depends_of_'a (trd_of_3 x) y) apl acc
+  | NoBindings -> acc
+
+let depends_of_'a_with_bindings depends_of_'a (a, ab) acc =
+  depends_of_'a a (depends_of_'a_bindings depends_of_'a ab acc)
+
+(* let depends_of_constr_with_bindings = depends_of_'a_with_bindings depends_of_constr *)
+(* and depends_of_open_constr_with_bindings = depends_of_'a_with_bindings depends_of_open_let *)
+
+let depends_of_'a_induction_arg depends_of_'a aia acc = match aia with
+  | ElimOnConstr a -> depends_of_'a a acc
+  | ElimOnIdent _ ->
+      (* TODO: Check that this really refers only to an hypothesis (not a section variable, etc.)
+       * It *seems* thaat section variables are seen as hypotheses, so we have a problem :-(
+
+       * Plan: Load all section variables before anything in that
+       * section and call the user's proof script "brittle" and refuse
+       * to handle if it breaks because of that
+       *)
+      acc
+  | ElimOnAnonHyp _ -> acc
+
+let depends_of_'a_or_var depends_of_'a aov acc = match aov with
+  | ArgArg a -> depends_of_'a a acc
+  | ArgVar _ -> acc
+
+let depends_of_'a_with_occurences depends_of_'a (_,a) acc =
+  depends_of_'a a acc
+
+let depends_of_'a_'b_red_expr_gen depends_of_'a reg acc = match reg with
+  (* TODO: dirty assumption that the 'b doesn't make any dependency *)
+  | Red _
+  | Hnf
+  | Cbv _
+  | Lazy _
+  | Unfold _
+  | ExtraRedExpr _
+  | CbvVm           -> acc
+  | Simpl awoo ->
+      Option.fold_right
+	(depends_of_'a_with_occurences depends_of_'a)
+	awoo
+	acc
+  | Fold al -> list_union_map depends_of_'a al acc
+  | Pattern awol ->
+      list_union_map
+	(depends_of_'a_with_occurences depends_of_'a)
+	awol
+	acc
+
+let depends_of_'a_'b_inversion_strength depends_of_'a is acc = match is with
+  (* TODO: dirty assumption that the 'b doesn't make any dependency *)
+  | NonDepInversion _       -> acc
+  | DepInversion (_, ao, _) -> Option.fold_right depends_of_'a ao acc
+  | InversionUsing (a, _)   -> depends_of_'a a acc
+
+let depends_of_'a_pexistential depends_of_'a (_, aa) acc = array_union_map depends_of_'a aa acc
+
+let depends_of_named_vals nvs acc =
+  (* TODO: I'm stopping here because I have noooo idea what to do with values... *)
+  acc
+
+let depends_of_inductive ind acc = (IndRef ind)::acc
+
+let rec depends_of_constr c acc = match kind_of_term c with
+  | Rel       _                -> acc
+  | Var       id               -> (VarRef id)::acc
+  | Meta      _                -> acc
+  | Evar      ev               -> depends_of_'a_pexistential depends_of_constr ev acc
+  | Sort      _                -> acc
+  | Cast      (c, _, t)        -> depends_of_constr c (depends_of_constr t acc)
+  | Prod      (_, t, t')       -> depends_of_constr t (depends_of_constr t' acc)
+  | Lambda    (_, t, c)        -> depends_of_constr t (depends_of_constr c acc)
+  | LetIn     (_, c, t, c')    -> depends_of_constr c (depends_of_constr t (depends_of_constr c' acc))
+  | App       (c, ca)          -> depends_of_constr c (array_union_map depends_of_constr ca acc)
+  | Const     cnst             -> (ConstRef cnst)::acc
+  | Ind       ind              -> (IndRef ind)::acc
+  | Construct cons             -> (ConstructRef cons)::acc
+  | Case      (_, c, c', ca)   -> depends_of_constr c (depends_of_constr c' (array_union_map depends_of_constr ca acc))
+  | Fix       (_, (_, ta, ca))
+  | CoFix     (_, (_, ta, ca)) -> array_union_map depends_of_constr ca (array_union_map depends_of_constr ta acc)
+and depends_of_evar_map evm acc =
+  Evd.fold (fun ev evi -> depends_of_evar_info evi) evm acc
+and depends_of_evar_info evi acc =
+  (* TODO: evi.evar_extra contains a dynamic... Figure out what to do with it. *)
+  depends_of_constr evi.Evd.evar_concl (depends_of_evar_body evi.Evd.evar_body (depends_of_named_context_val evi.Evd.evar_hyps acc))
+and depends_of_evar_body evb acc = match evb with
+  | Evd.Evar_empty -> acc
+  | Evd.Evar_defined c -> depends_of_constr c acc
+and depends_of_named_context nc acc = list_union_map depends_of_named_declaration nc acc
+and depends_of_named_context_val ncv acc =
+  depends_of_named_context (Environ.named_context_of_val ncv) (depends_of_named_vals (Environ.named_vals_of_val ncv) acc)
+and depends_of_named_declaration (_,co,t) acc = depends_of_constr t (Option.fold_right depends_of_constr co acc)
+
+
+
+let depends_of_open_constr (evm,c) acc =
+  depends_of_constr c (depends_of_evar_map evm acc)
+
+let rec depends_of_rawconstr rc acc = match rc with
+  | RRef (_,r)         -> r::acc
+  | RVar (_, id)       -> (VarRef id)::acc
+  | REvar (_, _, rclo) -> Option.fold_right depends_of_rawconstr_list rclo acc
+  | RPatVar _          -> acc
+  | RApp (_, rc, rcl)  -> depends_of_rawconstr rc (depends_of_rawconstr_list rcl acc)
+  | RLambda (_, _, _, rct, rcb)
+  | RProd   (_, _, _, rct, rcb)
+  | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
+  | RCases  (_, _, rco, tmt, cc) ->
+      (* LEM TODO: handle the cc *)
+      (Option.fold_right depends_of_rawconstr rco
+         (list_union_map
+	    (fun (rc, pp) acc ->
+	       Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp)
+	       (depends_of_rawconstr rc acc))
+	    tmt
+	    acc))
+  | RLetTuple (_,_,(_,rco),rc0,rc1) ->
+     depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc))
+  | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in
+      dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc))))
+  | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in
+      dorca rca0 (dorca rca1 (array_union_map
+				(list_union_map (fun (_,_,rco,rc) acc -> depends_of_rawconstr rc (Option.fold_right depends_of_rawconstr rco acc)))
+				rdla
+				acc))
+  | RSort _ -> acc
+  | RHole (_, hk) -> depends_of_hole_kind hk acc
+  | RCast (_, rc, rcct) -> depends_of_rawconstr rc (depends_of_'a_cast_type depends_of_rawconstr rcct acc)
+  | RDynamic (_, dyn) -> failwith "Depends of a dyn not implemented yet" (* TODO: figure out how these dyns are used*)
+and depends_of_rawconstr_list l = list_union_map depends_of_rawconstr l
+
+let depends_of_rawconstr_and_expr (rc, _) acc =
+  (* TODO Le constr_expr représente le même terme que le rawconstr. Vérifier ça. *)
+  depends_of_rawconstr rc acc
+
+let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of_'tac =
+  (* TODO:
+   * Dirty assumptions that the 'id, 'cst, 'ref don't generate dependencies
+   *)
+  let rec depends_of_tacexpr texp acc = match texp with
+    | TacAtom (_, atexpr) -> depends_of_atomic_tacexpr atexpr acc
+    | TacThen (tac0, taca0, tac1, taca1) ->
+	depends_of_tacexpr tac0 (array_union_map depends_of_tacexpr taca0 (depends_of_tacexpr tac1 (array_union_map depends_of_tacexpr taca1 acc)))
+    | TacThens (tac, tacl) ->
+	depends_of_tacexpr tac (list_union_map depends_of_tacexpr tacl acc)
+    | TacFirst tacl -> list_union_map depends_of_tacexpr tacl acc
+    | TacComplete tac -> depends_of_tacexpr tac acc
+    | TacSolve tacl -> list_union_map depends_of_tacexpr tacl acc
+    | TacTry tac -> depends_of_tacexpr tac acc
+    | TacOrelse (tac0, tac1) -> depends_of_tacexpr tac0 (depends_of_tacexpr tac1 acc)
+    | TacDo (_, tac) -> depends_of_tacexpr tac acc
+    | TacRepeat tac -> depends_of_tacexpr tac acc
+    | TacProgress tac -> depends_of_tacexpr tac acc
+    | TacAbstract (tac, _) -> depends_of_tacexpr tac acc
+    | TacId _
+    | TacFail _ -> acc
+    | TacInfo tac -> depends_of_tacexpr tac acc
+    | TacLetIn (_, igtal, tac) ->
+	depends_of_tacexpr
+	  tac
+	  (list_union_map
+	     (fun x y -> depends_of_tac_arg (snd x) y)
+	     igtal
+	     acc)
+    | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
+    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
+    | TacArg tacarg -> depends_of_tac_arg tacarg acc
+  and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
+      (* Basic tactics *)
+    | TacIntroPattern _
+    | TacIntrosUntil _
+    | TacIntroMove _
+    | TacAssumption  -> acc
+    | TacExact          c
+    | TacExactNoCheck   c
+    | TacVmCastNoCheck  c  -> depends_of_'constr c acc
+    | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacElim (_, cwb, cwbo) ->
+	depends_of_'constr_with_bindings cwb
+	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacElimType c -> depends_of_'constr c acc
+    | TacCase (_, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacCaseType c -> depends_of_'constr c acc
+    | TacFix _
+    | TacMutualFix _
+    | TacCofix _
+    | TacMutualCofix _ -> failwith "depends_of_atomic_tacexpr of a Tac(Mutual)(Co)Fix not implemented yet"
+    | TacCut c -> depends_of_'constr c acc
+    | TacAssert (taco, _, c) ->
+	Option.fold_right depends_of_'tac taco (depends_of_'constr c acc)
+    | TacGeneralize cl ->
+	list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl)
+	acc
+    | TacGeneralizeDep c -> depends_of_'constr c acc
+    | TacLetTac (_,c,_,_) -> depends_of_'constr c acc
+
+    (* Derived basic tactics *)
+    | TacSimpleInduction _
+    | TacSimpleDestruct  _
+    | TacDoubleInduction _ -> acc
+    | TacNewInduction (_, cwbial, cwbo, _, _)
+    | TacNewDestruct (_, cwbial, cwbo, _, _) ->
+	list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
+	  cwbial
+	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacDecomposeAnd c
+    | TacDecomposeOr  c -> depends_of_'constr c acc
+    | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc)
+    | TacSpecialize (_,cwb) -> depends_of_'constr_with_bindings cwb acc
+    | TacLApply c -> depends_of_'constr c acc
+
+    (* Automation tactics *)
+    | TacTrivial (cl, bs) -> 
+	(* TODO: Maybe make use of bs: list of hint bases to be used. *)
+	list_union_map depends_of_'constr cl acc
+    | TacAuto (_, cs, bs) ->
+	(* TODO: Maybe make use of bs: list of hint bases to be used.
+           None -> all ("with *")
+           Some list -> a list, "core" added implicitly *)
+	list_union_map depends_of_'constr cs acc
+    | TacAutoTDB _     -> acc
+    | TacDestructHyp _ -> acc
+    | TacDestructConcl -> acc
+    | TacSuperAuto _ -> (* TODO: this reference thing is scary*)
+	acc
+    | TacDAuto     _ -> acc
+
+    (* Context management *)
+    | TacClear     _
+    | TacClearBody _
+    | TacMove      _
+    | TacRename    _ 
+    | TacRevert    _ -> acc
+
+    (* Constructors *)
+    | TacLeft        (_,cb)
+    | TacRight       (_,cb)
+    | TacSplit       (_, _, cb)
+    | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc
+    | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc
+
+    (* Conversion *)
+    | TacReduce  (reg,_) ->
+	depends_of_'a_'b_red_expr_gen depends_of_'constr reg acc
+    | TacChange (cwoo, c, _) ->
+	depends_of_'constr
+	  c
+	  (Option.fold_right (depends_of_'a_with_occurences depends_of_'constr) cwoo acc)
+
+    (* Equivalence relations *)
+    | TacReflexivity
+    | TacSymmetry     _ -> acc
+    | TacTransitivity c -> depends_of_'constr c acc
+
+    (* Equality and inversion *)
+    | TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
+    | TacInversion (is, _)  -> depends_of_'a_'b_inversion_strength depends_of_'constr is acc
+
+    (* For ML extensions *)
+    | TacExtend (_, _, cgal) -> failwith "depends of TacExtend not implemented because depends of a generic_argument not implemented"
+
+    (* For syntax extensions *)
+    | TacAlias (_,_,gal,(_,gte)) -> failwith "depends of a TacAlias not implemented because depends of a generic_argument not implemented"
+  and depends_of_tac_fun_ast tfa acc = failwith "depend_of_tac_fun_ast not implemented yet"
+  and depends_of_tac_arg ta acc = match ta with
+    | TacDynamic (_,d)  -> failwith "Don't know what to do with a Dyn in tac_arg"
+    | TacVoid           -> acc
+    | MetaIdArg  _      -> failwith "Don't know what to do with a MetaIdArg in tac_arg"
+    | ConstrMayEval  me -> failwith "TODO: depends_of_tac_arg of a ConstrMayEval"
+    | IntroPattern   _  -> acc
+    | Reference     ltc -> acc (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *)
+    | Integer       _   -> acc
+    | TacCall (_,ltc,l) -> (* TODO: This assumes the "ltac constant" cannot somehow refer to a named object... *)
+	list_union_map depends_of_tac_arg l acc
+    | TacExternal (_,_,_,l) -> list_union_map depends_of_tac_arg l acc
+    | TacFreshId     _  -> acc
+    | Tacexp       tac  ->
+	depends_of_'tac tac acc
+  in
+    depends_of_tacexpr
+
+let rec depends_of_glob_tactic_expr (gte:glob_tactic_expr) acc =
+  depends_of_gen_tactic_expr
+    depends_of_rawconstr_and_expr
+    (depends_of_'a_or_var depends_of_inductive)
+    depends_of_glob_tactic_expr
+    gte
+    acc
+
+let rec depends_of_tacexpr te acc =
+  depends_of_gen_tactic_expr
+    depends_of_open_constr
+    depends_of_inductive
+    depends_of_glob_tactic_expr
+    te
+    acc
+
+let depends_of_compound_rule cr acc = match cr with
+  | Tactic (texp, _) -> depends_of_tacexpr texp acc
+  | Proof_instr (b, instr) ->
+      (* TODO: What is the boolean b? Should check. *)
+      failwith "Dependency calculation of Proof_instr not implemented yet"
+and depends_of_prim_rule pr acc = match pr with
+  | Refine c                     -> depends_of_constr c acc
+  | Intro id                     -> acc
+  | Intro_replacing id           -> acc
+  | Cut (_, _, t)                -> depends_of_constr t acc (* TODO: check what 2nd argument contains *)
+  | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+  | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+  | Convert_concl (t, _)         -> depends_of_constr t acc
+  | Convert_hyp (_, None, t)     -> depends_of_constr t acc
+  | Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
+  | Thin _                       -> acc
+  | ThinBody _                   -> acc
+  | Move _                       -> acc
+  | Rename _                     -> acc
+  | Change_evars                 -> acc
+
+let rec depends_of_pftree pt acc =
+  match pt.ref with
+    | None -> acc
+    | Some (Prim   pr    , l) -> depends_of_prim_rule pr (list_union_map depends_of_pftree l  acc)
+    | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p (list_union_map depends_of_pftree l acc))
+    | Some (Decl_proof _ , l) -> list_union_map depends_of_pftree l acc
+    | Some (Daimon,        l) -> list_union_map depends_of_pftree l acc
+
+let rec depends_of_pftree_head pt acc =
+  match pt.ref with
+    | None -> acc
+    | Some (Prim   pr    , l) -> depends_of_prim_rule pr acc
+    | Some (Nested (t, p), l) -> depends_of_compound_rule t (depends_of_pftree p acc)
+    | Some (Decl_proof _ , l) -> acc
+    | Some (Daimon,        l) -> acc
+
+let depends_of_pftreestate depends_of_pftree pfs =
+(*   print_string "depends_of_pftreestate called\n"; *)
+(*   explore_tree pfs; *)
+  let pt = proof_of_pftreestate pfs in
+    assert (is_top_pftreestate pfs);
+    assert (pt.open_subgoals = 0);
+    depends_of_pftree pt []
+
+let depends_of_definition_entry de ~acc =
+  Option.fold_right
+    depends_of_constr
+    de.const_entry_type
+    (depends_of_constr de.const_entry_body acc)