]> matita.cs.unibo.it Git - helm.git/commitdiff
added the geniric
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Jun 2006 15:33:02 +0000 (15:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Jun 2006 15:33:02 +0000 (15:33 +0000)
  auto params
syntax and the auto superposition tactic

12 files changed:
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/autoTactic.ml
components/tactics/autoTactic.mli
components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/saturation.mli
components/tactics/tactics.mli
matita/matita.ml
matita/matitaGui.ml

index ffd35c703b3ec30461ecbd94b58539c401094f86..a9ac1c6eb5a5cc418064febe5f88de7c283c6e46 100644 (file)
@@ -49,8 +49,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Apply of loc * 'term
   | ApplyS of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option * string option * string option 
-      (* depth, width, paramodulation, full *) (* ALB *)
+  | Auto of loc * (string * string) list
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
   | Clear of loc * 'ident
   | ClearBody of loc * 'ident
index 20d57ef9e5ab6cc63b92778d972fdf4f8a952bc5..24d37c4f318d8c1f0ee1b90b6521d5d6333861fa 100644 (file)
@@ -73,8 +73,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term) -> "applyS " ^ term_pp term
-  | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
-  | Auto _ -> "auto"
+  | Auto (_,params) -> "auto " ^ 
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
index e4f70117a344bb41db8700aaa5d588d2cd3b834c..ae497fc12cbdd25db29b319643cfbe444d421aa0 100644 (file)
@@ -63,9 +63,8 @@ let tactic_of_ast ast =
   | GrafiteAst.ApplyS (_, term) ->
      Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
-      AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
-        ~dbd:(LibraryDb.instance ()) ()
+  | GrafiteAst.Auto (_,params) ->
+      AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
index 0e96aaf2dc871b303ed8436d158ab8a9c3229701..16421efafb386df29236fe77b36e9a9ba05b0cfe 100644 (file)
@@ -129,8 +129,8 @@ let disambiguate_tactic
         metasenv,GrafiteAst.ApplyS (loc, cic)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
-    | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
-        metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+    | GrafiteAst.Auto (loc,params) ->
+        metasenv,GrafiteAst.Auto (loc,params)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in
index ad081d6641d1c8bd34b20478701404f95bb5e8e0..c0ce1c27d359097b676a436c05923127ffc53dda 100644 (file)
@@ -132,12 +132,10 @@ EXTEND
         GrafiteAst.ApplyS (loc, t)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto";
-      depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
-      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
-      paramodulation = OPT [ IDENT "paramodulation" ];
-      full = OPT [ IDENT "full" ] ->  (* ALB *)
-          GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+    | IDENT "auto"; params = 
+        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+        GrafiteAst.Auto (loc,params)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->
index 9f54c6cecc15764d460d307281f3fcf262749211..1ba1dd912495f63801c7ffbf90b0d785e93e883e 100644 (file)
@@ -46,7 +46,7 @@ type exitus =
     No of int 
   | Yes of Cic.term * int 
   | NotYetInspected
-       
+        
 let inspected_goals = Hashtbl.create 503;;
 
 let search_theorems_in_context status =
@@ -93,17 +93,17 @@ let compare_goals proof goal1 goal2 =
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
-                    CicUniv.empty_ugraph in
+                     CicUniv.empty_ugraph in
   let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 
-                    CicUniv.empty_ugraph in
+                     CicUniv.empty_ugraph in
   let prop1 =
     let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 
-               CicUniv.empty_ugraph in
+                CicUniv.empty_ugraph in
       if b then 0 else 1
   in
   let prop2 =
     let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 
-               CicUniv.empty_ugraph in
+                CicUniv.empty_ugraph in
       if b then 0 else 1
   in
   prop1 - prop2
@@ -139,90 +139,90 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
   let is_meta_closed = CicUtil.is_meta_closed ty in
     begin
       match exitus with
-         Yes (bo,_) ->
+          Yes (bo,_) ->
             (*
               debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
-             debug_print (lazy (CicPp.ppterm ty));
+              debug_print (lazy (CicPp.ppterm ty));
             *)
             let subst_in =
               (* if we just apply the subtitution, the type 
                  is irrelevant: we may use Implicit, since it will 
                  be dropped *)
-             CicMetaSubst.apply_subst 
-               [(goal,(ey, bo, Cic.Implicit None))] in
-           let (proof,_) = 
-             ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
-               proof goal subst_in metasenv in
-             [(subst_in,(proof,[],sign))]
+              CicMetaSubst.apply_subst 
+                [(goal,(ey, bo, Cic.Implicit None))] in
+            let (proof,_) = 
+              ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
+                proof goal subst_in metasenv in
+              [(subst_in,(proof,[],sign))]
         | No d when (d >= depth) -> 
-           (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
-           [] (* the empty list means no choices, i.e. failure *)
-       | No _ 
-       | NotYetInspected ->
-             debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty));
-             debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p));
-             debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey));
-           let sign, new_sign =
-             if is_meta_closed then
-               None, Some (MetadataConstraints.signature_of ty)
-             else sign,sign in (* maybe the union ? *)
-           let local_choices =
-             new_search_theorems 
-               search_theorems_in_context dbd
-               proof goal (depth-1) new_sign in
-           let global_choices =
-             new_search_theorems 
-               (fun status -> 
-                  List.map snd
-                  (new_experimental_hint 
-                     ~dbd ~facts:facts ?signature:sign ~universe status))
-               dbd proof goal (depth-1) new_sign in 
-           let all_choices =
-             local_choices@global_choices in
-           let sorted_choices = 
-             List.stable_sort
-               (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
-                  Pervasives.compare 
-                  (List.length goals1) (List.length goals2))
-               all_choices in 
-             (match (auto_new dbd width already_seen_goals universe sorted_choices) 
-              with
-                  [] -> 
-                    (* no proof has been found; we update the
-                       hastable *)
-                    (* if is_meta_closed then *)
-                      Hashtbl.add inspected_goals ty (No depth);
-                    []
-                | (subst,(proof,[],sign))::tl1 -> 
-                    (* a proof for goal has been found:
-                       in order to get the proof we apply subst to
-                       Meta[goal] *)
-                    if is_meta_closed  then
-                      begin 
-                        let irl = 
-                          CicMkImplicit.identity_relocation_list_for_metavariable ey in
-                        let meta_proof = 
-                          subst (Cic.Meta(goal,irl)) in
-                          Hashtbl.add inspected_goals 
-                            ty (Yes (meta_proof,depth));
+            (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
+            [] (* the empty list means no choices, i.e. failure *)
+        | No _ 
+        | NotYetInspected ->
+              debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty));
+              debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p));
+              debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey));
+            let sign, new_sign =
+              if is_meta_closed then
+                None, Some (MetadataConstraints.signature_of ty)
+              else sign,sign in (* maybe the union ? *)
+            let local_choices =
+              new_search_theorems 
+                search_theorems_in_context dbd
+                proof goal (depth-1) new_sign in
+            let global_choices =
+              new_search_theorems 
+                (fun status -> 
+                   List.map snd
+                   (new_experimental_hint 
+                      ~dbd ~facts:facts ?signature:sign ~universe status))
+                dbd proof goal (depth-1) new_sign in 
+            let all_choices =
+              local_choices@global_choices in
+            let sorted_choices = 
+              List.stable_sort
+                (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
+                   Pervasives.compare 
+                   (List.length goals1) (List.length goals2))
+                all_choices in 
+              (match (auto_new dbd width already_seen_goals universe sorted_choices) 
+               with
+                   [] -> 
+                     (* no proof has been found; we update the
+                        hastable *)
+                     (* if is_meta_closed then *)
+                       Hashtbl.add inspected_goals ty (No depth);
+                     []
+                 | (subst,(proof,[],sign))::tl1 -> 
+                     (* a proof for goal has been found:
+                        in order to get the proof we apply subst to
+                        Meta[goal] *)
+                     if is_meta_closed  then
+                       begin 
+                         let irl = 
+                           CicMkImplicit.identity_relocation_list_for_metavariable ey in
+                         let meta_proof = 
+                           subst (Cic.Meta(goal,irl)) in
+                           Hashtbl.add inspected_goals 
+                             ty (Yes (meta_proof,depth));
 (*
-                          begin
-                            let cty,_ = 
-                              CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
-                            in
-                              if not (cty = ty) then
-                                begin
-                                  debug_print (lazy ("ty =  "^CicPp.ppterm ty));
-                                  debug_print (lazy ("cty =  "^CicPp.ppterm cty));
-                                  assert false
-                                end
-                                  Hashtbl.add inspected_goals 
-                                  ty (Yes (meta_proof,depth));
-                          end;
+                           begin
+                             let cty,_ = 
+                               CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
+                             in
+                               if not (cty = ty) then
+                                 begin
+                                   debug_print (lazy ("ty =  "^CicPp.ppterm ty));
+                                   debug_print (lazy ("cty =  "^CicPp.ppterm cty));
+                                   assert false
+                                 end
+                                   Hashtbl.add inspected_goals 
+                                   ty (Yes (meta_proof,depth));
+                           end;
 *)
-                      end;
-                    (subst,(proof,[],sign))::tl1
-                | _ -> assert false)
+                       end;
+                     (subst,(proof,[],sign))::tl1
+                 | _ -> assert false)
     end
       
 and auto_new dbd width already_seen_goals universe = function
@@ -232,7 +232,7 @@ and auto_new dbd width already_seen_goals universe = function
       let goals'=
         List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
       in
-       auto_new_aux dbd 
+            auto_new_aux dbd 
         width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 
 and auto_new_aux dbd width already_seen_goals universe = function
@@ -247,23 +247,23 @@ and auto_new_aux dbd width already_seen_goals universe = function
       let _,metasenv,p,_ = proof in
       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
       match (auto_single dbd proof goal ey ty depth
-       (width - (List.length gtl)) sign already_seen_goals) universe
+        (width - (List.length gtl)) sign already_seen_goals) universe
       with
-         [] -> auto_new dbd width already_seen_goals universe tl 
-       | (local_subst,(proof,[],sign))::tl1 -> 
-           let new_subst f t = f (subst t) in
-           let is_meta_closed = CicUtil.is_meta_closed ty in
-           let all_choices =
-             if is_meta_closed then 
-               (new_subst local_subst,(proof,gtl,sign))::tl
-             else
-               let tl2 = 
-                 (List.map 
-                    (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
-               in                       
-                 (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
-             auto_new dbd width already_seen_goals universe all_choices
-       | _ -> assert false
+          [] -> auto_new dbd width already_seen_goals universe tl 
+        | (local_subst,(proof,[],sign))::tl1 -> 
+            let new_subst f t = f (subst t) in
+            let is_meta_closed = CicUtil.is_meta_closed ty in
+            let all_choices =
+              if is_meta_closed then 
+                (new_subst local_subst,(proof,gtl,sign))::tl
+              else
+                let tl2 = 
+                  (List.map 
+                     (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
+                in                         
+                  (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
+              auto_new dbd width already_seen_goals universe all_choices
+        | _ -> assert false
  ;; 
 
 let default_depth = 5
@@ -281,14 +281,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
   let t1 = Unix.gettimeofday () in
   match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
       [] ->  debug_print (lazy "Auto failed");
-       raise (ProofEngineTypes.Fail "No Applicable theorem")
+        raise (ProofEngineTypes.Fail "No Applicable theorem")
     | (_,(proof,[],_))::_ ->
         let t2 = Unix.gettimeofday () in
-       debug_print (lazy "AUTO_TAC HA FINITO");
-       let _,_,p,_ = proof in
-       debug_print (lazy (CicPp.ppterm p));
+        debug_print (lazy "AUTO_TAC HA FINITO");
+        let _,_,p,_ = proof in
+        debug_print (lazy (CicPp.ppterm p));
         Printf.printf "tempo: %.9f\n" (t2 -. t1);
-       (proof,[])
+        (proof,[])
     | _ -> assert false
   in
   ProofEngineTypes.mk_tactic (auto_tac dbd)
@@ -304,8 +304,35 @@ let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
 *)
 
-let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
-    ?full ~(dbd:HMysql.dbd) () =
+let bool name params =
+    try let _ = List.assoc name params in true with
+    | Not_found -> false
+;; 
+
+let string name params =
+    try List.assoc name params with
+    | Not_found -> ""
+;; 
+
+let int name params =
+    try int_of_string (List.assoc name params) with
+    | Not_found -> default_depth
+    | Failure _ -> 
+        raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;  
+
+let auto_tac ~params ~(dbd:HMysql.dbd) =
+  (* argument parsing *)
+  let depth = int "depth" params in
+  let width = int "width" params in
+  let paramodulation = bool "paramodulation" params in
+  let full = bool "full" params in
+  let superposition = bool "superposition" params in
+  let what = string "what" params in
+  let other = string "other" params in
+  let subterms_only = bool "subterms_only" params in
+  let demodulate = bool "demodulate" params in
+  (* the real tactic *)
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
@@ -317,24 +344,20 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
         auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)]
       with
         [] ->  debug_print(lazy "Auto failed");
-         raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
+          raise (ProofEngineTypes.Fail (lazy "No Applicable theorem"))
       | (_,(proof,[],_))::_ ->
           let t2 = Unix.gettimeofday () in
-         debug_print (lazy "AUTO_TAC HA FINITO");
-         let _,_,p,_ = proof in
-         debug_print (lazy (CicPp.ppterm p));
+          debug_print (lazy "AUTO_TAC HA FINITO");
+          let _,_,p,_ = proof in
+          debug_print (lazy (CicPp.ppterm p));
           debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
-         (proof,[])
+          (proof,[])
       | _ -> assert false
     in
-    let full = match full with None -> false | Some _ -> true in
     let paramodulation_ok =
-      match paramodulation with
-      | None -> false
-      | Some _ ->
-          let _, metasenv, _, _ = proof in
-          let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          full || (Equality.term_is_equality meta_goal)
+      let _, metasenv, _, _ = proof in
+      let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
+      paramodulation && (full || (Equality.term_is_equality meta_goal))
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
@@ -352,7 +375,11 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
     ) else
       normal_auto () 
   in
-  ProofEngineTypes.mk_tactic (auto_tac dbd)
+  match superposition with
+  | true -> 
+      ProofEngineTypes.mk_tactic
+       (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate)
+  | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
 
 (********************** applyS *******************)
@@ -368,37 +395,37 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term'
    let proof'',goals =
     match LibraryObjects.eq_URI () with
     | Some uri -> 
-           ProofEngineTypes.apply_tactic
-            (Tacticals.then_
-              ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
-              ~continuation:
-                (PrimitiveTactics.cut_tac
-                  (CicSubstitution.lift 1
-                   (Cic.Appl
-                    [Cic.MutInd (uri,0,[]);
-                     Cic.Sort Cic.Prop;
-                     consthead;
-                     ty])))) (proof',goal)
+            ProofEngineTypes.apply_tactic
+             (Tacticals.then_
+               ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
+               ~continuation:
+                 (PrimitiveTactics.cut_tac
+                   (CicSubstitution.lift 1
+                    (Cic.Appl
+                     [Cic.MutInd (uri,0,[]);
+                      Cic.Sort Cic.Prop;
+                      consthead;
+                      ty])))) (proof',goal)
    | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
     in
      match goals with
         [g1;g2] ->
-         let proof'',goals =
-          ProofEngineTypes.apply_tactic
-           (auto_tac ~paramodulation:"qualsiasi" ~dbd ()) (proof'',g2)
-         in
-          let proof'',goals =
-           ProofEngineTypes.apply_tactic
-            (Tacticals.then_
-             ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
-               ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
+          let proof'',goals =
+           ProofEngineTypes.apply_tactic
+           (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2)
+          in
+           let proof'',goals =
+            ProofEngineTypes.apply_tactic
+             (Tacticals.then_
+              ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
+                ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
               ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
-            ) (proof'',g1)
-          in
+             ) (proof'',g1)
+           in
             proof'',
-            (*CSC: Brrrr.... *)
-            ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
-             ~newmetasenv:(let _,m,_,_ = proof'' in m)
+             (*CSC: Brrrr.... *)
+             ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+              ~newmetasenv:(let _,m,_,_ = proof'' in m)
       | _ -> assert false
 
 let rec count_prods context ty =
index 2070116488d577308330a210a0c860f0fd53bfe9..1dfe0e2a94c60284fa8c262f8caf5caf8c86c4d7 100644 (file)
@@ -25,8 +25,8 @@
  *)
 
 val auto_tac:
-  ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string ->
-  dbd:HMysql.dbd -> unit ->
+  params:(string * string) list ->
+  dbd:HMysql.dbd -> 
   ProofEngineTypes.tactic
 
 val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
index ca9dc194bd8f0af487c3c0faafb13e82080ec5ee..f81556c8f997e7088fbfe006b3552fdec48c8132 100644 (file)
@@ -1454,6 +1454,12 @@ let eq_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
+let eq_and_ty_of_goal = function
+  | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
+      uri,t
+  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
 let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
@@ -1819,7 +1825,6 @@ let main_demod_equalities dbd term metasenv ugraph =
 ;;
 
 let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
-  let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let eq_uri = eq_of_goal ty in 
@@ -1827,7 +1832,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
     Inference.find_equalities context proof 
   in
   let lib_eq_uris, library_equalities, maxm =
-    I.find_library_equalities dbd context (proof, goal) (maxm+2) in
+    Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
@@ -1871,6 +1876,74 @@ let demodulate_tac ~dbd ~pattern =
   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
 ;;
 
+let rec find_in_ctx i name = function
+  | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
+  | Some (Cic.Name name', _)::tl when name = name' -> i
+  | _::tl -> find_in_ctx (i+1) name tl
+;;
+
+let rec position_of i x = function
+  | [] -> assert false
+  | j::tl when j <> x -> position_of (i+1) x tl
+  | _ -> i
+;;
+
+let superposition_tac ~what ~other ~subterms_only ~demodulate status = 
+  reset_refs();
+  let proof,goalno = status in 
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri,tty = eq_and_ty_of_goal ty in
+  let env = (metasenv, context, CicUniv.empty_ugraph) in
+  let names = names_of_context context in
+  let eq_index, equalities, maxm = find_equalities context proof in
+  let what = find_in_ctx 1 what context in
+  let other = find_in_ctx 1 other context in
+  let eq_what = List.nth equalities (position_of 0 what eq_index) in
+  let eq_other = List.nth equalities (position_of 0 other eq_index) in
+  let index = Indexing.index Indexing.empty eq_other in
+  let maxm, eql = 
+    Indexing.superposition_right 
+      ~subterms_only eq_uri maxm env index eq_what
+  in
+  prerr_endline ("Superposition right:");
+  prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
+  prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env);
+  prerr_endline ("\n result: ");
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+  prerr_endline ("\n result (cut&paste): ");
+  List.iter 
+    (fun e -> 
+      let t = Equality.term_of_equality eq_uri e in
+      prerr_endline (CicPp.pp t names)) 
+  eql;
+  if demodulate then
+    begin
+      let table = List.fold_left Indexing.index Indexing.empty equalities in
+      let maxm,eql = 
+        List.fold_left 
+          (fun (maxm,acc) e -> 
+            let maxm,eq = 
+              Indexing.demodulation_equality 
+                eq_uri maxm env table Utils.Positive e
+            in
+            maxm,eq::acc) 
+          (maxm,[]) eql
+      in
+      let eql = List.rev eql in
+      prerr_endline ("\n result [demod]: ");
+      List.iter 
+        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+      prerr_endline ("\n result [demod] (cut&paste): ");
+      List.iter 
+        (fun e -> 
+          let t = Equality.term_of_equality eq_uri e in
+          prerr_endline (CicPp.pp t names)) 
+      eql;
+    end;
+  proof,[goalno]
+;;
+
 let get_stats () = 
   <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
   Equality.get_stats ();;
index 7a16895a77a8abe67d9f1eb4eeadfcc33ae39590..6a46887113343e2bf436729494a9ab97de61d584 100644 (file)
@@ -32,8 +32,7 @@ val saturate :
   ?depth:int ->
   ?width:int ->
   ProofEngineTypes.proof * ProofEngineTypes.goal ->
-  (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
-  ProofEngineTypes.goal list
+  ProofEngineTypes.proof * ProofEngineTypes.goal list
 
 val weight_age_ratio : int ref
 val weight_age_counter: int ref
@@ -52,4 +51,10 @@ val demodulate_tac:
   dbd:HMysql.dbd ->  
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 
+val superposition_tac: 
+  what:string -> other:string -> subterms_only:bool ->
+  demodulate:bool ->  
+  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+   ProofEngineTypes.proof * ProofEngineTypes.goal list
+
 val get_stats: unit -> string
index 06b62911c95492ad6c14468ee9986459afa38d40..2ff482ff1c6cc7ac10fc41f2c433b825b9169278 100644 (file)
@@ -3,11 +3,8 @@ val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-val auto :
-  ?depth:int ->
-  ?width:int ->
-  ?paramodulation:string ->
-  ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
+val auto : 
+  params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term -> ProofEngineTypes.tactic
index 58b7de9f34c2a9f02d94b39cc0ac589e5d0ecc8d..3c5bf8441555a33c98bd54d273616c4b018be067 100644 (file)
@@ -149,6 +149,17 @@ let _ =
             (MatitaScript.current ())#proofMetasenv));
         prerr_endline ("stack: " ^ Continuationals.Stack.pp
           (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_status)));
+     addDebugItem "Print current proof term" 
+       (fun _ -> 
+        HLog.debug
+          (CicPp.ppterm 
+            (match 
+            (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+            with
+            | GrafiteTypes.No_proof -> (Cic.Implicit None)
+            | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
+            | Proof p -> let _,_,p,_ = p in p
+            | Intermediate _ -> assert false)));
 (*     addDebugItem "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int
index b1b2a6ad3fa683c2856a9f4226bd547077534365..b230adecc50f41ae68cb8c22c3facd47b25ac30d 100644 (file)
@@ -612,7 +612,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,[])));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;