X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=4e14964ff3dc26016818fecd566e83ced817214c;hb=731309ad239f4a6d3fbe0fa7eb5d5066a446dcbf;hp=546fff631b1a6bf855a410e6ed0df65a15ab7520;hpb=5ca3189127b10847b4986330482f34157661bbcf;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 546fff631..4e14964ff 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -294,6 +294,7 @@ let find_matches metasenv context ugraph lift_amount term termty =
   as above, but finds all the matching equalities, and the matching condition
   can be either Founif.matching or Inference.unification
 *)
+(* XXX termty unused *)
 let rec find_all_matches ?(unif_fun=Founif.unification)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
@@ -363,10 +364,12 @@ let find_all_matches
 (*
   returns true if target is subsumed by some equality in table
 *)
+(*
 let print_res l =
   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
 ;;
+*)
 
 let subsumption_aux use_unification env table target = 
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
@@ -404,7 +407,7 @@ let subsumption_aux use_unification env table target =
         | Founif.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
-  match ok right Utils.Left  leftr with
+  match ok right Utils.Left leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
@@ -426,6 +429,61 @@ let unification x y z =
   subsumption_aux true x y z
 ;;
 
+let subsumption_aux_all use_unification env table target = 
+  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+  let _, context, ugraph = env in
+  let metasenv = tmetas in
+  let predicate, unif_fun = 
+    if use_unification then
+      Unification, Founif.unification
+    else
+      Matching, Founif.matching
+  in
+  let leftr =
+    match left with
+    | Cic.Meta _ when not use_unification -> []   
+    | _ ->
+        let leftc = get_candidates predicate table left in
+        find_all_matches ~unif_fun
+          metasenv context ugraph 0 left ty leftc
+  in
+  let rightr =
+        match right with
+          | Cic.Meta _ when not use_unification -> [] 
+          | _ ->
+              let rightc = get_candidates predicate table right in
+                find_all_matches ~unif_fun
+                  metasenv context ugraph 0 right ty rightc
+  in
+  let rec ok_all what leftorright = function
+    | [] -> []
+    | (_, subst, menv, ug, (pos,equation))::tl ->
+        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+        try
+          let other = if pos = Utils.Left then r else l in
+          let what' = Subst.apply_subst subst what in
+          let other' = Subst.apply_subst subst other in
+          let subst', menv', ug' =
+            unif_fun metasenv m context what' other' ugraph
+          in
+          (match Subst.merge_subst_if_possible subst subst' with
+          | None -> ok_all what leftorright tl
+          | Some s -> 
+	      (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
+        with 
+        | Founif.MatchingFailure 
+        | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
+  in
+  (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
+;;
+
+let subsumption_all x y z =
+  subsumption_aux_all false x y z
+;;
+
+let unification_all x y z = 
+  subsumption_aux_all true x y z
+;;
 let rec demodulation_aux bag ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
 (*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
@@ -566,6 +624,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
+    let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = 
@@ -600,9 +659,9 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-          assert (not (Equality.meta_convertibility_eq target newtarget));
-          if (Equality.is_weak_identity newtarget) ||
-            (Equality.meta_convertibility_eq target newtarget) then
+          (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
+          if (Equality.is_weak_identity newtarget) (* || *)
+            (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
           else 
             demodulation_equality bag ?from eq_uri newmeta env table newtarget
@@ -803,6 +862,7 @@ let superposition_right bag
       Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
 
+    let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
     let newgoal, newproof =
       (* qua *)
       let bo' =
@@ -904,7 +964,7 @@ let rec demodulation_theorem bag newmeta env table theorem =
 let open_goal g =
   match g with
   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
-      assert (LibraryObjects.is_eq_URI uri);
+      (* assert (LibraryObjects.is_eq_URI uri); *)
       proof,menv,eq,ty,l,r
   | _ -> assert false
 ;;
@@ -948,8 +1008,9 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = (*apply_subst subst*) t in 
-    let name = Cic.Name "x" in
+    let bo' = apply_subst subst t in
+    let ty = apply_subst subst ty in 
+    let name = Cic.Name "x" in 
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in
@@ -1035,4 +1096,118 @@ let rec demodulation_goal bag env table goal =
   | None -> do_right ()
 ;;
 
+type next = L | R 
+type solved = Yes of Equality.goal | No of Equality.goal list
+
+(* returns all the 1 step demodulations *)
+module C = Cic;; 
+module S = CicSubstitution;;
+let rec demodulation_all_aux 
+  metasenv context ugraph table lift_amount term 
+=
+  let candidates = 
+    get_candidates ~env:(metasenv,context,ugraph) Matching table term 
+  in
+  match term with
+  | C.Meta _ -> []
+  | _ ->
+      let termty, ugraph = C.Implicit None, ugraph in
+      let res =
+        find_all_matches 
+          metasenv context ugraph lift_amount term termty candidates
+      in
+      match term with
+      | C.Appl l ->
+         let res, _, _ = 
+           List.fold_left
+            (fun (res,l,r) t ->
+               res @ 
+               List.map 
+                 (fun (rel, s, m, ug, c) -> 
+                   (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+                 (demodulation_all_aux 
+                   metasenv context ugraph table lift_amount t),
+               l@[List.hd r], List.tl r)
+            (res, [], List.map (S.lift 1) l) l
+         in
+         res
+      | C.Prod (nn, s, t) 
+      | C.Lambda (nn, s, t) ->
+          let context = (Some (nn, C.Decl s))::context in
+          let mk s t = 
+            match term with 
+            | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
+          in
+          res @ 
+          List.map
+            (fun (rel, subst, m, ug, c) -> 
+               mk (S.lift 1 s) rel, subst, m, ug, c)
+            (demodulation_all_aux
+              metasenv context ugraph table (lift_amount+1) t)
+              (* we could demodulate also in s, but then t may be badly
+               * typed... *)
+      | t -> res
+;;
+
+let solve_demodulating bag env table initgoal steps =
+  let _, context, ugraph = env in
+  let solved goal res side = 
+    let newg = build_newgoal bag context goal side Equality.Demodulation res in
+    match newg with
+    | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) 
+      when LibraryObjects.is_eq_URI uri ->
+        (try 
+          let _ = 
+            Founif.unification m m context left right CicUniv.empty_ugraph 
+          in
+          Yes newg
+        with CicUnification.UnificationFailure _ -> No [newg])
+    | _ -> No [newg]
+  in
+  let solved goal res_list side = 
+    let newg = List.map (fun x -> solved goal x side) res_list in
+    try
+      List.find (function Yes _ -> true | _ -> false) newg
+    with Not_found -> 
+      No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
+  in
+  let rec first f l =
+    match l with
+    | [] -> None
+    | x::tl -> 
+       match f x with
+       | None -> first f tl
+       | Some x as ok -> ok
+  in
+  let rec aux steps next goal = 
+    if steps = 0 then None else
+    let goalproof,menv,_,_,left,right = open_goal goal in
+    let do_step t = 
+      demodulation_all_aux menv context ugraph table 0 t
+    in
+    match next with
+    | L -> 
+        (match do_step left with
+        | _::_ as res -> 
+            (match solved goal res Utils.Right with
+            | No newgoals -> 
+                 (match first (aux (steps - 1) L) newgoals with
+                 | Some g as success -> success
+                 | None -> aux steps R goal)
+            | Yes newgoal -> Some newgoal)
+        | [] -> aux steps R goal)
+    | R -> 
+        (match do_step right with
+        | _::_ as res -> 
+            (match solved goal res Utils.Left with
+            | No newgoals -> 
+                 (match first (aux (steps - 1) L) newgoals with
+                 | Some g as success -> success
+                 | None -> None)
+            | Yes newgoal -> Some newgoal)
+        | [] -> None) 
+  in
+  aux steps L initgoal
+;;
+
 let get_stats () = "" ;;