From 16d6d961a5d7db08bfdf1bccae7f36c6b2fd7fe2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 18 May 2004 13:25:35 +0000 Subject: [PATCH] Nuova implementazione di Auto "breadth-first". --- helm/ocaml/tactics/filter_auto.ml | 2 + helm/ocaml/tactics/tacticChaser.ml | 74 ++-------------------------- helm/ocaml/tactics/variousTactics.ml | 54 ++++++++++++++++++++ 3 files changed, 59 insertions(+), 71 deletions(-) diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml index 6fae7b737..73eaed638 100644 --- a/helm/ocaml/tactics/filter_auto.ml +++ b/helm/ocaml/tactics/filter_auto.ml @@ -32,8 +32,10 @@ let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConc let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;; +let escape = Str.global_replace (Str.regexp_string "\'") "\\'";; let hyp_const (conn:Mysql.dbd) uri = + let uri = escape uri in (*query to obtain all the constants in the hypothesis of the theorem*) let query = "select h_occurrence from refObj where source='"^uri^ diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index d3ba1d2a3..689102fe2 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -124,8 +124,10 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st MQIConn.MySQL_C conn -> conn | _ -> assert false in let result = Match_concl.cmatch conn ty in + (* Stampa il risultato della query List.iter (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result; + *) let uris = List.map (fun (n,u) -> @@ -140,7 +142,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st (* delete all not "cic:/Coq" uris *) let uris = (* TODO ristretto per ragioni di efficienza *) - List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in + List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in (* concl_cost are the costants in the conclusion of the proof while hyp_const are the constants in the hypothesis *) let (_,concl_const) = NewConstraints.constants_of ty in @@ -207,74 +209,6 @@ let choose_must list_of_must only = with _ -> 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 (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() (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 (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' (proof,goal) -;; -*) - - let searchTheorems mqi_handle (proof,goal) = (*prerr_endline "1";*) let subproofs = @@ -292,7 +226,5 @@ let searchTheorems mqi_handle (proof,goal) = in (* now we may drop the prefix tag *) List.map snd res - - ;; diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index f8c9cfa94..0df44420c 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -85,6 +85,7 @@ exception MaxDepth;; let depth = 3;; +(* let rec auto_tac_aux mqi_handle level proof goal = prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level)); if level = 0 then @@ -168,6 +169,59 @@ prerr_endline "AUTO_TAC HA FINITO"; | NotApplicableTheorem -> prerr_endline("No applicable theorem"); raise (ProofEngineTypes.Fail "No Applicable theorem");; +*) + +(**** ESPERIMENTO ************************) + +let new_search_theorems f proof goal depth gtl = + let local_choices = f (proof,goal) + in + List.map + (function (proof, goallist) -> + (proof, (List.map (function g -> (g,depth)) goallist)@gtl)) + local_choices +;; + +exception NoOtherChoices;; + +let rec auto_new mqi_handle = function + [] -> raise NoOtherChoices + | (proof, [])::tl -> (proof, [])::tl + | (proof, (goal,0)::gtl)::tl -> auto_new mqi_handle tl + | (proof, (goal,depth)::gtl)::tl -> + let _,metasenv,_,_ = proof in + let meta_inf = + (try + let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in + Some (ey, ty) + with _ -> None) in + match meta_inf with + Some _ -> + let local_choices = + new_search_theorems + search_theorems_in_context proof goal (depth-1) gtl in + let global_choices = + new_search_theorems + (TacticChaser.searchTheorems mqi_handle) + proof goal (depth-1) gtl in + let all_choices = + local_choices@global_choices@tl in + let reorder = all_choices in + auto_new mqi_handle reorder + | None -> auto_new mqi_handle ((proof,gtl)::tl) +;; + + +let auto_tac mqi_handle (proof,goal) = + prerr_endline "Entro in Auto"; + try + let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in +prerr_endline "AUTO_TAC HA FINITO"; + (proof,[]) + with + | NoOtherChoices -> + prerr_endline("Auto failed"); + 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 -- 2.39.2