]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/paramodulation/indexing.ml
version 0.7.1
[helm.git] / helm / ocaml / paramodulation / indexing.ml
index 5a8960101d21c2a513b4acc18223817c1aad27c7..bd9091e4c927dea2d8be0c9c27d1ee50ac979fa3 100644 (file)
@@ -143,7 +143,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -200,7 +200,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (proof, (ty, left, right, o), metas, args) = candidate in
+        let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
         let do_match c other eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -277,7 +277,7 @@ let subsumption env table target =
         find_all_matches ~unif_fun:Inference.matching
           metasenv context ugraph 0 left leftc
   in
-  let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
+  let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
     try
       let other = if pos = Utils.Left then r else l in
       let subst', menv', ug' =
@@ -377,29 +377,43 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
 
 let build_newtarget_time = ref 0.;;
 
+
+let demod_counter = ref 1;;
+
 let rec demodulation newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let metasenv, context, ugraph = env in
-  let proof, (eq_ty, left, right, order), metas, args = target in
+  let _, proof, (eq_ty, left, right, order), metas, args = target in
   let metasenv' = metasenv @ metas in
   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
       let bo = (* M. *)apply_subst subst (S.subst other t) in
-      let bo'' =
-        C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
-                 S.lift 1 eq_ty] @
-                 if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
+      let t' =
+        let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
+        incr demod_counter;
+        let l, r = if is_left then bo, right else left, bo in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []); *)
+(*                  S.lift 1 eq_ty] @ *)
+(*                  if is_left then [S.lift 1 bo; S.lift 1 right] *)
+(*                  else [S.lift 1 left; S.lift 1 bo]) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
+(*         incr demod_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo,
-      C.Implicit None
+      Inference.ProofBlock (subst, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                                    proof; other; proof']) *)
     in
@@ -417,19 +431,23 @@ let rec demodulation newmeta env table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
-    newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
+
+    let res =
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
+    in
+    newmeta, res
   in
 (*   let build_newtarget = *)
 (*     let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
 (*     (fun a b -> profile (build_newtarget a) b) *)
 (*   in *)
   let res = demodulate_term metasenv' context ugraph table 0 left in
-  let build_identity (p, (t, l, r, o), m, a) =
-    match o with
-    | Utils.Gt -> (p, (t, r, r, Utils.Eq), m, a)
-    | _ -> (p, (t, l, l, Utils.Eq), m, a)
-  in
+(*   let build_identity (w, p, (t, l, r, o), m, a) = *)
+(*     match o with *)
+(*     | Utils.Gt -> (w, p, (t, r, r, Utils.Eq), m, a) *)
+(*     | _ -> (w, p, (t, l, l, Utils.Eq), m, a) *)
+(*   in *)
   match res with
   | Some t ->
       let newmeta, newtarget = build_newtarget true t in
@@ -558,6 +576,8 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
 ;;
 
 
+let sup_l_counter = ref 1;;
+
 let superposition_left (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -565,7 +585,7 @@ let superposition_left (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let proof, (eq_ty, left, right, ordering), _, _ = target in
+  let _, proof, (eq_ty, left, right, ordering), _, _ = target in
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
     betaexpand_term metasenv context ugraph table 0 term
@@ -573,20 +593,30 @@ let superposition_left (metasenv, context, ugraph) table target =
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' = (* M. *)apply_subst s (S.subst other bo) in
-      let bo'' =
-        C.Appl (
-          [C.MutInd (HL.Logic.eq_URI, 0, []);
-           S.lift 1 eq_ty] @
-            if ordering = U.Gt then [bo'; S.lift 1 right]
-            else [S.lift 1 left; bo'])
+      let t' =
+        let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
+        incr sup_l_counter;
+        let l, r = if ordering = U.Gt then bo', right else left, bo' in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ( *)
+(*           [C.MutInd (HL.Logic.eq_URI, 0, []); *)
+(*            S.lift 1 eq_ty] @ *)
+(*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
+(*             else [S.lift 1 left; S.lift 1 bo']) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
+(*         incr sup_l_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo',
-      C.Implicit None
+      Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                  proof; other; proof']) *)
@@ -597,8 +627,12 @@ let superposition_left (metasenv, context, ugraph) table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
-    (newproof, (eq_ty, left, right, neworder), [], [])
+
+    let res =
+      let w = Utils.compute_equality_weight eq_ty left right in
+      (w, newproof, (eq_ty, left, right, neworder), [], [])
+    in
+    res
   in
 (*   let build_new = *)
 (*     let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
@@ -608,6 +642,8 @@ let superposition_left (metasenv, context, ugraph) table target =
 ;;
 
 
+let sup_r_counter = ref 1;;
+
 let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -615,7 +651,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
+  let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
   let metasenv' = metasenv @ newmetas in
   let maxmeta = ref newmeta in
   let res1, res2 =
@@ -637,19 +673,29 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 
     let time1 = Unix.gettimeofday () in
     
-    let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
+    let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' = (* M. *)apply_subst s (S.subst other bo) in
-      let bo'' =
-        C.Appl (
-          [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
-            if ordering = U.Gt then [bo'; S.lift 1 right]
-            else [S.lift 1 left; bo'])
+      let t' =
+        let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+        incr sup_r_counter;
+        let l, r = if ordering = U.Gt then bo', right else left, bo' in
+        (name, ty, eq_ty, l, r)
       in
-      let t' = C.Lambda (C.Anonymous, ty, bo'') in
+(*       let bo'' = *)
+(*         C.Appl ( *)
+(*           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ *)
+(*             if ordering = U.Gt then [S.lift 1 bo'; S.lift 1 right] *)
+(*             else [S.lift 1 left; S.lift 1 bo']) *)
+(*       in *)
+(*       let t' = *)
+(*         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in *)
+(*         incr sup_r_counter; *)
+(*         C.Lambda (name, ty, bo'') *)
+(*       in *)
       bo',
-      C.Implicit None
+      Inference.ProofBlock (s, eq_URI, t', eq_found, target)
 (*       (\* M. *\)apply_subst s *)
 (*         (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
 (*                  eqproof; other; proof']) *)
@@ -661,7 +707,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let neworder = !Utils.compare_terms left right 
       and newmenv = newmetas @ menv'
       and newargs = args @ args' in
-      let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs)
+      let eq' =
+        let w = Utils.compute_equality_weight eq_ty left right in
+        (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
       and env = (metasenv, context, ugraph) in
       let newm, eq' = Inference.fix_metas !maxmeta eq' in
       newm, eq'
@@ -670,7 +718,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
 
     let time2 = Unix.gettimeofday () in
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-    
+
     newequality
   in
 
@@ -682,7 +730,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
   let ok = function
-    | _, (_, left, right, _), _, _ ->
+    | _, _, (_, left, right, _), _, _ ->
         not (fst (CR.are_convertible context left right ugraph))
   in
   (!maxmeta,