diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/interface/depends.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/interface/depends.ml')
-rw-r--r-- | contrib/interface/depends.ml | 454 |
1 files changed, 0 insertions, 454 deletions
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml deleted file mode 100644 index e0f43193..00000000 --- a/contrib/interface/depends.ml +++ /dev/null @@ -1,454 +0,0 @@ -(************************************************************************) -(* 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" - | 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" - | Order _ -> "Order" - 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" - | TacMatchGoal (_, _, 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], None) -> depends_of_'constr_with_bindings cb acc - | TacApply (_, _, _, _) -> failwith "TODO" - | 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 *) - | TacSimpleInductionDestruct _ - | TacDoubleInduction _ -> acc - | TacInductionDestruct (_, _, [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) - | TacInductionDestruct (_, _, _) -> failwith "TODO" - | 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 - | Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd 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 - | Order _ -> 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) |