From f654787b2156ede958a1d35ca8daf239de1b7b89 Mon Sep 17 00:00:00 2001
From: acerioni
Date: Fri, 12 Mar 2004 09:54:38 +0000
Subject: [PATCH] First implementation of the Auto tactic. - tacticChaser:
added a function to locate all the theorem tha can be applied -
variousTactics: the Auto tactic
---
helm/ocaml/tactics/.depend | 10 +-
helm/ocaml/tactics/Makefile | 13 +-
helm/ocaml/tactics/tacticChaser.ml | 213 ++++++++++++++++++++------
helm/ocaml/tactics/tacticChaser.mli | 8 +
helm/ocaml/tactics/variousTactics.ml | 72 +++++++++
helm/ocaml/tactics/variousTactics.mli | 7 +
6 files changed, 265 insertions(+), 58 deletions(-)
diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index 356cf4b85..683e59f88 100644
--- a/helm/ocaml/tactics/.depend
+++ b/helm/ocaml/tactics/.depend
@@ -3,6 +3,7 @@ tacticals.cmi: proofEngineTypes.cmo
reductionTactics.cmi: proofEngineTypes.cmo
proofEngineStructuralRules.cmi: proofEngineTypes.cmo
primitiveTactics.cmi: proofEngineTypes.cmo
+tacticChaser.cmi: proofEngineTypes.cmo
variousTactics.cmi: proofEngineTypes.cmo
introductionTactics.cmi: proofEngineTypes.cmo
eliminationTactics.cmi: proofEngineTypes.cmo
@@ -11,7 +12,6 @@ equalityTactics.cmi: proofEngineTypes.cmo
discriminationTactics.cmi: proofEngineTypes.cmo
ring.cmi: proofEngineTypes.cmo
fourierR.cmi: proofEngineTypes.cmo
-tacticChaser.cmi: proofEngineTypes.cmo
proofEngineReduction.cmo: proofEngineReduction.cmi
proofEngineReduction.cmx: proofEngineReduction.cmi
proofEngineHelpers.cmo: proofEngineHelpers.cmi
@@ -32,10 +32,12 @@ primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \
primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
primitiveTactics.cmi
+tacticChaser.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi
+tacticChaser.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi
variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \
- proofEngineTypes.cmo tacticals.cmi variousTactics.cmi
+ proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi
variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \
- proofEngineTypes.cmx tacticals.cmx variousTactics.cmi
+ proofEngineTypes.cmx tacticChaser.cmx tacticals.cmx variousTactics.cmi
introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \
introductionTactics.cmi
introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \
@@ -74,5 +76,3 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \
fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \
proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \
tacticals.cmx fourierR.cmi
-tacticChaser.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi
-tacticChaser.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi
diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile
index 0018ce230..4436c2142 100644
--- a/helm/ocaml/tactics/Makefile
+++ b/helm/ocaml/tactics/Makefile
@@ -1,20 +1,21 @@
PACKAGE = tactics
REQUIRES = \
+ pcre \
helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification \
helm-mathql_interpreter helm-mathql_generator
INTERFACE_FILES = \
proofEngineReduction.mli proofEngineHelpers.mli \
- tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
- primitiveTactics.mli variousTactics.mli introductionTactics.mli \
+ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
+ primitiveTactics.mli tacticChaser.mli variousTactics.mli introductionTactics.mli \
eliminationTactics.mli negationTactics.mli equalityTactics.mli \
- discriminationTactics.mli ring.mli fourierR.mli tacticChaser.mli
+ discriminationTactics.mli ring.mli fourierR.mli
IMPLEMENTATION_FILES = \
proofEngineTypes.ml proofEngineReduction.ml proofEngineHelpers.ml \
- fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \
- primitiveTactics.ml variousTactics.ml introductionTactics.ml \
+ fourier.ml tacticals.ml reductionTactics.ml proofEngineStructuralRules.ml \
+ primitiveTactics.ml tacticChaser.ml variousTactics.ml introductionTactics.ml \
eliminationTactics.ml negationTactics.ml equalityTactics.ml \
- discriminationTactics.ml ring.ml fourierR.ml tacticChaser.ml
+ discriminationTactics.ml ring.ml fourierR.ml
include ../Makefile.common
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 7270b70b3..a4ce74bb5 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -33,65 +33,184 @@
(* *)
(******************************************************************************)
+module MQI = MQueryInterpreter
+module MQIC = MQIConn
module I = MQueryInterpreter
module U = MQGUtil
module G = MQueryGenerator
(* search arguments on which Apply tactic doesn't fail *)
-let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() ~status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
+match list_of_must with
+ [] -> []
+|_ ->
let must = choose_must list_of_must only in
let result =
- I.execute mqi_handle
- (G.query_of_constraints
+ I.execute mqi_handle
+ (G.query_of_constraints
(Some CGMatchConclusion.universe)
(must,[],[]) (Some only,None,None)) in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let uris',exc =
- let rec filter_out =
- function
- [] -> [],""
- | uri::tl ->
- let tl',exc = filter_out tl in
- try
- if
- (try
- ignore
- (PrimitiveTactics.apply_tac
- ~term:(MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri))
- ~status);
- true
- with ProofEngineTypes.Fail _ -> false)
- then
- uri::tl',exc
- else
- tl',exc
- with
+ let uris =
+ List.map
+ (function uri,_ ->
+ MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result
+ in
+ let uris =
+ (* TODO ristretto per ragioni di efficienza *)
+ prerr_endline "STO FILTRANDO";
+ List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
+ in
+ prerr_endline "HO FILTRATO";
+ let uris',exc =
+ let rec filter_out =
+ function
+ [] -> [],""
+ | uri::tl ->
+ let tl',exc = filter_out tl in
+ try
+ if
+ (try
+ ignore
+ (PrimitiveTactics.apply_tac
+ ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string uri))
+ ~status);
+ true
+ with ProofEngineTypes.Fail _ -> false)
+ then
+ uri::tl',exc
+ else
+ tl',exc
+ with
(ProofEngineTypes.Fail _) as e ->
- let exc' =
- " ^ Exception raised trying to apply " ^
- uri ^ ": " ^ Printexc.to_string e ^ "
" ^ exc
- in
- tl',exc'
- in
- filter_out uris
- in
- let html' =
- " Objects that can actually be applied:
" ^
- String.concat "
" uris' ^ exc ^
- " Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "
" ^
- " Number of good matches: " ^
- string_of_int (List.length uris') ^ "
"
- in
- output_html html' ;
- uris'
+ let exc' =
+ " ^ Exception raised trying to apply " ^
+ uri ^ ": " ^ Printexc.to_string e ^ "
" ^ exc
+ in
+ tl',exc'
+ in
+ filter_out uris
+ in
+ let html' =
+ " Objects that can actually be applied:
" ^
+ String.concat "
" uris' ^ exc ^
+ " Number of false matches: " ^
+ string_of_int (List.length uris - List.length uris') ^ "
" ^
+ " Number of good matches: " ^
+ string_of_int (List.length uris') ^ "
"
+ in
+ output_html html' ;
+ uris'
+;;
+
+
+(*funzione che sceglie il penultimo livello di profondita' dei must*)
+
+(*
+let choose_must list_of_must only=
+let n = (List.length list_of_must) - 1 in
+ List.nth list_of_must n
+;;*)
+
+let choose_must list_of_must only =
+ List.nth list_of_must 0
+
+(* OLD CODE: TO BE REMOVED
+(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
+(*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
+
+exception NotInTheList;;
+
+
+let position n =
+ let rec aux k =
+ function
+ [] -> raise NotInTheList
+ | m::_ when m=n -> k
+ | _::tl -> aux (k+1) tl in
+ aux 1
+;;
+
+
+
+(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
+(*generate the less number of subgoals*)
+
+let searchTheorem ~status:(proof,goal) =
+ let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+ in
+ let mqi_handle = MQIC.init mqi_flags prerr_string
+in
+ let uris' =
+ matchConclusion
+ mqi_handle ~choose_must() ~status:(proof, goal)
+ in
+ let list_of_termin =
+ List.map
+ (function string ->
+ (MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string string))
+ )
+ uris'
+ in
+ let list_proofgoal =
+ List.map
+ (function term ->
+ PrimitiveTactics.apply_tac ~term ~status:(proof,goal))
+ list_of_termin
+ in
+ let (list_of_subgoal: int list list) =
+ List.map snd list_proofgoal
+ in
+ let list_of_num =
+ List.map List.length list_of_subgoal
+ in
+ let list_sort =
+ List.sort Pervasives.compare list_of_num
+ in (*ordino la lista in modo cresc*)
+ let min= List.nth list_sort 0 (*prendo il minimo*)
+ in
+ let uri' = (*cerco il teo di pos k*)
+ List.nth list_of_termin (position min list_of_num)
+ in
+ (* let teo=
+ String.sub uri' 4 (String.length uri' - 4)
+
+ (* modifico la str in modo che sia accettata da apply*)
+ in*)
+ PrimitiveTactics.apply_tac ~term:uri' ~status:(proof,goal)
+;;
+*)
+
+
+let searchTheorems mqi_handle ~status:(proof,goal) =
+prerr_endline "1";
+ let uris' =
+ matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
+prerr_endline "2";
+ let list_of_termin =
+ List.map
+ (function string ->
+ (MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string string)))
+ uris' in
+prerr_endline "3";
+ let list_proofgoal =
+ List.map
+ (function term ->
+ PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
+prerr_endline "4";
+let res =
+ List.sort
+ (fun (_,gl1) (_,gl2) ->
+ Pervasives.compare (List.length gl1) (List.length gl2))
+ list_proofgoal
+ in
+prerr_endline "5";
+res
;;
diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli
index d54de4603..e7e63954a 100644
--- a/helm/ocaml/tactics/tacticChaser.mli
+++ b/helm/ocaml/tactics/tacticChaser.mli
@@ -30,3 +30,11 @@ val matchConclusion : MQIConn.handle ->
MQGTypes.r_obj list) ->
unit -> status: ProofEngineTypes.status -> string list
+
+(* TODO: OLD CODE TO BE REMOVED
+val searchTheorem : status: ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
+*)
+
+val searchTheorems : MQIConn.handle -> status: ProofEngineTypes.status -> (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
+
+
diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 64b9ff790..70952d84d 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -23,6 +23,78 @@
* http://cs.unibo.it/helm/.
*)
+let search_theorems_in_context ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module S = CicSubstitution 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
+ [] -> []
+ | hd::tl ->
+ let res =
+ try
+ Some (PrimitiveTactics.apply_tac ~status ~term:(C.Rel n))
+ with
+ ProofEngineTypes.Fail _ -> None in
+ (match res with
+ Some res -> res::(find (n+1) tl)
+ | None -> find (n+1) tl)
+ in
+ try
+ let res = find 1 context in
+ prerr_endline "Ho finito context";
+ res
+ with Failure s ->
+ prerr_endline ("SIAM QUI = " ^ s); []
+;;
+
+
+exception NotApplicableTheorem;;
+exception MaxDepth;;
+
+let depth = 5;;
+
+let rec auto_tac mqi_handle level proof goal =
+prerr_endline "Entro in Auto_rec";
+if level = 0 then
+ (* (proof, [goal]) *)
+ (prerr_endline ("NON ci credo");
+ raise MaxDepth)
+else
+ (* choices is a list of pairs proof and goallist *)
+ let choices =
+ (search_theorems_in_context ~status:(proof,goal))@
+ (TacticChaser.searchTheorems mqi_handle ~status:(proof,goal))
+ in
+ let rec try_choices = function
+ [] -> raise NotApplicableTheorem
+ | (proof,goallist)::tl ->
+prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
+ (try
+ List.fold_left
+ (fun (proof,opengoals) goal ->
+ let newproof, newgoals = auto_tac mqi_handle (level-1) proof goal in
+ (newproof, newgoals@opengoals))
+ (proof,[]) goallist
+ with
+ | MaxDepth
+ | NotApplicableTheorem ->
+ try_choices tl) in
+ try_choices choices;;
+
+let auto_tac mqi_handle ~status:(proof,goal) =
+ prerr_endline "Entro in Auto";
+ try
+ let res = auto_tac mqi_handle depth proof goal in
+prerr_endline "AUTO_TAC HA FINITO";
+ res
+ with
+ | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
+ | NotApplicableTheorem ->
+ prerr_endline("No applicable theorem");
+ raise (ProofEngineTypes.Fail "No Applicable theorem");;
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli
index 2b45aa156..2be47c1ec 100644
--- a/helm/ocaml/tactics/variousTactics.mli
+++ b/helm/ocaml/tactics/variousTactics.mli
@@ -1,3 +1,4 @@
+
(* Copyright (C) 2002, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
@@ -24,8 +25,14 @@
*)
exception AllSelectedTermsMustBeConvertible;;
+exception NotApplicableTheorem;;
val assumption_tac: ProofEngineTypes.tactic
val generalize_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
ProofEngineTypes.tactic
+
+val auto_tac :
+ MQIConn.handle ->
+ status:ProofEngineTypes.status
+ -> ProofEngineTypes.proof * ProofEngineTypes.goal list
--
2.39.2