From: Andrea Asperti Date: Tue, 30 Nov 2004 14:55:27 +0000 (+0000) Subject: Bug in the management of substitutions into auto corrected. X-Git-Tag: PRE_UNIVERSES~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e09713d333183e929f108ff8bb8fbe2a25bfcac7;p=helm.git Bug in the management of substitutions into auto corrected. No significative loss in performance. Comments commented. --- diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index bc9991664..ce700f2de 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -54,7 +54,6 @@ let search_theorems_in_context status = let module S = CicSubstitution in let module PET = ProofEngineTypes in let module PT = PrimitiveTactics in - prerr_endline "Entro in search_context"; let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function @@ -76,7 +75,7 @@ let search_theorems_in_context status = [] ;; -let depth = 4;; +let depth = 6;; let new_search_theorems f proof goal depth gtl sign = let choices = f (proof,goal) @@ -105,9 +104,11 @@ let rec auto dbd = function match meta_inf with Some (ey, ty) -> (* the goal is still there *) + (* prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p)); prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); + *) (* if the goal contains metavariables we use the input signature for at_most constraints *) let is_meta_closed = CicUtil.is_meta_closed ty in @@ -189,7 +190,6 @@ let search_theorems_in_context status = let module S = CicSubstitution in let module PET = ProofEngineTypes in let module PT = PrimitiveTactics in - prerr_endline "Entro in search_context"; let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function @@ -210,12 +210,13 @@ let search_theorems_in_context status = [] ;; -let new_search_theorems f proof goal depth gtl sign = +let new_search_theorems f proof goal depth subst sign = let choices = f (proof,goal) in List.map - (function (subst,(proof, goallist)) -> - (subst,(proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))) + (function (local_subst,(proof, goallist)) -> + let new_subst t= local_subst (subst t) in + (new_subst,(proof,(List.map (function g -> (g,depth)) goallist), sign))) choices ;; @@ -243,8 +244,10 @@ let rec auto_new dbd = function begin match exitus with Yes (bo,_) -> + (* prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; prerr_endline (CicPp.ppterm ty); + *) let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will @@ -257,13 +260,18 @@ let rec auto_new dbd = function let new_subst t = (subst_in (subst t)) in auto_new dbd ((new_subst,(proof,gtl,sign))::tl) | No d when (d >= depth) -> + (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; + *) auto_new dbd tl + | No _ | NotYetInspected -> + (* prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty)); prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p)); prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey))); + *) let sign, new_sign = if is_meta_closed then None, Some (MetadataConstraints.signature_of ty) @@ -271,14 +279,14 @@ let rec auto_new dbd = function let local_choices = new_search_theorems search_theorems_in_context - proof goal (depth-1) [] new_sign in + proof goal (depth-1) subst new_sign in let global_choices = new_search_theorems (fun status -> List.map snd (MetadataQuery.experimental_hint ~dbd ~facts:facts ?signature:sign status)) - proof goal (depth-1) [] new_sign in + proof goal (depth-1) subst new_sign in let all_choices = local_choices@global_choices in (match (auto_new dbd all_choices) @@ -288,7 +296,7 @@ let rec auto_new dbd = function hastable *) Hashtbl.add inspected_goals ty (No depth); auto_new dbd tl - | (local_subst,(proof,[],_))::tl1 -> + | (new_subst,(proof,[],_))::tl1 -> (* a proof for goal has been found: in order to get the proof we apply subst to Meta[goal] *) @@ -297,11 +305,10 @@ let rec auto_new dbd = function let irl = CicMkImplicit.identity_relocation_list_for_metavariable ey in let meta_proof = - local_subst (Cic.Meta(goal,irl)) in + new_subst (Cic.Meta(goal,irl)) in Hashtbl.add inspected_goals ty (Yes (meta_proof,depth)); end; - let new_subst t = (local_subst (subst t)) in let all_choices = let gtl' = List.map fst gtl in if (gtl = [] || is_meta_closed) then diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index bb5594a35..e5656b9b3 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -126,7 +126,6 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -prerr_endline "HYP SIGNATURE"; Constr.StringSet.iter prerr_endline hyp_constants; let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = @@ -144,7 +143,7 @@ Constr.StringSet.iter prerr_endline hyp_constants; (let status' = try let (proof, goal_list) = - prerr_endline ("STO APPLICANDO " ^ uri); +(* prerr_endline ("STO APPLICANDO " ^ uri); *) PET.apply_tactic (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) @@ -198,7 +197,6 @@ let experimental_hint let hyp_constants = Constr.StringSet.diff (signature_of_hypothesis context) types_constants in -prerr_endline "HYP SIGNATURE"; Constr.StringSet.iter prerr_endline hyp_constants; let other_constants = Constr.StringSet.union sig_constants hyp_constants in let uris = @@ -216,7 +214,7 @@ Constr.StringSet.iter prerr_endline hyp_constants; (let status' = try let (subst,(proof, goal_list)) = - prerr_endline ("STO APPLICANDO" ^ uri); + (* prerr_endline ("STO APPLICANDO" ^ uri); *) PrimitiveTactics.apply_tac_verbose ~term:(CicUtil.term_of_uri uri) status