summaryrefslogtreecommitdiff
path: root/contrib/interface/depends.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /contrib/interface/depends.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/interface/depends.ml')
-rw-r--r--contrib/interface/depends.ml454
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)