X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Ftacticals.ml;h=28bd71b2da5901c199114dde8ce8bacf79aaa17f;hb=5aa1f1918c39c0d4130574927fa0f870e613cdea;hp=ceb2d2de88cb28fc8a7554ee87c1167e5c846af8;hpb=cbf47ddef11207628a9838973a192566e1e60ba7;p=helm.git diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml index ceb2d2de8..28bd71b2d 100644 --- a/components/tactics/tacticals.ml +++ b/components/tactics/tacticals.ml @@ -38,23 +38,25 @@ let debug_print = fun _ -> () (** debugging print *) let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s))) +module PET = ProofEngineTypes + let id_tac = let id_tac (proof,goal) = let _, metasenv, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in (proof,[goal]) in - ProofEngineTypes.mk_tactic id_tac + PET.mk_tactic id_tac let fail_tac = let fail_tac (proof,goal) = let _, metasenv, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in - raise (ProofEngineTypes.Fail (lazy "fail tactical")) + raise (PET.Fail (lazy "fail tactical")) in - ProofEngineTypes.mk_tactic fail_tac + PET.mk_tactic fail_tac -type goal = ProofEngineTypes.goal +type goal = PET.goal (** TODO needed until tactics start returning both opened and closed goals * First part of the function performs a diff among goals ~before tactic @@ -97,6 +99,7 @@ sig val do_tactic: n: int -> tactic: tactic -> tactic val try_tactic: tactic: tactic -> tactic val solve_tactics: tactics: (string * tactic) list -> tactic + val progress_tactic: tactic: tactic -> tactic val tactic: tactic -> tactic val skip: tactic @@ -141,7 +144,7 @@ struct with e -> match e with - | (ProofEngineTypes.Fail _) + | (PET.Fail _) | (CicTypeChecker.TypeCheckerFailure _) | (CicUnification.UnificationFailure _) -> info (lazy ( @@ -149,7 +152,7 @@ struct Printexc.to_string e)); first ~tactics istatus | _ -> raise e) (* [e] must not be caught ; let's re-raise it *) - | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left")) + | [] -> raise (PET.Fail (lazy "first: no tactics left")) in S.mk_tactic (first ~tactics) @@ -210,7 +213,7 @@ struct in S.set_goals (opened', closed') output_status with - (ProofEngineTypes.Fail _) as e -> + (PET.Fail _) as e -> info (lazy ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e)); @@ -232,7 +235,7 @@ struct in S.set_goals (opened', closed') output_status with - (ProofEngineTypes.Fail _) as e -> + (PET.Fail _) as e -> info (lazy ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e)) ; @@ -242,17 +245,17 @@ struct (* This applies tactic and catches its possible failure *) let try_tactic ~tactic = - let rec try_tactic ~tactic status = + let try_tactic status = info (lazy "in Tacticals.try_tactic"); try S.apply_tactic tactic status with - (ProofEngineTypes.Fail _) as e -> + (PET.Fail _) as e -> info (lazy ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); S.apply_tactic S.id_tactic status in - S.mk_tactic (try_tactic ~tactic) + S.mk_tactic try_tactic (* This tries tactics until one of them doesn't _solve_ the goal *) (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) @@ -275,18 +278,35 @@ struct | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic")); solve_tactics ~tactics:(moretactics) status with - (ProofEngineTypes.Fail _) as e -> + (PET.Fail _) as e -> info (lazy ( "Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e)); solve_tactics ~tactics status ) | [] -> - raise (ProofEngineTypes.Fail + raise (PET.Fail (lazy "solve_tactics cannot solve the goal")) in S.mk_tactic (solve_tactics ~tactics) + let progress_tactic ~tactic = + let msg = lazy "Failed to progress" in + let get_sequent (proof, goal) = + let (_, metasenv, _, _) = proof in + let _, context, ty = CicUtil.lookup_meta goal metasenv in + context, ty + in + let progress_tactic ist = + let before = get_sequent (S.get_status ist) in + let ost = S.apply_tactic tactic ist in + match S.goals ost with + | [goal], _ when before <> get_sequent (S.get_proof ost, goal) -> + raise (PET.Fail msg) + | _ -> ost + in + S.mk_tactic progress_tactic + let cont_proxy cont = S.mk_tactic (C.eval cont) let tactic t = cont_proxy (C.Tactical (C.Tactic t)) @@ -307,17 +327,17 @@ struct module Stack = Continuationals.Stack type input_status = - ProofEngineTypes.status (* (proof, goal) *) * Stack.t + PET.status (* (proof, goal) *) * Stack.t type output_status = - (ProofEngineTypes.proof * goal list * goal list) * Stack.t + (PET.proof * goal list * goal list) * Stack.t - type tactic = ProofEngineTypes.tactic + type tactic = PET.tactic let id_tactic = id_tac let mk_tactic f = - ProofEngineTypes.mk_tactic + PET.mk_tactic (fun (proof, goal) as pstatus -> let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in let istatus = pstatus, stack in @@ -328,14 +348,17 @@ struct proof, opened) let apply_tactic tac ((proof, _) as pstatus, stack) = - let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in + let proof', opened = PET.apply_tactic tac pstatus in (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *) - let before = ProofEngineTypes.goals_of_proof proof in - let after = ProofEngineTypes.goals_of_proof proof' in + let before = PET.goals_of_proof proof in + let after = PET.goals_of_proof proof' in let opened_goals, closed_goals = goals_diff ~before ~after ~opened in (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *) (proof', opened_goals, closed_goals), stack + let get_status (status, _) = status + let get_proof ((proof, _, _), _) = proof + let goals ((_, opened, closed), _) = opened, closed let set_goals (opened, closed) ((proof, _, _), stack) = (proof, opened, closed), stack