]> matita.cs.unibo.it Git - helm.git/commitdiff
- removed Positive and Negative (all is positive)
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 11 Jul 2006 08:19:16 +0000 (08:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 11 Jul 2006 08:19:16 +0000 (08:19 +0000)
- eq_f and eq_f1 used in proofs

helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/inference.ml
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/utils.ml
helm/software/components/tactics/paramodulation/utils.mli

index 91ed61cd5ea9426b7e111029a1e68cf84625f784..4414d2f435f3af14a1d8cc1d32c131bd0b241db7 100644 (file)
@@ -237,8 +237,35 @@ let is_not_fixed t =
    CicSubstitution.subst (Cic.Rel 1) t
 ;;
 
+let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
+let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
+let count_args t = List.length (tail_of_apply t);;
+let rec build_nat = 
+  let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+  function
+    | 0 -> Cic.MutConstruct(u,0,1,[])
+    | n -> 
+        Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
+;;
+let tyof context menv t =
+  try
+    fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
+  with
+  | CicTypeChecker.TypeCheckerFailure _
+  | CicTypeChecker.AssertFailure _ -> assert false
+;;
+let rec lambdaof left context = function
+  | Cic.Prod (n,s,t) ->
+      Cic.Lambda (n,s,lambdaof left context t)
+  | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r] 
+      when LibraryObjects.is_eq_URI uri -> if left then l else r
+  | t -> 
+      let names = Utils.names_of_context context in
+      prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
+      assert false
+;;
 
-let canonical t = 
+let canonical t context menv 
   let rec remove_refl t =
     match t with
     | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
@@ -255,21 +282,54 @@ let canonical t =
         Cic.LetIn (name,remove_refl bo,remove_refl rest)
     | _ -> t
   in
-  let rec canonical t =
+  let rec canonical context t =
     match t with
-      | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+      | Cic.LetIn(name,bo,rest) -> 
+          let context' = (Some (name,Cic.Def (bo,None)))::context in
+          Cic.LetIn(name,canonical context bo,canonical context' rest)
       | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
           when LibraryObjects.is_sym_eq_URI uri_sym ->
           (match p_of_sym ens tl with
              | Cic.Appl ((Cic.Const(uri,ens))::tl)
                  when LibraryObjects.is_sym_eq_URI uri -> 
-                   canonical (p_of_sym ens tl)
+                   canonical context (p_of_sym ens tl)
              | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
                  when LibraryObjects.is_trans_eq_URI uri_trans ->
                  let ty,l,m,r,p1,p2 = open_trans ens tl in
                    mk_trans uri_trans ty r m l 
-                     (canonical (mk_sym uri_sym ty m r p2)) 
-                     (canonical (mk_sym uri_sym ty l m p1))
+                     (canonical context (mk_sym uri_sym ty m r p2)) 
+                     (canonical context (mk_sym uri_sym ty l m p1))
+             | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) ->
+                 
+                 let eq_f_sym = 
+                   Cic.Const (UriManager.uri_of_string
+                     "cic:/matita/logic/equality/eq_f1.con",[]) 
+                 in
+                 Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))  
+
+(*
+                 let sym_eq = Cic.Const(uri_sym,ens) in
+                 let eq_f = Cic.Const(uri_feq,[]) in
+                 let b = Cic.MutConstruct (UriManager.uri_of_string
+                   "cic:/matita/datatypes/bool/bool.ind",0,1,[])
+                 in
+                 let u = ty1 in
+                 let ctx = f in
+                 let n = build_nat (count_args p) in
+                 let h = head_of_apply p in
+                 let predl = lambdaof true context (tyof context menv h) in 
+                 let predr = lambdaof false context (tyof context menv h) in
+                 let args = tail_of_apply p in
+                 let appl = 
+                   Cic.Appl
+                    ([Cic.Const(UriManager.uri_of_string
+                      "cic:/matita/paramodulation/rewrite.con",[]);
+                      eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
+                      args)
+                 in
+                 appl
+*)
+(*
              | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
                  when LibraryObjects.is_eq_ind_URI uri_ind || 
                       LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -293,13 +353,14 @@ let canonical t =
                  Cic.Appl 
                    [he;ty;what;pred;
                     canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+*)
              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
                  when LibraryObjects.is_eq_URI uri -> t
-             | _ -> Cic.Appl (List.map canonical args))
-      | Cic.Appl l -> Cic.Appl (List.map canonical l)
+             | _ -> Cic.Appl (List.map (canonical context) args))
+      | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
       | _ -> t
   in
-  remove_refl (canonical t)
+  remove_refl (canonical context t)
 ;;
   
 let ty_of_lambda = function
@@ -331,6 +392,10 @@ let open_eq = function
   | _ -> assert false
 ;;
 
+let mk_feq uri_feq ty ty1 left pred right t = 
+  Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+;;
+
 let contextualize uri ty left right t = 
   let hole = Cic.Implicit (Some `Hole) in
   (* aux [uri] [ty] [left] [right] [ctx] [t] 
@@ -404,23 +469,27 @@ let contextualize uri ty left right t =
           mk_trans uri_trans ctx_ty a b c paeqb pbeqc
     | t when ctx_d = hole -> t 
     | t -> 
-        let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
-        let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+(*         let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *)
+(*         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *)
+        let uri_feq = 
+          UriManager.uri_of_string "cic:/matita/logic/equality/eq_f.con"
+        in
         let pred = 
-          (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
-          let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+(*           let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *)
           let l = 
             let ctx_d = CicSubstitution.lift 1 ctx_d in
             put_in_ctx ctx_d (Cic.Rel 1)
           in
-          let lty = CicSubstitution.lift 1 ctx_ty in 
-          Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
+(*           let lty = CicSubstitution.lift 1 ctx_ty in  *)
+(*           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) *)
+          Cic.Lambda (Cic.Name "foo",ty,l)
         in
-        let d_left = put_in_ctx ctx_d left in
-        let d_right = put_in_ctx ctx_d right in
-        let refl_eq = mk_refl uri ctx_ty d_left in
-        mk_sym uri_sym ctx_ty d_right d_left
-          (mk_eq_ind uri_ind ty left pred refl_eq right t)
+(*         let d_left = put_in_ctx ctx_d left in *)
+(*         let d_right = put_in_ctx ctx_d right in *)
+(*         let refl_eq = mk_refl uri ctx_ty d_left in *)
+(*         mk_sym uri_sym ctx_ty d_right d_left *)
+(*           (mk_eq_ind uri_ind ty left pred refl_eq right t) *)
+          (mk_feq uri_feq ty ctx_ty left pred right t)
   in
   aux uri ty left right hole ty t
 ;;
@@ -681,7 +750,7 @@ let build_proof_term eq h lift proof =
    aux proof
 ;;
 
-let build_goal_proof eq l initial ty se =
+let build_goal_proof eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo l initial in
   let letsno = List.length lets in
@@ -736,7 +805,9 @@ let build_goal_proof eq l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   canonical 
+     (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
+     context menv,
    se 
 ;;
 
index d4a94cdb5a046429d96bc0bfb9975234cfe43a2f..1a62ee2ff0e2a7e159e059ca2db41cafe7a95e7b 100644 (file)
@@ -67,6 +67,7 @@ val string_of_proof :
  *  [ty] is the type of the goal *)
 val build_goal_proof: 
   UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
+    Cic.context -> Cic.metasenv -> 
     Cic.term * Cic.term list
 val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
 val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term 
index 7b545dd47c5b72a1cec282bc92f40c25b57c60b7..a4bdef1a2a48b0121246ead95c73f21edb56183a 100644 (file)
@@ -534,7 +534,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -582,90 +582,10 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
-      if sign = Utils.Positive then
           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
           (Cic.Lambda (name, ty, bo'))))))
-      else
-        assert false
-(*
-        begin
-        prerr_endline "***************************************negative";
-        let metaproof = 
-          incr maxmeta;
-          let irl =
-            CicMkImplicit.identity_relocation_list_for_metavariable context in
-(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(*        print_newline (); *)
-          C.Meta (!maxmeta, irl)
-        in
-          let eq_found =
-            let proof'_old' =
-              let termlist =
-                if pos = Utils.Left then [ty; what; other]
-                else [ty; other; what]
-              in
-              Equality.ProofSymBlock (termlist, proof'_old)
-            in
-            let proof'_new' = assert false (* not implemented *) in
-            let what, other =
-              if pos = Utils.Left then what, other else other, what
-            in
-            pos, 
-              Equality.mk_equality 
-                (0, (proof'_new',proof'_old'), 
-                (ty, other, what, Utils.Incomparable),menv')
-          in
-          let target_proof =
-            let pb =
-              Equality.ProofBlock 
-                (subst, eq_URI, (name, ty), bo',
-                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
-            in
-            assert false, (* not implemented *)
-            (match snd proof with
-            | Equality.BasicProof _ ->
-                (* print_endline "replacing a BasicProof"; *)
-                pb
-            | Equality.ProofGoalBlock (_, parent_proof) ->
-  (* print_endline "replacing another ProofGoalBlock"; *)
-                Equality.ProofGoalBlock (pb, parent_proof)
-            | _ -> assert false)
-          in
-        let refl =
-          C.Appl [C.MutConstruct (* reflexivity *)
-                    (LibraryObjects.eq_URI (), 0, 1, []);
-                  eq_ty; if is_left then right else left]          
-        in
-        (bo,
-         (assert false, (* not implemented *)
-         Equality.ProofGoalBlock 
-           (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
-      end
-*)
     in
-    let newmenv = (* Inference.filter subst *) menv in
-(*
-    let _ = 
-      if Utils.debug_metas then 
-        try ignore(CicTypeChecker.type_of_aux'
-          newmenv context 
-            (Equality.build_proof_term newproof) ugraph);
-          () 
-        with exc ->                   
-          prerr_endline "sempre lui";
-          prerr_endline (Subst.ppsubst subst);
-          prerr_endline (CicPp.ppterm 
-            (Equality.build_proof_term newproof));
-          prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
-          prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
-          prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
-          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
-            newmenv));
-          raise exc;
-      else () 
-    in
-*)
+    let newmenv = menv in
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
     let stat = (eq_ty, left, right, ordering) in
@@ -689,7 +609,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from eq_uri newmeta env table sign newtarget
+            demodulation_equality ?from eq_uri newmeta env table newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -700,7 +620,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from eq_uri newmeta env table sign newtarget
+                   demodulation_equality ?from eq_uri newmeta env table newtarget
           | None ->
               newmeta, target
   in
index 75e16ec1b38e254ce637c6dbc34f25e689cc9dd8..836a267dea78fa0f57cb0d8eb883d5f9e0c96f29 100644 (file)
@@ -70,7 +70,7 @@ val demodulation_equality :
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Utils.equality_sign -> Equality.equality -> int * Equality.equality
+  Equality.equality -> int * Equality.equality
 val demodulation_goal :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
index a27116bc9f007e232f1d1f9856140fea683f6b86..8f031a4a7728d2fb44acf33c919fec90fc6b4f78 100644 (file)
@@ -243,7 +243,8 @@ let find_equalities context proof =
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
-                    let w = compute_equality_weight stat in
+(*                     let w = compute_equality_weight stat in *)
+                    let w = 0 in
                     let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
index 4fe509981954ec67c774242fcc20a07e4dfd4ec7..d4ccf8f42bbcc71f172f6b69085c273437541f36 100644 (file)
@@ -119,23 +119,32 @@ module EqualitySet = Set.Make(OrderedEquality);;
 
 exception Empty_list;;
 
-let passive_is_empty = function
-  | ([], _), _ -> true
-  | _ -> false
+type passives = Equality.equality list * EqualitySet.t;;
+type actives = Equality.equality list * Indexing.Index.t;;
+
+(* initializes the passive set of equalities 
+ * XXX I think EqualitySet.elements should be ok (to eliminate duplicates)
+ *)
+let make_passive pos =
+  let set =
+    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty pos
+  in
+  (*EqualitySet.elements*) pos, set
 ;;
 
-let no_more_passive_goals = function
-  | _,[] -> true
+let make_active () = [], Indexing.empty ;;
+let size_of_passive (passive_list, _) = List.length passive_list;;
+let size_of_active (active_list, _) = List.length active_list;;
+let passive_is_empty = function
+  | [], s when EqualitySet.is_empty s -> true
+  | [], s -> assert false (* the set and the list should be in sync *)
   | _ -> false
 ;;
-  
-let size_of_passive ((passive_list, ps), _) = List.length passive_list
-(* EqualitySet.cardinal ps *)
-;;
 
+type goals = Equality.goal list * Equality.goal list
 
-let size_of_active (active_list, _) = List.length active_list
-;;
+let no_more_passive_goals g = match g with | _,[] -> true | _ -> false;;
+  
 
 let age_factor = 0.01;;
 
@@ -149,29 +158,27 @@ let rec select env (goals,_) passive =
   let goal =
     match (List.rev goals) with goal::_ -> goal | _ -> assert false
   in
-  let (pos_list, pos_set), passive_table = passive in
+  let pos_list, pos_set = passive in
   let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
   if !weight_age_ratio > 0 then
     weight_age_counter := !weight_age_counter - 1;
   match !weight_age_counter with
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
-      let rec skip_giant pos_list pos_set passive_table =
+      let rec skip_giant pos_list pos_set =
         match pos_list with
           | (hd:EqualitySet.elt)::tl ->
               let w,_,_,_,_ = Equality.open_equality hd in
-              let passive_table =
-                Indexing.remove_index passive_table hd
-              in 
               let pos_set = EqualitySet.remove hd pos_set in
                 if w < 500 then
-                  hd, ((tl, pos_set), passive_table)
+                  hd, (tl, pos_set)
                 else
-                  (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n");
-                  skip_giant tl pos_set passive_table)
+                  (prerr_endline 
+                    ("+++ skipping giant of size "^string_of_int w^" +++");
+                  skip_giant tl pos_set)
           | _ -> assert false
       in
-        skip_giant pos_list pos_set passive_table)
+        skip_giant pos_list pos_set)
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
@@ -207,82 +214,47 @@ let rec select env (goals,_) passive =
         (others + (abs (common - card))), e1
       in
       let _, current = EqualitySet.fold f pos_set initial in
-      let passive_table =
-        Indexing.remove_index passive_table current
-      in
         current,
-      ((remove current pos_list, EqualitySet.remove current pos_set),
-       passive_table))
+      (remove current pos_list, EqualitySet.remove current pos_set))
   | _ ->
       symbols_counter := !symbols_ratio;
       let my_min e1 e2 =
         let w1,_,_,_,_ = Equality.open_equality e1 in
-       let w2,_,_,_,_ = Equality.open_equality e2 in
-       if w1 < w2 then e1 else e2
+        let w2,_,_,_,_ = Equality.open_equality e2 in
+        if w1 < w2 then e1 else e2
       in
       let rec my_min_elt min = function
         | [] -> min
-       | hd::tl -> my_min_elt (my_min hd min) tl
+        | hd::tl -> my_min_elt (my_min hd min) tl
       in
-(*        let current = EqualitySet.min_elt pos_set in  *)
+(*     let current = EqualitySet.min_elt pos_set in  *)
        let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in 
-      let passive_table =
-        Indexing.remove_index passive_table current
-      in
-        current, 
-      ((remove current pos_list, EqualitySet.remove current pos_set),
-      passive_table)
+       current,(remove current pos_list, EqualitySet.remove current pos_set)
 ;;
 
+
 let filter_dependent passive id =
-  prerr_endline ("+++++++++++++++passives "^
-                   ( string_of_int (size_of_passive passive)));
-  let (pos_list, pos_set), passive_table = passive in
-  let passive =
+  let pos_list, pos_set = passive in
+  let passive,no_pruned =
     List.fold_right
-      (fun eq ((list,set),table) ->
+      (fun eq ((list,set),no) ->
          if Equality.depend eq id then
-           (let _,_,_,_,id_eq = Equality.open_equality eq in
-              if id_eq = 9228 then 
-                prerr_endline ("\n\n--------filtering "^(string_of_int id_eq));
-           ((list, 
-             EqualitySet.remove eq set),
-            Indexing.remove_index table eq))
+           (list, EqualitySet.remove eq set), no + 1
          else 
-              ((eq::list, set),table))
-      pos_list (([],pos_set),passive_table) in
-  prerr_endline ("+++++++++++++++passives "^
-                   ( string_of_int (size_of_passive passive)));  
-  passive
-;;
-
-
-(* initializes the passive set of equalities *)
-let make_passive pos =
-  let set_of equalities =
-    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
-  in
-  let table =
-      List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
+           (eq::list, set), no)
+      pos_list (([],pos_set),0)
   in
-  (pos, set_of pos),
-  table
-;;
-
-
-let make_active () =
-  [], Indexing.empty
+  if no_pruned > 0 then
+    prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++");  
+  passive
 ;;
 
 
 (* adds to passive a list of equalities new_pos *)
 let add_to_passive passive new_pos preferred =
-  let (pos_list, pos_set), table = passive in
+  let pos_list, pos_set = passive in
   let ok set equality = not (EqualitySet.mem equality set) in
   let pos = List.filter (ok pos_set) new_pos in
-  let table = 
-     List.fold_left (fun tbl e -> Indexing.index tbl e) table pos 
-  in
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
   in
@@ -291,8 +263,8 @@ let add_to_passive passive new_pos preferred =
       (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)  
       pos 
   in
-  (pos_head @ pos_list @ pos_tail, add pos_set pos),
-  table
+  assert(pos_head = []);
+  pos_head @ pos_list @ pos_tail, add pos_set pos
 ;;
 
 (* TODO *)
@@ -446,26 +418,15 @@ let check_for_deep_subsumption env active_table eq =
   fst (aux false (true,false) left right)
 ;;
 
-(* buttare via sign *)
-
 (** simplifies current using active and passive *)
-let forward_simplify 
-  eq_uri env (sign,current) ?passive (active_list, active_table) 
-=
+let forward_simplify eq_uri env current (active_list, active_table) =
   let _, context, _ = env in
-  let passive_table =
-    match passive with
-    | None -> None
-    | Some ((_, _), pt) -> Some pt
-  in
   let demodulate table current = 
     let newmeta, newcurrent =
-      Indexing.demodulation_equality eq_uri !maxmeta env table sign current in
+      Indexing.demodulation_equality eq_uri !maxmeta env table current
+    in
     maxmeta := newmeta;
-    if Equality.is_identity env newcurrent then
-      None
-    else
-      Some newcurrent
+    if Equality.is_identity env newcurrent then None else Some newcurrent
   in
   let rec demod current =
     if Utils.debug_metas then
@@ -474,59 +435,22 @@ let forward_simplify
       if Utils.debug_metas then
         ignore ((function None -> () | Some x -> 
                    ignore (Indexing.check_target context x "demod1");()) res);
-    match res with
-    | None -> None
-    | Some newcurrent ->
-        match passive_table with
-        | None -> res
-        | Some passive_table -> 
-            match demodulate passive_table newcurrent with
-              | None -> None
-              | Some newnewcurrent -> 
-                  if Equality.compare newcurrent newnewcurrent <> 0 then 
-                    demod newnewcurrent
-                  else Some newnewcurrent
+    res
   in 
   let res = demod current in
   match res with
   | None -> None
   | Some c ->
-      if Indexing.in_index active_table c then
+      if Indexing.in_index active_table c ||
+         check_for_deep_subsumption env active_table c 
+      then
         None
-      else
-        match passive_table with
-        | None -> 
-            if check_for_deep_subsumption env active_table c then
-              None
-            else 
-              res
-(*
-            if Indexing.subsumption env active_table c = None then
-              res
-            else
-              None
-*)
-        | Some passive_table ->
-            if Indexing.in_index passive_table c then None
-            else 
-              if check_for_deep_subsumption env active_table c then
-                None
-              else 
-(*              if Indexing.subsumption env active_table c = None then*)
-                (match Indexing.subsumption env passive_table c with
-                | None -> res
-                | Some (_,c',_) -> 
-                    None
-                    (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
-                    Some c'*))
-(*
-              else
-                None
-*)
+      else 
+        res
 ;;
 
 (** simplifies new using active and passive *)
-let forward_simplify_new eq_uri env new_pos ?passive active =
+let forward_simplify_new eq_uri env new_pos active =
   if Utils.debug_metas then
     begin
       let m,c,u = env in
@@ -535,22 +459,15 @@ let forward_simplify_new eq_uri env new_pos ?passive active =
       new_pos;)
     end;
   let active_list, active_table = active in
-  let passive_table =
-    match passive with
-    | None -> None
-    | Some ((_, _), pt) -> Some pt
-  in
-  let demodulate sign table target =
+  let demodulate table target =
     let newmeta, newtarget =
-      Indexing.demodulation_equality eq_uri !maxmeta env table sign target 
+      Indexing.demodulation_equality eq_uri !maxmeta env table target 
     in
     maxmeta := newmeta;
     newtarget
   in
   (* we could also demodulate using passive. Currently we don't *)
-  let new_pos =
-    List.map (demodulate Utils.Positive active_table) new_pos 
-  in
+  let new_pos = List.map (demodulate active_table) new_pos in
   let new_pos_set =
     List.fold_left
       (fun s e ->
@@ -561,63 +478,28 @@ let forward_simplify_new eq_uri env new_pos ?passive active =
   in
   let new_pos = EqualitySet.elements new_pos_set in
 
-  let subs =
-    match passive_table with
-    | None ->
-        (fun e -> (Indexing.subsumption env active_table e = None))
-    | Some passive_table ->
-        (fun e -> ((Indexing.subsumption env active_table e = None) &&
-                         (Indexing.subsumption env passive_table e = None)))
-  in
-  let is_duplicate =
-    match passive_table with
-    | None ->
-        (fun e -> not (Indexing.in_index active_table e))
-    | Some passive_table ->
-        (fun e ->
-           not ((Indexing.in_index active_table e) ||
-                  (Indexing.in_index passive_table e)))
-  in
-    List.filter subs (List.filter is_duplicate new_pos)
+  let subs e = Indexing.subsumption env active_table e = None in
+  let is_duplicate e = not (Indexing.in_index active_table e) in
+  List.filter subs (List.filter is_duplicate new_pos)
 ;;
 
 
 (** simplifies a goal with equalities in active and passive *)  
-let rec simplify_goal env goal ?passive (active_list, active_table) =
-  let passive_table =
-    match passive with
-    | None -> None
-    | Some ((_, _), pt) -> Some pt
-  in
+let rec simplify_goal env goal (active_list, active_table) =
   let demodulate table goal = Indexing.demodulation_goal env table goal in
-  let changed, goal =
-    match passive_table with
-    | None -> demodulate active_table goal
-    | Some passive_table ->
-        let changed, goal = demodulate active_table goal in
-(*        let changed', goal = demodulate passive_table goal in*)
-        (changed (*|| changed'*)), goal
-  in
+  let changed, goal = demodulate active_table goal in
   changed,
   if not changed then 
     goal 
   else 
-    snd (simplify_goal env goal ?passive (active_list, active_table)) 
+    snd (simplify_goal env goal (active_list, active_table)) 
 ;;
 
 
-let simplify_goals env goals ?passive active =
+let simplify_goals env goals active =
   let a_goals, p_goals = goals in
-  let p_goals = 
-    List.map
-      (fun g -> snd (simplify_goal env g ?passive active))
-      p_goals
-  in
-  let a_goals = 
-    List.map
-      (fun g -> snd (simplify_goal env g ?passive active))
-      a_goals
-  in
+  let p_goals = List.map (fun g -> snd (simplify_goal env g active)) p_goals in
+  let a_goals = List.map (fun g -> snd (simplify_goal env g active)) a_goals in
   a_goals, p_goals
 ;;
 
@@ -633,8 +515,7 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
            equality::res, newn,pruned
          else
            match 
-             forward_simplify 
-               eq_uri env (Utils.Positive, equality) (new_pos, new_table) 
+             forward_simplify eq_uri env equality (new_pos, new_table) 
            with
            | None -> res, newn, id::pruned
            | Some e ->
@@ -676,13 +557,13 @@ let backward_simplify_active eq_uri env new_pos new_table min_weight active =
 (** simplifies passive using new *)
 let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
   let (pl, ps), passive_table = passive in
-  let f sign equality (resl, ress, newn) =
+  let f equality (resl, ress, newn) =
     let ew, _, _, _ , _ = Equality.open_equality equality in
     if ew < min_weight then
       equality::resl, ress, newn
     else
       match 
-        forward_simplify eq_uri env (sign, equality) (new_pos, new_table) 
+        forward_simplify eq_uri env equality (new_pos, new_table) 
       with
       | None -> resl, EqualitySet.remove equality ress, newn
       | Some e ->
@@ -692,7 +573,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
             let ress = EqualitySet.remove equality ress in
               resl, ress, e::newn
   in
-  let pl, ps, newp = List.fold_right (f Utils.Positive) pl ([], ps, []) in
+  let pl, ps, newp = List.fold_right f pl ([], ps, []) in
   let passive_table =
     List.fold_left
       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
@@ -711,28 +592,12 @@ let build_table equations =
 ;;
   
 
-let backward_simplify eq_uri env new' ?passive active =
+let backward_simplify eq_uri env new' active =
   let new_pos, new_table, min_weight = build_table new' in
-(*
-    List.fold_left
-      (fun (l, t, w) e ->
-         let ew, _, _, _ , _ = Equality.open_equality e in
-         e::l, Indexing.index t e, min ew w)
-      ([], Indexing.empty, 1000000) new'
-  in
-*)
   let active, newa, pruned =
     backward_simplify_active eq_uri env new_pos new_table min_weight active 
   in
-  match passive with
-  | None ->
-      active, (make_passive []), newa, None, pruned
-  | Some passive ->
-     active, passive, newa, None, pruned
-(* prova
-      let passive, newp =
-        backward_simplify_passive env new_pos new_table min_weight passive in
-      active, passive, newa, newp *)
+  active, newa, None, pruned
 ;;
 
 let close eq_uri env new' given =
@@ -824,10 +689,7 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
     | None -> [], None
-    | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Utils.Negative, e)) pn
-        and pp = List.map (fun e -> (Utils.Positive, e)) pp in
-        pn @ pp, Some pt
+    | Some ((pn, _), (pp, _), pt) -> pn @ pp, Some pt
   in
   let a_theorems, p_theorems = theorems in
   let demodulate table theorem =
@@ -861,7 +723,7 @@ let rec simpl eq_uri env e others others_simpl =
       (fun t e -> Indexing.index t e)
       Indexing.empty active
   in
-  let res = forward_simplify eq_uri env (Utils.Positive,e) (active, tbl) in
+  let res = forward_simplify eq_uri env e (active, tbl) in
     match others with
       | hd::tl -> (
           match res with
@@ -976,14 +838,14 @@ let rec check goal = function
       | (Some p) as ok  -> ok
 ;;
   
-let simplify_goal_set env goals ?passive active = 
+let simplify_goal_set env goals active = 
   let active_goals, passive_goals = goals in 
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
   in
     List.fold_left
       (fun (acc_a,acc_p) goal -> 
-        match simplify_goal env goal ?passive active with 
+        match simplify_goal env goal active with 
         | changed, g -> 
             if changed then 
               if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
@@ -1037,33 +899,6 @@ let infer_goal_set env active goals =
   aux passive_goals
 ;;
 
-(* old
-let infer_goal_set env active goals = 
-  let active_goals, passive_goals = goals in
-  let rec aux = function
-    | [] -> goals
-    | ((_,_,t1) as hd)::tl when 
-        not (List.exists 
-              (fun (_,_,t) -> 
-                 Equality.meta_convertibility t t1) 
-              active_goals)
-       -> 
-        let selected = hd in
-        let passive_goals = tl in
-        let new_passive_goals =
-          if CicUtil.is_meta_closed t1 then 
-           passive_goals
-          else 
-            let new' = Indexing.superposition_left env (snd active) selected in
-            passive_goals @ new'
-        in
-        selected::active_goals, new_passive_goals
-    | _::tl -> aux tl
-  in 
-  aux passive_goals
-;;
-*)
-
 let infer_goal_set_with_current env current goals active = 
   let active_goals, passive_goals = 
     simplify_goal_set env goals active
@@ -1123,6 +958,7 @@ let given_clause
     int_of_float iterations_left 
   in
   let rec step goals theorems passive active iterno =
+    pp_goals "xxx" goals context;
     if iterno > max_iterations then
       (ParamodulationFailure "No more iterations to spend")
     else if Unix.gettimeofday () > max_time then
@@ -1174,7 +1010,7 @@ let given_clause
               if iterno mod 40 = 0 then
                 begin
                   let active = List.map Equality.id_of (fst active) in
-                  let passive = List.map Equality.id_of (fst (fst passive)) in
+                  let passive = List.map Equality.id_of (fst passive) in
                   let goal = ids_of_goal_set goals in
                   Equality.collect active passive goal
                 end;
@@ -1184,7 +1020,7 @@ let given_clause
                     ("Selected : " ^ 
                       Equality.string_of_equality ~env  current);
               let res = 
-                forward_simplify eq_uri env (Utils.Positive, current) active 
+                forward_simplify eq_uri env current active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
@@ -1218,10 +1054,10 @@ let given_clause
                   prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive head =
                     let new' = 
-                      forward_simplify_new eq_uri env new' ~passive active 
+                      forward_simplify_new eq_uri env new' active 
                     in
-                    let active, passive, newa, retained, pruned =
-                      backward_simplify eq_uri env new' ~passive  active 
+                    let active, newa, retained, pruned =
+                      backward_simplify eq_uri env new' active 
                     in
                     let passive = 
                       List.fold_left filter_dependent passive pruned 
@@ -1240,7 +1076,7 @@ let given_clause
                   let goals = 
                     let a,b,_ = build_table new' in
                     let _ = <:start<simplify_goal_set new>> in
-                    let rc = simplify_goal_set env goals ~passive (a,b) in
+                    let rc = simplify_goal_set env goals (a,b) in
                     let _ = <:stop<simplify_goal_set new>> in
                     rc
                   in
@@ -1257,7 +1093,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
     (active, passive)
   else
     let current, passive = select env ([goal],[]) passive in
-    let res = forward_simplify eq_uri env (Utils.Positive, current) ~passive active in
+    let res = forward_simplify eq_uri env current active in
     match res with
     | None ->
         saturate_equations eq_uri env goal accept_fun passive active
@@ -1274,9 +1110,9 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         (* alla fine new' contiene anche le attive semplificate!
          * quindi le aggiungo alle passive insieme alle new *)
         let rec simplify new' active passive =
-          let new' = forward_simplify_new eq_uri env new' ~passive active in
-          let active, passive, newa, retained, pruned =
-            backward_simplify eq_uri env new' ~passive active in
+          let new' = forward_simplify_new eq_uri env new' active in
+          let active, newa, retained, pruned =
+            backward_simplify eq_uri env new' active in
           let passive = 
             List.fold_left filter_dependent passive pruned in
           match newa, retained with
@@ -1309,172 +1145,6 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         saturate_equations eq_uri env goal accept_fun passive active
 ;;
   
-let main dbd full term metasenv ugraph = ()
-(*
-let main dbd full term metasenv ugraph =
-  let module C = Cic in
-  let module T = CicTypeChecker in
-  let module PET = ProofEngineTypes in
-  let module PP = CicPp in
-  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
-  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
-  let proof, goals = status in
-  let goal' = List.nth goals 0 in
-  let _, metasenv, meta_proof, _ = proof in
-  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
-  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
-  let lib_eq_uris, library_equalities, maxm =
-
-    Inference.find_library_equalities dbd context (proof, goal') (maxm+2)
-  in
-  let library_equalities = List.map snd library_equalities in
-  maxmeta := maxm+2; (* TODO ugly!! *)
-  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-  let new_meta_goal, metasenv, type_of_goal =
-    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
-    Cic.Meta (maxm+1, irl),
-    (maxm+1, context, ty)::metasenv,
-    ty
-  in
-  let env = (metasenv, context, ugraph) in
-  let t1 = Unix.gettimeofday () in
-  let theorems =
-    if full then
-      let theorems = Inference.find_library_theorems dbd env (proof, goal') lib_eq_uris in
-      let context_hyp = Inference.find_context_hypotheses env eq_indexes in
-      context_hyp @ theorems, []
-    else
-      let refl_equal =
-        let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
-        UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
-      in
-      let t = CicUtil.term_of_uri refl_equal in
-      let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-      [(t, ty, [])], []
-  in
-  let t2 = Unix.gettimeofday () in
-  Utils.debug_print
-    (lazy
-       (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
-  let _ =
-    Utils.debug_print
-      (lazy
-         (Printf.sprintf
-            "Theorems:\n-------------------------------------\n%s\n"
-            (String.concat "\n"
-               (List.map
-                  (fun (t, ty, _) ->
-                     Printf.sprintf
-                       "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
-                  (fst theorems)))))
-  in
-  (*try*)
-    let goal = 
-      ([],Equality.BasicProof (Equality.empty_subst ,new_meta_goal)), [], goal 
-    in
-    let equalities = simplify_equalities env 
-      (equalities@library_equalities) in 
-    let active = make_active () in
-    let passive = make_passive equalities in
-    Printf.printf "\ncurrent goal: %s\n"
-      (let _, _, g = goal in CicPp.ppterm g);
-    Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
-    Printf.printf "\nequalities:\n%s\n"
-      (String.concat "\n"
-         (List.map
-            (Equality.string_of_equality ~env) equalities));
-(*             (equalities @ library_equalities))); *)
-      print_endline "--------------------------------------------------";
-      let start = Unix.gettimeofday () in
-      print_endline "GO!";
-      start_time := Unix.gettimeofday ();
-      let res =
-        let goals = make_goals goal in
-        (if !use_fullred then given_clause_fullred else given_clause_fullred)
-          dbd env goals theorems passive active
-      in
-      let finish = Unix.gettimeofday () in
-      let _ =
-        match res with
-        | ParamodulationFailure ->
-            Printf.printf "NO proof found! :-(\n\n"
-        | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) ->
-            Printf.printf "OK, found a proof!\n";
-            let oldproof = Equation.build_proof_term proof in
-            let newproof,_,newenv,_ = 
-                CicRefine.type_of_aux' 
-                  cicmenv context cicproof CicUniv.empty_ugraph
-            in
-            (* REMEMBER: we have to instantiate meta_proof, we should use
-               apply  the "apply" tactic to proof and status 
-            *)
-            let names = Utils.names_of_context context in
-            prerr_endline "OLD PROOF";
-            print_endline (PP.pp proof names);
-            prerr_endline "NEW PROOF";
-            print_endline (PP.pp newproof names);
-            let newmetasenv =
-              List.fold_left
-                (fun m eq -> 
-                  let (_, _, _, menv,_) = Equality.open_equality eq in 
-                  m @ menv) 
-              metasenv equalities
-            in
-            let _ =
-              (*try*)
-                let ty, ug =
-                  CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
-                in
-                print_endline (string_of_float (finish -. start));
-                Printf.printf
-                  "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
-                  (CicPp.pp type_of_goal names) (CicPp.pp ty names)
-                  (string_of_bool
-                     (fst (CicReduction.are_convertible
-                             context type_of_goal ty ug)));
-              (*with e ->
-                Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
-                Printf.printf "MAXMETA USED: %d\n" !maxmeta;
-                print_endline (string_of_float (finish -. start));*)
-            in
-            ()
-              
-        | ParamodulationSuccess None ->
-            Printf.printf "Success, but no proof?!?\n\n"
-      in
-        if Utils.time then
-          begin
-            prerr_endline 
-              ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
-                       "forward_simpl_new_time: %.9f\n" ^^
-                       "backward_simpl_time: %.9f\n")
-              !infer_time !forward_simpl_time !forward_simpl_new_time
-              !backward_simpl_time) ^
-              (Printf.sprintf "passive_maintainance_time: %.9f\n"
-                 !passive_maintainance_time) ^
-              (Printf.sprintf "    successful unification/matching time: %.9f\n"
-                 !Indexing.match_unif_time_ok) ^
-              (Printf.sprintf "    failed unification/matching time: %.9f\n"
-                 !Indexing.match_unif_time_no) ^
-              (Printf.sprintf "    indexing retrieval time: %.9f\n"
-                 !Indexing.indexing_retrieval_time) ^
-              (Printf.sprintf "    demodulate_term.build_newtarget_time: %.9f\n"
-                 !Indexing.build_newtarget_time) ^
-              (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
-                 !derived_clauses !kept_clauses)) 
-            end
-(*
-  with exc ->
-    print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
-    raise exc
-*)
-;;
-*)
-
 let default_depth = !maxdepth
 and default_width = !maxwidth;;
 
@@ -1608,6 +1278,7 @@ let saturate
         let initial = Equality.add_subst subsumption_subst newproof in
         Equality.build_goal_proof 
           eq_uri goalproof initial type_of_goal side_effects
+          context proof_menv
       in
       prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
@@ -1632,8 +1303,8 @@ let saturate
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) 
           (List.filter 
-          (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
-          proof_menv)
+           (fun (i,_,_) -> List.mem i metas_still_open_in_proof) 
+           proof_menv)
       in
       let replace where = 
         (* we need this fake equality since the metas of the hypothesis may be
@@ -1708,6 +1379,8 @@ prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
       proof, open_goals
 ;;
 
+let main _ _ _ _ _ = () ;;
+
 let retrieve_and_print dbd term metasenv ugraph = 
   let module C = Cic in
   let module T = CicTypeChecker in
@@ -1743,14 +1416,13 @@ let retrieve_and_print dbd term metasenv ugraph =
   Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
   let rec simpl e others others_simpl =
     let (u, e) = e in
-    let active = List.map (fun (u, e) -> (Utils.Positive, e))
-      (others @ others_simpl) in
+    let active = (others @ others_simpl) in
     let tbl =
       List.fold_left
         (fun t (_, e) -> Indexing.index t e)
         Indexing.empty active
     in
-    let res = forward_simplify eq_uri env (Utils.Positive, e) (active, tbl) in
+    let res = forward_simplify eq_uri env e (active, tbl) in
     match others with
         | hd::tl -> (
             match res with
@@ -1851,7 +1523,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 
     let passive =
       match rp with
-      | (p, _), _ ->
+      | p, _ ->
           EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
     in
     let active =
@@ -1904,7 +1576,8 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
     begin
       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
       let proofterm,_ = 
-        Equality.build_goal_proof eq_uri newproof opengoal ty [] 
+        Equality.build_goal_proof 
+          eq_uri newproof opengoal ty [] context metasenv
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
@@ -2016,8 +1689,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
         List.fold_left 
           (fun (maxm,acc) e -> 
             let maxm,eq = 
-              Indexing.demodulation_equality 
-                eq_uri maxm env table Utils.Positive e
+              Indexing.demodulation_equality eq_uri maxm env table e
             in
             maxm,eq::acc) 
           (maxm,[]) eql
index 8d0ba901b055d9dba4b20b5b02d8f2b3829f0c69..eabf24353395f443beea557563d0daa4a4a7273c 100644 (file)
@@ -754,14 +754,6 @@ let guarded_simpl ?(debug=false) context t =
       end
 ;;
 
-type equality_sign = Negative | Positive;;
-
-let string_of_sign = function
-  | Negative -> "Negative"
-  | Positive -> "Positive"
-;;
-
-
 type pos = Left | Right 
 
 let string_of_pos = function
index d761045b85a75c18eb27d36e66cff82c558f518e..2f25415ac5ba528ecca3537e160d293c2af716bd 100644 (file)
@@ -76,10 +76,6 @@ val compare_terms: (Cic.term -> Cic.term -> comparison) ref
 
 val guarded_simpl:  ?debug:bool -> Cic.context -> Cic.term -> Cic.term
 
-type equality_sign = Negative | Positive
-
-val string_of_sign: equality_sign -> string
-
 type pos = Left | Right 
 
 val string_of_pos: pos -> string