]> matita.cs.unibo.it Git - helm.git/commitdiff
- Removed old proofs
authorEnrico Tassi <enrico.tassi@inria.fr>
Sun, 14 May 2006 13:53:37 +0000 (13:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sun, 14 May 2006 13:53:37 +0000 (13:53 +0000)
- Equality.ml splittend in to subst.ml and equality.ml, the former only for substs
- patch to kill passive generated from an active that is dropped
- fixed deep subsumption

helm/software/components/tactics/.depend
helm/software/components/tactics/Makefile
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/inference.mli
helm/software/components/tactics/paramodulation/saturation.ml
helm/software/components/tactics/paramodulation/subst.ml [new file with mode: 0644]
helm/software/components/tactics/paramodulation/subst.mli [new file with mode: 0644]

index 41cc4bb6779322542701fec58bf8f6396a29d986..360128fce2e634088cef07c706ba628cc86cbfce 100644 (file)
@@ -5,7 +5,8 @@ reductionTactics.cmi: proofEngineTypes.cmi
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
 metadataQuery.cmi: proofEngineTypes.cmi 
-paramodulation/equality.cmi: paramodulation/utils.cmi 
+paramodulation/equality.cmi: paramodulation/utils.cmi \
+    paramodulation/subst.cmi 
 paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
     paramodulation/equality.cmi 
 paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
@@ -58,10 +59,14 @@ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
 paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
 paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
+paramodulation/subst.cmo: paramodulation/subst.cmi 
+paramodulation/subst.cmx: paramodulation/subst.cmi 
 paramodulation/equality.cmo: paramodulation/utils.cmi \
-    proofEngineReduction.cmi paramodulation/equality.cmi 
+    paramodulation/subst.cmi proofEngineReduction.cmi \
+    paramodulation/equality.cmi 
 paramodulation/equality.cmx: paramodulation/utils.cmx \
-    proofEngineReduction.cmx paramodulation/equality.cmi 
+    paramodulation/subst.cmx proofEngineReduction.cmx \
+    paramodulation/equality.cmi 
 paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \
     metadataQuery.cmi paramodulation/equality.cmi \
     paramodulation/inference.cmi 
index 2cecc04019710d2e02ea38b98dc2dd535dc25c89..1fe925282a52f79786cf8e3ed2e7ce6a58841168 100644 (file)
@@ -7,6 +7,7 @@ INTERFACE_FILES = \
        tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
        primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
   paramodulation/utils.mli \
+  paramodulation/subst.mli\
   paramodulation/equality.mli\
   paramodulation/inference.mli\
   paramodulation/equality_indexing.mli\
index 5248a6a924c84bf6f2b06c1d36c5f16bff12dd4a..b921f78c1984bfed44701c202e20deede6d77ecd 100644 (file)
 
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
-
-(******* CIC substitution ***************************************************)
-
-type cic_substitution = Cic.substitution
-let cic_apply_subst = CicMetaSubst.apply_subst
-let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
-let cic_ppsubst = CicMetaSubst.ppsubst
-let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
-let cic_flatten_subst subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-         let context = (* cic_apply_subst_context subst*) context in
-         let term = cic_apply_subst subst term in
-         let ty = cic_apply_subst subst ty in  
-         (i, (context, term, ty))) subst
-let rec cic_lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
-      in cic_lookup_subst t subst 
-      with Not_found -> meta
-    )
-  | _ -> meta
-;;
-
-let cic_merge_subst_if_possible s1 s2 =
-  let already_in = Hashtbl.create 13 in
-  let rec aux acc = function
-    | ((i,_,x) as s)::tl ->
-        (try 
-          let x' = Hashtbl.find already_in i in
-          if x = x' then aux acc tl else None
-        with
-        | Not_found -> 
-            Hashtbl.add already_in i x;
-            aux (s::acc) tl)
-    | [] -> Some acc 
-  in  
-    aux [] (s1@s2)
-;;
-
-(******** NAIF substitution **************************************************)
-(* 
- * naif version of apply subst; the local context of metas is ignored;
- * we assume the substituted term must be lifted according to the nesting
- * depth of the meta. 
- * Alternatively, we could used implicit instead of metas 
- *)
-
-type naif_substitution = (int * Cic.term) list 
-
-let naif_apply_subst subst term =
- let rec aux k t =
-   match t with
-       Cic.Rel _ -> t
-     | Cic.Var (uri,exp_named_subst) -> 
-         let exp_named_subst' =
-           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-         in
-           Cic.Var (uri, exp_named_subst')
-    | Cic.Meta (i, l) -> 
-        (try
-          aux k (CicSubstitution.lift k (List.assoc i subst)) 
-         with Not_found -> t)
-    | Cic.Sort _
-    | Cic.Implicit _ -> t
-    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
-    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
-    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
-    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
-    | Cic.Appl [] -> assert false
-    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
-    | Cic.Const (uri,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          if exp_named_subst' != exp_named_subst then
-            Cic.Const (uri, exp_named_subst')
-          else
-            t (* TODO: provare a mantenere il piu' possibile sharing *)
-    | Cic.MutInd (uri,typeno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          Cic.MutInd (uri,typeno,exp_named_subst')
-    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | Cic.MutCase (sp,i,outty,t,pl) ->
-        let pl' = List.map (aux k) pl in
-          Cic.MutCase (sp, i, aux k outty, aux k t, pl')
-    | Cic.Fix (i, fl) ->
-        let len = List.length fl in
-        let fl' =
-         List.map 
-           (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
-        in
-          Cic.Fix (i, fl')
-    | Cic.CoFix (i, fl) ->
-        let len = List.length fl in
-        let fl' =
-          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
-        in
-          Cic.CoFix (i, fl')
-in
-  aux 0 term
-;;
-
-(* naif version of apply_subst_metasenv: we do not apply the 
-substitution to the context *)
-
-let naif_apply_subst_metasenv subst metasenv =
-  List.map
-    (fun (n, context, ty) ->
-      (n, context, naif_apply_subst subst ty))
-    (List.filter
-      (fun (i, _, _) -> not (List.mem_assoc i subst))
-      metasenv)
-
-let naif_ppsubst names subst =
-  "{" ^ String.concat "; "
-    (List.map
-      (fun (idx, t) ->
-         Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
-    subst) ^ "}"
-;;
-
-let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
-
-let naif_flatten_subst subst = 
-  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
-;;
-
-let rec naif_lookup_subst meta subst =
-  match meta with
-    | Cic.Meta (i, _) ->
-        (try
-          naif_lookup_subst (List.assoc i subst) subst
-        with
-            Not_found -> meta)
-    | _ -> meta
-;;
-
-let naif_merge_subst_if_possible s1 s2 =
-  let already_in = Hashtbl.create 13 in
-  let rec aux acc = function
-    | ((i,x) as s)::tl ->
-        (try 
-          let x' = Hashtbl.find already_in i in
-          if x = x' then aux acc tl else None
-        with
-        | Not_found -> 
-            Hashtbl.add already_in i x;
-            aux (s::acc) tl)
-    | [] -> Some acc 
-  in  
-    aux [] (s1@s2)
-;;
-
-(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
-
-type substitution = naif_substitution
-let apply_subst = naif_apply_subst
-let apply_subst_metasenv = naif_apply_subst_metasenv
-let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
-let buildsubst = naif_buildsubst
-let flatten_subst = naif_flatten_subst
-let lookup_subst = naif_lookup_subst
-
-(* filter out from metasenv the variables in substs *)
-let filter subst metasenv =
-  List.filter
-    (fun (m, _, _) ->
-         try let _ = List.find (fun (i, _) -> m = i) subst in false
-         with Not_found -> true)
-    metasenv
-;;
-
-let is_in_subst i subst = List.mem_assoc i subst;;
-  
-let merge_subst_if_possible = naif_merge_subst_if_possible;;
-
-let empty_subst = [];;
-
-(********* EQUALITY **********************************************************)
-
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type uncomparable = int -> int 
 type equality =
@@ -225,21 +37,11 @@ type equality =
      Utils.comparison) * (* ordering *)  
     Cic.metasenv  *      (* environment for metas *)
     int                  (* id *)
-and proof = new_proof * old_proof 
-
-and new_proof = 
+and proof = 
   | Exact of Cic.term
-  | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)  
-and old_proof =
-  | NoProof (* term is the goal missing a proof *)
-  | BasicProof of substitution * Cic.term
-  | ProofBlock of
-      substitution * UriManager.uri *
-        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
-  | ProofGoalBlock of old_proof * old_proof 
-  | ProofSymBlock of Cic.term list * old_proof
-  | SubProof of Cic.term * int * old_proof
-and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+  | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) 
+            (* subst, (rule,eq1, eq2,predicate) *)  
+and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
 (* globals *)
@@ -257,16 +59,16 @@ let reset () =
 
 let uncomparable = fun _ -> 0
 
-let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
-  let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+  let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
   eq
 ;;
 
 let mk_tmp_equality (weight,(ty,l,r,o),m) =
   let id = -1 in
-  uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+  uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
 ;;
 
 
@@ -294,34 +96,15 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
-let rec string_of_proof_old ?(names=[]) = function
-  | NoProof -> "NoProof " 
-  | BasicProof (s, t) -> "BasicProof(" ^ 
-      ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
-  | SubProof (t, i, p) ->
-      Printf.sprintf "SubProof(%s, %s, %s)"
-        (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
-  | ProofSymBlock (_,p) -> 
-      Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
-  | ProofBlock (subst, _, _, _ ,(_,eq),old) -> 
-      let _,(_,p),_,_,_ = open_equality eq in 
-      "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
-      string_of_proof_old p ^ ")"
-  | ProofGoalBlock (p1, p2) ->
-      Printf.sprintf "ProofGoalBlock(%s, %s)"
-        (string_of_proof_old p1) (string_of_proof_old p2)
-;;
-
-
 let proof_of_id id =
   try
-    let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
       p,l,r
   with
       Not_found -> assert false
 
 
-let string_of_proof_new ?(names=[]) p gp = 
+let string_of_proof ?(names=[]) p gp = 
   let str_of_rule = function
     | SuperpositionRight -> "SupR"
     | SuperpositionLeft -> "SupL"
@@ -339,7 +122,7 @@ let string_of_proof_new ?(names=[]) p gp =
           prefix (CicPp.pp t names)
     | Step (subst,(rule,eq1,(pos,eq2),pred)) -> 
         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
-          prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
+          prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
           (CicPp.pp pred names)^ 
         aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
         aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
@@ -350,23 +133,23 @@ let string_of_proof_new ?(names=[]) p gp =
       (fun (pos,i,s,t) -> 
         (Printf.sprintf 
           "GOAL: %s %d %s %s\n" 
-            (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ 
+            (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ 
         aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
       gp)
 ;;
 
 let rec depend eq id =
-  let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
+  let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
   if id = ideq then true else  
   match p with
       Exact _ -> false
     | Step (_,(_,id1,(_,id2),_)) ->
-       let eq1 = Hashtbl.find id_to_eq id1 in
-       let eq2 = Hashtbl.find id_to_eq id2 in  
-        depend eq1 id || depend eq1 id2 
+        let eq1 = Hashtbl.find id_to_eq id1 in
+        let eq2 = Hashtbl.find id_to_eq id2 in  
+        depend eq1 id || depend eq2 id2 
 ;;
-    
-let ppsubst = ppsubst ~names:[]
+
+let ppsubst = Subst.ppsubst ~names:[];;
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
 let build_ens uri termlist =
@@ -385,61 +168,6 @@ let build_ens uri termlist =
   | _ -> assert false
 ;;
 
-let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
-  let rec do_build_proof proof = 
-    match proof with
-    | NoProof ->
-        Printf.fprintf stderr "WARNING: no proof!\n";
-        noproof
-    | BasicProof (s,term) -> apply_subst s term
-    | ProofGoalBlock (proofbit, proof) ->
-        print_endline "found ProofGoalBlock, going up...";
-        do_build_goal_proof proofbit proof
-    | ProofSymBlock (termlist, proof) ->
-        let proof = do_build_proof proof in
-        let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
-        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
-    | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
-        let t' = Cic.Lambda (name, ty, bo) in
-        let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
-        let proof' = do_build_proof proof in
-        let eqproof = do_build_proof eqproof in
-        let what, other =
-          if pos = Utils.Left then what, other else other, what
-        in
-        apply_subst subst
-          (Cic.Appl [Cic.Const (eq_URI, []); ty;
-                     what; t'; eqproof; other; proof'])
-    | SubProof (term, meta_index, proof) ->
-        let proof = do_build_proof proof in
-        let eq i = function
-          | Cic.Meta (j, _) -> i = j
-          | _ -> false
-        in
-        ProofEngineReduction.replace
-          ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
-
-  and do_build_goal_proof proofbit proof =
-    match proof with
-    | ProofGoalBlock (pb, p) ->
-        do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
-    | _ -> do_build_proof (replace_proof proofbit proof)
-
-  and replace_proof newproof = function
-    | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
-        let eqproof' = replace_proof newproof eqproof in
-        ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
-    | ProofGoalBlock (pb, p) ->
-        let pb' = replace_proof newproof pb in
-        ProofGoalBlock (pb', p)
-    | BasicProof _ -> newproof
-    | SubProof (term, meta_index, p) ->
-        SubProof (term, meta_index, replace_proof newproof p)
-    | p -> p
-  in
-  do_build_proof proof 
-;;
-
 let mk_sym uri ty t1 t2 p =
   let ens, args =  build_ens uri [ty;t1;t2;p] in
     Cic.Appl (Cic.Const(uri, ens) :: args)
@@ -468,6 +196,25 @@ let open_trans ens tl =
     | _ -> assert false   
 ;;
 
+let open_eq_ind args =
+  match args with 
+  | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
+  | _ -> assert false   
+;;
+
+let open_pred pred =
+  match pred with 
+  | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) 
+     when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
+  | _ -> prerr_endline (CicPp.ppterm pred); assert false   
+;;
+
+let is_not_fixed t =
+   CicSubstitution.subst (Cic.Implicit None) t <>
+   CicSubstitution.subst (Cic.Rel 1) t
+;;
+
+
 let canonical t = 
   let rec remove_refl t =
     match t with
@@ -526,189 +273,147 @@ let canonical t =
       | Cic.Appl l -> Cic.Appl (List.map canonical l)
       | _ -> t
   in
-  remove_refl (canonical t)  
+  remove_refl (canonical t)
+;;
+  
+let ty_of_lambda = function
+  | Cic.Lambda (_,ty,_) -> ty
+  | _ -> assert false 
+;;
+
+let compose_contexts ctx1 ctx2 = 
+  ProofEngineReduction.replace_lifting 
+    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t = 
+  ProofEngineReduction.replace_lifting
+    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
+;;
+
+let mk_eq uri ty l r =
+  Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+;;
+
+let mk_refl uri ty t = 
+  Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+;;
+
+let open_eq = function 
+  | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
+      uri, ty, l ,r
+  | _ -> assert false
+;;
+
+let contextualize uri ty left right t = 
+  (* aux [uri] [ty] [left] [right] [ctx] [t] 
+   * 
+   * the parameters validate this invariant  
+   *   t: eq(uri) ty left right
+   * that is used only by the base case
+   *
+   * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
+   *)
+    let rec aux uri ty left right ctx_d = function
+      | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+          let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+          let ty2,eq,lp,rp = open_pred pred in 
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+          let is_not_fixed_lp = is_not_fixed lp in
+          let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
+          (* extract the context and the fixed term from the predicate *)
+          let m, ctx_c = 
+            let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
+            (* they were under a lambda *)
+            let m =  CicSubstitution.subst (Cic.Implicit None) m in
+            let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
+            m, ctx_c          
+          in
+          (* create the compound context and put the terms under it *)
+          let ctx_dc = compose_contexts ctx_d ctx_c in
+          let dc_what = put_in_ctx ctx_dc what in
+          let dc_other = put_in_ctx ctx_dc other in
+          (* m is already in ctx_c so it is put in ctx_d only *)
+          let d_m = put_in_ctx ctx_d m in
+          (* we also need what in ctx_c *)
+          let c_what = put_in_ctx ctx_c what in
+          (* now put the proofs in the compound context *)
+          let p1 = (* p1: dc_what = d_m *)
+            if is_not_fixed_lp then 
+              aux uri ty1 c_what m ctx_d p1 
+            else
+              mk_sym uri_sym ty d_m dc_what
+                (aux uri ty1 m c_what ctx_d p1)
+          in
+          let p2 = (* p2: dc_other = dc_what *)
+            if avoid_eq_ind then
+              mk_sym uri_sym ty dc_what dc_other
+                (aux uri ty1 what other ctx_dc p2)
+            else
+              aux uri ty1 other what ctx_dc p2
+          in
+          (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
+             if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
+          let a,b,c,paeqb,pbeqc =
+            if is_not_fixed_lp then
+              dc_other,dc_what,d_m,p2,p1
+            else
+              d_m,dc_what,dc_other,
+                (mk_sym uri_sym ty dc_what d_m p1),
+                (mk_sym uri_sym ty dc_other dc_what p2)
+          in
+          mk_trans uri_trans ty a b c paeqb pbeqc
+    | t -> 
+        let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+        let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+        let pred = 
+          (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
+          let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
+          let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
+          let l = ctx_d in
+          let lty = CicSubstitution.lift 1 ty in 
+          Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
+        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 ty d_left in
+        mk_sym uri_sym ty d_right d_left
+          (mk_eq_ind uri_ind ty left pred refl_eq right t)
+  in
+  let empty_context = Cic.Rel 1 in
+  aux uri ty left right empty_context t
 ;;
 
+let contextualize_rewrites t ty = 
+  let eq,ty,l,r = open_eq ty in
+  contextualize eq ty l r t
+;;
+  
 let build_proof_step subst p1 p2 pos l r pred =
-  let p1 = apply_subst subst p1 in
-  let p2 = apply_subst subst p2 in
-  let l apply_subst subst l in
-  let r apply_subst subst r in
-  let pred = apply_subst subst pred in
-  let ty,body = (* Cic.Implicit None *) 
+  let p1 = Subst.apply_subst subst p1 in
+  let p2 = Subst.apply_subst subst p2 in
+  let l  = Subst.apply_subst subst l in
+  let r  = Subst.apply_subst subst r in
+  let pred = Subst.apply_subst subst pred in
+  let ty,body = 
     match pred with
       | Cic.Lambda (_,ty,body) -> ty,body 
       | _ -> assert false
   in
-  let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+  let what, other = 
     if pos = Utils.Left then l,r else r,l
   in
-  let is_not_fixed t =
-   CicSubstitution.subst (Cic.Implicit None) t <>
-   CicSubstitution.subst (Cic.Rel 1) t
-  in
-    match body,pos with
-(*
-      |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
-         let third = CicSubstitution.subst (Cic.Implicit None) third in
-         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-         let uri_sym = LibraryObjects.sym_eq_URI ~eq in
-           mk_trans uri_trans ty other what third
-            (mk_sym uri_sym ty what other p2) p1
-      |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
-         let third = CicSubstitution.subst (Cic.Implicit None) third in
-         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-           mk_trans uri_trans ty other what third p2 p1
-      |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left -> 
-         let third = CicSubstitution.subst (Cic.Implicit None) third in
-         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-           mk_trans uri_trans ty third what other p1 p2  
-      |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right -> 
-         let third = CicSubstitution.subst (Cic.Implicit None) third in
-         let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-         let uri_sym = LibraryObjects.sym_eq_URI ~eq in
-           mk_trans uri_trans ty third what other p1
-            (mk_sym uri_sym ty other what p2)
-      | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
-        ->
-          let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
-          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let pred_of t = CicSubstitution.subst t lhs in
-          let pred_of_what = pred_of what in
-          let pred_of_other = pred_of other in
-          (*           p2 : what = other
-           * ====================================
-           *  inject p2:  P(what) = P(other)
-           *)
-          let rec inject ty lhs what other p2 =
-           match p2 with
-           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
-               when LibraryObjects.is_trans_eq_URI uri_trans ->
-               let ty,l,m,r,plm,pmr = open_trans ens tl in
-               mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
-                 (inject ty lhs m r pmr) (inject ty lhs l m plm)
-           | _ -> 
-           let liftedty = CicSubstitution.lift 1 ty in
-           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
-           let refl_eq_part =
-            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
-           in
-            (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
-             (Cic.Lambda (Cic.Name "foo",ty,
-               (Cic.Appl
-               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
-                refl_eq_part what p2)
-          in
-           mk_trans uri_trans ty pred_of_other pred_of_what rhs
-             (inject ty lhs what other p2) p1
-      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
-        ->
-          let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
-          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let pred_of t = CicSubstitution.subst t lhs in
-          let pred_of_what = pred_of what in
-          let pred_of_other = pred_of other in
-          (*           p2 : what = other
-           * ====================================
-           *  inject p2:  P(what) = P(other)
-           *)
-          let rec inject ty lhs what other p2 =
-           match p2 with
-           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
-               when LibraryObjects.is_trans_eq_URI uri_trans ->
-               let ty,l,m,r,plm,pmr = open_trans ens tl in
-               mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
-                 (inject ty lhs m l plm)
-                 (inject ty lhs r m pmr)
-           | _ ->
-             let liftedty = CicSubstitution.lift 1 ty in
-             let lifted_pred_of_other = 
-               CicSubstitution.lift 1 (pred_of other) in
-             let refl_eq_part =
-              Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
-             in
-              mk_eq_ind (Utils.eq_ind_URI ()) ty other
-               (Cic.Lambda (Cic.Name "foo",ty,
-                 (Cic.Appl
-                 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
-                  refl_eq_part what p2
-          in
-           mk_trans uri_trans ty pred_of_other pred_of_what rhs
-            (inject ty lhs what other p2) p1
-      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
-        ->
-          let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
-          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let pred_of t = CicSubstitution.subst t rhs in
-          let pred_of_what = pred_of what in
-          let pred_of_other = pred_of other in
-          (*           p2 : what = other
-           * ====================================
-           *  inject p2:  P(what) = P(other)
-           *)
-          let rec inject ty lhs what other p2 =
-           match p2 with
-           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
-               when LibraryObjects.is_trans_eq_URI uri_trans ->
-               let ty,l,m,r,plm,pmr = open_trans ens tl in
-                 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
-                   (inject ty lhs m r pmr)
-                   (inject ty lhs l m plm)
-           | _ ->
-           let liftedty = CicSubstitution.lift 1 ty in
-           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
-           let refl_eq_part =
-            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
-           in
-            (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
-             (Cic.Lambda (Cic.Name "foo",ty,
-               (Cic.Appl
-               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
-                refl_eq_part what p2)
-          in
-           mk_trans uri_trans ty lhs pred_of_what pred_of_other
-             p1 (inject ty rhs other what p2)
-      | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
-        ->
-          let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
-          let uri_trans = LibraryObjects.trans_eq_URI ~eq in
-          let pred_of t = CicSubstitution.subst t rhs in
-          let pred_of_what = pred_of what in
-          let pred_of_other = pred_of other in
-          (*           p2 : what = other
-           * ====================================
-           *  inject p2:  P(what) = P(other)
-           *)
-          let rec inject ty lhs what other p2 =
-           match p2 with
-           | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
-               when LibraryObjects.is_trans_eq_URI uri_trans ->
-               let ty,l,m,r,plm,pmr = open_trans ens tl in
-                 (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
-                   (inject ty lhs m l plm)
-                   (inject ty lhs r m pmr))
-           | _ ->
-           let liftedty = CicSubstitution.lift 1 ty in
-           let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
-           let refl_eq_part =
-            Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
-           in
-            mk_eq_ind (Utils.eq_ind_URI ()) ty other
-             (Cic.Lambda (Cic.Name "foo",ty,
-               (Cic.Appl
-               [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
-                refl_eq_part what p2
-          in
-           mk_trans uri_trans ty lhs pred_of_what pred_of_other 
-             p1 (inject ty rhs other what p2)
-*)
-      | _, Utils.Left ->
+    match pos with
+      | Utils.Left ->
         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
-      | _, Utils.Right ->
+      | Utils.Right ->
         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 ;;
 
-let build_proof_term_new proof =
+let build_proof_term proof =
   let rec aux = function
      | Exact term -> term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
@@ -741,7 +446,7 @@ let wfo goalproof proof =
 
 let string_of_id names id = 
   try
-    let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
     match p with
     | Exact t -> 
         Printf.sprintf "%d = %s: %s = %s" id
@@ -760,17 +465,17 @@ let pp_proof names goalproof proof =
       ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
 ;;
 
-let build_goal_proof l initial =
+let build_goal_proof l initial ty =
   let proof = 
    List.fold_left 
    (fun  current_proof (pos,id,subst,pred) -> 
       let p,l,r = proof_of_id id in
-      let p = build_proof_term_new p in
+      let p = build_proof_term p in
       let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
         build_proof_step subst current_proof p pos l r pred)
    initial l
   in
-  canonical proof
+  canonical (contextualize_rewrites proof ty)
 ;;
 
 let refl_proof ty term = 
@@ -780,7 +485,9 @@ let refl_proof ty term =
        ty; term]
 ;;
 
-let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+let metas_of_proof p = 
+  Utils.metas_of_term (build_proof_term p)
+;;
 
 let relocate newmeta menv =
   let subst, metasenv, newmeta = 
@@ -789,49 +496,33 @@ let relocate newmeta menv =
         let irl = [] (*
          CicMkImplicit.identity_relocation_list_for_metavariable context *)
         in
-        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
+        let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
         let newmeta = maxmeta, context, ty in
         newsubst, newmeta::menv, maxmeta+1) 
-      menv ([], [], newmeta+1)
+      menv (Subst.empty_subst, [], newmeta+1)
   in
-  let metasenv = apply_subst_metasenv subst metasenv in
-  let subst = flatten_subst subst in
+  let metasenv = Subst.apply_subst_metasenv subst metasenv in
+  let subst = Subst.flatten_subst subst in
   subst, metasenv, newmeta
 
 
 let fix_metas newmeta eq = 
-  let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
+  let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   (* debug 
   let _ , eq = 
     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
   prerr_endline (string_of_equality eq); *)
   let subst, metasenv, newmeta = relocate newmeta menv in
-  let ty = apply_subst subst ty in
-  let left = apply_subst subst left in
-  let right = apply_subst subst right in
+  let ty = Subst.apply_subst subst ty in
+  let left = Subst.apply_subst subst left in
+  let right = Subst.apply_subst subst right in
   let fix_proof = function
-    | NoProof -> NoProof 
-    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
-    | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
-        (*
-        let newsubst = 
-          List.map
-            (fun (i, (context, term, ty)) ->
-               let context = apply_subst_context subst context in
-               let term = apply_subst subst term in
-               let ty = apply_subst subst ty in  
-                 (i, (context, term, ty))) subst' in *)
-          ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
-    | p -> assert false
-  in
-  let fix_new_proof = function
-    | Exact p -> Exact (apply_subst subst p)
+    | Exact p -> Exact (Subst.apply_subst subst p)
     | Step (s,(r,id1,(pos,id2),pred)) -> 
-        Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+        Step (Subst.concat_substs s subst,(r,id1,(pos,id2), pred))
   in
-  let new_p = fix_new_proof p1 in
-  let old_p = fix_proof p2 in
-  let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
+  let p = fix_proof p in
+  let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
   (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
@@ -979,7 +670,7 @@ let equality_of_term proof term =
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = Utils.compute_equality_weight stat in
-      let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
+      let e = mk_equality (w, Exact proof, stat,[]) in
       e
   | _ ->
       raise TermIsNotAnEquality
index 1a2a3a2808d3d284a4f00f4eda4ebe289f5b2ca5..d2c58041d680089c804b6ef90a29c03ecbb9bbf9 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
-type substitution 
-
-type rule = SuperpositionRight | SuperpositionLeft |Demodulation
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 
 type equality 
 
-and proof = new_proof * old_proof
-
-and new_proof =
+and proof =
     Exact of Cic.term
-  | Step of substitution * (rule * int * (Utils.pos * int) * Cic.term)
-
-and old_proof =
-    NoProof
-  | BasicProof of substitution * Cic.term
-  | ProofBlock of substitution * UriManager.uri * (Cic.name * Cic.term) *
-      Cic.term * (Utils.pos * equality) * old_proof
-  | ProofGoalBlock of old_proof * old_proof
-  | ProofSymBlock of Cic.term list * old_proof
-  | SubProof of Cic.term * int * old_proof
+  | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term)
 
-and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
 
-val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string
-
-val empty_subst : substitution
-val apply_subst : substitution -> Cic.term -> Cic.term
-val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
-val ppsubst : substitution -> string
-val buildsubst : 
-  int -> Cic.context -> Cic.term -> Cic.term -> substitution -> 
-    substitution
-val flatten_subst : substitution -> substitution 
-val lookup_subst : Cic.term -> substitution -> Cic.term
-val filter : substitution -> Cic.metasenv -> Cic.metasenv
-val is_in_subst : int -> substitution -> bool
-val merge_subst_if_possible: 
-  substitution -> substitution -> 
-    substitution option
+val pp_proof: (Cic.name option) list -> goal_proof -> proof -> string
 
 val reset : unit -> unit
 
@@ -80,14 +52,15 @@ val open_equality :
     int * proof * 
     (Cic.term * Cic.term * Cic.term * Utils.comparison) *
     Cic.metasenv * int
+val depend : equality -> int -> bool
 val compare : equality -> equality -> int
 val string_of_equality : ?env:Utils.environment -> equality -> string
-val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
-val string_of_proof_new : 
-  ?names:(Cic.name option)list -> new_proof -> goal_proof -> string
-val build_proof_term_new: new_proof -> Cic.term 
-val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
-val build_goal_proof: goal_proof -> Cic.term -> Cic.term
+val string_of_proof : 
+  ?names:(Cic.name option)list -> proof -> goal_proof -> string
+val build_proof_term: proof -> Cic.term 
+(* build_goal_proof [goal_proof] [initial_proof] [ty] 
+ *  [ty] is the type of the goal *)
+val build_goal_proof: goal_proof -> Cic.term -> Cic.term-> Cic.term
 val refl_proof: Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
@@ -116,4 +89,3 @@ val meta_convertibility_eq: equality -> equality -> bool
 
 val is_weak_identity: equality -> bool
 val is_identity: Utils.environment -> equality -> bool
-
index 4ac1c94e29f12a0f93a22f085d5a75ca94f19068..e3ef59d9b54f538ebd50ca4cc8d70d01d065e1f0 100644 (file)
@@ -93,7 +93,7 @@ let print_candidates ?env mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
-let apply_subst = Equality.apply_subst
+let apply_subst = Subst.apply_subst
 
 let index = Index.index
 let remove_index = Index.remove_index
@@ -103,7 +103,7 @@ let init_index = Index.init_index
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+        (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -250,7 +250,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
             let p="proof = "^
-              (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n" 
+              (CicPp.ppterm(Equality.build_proof_term proof))^"\n" 
             in
               check_for_duplicates metas "gia nella metas";
               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
@@ -445,7 +445,7 @@ let subsumption env table target =
               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
               raise e
           in
-          (match Equality.merge_subst_if_possible subst subst' with
+          (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what tl
           | Some s -> Some (s, equation))
         with Inference.MatchingFailure ->
@@ -593,9 +593,9 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, ((proof_new, proof_old) (*as proof*)), 
-     (eq_ty, left, right, order), metas, id = 
-    Equality.open_equality target in
+  let w, proof, (eq_ty, left, right, order), metas, id = 
+    Equality.open_equality target 
+  in
   (* first, we simplify *)
 (*   let right = U.guarded_simpl context right in *)
 (*   let left = U.guarded_simpl context left in *)
@@ -615,11 +615,11 @@ let rec demodulation_equality ?from newmeta env table sign target =
       begin
         ignore(check_for_duplicates menv "input1");
         ignore(check_disjoint_invariant subst menv "input2");
-        let substs = Equality.ppsubst subst in 
+        let substs = Subst.ppsubst subst in 
         ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
     let pos, equality = eq_found in
-    let (_, (proof'_new,proof'_old)
+    let (_, proof'
         (ty, what, other, _), menv',id') = Equality.open_equality equality in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
@@ -638,12 +638,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
-          (bo,
-           (Equality.Step (subst,(Equality.Demodulation,
-             id,(pos,id'),
-                        (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
-           Equality.ProofBlock (
-             subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
+          (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
+          (Cic.Lambda (name, ty, bo'))))))
       else
         assert false
 (*
@@ -707,17 +703,17 @@ let rec demodulation_equality ?from newmeta env table sign target =
       if Utils.debug_metas then 
         try ignore(CicTypeChecker.type_of_aux'
           newmenv context 
-            (Equality.build_proof_term_old (snd newproof)) ugraph);
+            (Equality.build_proof_term newproof) ugraph);
           () 
         with exc ->                   
           prerr_endline "sempre lui";
-          prerr_endline (Equality.ppsubst subst);
+          prerr_endline (Subst.ppsubst subst);
           prerr_endline (CicPp.ppterm 
-            (Equality.build_proof_term_old (snd newproof)));
+            (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: " ^ (Equality.ppsubst subst));
+          prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
           prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
             newmenv));
           raise exc;
@@ -1027,7 +1023,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 w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id = 
+  let w, eqproof, (eq_ty, left, right, ordering), newmetas,id = 
     Equality.open_equality target 
   in 
   if Utils.debug_metas then 
@@ -1079,11 +1075,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                 S.lift 1 eq_ty; l; r]
       in
       bo',
-      (Equality.Step 
-        (s,(Equality.SuperpositionRight,
-           id,(pos,id'),(Cic.Lambda(name,ty,bo'')))),
-       Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
-       
+        Equality.Step 
+          (s,(Equality.SuperpositionRight,
+               id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
     in
     let newmeta, newequality = 
       let left, right =
@@ -1125,78 +1119,32 @@ let rec demodulation_goal newmeta env table goal =
   let module HL = HelmLibraryObjects in
   let metasenv, context, ugraph = env in
   let maxmeta = ref newmeta in
-  let (cicproof,proof), metas, term = goal in
+  let goalproof, metas, term = goal in
   let term = Utils.guarded_simpl (~debug:true) context term in
-  let goal = (cicproof,proof), metas, term in
+  let goal = goalproof, metas, term in
   let metasenv' = metas in
   
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
     let pos, equality = eq_found in
-    let (_, (proofnew',proof'), (ty, what, other, _), menv',id) = 
+    let (_, proof', (ty, what, other, _), menv',id) = 
       Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
-    let newterm, newproof, newcicproof =
+    let newterm, newgoalproof =
       let bo = 
        Utils.guarded_simpl context (apply_subst subst(S.subst other t)) 
       in
-      let bo' = apply_subst subst t in 
-(*      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+      let bo' = (*apply_subst subst*) t in 
       let name = C.Name "x" in
       incr demod_counter;
-      let metaproof = 
-        incr maxmeta;
-        let irl = [] (*
-          CicMkImplicit.identity_relocation_list_for_metavariable context *) in 
-(*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-        C.Meta (!maxmeta, irl)
-      in
-      let eq_found =
-        let eq_found_proof =
-          let termlist =
-            if pos = Utils.Left then [ty; what; other]
-            else [ty; other; what]
-          in
-          Equality.ProofSymBlock (termlist, proof')
-        in
-        let what, other =
-          if pos = Utils.Left then what, other else other, what
-        in
-        pos, 
-       Equality.mk_equality 
-         (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
-      in
-      let goal_proof =
-        let pb =
-          Equality.ProofBlock 
-           (subst, eq_URI, (name, ty), bo',
-             eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
-        in
-        let rec repl = function
-          | Equality.NoProof ->
-(*               debug_print (lazy "replacing a NoProof"); *)
-              pb
-          | Equality.BasicProof _ ->
-(*               debug_print (lazy "replacing a BasicProof"); *)
-              pb
-          | Equality.ProofGoalBlock (_, parent_proof) ->
-(*               debug_print (lazy "replacing another ProofGoalBlock"); *)
-              Equality.ProofGoalBlock (pb, parent_proof)
-          | Equality.SubProof (term, meta_index, p)  ->
-              prerr_endline "subproof!";
-              Equality.SubProof (term, meta_index, repl p)
-          | _ -> assert false
-        in repl proof
-      in
-      let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
-      bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
-        (newcicproofstep::cicproof)
+      let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+      bo, (newgoalproofstep::goalproof)
     in
     let newmetasenv = (* Inference.filter subst *) menv in
-    !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
+    !maxmeta, (newgoalproof, newmetasenv, newterm)
   in  
   let res =
     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
@@ -1234,14 +1182,18 @@ let rec demodulation_theorem newmeta env table theorem =
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newty =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-      let bo' = apply_subst subst t in 
-      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
+(*      let bo' = apply_subst subst t in *)
+(*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
       incr demod_counter;
+(*
       let newproofold =
         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
                               Equality.BasicProof (Equality.empty_subst,term))
       in
       (Equality.build_proof_term_old newproofold, bo)
+*)
+      (* TODO, not ported to the new proofs *) 
+      if true then assert false; term, bo
     in    
     !maxmeta, (newterm, newty, menv)
   in  
index 1c6102a07aa304563d70aac7825a12357aec3e02..8af265f907f945c4a597b24e299e64b5da29dc22 100644 (file)
@@ -47,7 +47,7 @@ val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Equality.substitution * Equality.equality) option
+  (Subst.substitution * Equality.equality) option
 val superposition_left :
   int ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
@@ -72,9 +72,9 @@ val demodulation_goal :
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key ->
+  Equality.goal_proof * Cic.metasenv * Index.key ->
   bool * int * 
-   ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key)
+   (Equality.goal_proof * Cic.metasenv * Index.key)
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
index f088d54543aa265f6550e53bf0552f886c409e8f..272a8100337c082485a6935fe270d5d3a2c8827f 100644 (file)
@@ -30,7 +30,7 @@ open Printf;;
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+        (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -65,7 +65,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   let module C = Cic in
   let module M = CicMetaSubst in
   let module U = CicUnification in
-  let lookup = Equality.lookup_subst in
+  let lookup = Subst.lookup_subst in
   let rec occurs_check subst what where =
     match where with
     | t when what = t -> true
@@ -99,8 +99,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
-          assert (not (Equality.is_in_subst i subst));
-          let subst = Equality.buildsubst i context t ty subst in
+          assert (not (Subst.is_in_subst i subst));
+          let subst = Subst.buildsubst i context t ty subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -126,8 +126,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | _, _ ->
         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
-  let subst, menv = unif Equality.empty_subst metasenv t1 t2 in
-  let menv = Equality.filter subst menv in
+  let subst, menv = unif Subst.empty_subst metasenv t1 t2 in
+  let menv = Subst.filter subst menv in
   subst, menv, ugraph
 ;;
 
@@ -234,10 +234,7 @@ let find_equalities context proof =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new , proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -251,9 +248,7 @@ let find_equalities context proof =
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
               let p = C.Rel index in
-              let proof_old = Equality.BasicProof (Equality.empty_subst,p) in
-              let proof_new = Equality.Exact p in
-              let proof = proof_new, proof_old in
+              let proof = Equality.Exact p in
               let e = Equality.mk_equality (w, proof,stat,[]) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
@@ -391,10 +386,7 @@ let find_library_equalities dbd context status maxmeta =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof_old = 
-                      Equality.BasicProof (Equality.empty_subst,p) in
-                    let proof_new = Equality.Exact p in
-                    let proof = proof_new, proof_old in
+                    let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
@@ -404,9 +396,7 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let old_proof = Equality.BasicProof (Equality.empty_subst,term) in
-              let new_proof = Equality.Exact term in 
-              let proof = new_proof, old_proof in
+              let proof = Equality.Exact term in 
               let e = Equality.mk_equality (w, proof, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
index 08d1c8f266010354deb9c48dbcf86d9c16fc7c1d..9bfb84cb21f8ea7f0164845544ba556a02c51e0d 100644 (file)
@@ -30,7 +30,7 @@ val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -40,7 +40,7 @@ val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> 
   Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
+    Subst.substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
index 6b1b65e276eef42a34c2426490a62da745cbace4..f8c20d0e3b61250633e5dc4841fabe932b911470 100644 (file)
@@ -71,14 +71,13 @@ let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
 type new_proof = 
-  Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv
-type old_proof = Equality.old_proof * Cic.metasenv
+  Equality.goal_proof * Equality.proof * Subst.substitution * Cic.metasenv
 type result =
   | ParamodulationFailure
-  | ParamodulationSuccess of (new_proof * old_proof) option
+  | ParamodulationSuccess of new_proof option
 ;;
 
-type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;;
+type goal = Equality.goal_proof * Cic.metasenv * Cic.term;;
 
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
@@ -153,12 +152,22 @@ let rec select env goals passive =
   match !weight_age_counter with
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
-      match pos_list with
-      | (hd:EqualitySet.elt)::tl ->
-          let passive_table =
-            Indexing.remove_index passive_table hd
-          in  hd, ((tl, EqualitySet.remove hd pos_set), passive_table)
-      | _ -> assert false)
+      let rec skip_giant pos_list pos_set passive_table =
+       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 < 50 then
+                 hd, ((tl, pos_set), passive_table)
+               else
+                 (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n");
+                 skip_giant tl pos_set passive_table)
+         | _ -> assert false
+      in
+       skip_giant pos_list pos_set passive_table)
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
@@ -211,6 +220,27 @@ let rec select env goals passive =
       passive_table)
 ;;
 
+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 =
+    List.fold_right
+      (fun eq ((list,set),table) ->
+        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))
+        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 =
@@ -374,18 +404,35 @@ let check_for_deep_subsumption env active_table eq =
     match t1,t2 with
       | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
       | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
+(* VERSIONE ERRATA 
       | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
           let rc = check_subsumed b t1 t1 in 
             if rc then 
              true, true
+           else if h1 = h2 then
+              (try 
+                List.fold_left2 
+                  (fun (ok_so_far, subsumption_used) t t' -> 
+                     aux true (ok_so_far, subsumption_used) t t')
+                  (ok_so_far, subsumption_used) l l'
+               with Invalid_argument _ -> false,subsumption_used)
            else
+             false, subsumption_used
+      | _ -> false, subsumption_used *)
+      | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
+          let rc = check_subsumed b t1 t2 in 
+            if rc then 
+             true, true
+           else if h1 = h2 then
               (try 
                 List.fold_left2 
                   (fun (ok_so_far, subsumption_used) t t' -> 
                      aux true (ok_so_far, subsumption_used) t t')
                   (ok_so_far, subsumption_used) l l'
                with Invalid_argument _ -> false,subsumption_used)
-    | _ -> false, subsumption_used
+           else
+             false, subsumption_used
+    | _ -> false, subsumption_used 
   in
   fst (aux false (true,false) left right)
 ;;
@@ -481,7 +528,10 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
 (*              if Indexing.subsumption env active_table c = None then*)
                 (match Indexing.subsumption env passive_table c with
                 | None -> res
-                | Some (_,c') -> None (*Some c'*))
+                | Some (_,c') -> 
+                   None
+                   (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n";
+                   Some c'*))
 (*
               else
                 None
@@ -643,26 +693,31 @@ let backward_simplify_active env new_pos new_table min_weight active =
   let find eq1 where =
     List.exists (Equality.meta_convertibility_eq eq1) where
   in
-  let active, newa =
+  let id_of_eq eq = 
+    let _, _, _, _,id = Equality.open_equality eq in id
+  in
+  let ((active1,pruned),tbl), newa =
     List.fold_right
-      (fun eq (res, tbl) ->
+      (fun eq ((res,pruned), tbl) ->
          if List.mem eq res then
-           res, tbl
+           (res, (id_of_eq eq)::pruned),tbl 
          else if (Equality.is_identity env eq) || (find eq res) then (
-           res, tbl
+           (res, (id_of_eq eq)::pruned),tbl
          ) 
          else
-           eq::res, Indexing.index tbl eq)
-      active_list ([], Indexing.empty),
+           (eq::res,pruned), Indexing.index tbl eq)
+      active_list (([],pruned), Indexing.empty),
     List.fold_right
       (fun eq p ->
          if (Equality.is_identity env eq) then p
          else eq::p)
       newa []
   in
+  if List.length active1 <> List.length (fst active) then
+    prerr_endline "\n\n\nMANCAVANO DELLE PRUNED!!!!\n\n\n";
   match newa with
-  | [] -> active, None
-  | _ -> active, Some newa
+  | [] -> (active1,tbl), None, pruned 
+  | _ -> (active1,tbl), Some newa, pruned
 ;;
 
 
@@ -712,13 +767,13 @@ let backward_simplify env new' ?passive active =
       ([], Indexing.empty, 1000000) new'
   in
 *)
-  let active, newa =
+  let active, newa, pruned =
     backward_simplify_active env new_pos new_table min_weight active in
   match passive with
   | None ->
-      active, (make_passive []), newa, None
+      active, (make_passive []), newa, None, pruned
   | Some passive ->
-     active, passive, newa, None
+     active, passive, newa, None, pruned
 (* prova
       let passive, newp =
         backward_simplify_passive env new_pos new_table min_weight passive in
@@ -896,48 +951,21 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
 
-let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
+let check_if_goal_is_subsumed env (goalproof,menv,ty) table =
   prerr_endline "check_goal_subsumed";
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
       (let goal_equation = 
          Equality.mk_equality
-           (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv) 
-       in
-         match Indexing.subsumption env table goal_equation with
-           | Some (subst, equality ) ->
-               let (_,(np,p),(ty,l,r,_),m,id) = 
-                 Equality.open_equality equality in
-              prerr_endline "1";
-               let p = Equality.apply_subst subst 
-                 (Equality.build_proof_term_old p) in
-              prerr_endline "2";
-               let newp =
-                 let rec repl = function
-                   | Equality.ProofGoalBlock (_, gp) ->
-                       Equality.ProofGoalBlock 
-                         (Equality.BasicProof (Equality.empty_subst,p), gp)
-                   | Equality.NoProof -> 
-                       Equality.BasicProof (Equality.empty_subst,p)
-                   | Equality.BasicProof _ -> 
-                       Equality.BasicProof (Equality.empty_subst,p)
-                   | Equality.SubProof (t, i, p2) ->
-                       Equality.SubProof (t, i, repl p2)
-                   | _ -> assert false
-                 in
-                   repl proof
-               in
-              prerr_endline "3";
-               let newcicp,np,subst,cicmenv = 
-                 cicproof,np, subst, 
-                 Equality.apply_subst_metasenv subst (m @ menv) 
-               in
-              prerr_endline ".";
-                 Some 
-                  ((newcicp,np,subst,cicmenv),
-                   (newp, Equality.apply_subst_metasenv subst m @ menv ))
-           | None -> None)
+           (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
+      in
+      match Indexing.subsumption env table goal_equation with
+        | Some (subst, equality ) ->
+            let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
+            let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
+            Some (goalproof, p, subst, cicmenv)
+        | None -> None)
   | _ -> None
 ;;
 
@@ -969,35 +997,12 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
       (* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
       let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
       match (fst goals) with
-        | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ 
+        | (_,[goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ 
             when left = right && iseq uri -> 
-            let p =
-              Cic.Appl [Cic.MutConstruct (* reflexivity *)
-                        (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
-            in
-            let newp =
-              let rec repl = function
-                | Equality.ProofGoalBlock (_, gp) ->
-                    Equality.ProofGoalBlock 
-                      (Equality.BasicProof (Equality.empty_subst,p), gp)
-                | Equality.NoProof -> 
-
-                    Equality.BasicProof (Equality.empty_subst,p)
-                | Equality.BasicProof _ -> 
-                    Equality.BasicProof (Equality.empty_subst,p)
-                | Equality.SubProof (t, i, p2) ->
-                    Equality.SubProof (t, i, repl p2)
-                | _ -> assert false
-              in
-              repl (snd proof)
-            in 
-                 let reflproof = Equality.refl_proof eq_ty left in
-            true, 
-              Some ((fst proof,Equality.Exact reflproof,
-                     Equality.empty_subst,m),
-                    (newp,m))
-        | (_, [proof,m,ty])::_ ->
-            (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with
+            let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+            true, Some (goalproof, reflproof, Subst.empty_subst,m)
+        | (_, [goal])::_ ->
+            (match check_if_goal_is_subsumed env goal (snd active) with
             | None -> false,None
             | Some p ->
                 prerr_endline "Proof found by subsumption!";
@@ -1159,8 +1164,10 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               forward_simpl_new_time :=
                 !forward_simpl_new_time +. (t2 -. t1);
               let t1 = Unix.gettimeofday () in
-              let active, passive, newa, retained =
+              let active, passive, newa, retained, pruned =
                 backward_simplify env new' ~passive  active in
+             let passive = 
+               List.fold_left filter_dependent passive pruned in
               let t2 = Unix.gettimeofday () in
                 backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
               match newa, retained with
@@ -1177,7 +1184,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               | Some p, Some rp ->
                   simplify (new' @ p @ rp) active passive
             in
-            let active, _, new' = simplify new' active passive in
+            let active, passive, new' = simplify new' active passive in
             let goals = 
               let a,b,_ = build_table new' in
               simplify_goals env goals ~passive (a,b)
@@ -1258,8 +1265,10 @@ let rec saturate_equations env goal accept_fun passive active =
         in
         let rec simplify new' active passive =
           let new' = forward_simplify_new env new' ~passive active in
-          let active, passive, newa, retained =
+          let active, passive, newa, retained, pruned =
             backward_simplify env new' ~passive active in
+         let passive = 
+           List.fold_left filter_dependent passive pruned in
           match newa, retained with
           | None, None -> active, passive, new'
           | Some p, None
@@ -1504,9 +1513,7 @@ let saturate
   in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let goal = 
-    ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal 
-  in
+  let goal = [], [], goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -1563,9 +1570,7 @@ let saturate
   in
   match res with
   | ParamodulationSuccess 
-      (Some 
-        ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *)
-         (proof, proof_menv))) (* OLD *)
+      (Some (goalproof,newproof,subsumption_subst, proof_menv))
       ->
       prerr_endline "OK, found a proof!";
 
@@ -1574,16 +1579,13 @@ let saturate
       * goalproof);*)
       prerr_endline (Equality.pp_proof names goalproof newproof);
       
-      (* generation of the old proof *)
-      let cic_proof = Equality.build_proof_term_old proof in
-     
-      (* generation of the new proof *)
+      (* generation of the proof *)
       let cic_proof_new = 
         Equality.build_goal_proof 
-          goalproof (Equality.build_proof_term_new newproof) 
+          goalproof (Equality.build_proof_term newproof) type_of_goal
       in
       let cic_proof_new = 
-        Equality.apply_subst subsumption_subst cic_proof_new 
+        Subst.apply_subst subsumption_subst cic_proof_new 
       in
       
       (* replacing fake mets with real ones *)
@@ -1593,21 +1595,6 @@ let saturate
         | _ -> false
       in
       let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
-      prerr_endline "replacing metas (old)";
-      let proof_menv, what, with_what = 
-        let irl = mkirl context in
-        List.fold_left 
-          (fun (acc1,acc2,acc3) (i,_,ty) -> 
-            (i,context,ty)::acc1, 
-            (Cic.Meta(i,[]))::acc2, 
-            (Cic.Meta(i,irl)) ::acc3) 
-          ([],[],[]) proof_menv 
-      in
-      let cic_proof = ProofEngineReduction.replace_lifting
-              ~equality:(=)
-              ~what ~with_what
-              ~where:cic_proof
-      in
       prerr_endline "replacing metas (new)";
       let newproof_menv, what, with_what = 
         let irl = mkirl context in
@@ -1616,7 +1603,7 @@ let saturate
             (i,context,ty)::acc1, 
             (Cic.Meta(i,[]))::acc2, 
             (Cic.Meta(i,irl)) ::acc3) 
-          ([],[],[]) newproof_menv 
+          ([],[],[]) proof_menv 
       in
       let cic_proof_new = ProofEngineReduction.replace_lifting
               ~equality:(=)
@@ -1625,10 +1612,6 @@ let saturate
       in
 
       (* pp new/old proof *)
-(*      prerr_endline "OLDPROOF";*)
-(*      prerr_endline (Equality.string_of_proof_old proof);*)
-(*      prerr_endline "OLDPROOFCIC";*)
-(*      prerr_endline (CicPp.pp cic_proof names); *)
 (*      prerr_endline "NEWPROOFCIC";*)
 (*      prerr_endline (CicPp.pp cic_proof_new names); *)
 
@@ -1641,20 +1624,9 @@ let saturate
         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
       in
       let newmetasenv_new = newmetasenv@newproof_menv in
-      let newmetasenv = newmetasenv@proof_menv in
       (* check/refine/... build the new proof *)
       let newstatus =
         let cic_proof,newmetasenv,proof_menv,ty, ug =
-          prerr_endline "type checking ... (old) ";
-          let _old_ty, _oldug = 
-            try 
-              CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph
-            with 
-              CicTypeChecker.TypeCheckerFailure s ->
-                prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!";
-                prerr_endline (Lazy.force s);
-                Cic.Implicit None, CicUniv.empty_ugraph
-          in
           let cic_proof_new,new_ty,newmetasenv_new,newug = 
             try
               (*
@@ -1869,8 +1841,7 @@ let main_demod_equalities dbd term metasenv ugraph =
   in
   let env = (metasenv, context, ugraph) in
   (*try*)
-    let goal = 
-      ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal 
+    let goal = [], [], goal 
     in
     let equalities = simplify_equalities env (equalities@library_equalities) in
     let active = make_active () in
@@ -1930,10 +1901,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
   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
-  let goalterm = Cic.Meta (metano,irl) in
-  let initgoal = 
-    ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty 
-  in
+  let initgoal = [], [], ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let equalities = simplify_equalities env (equalities@library_equalities) in   
   let table = 
@@ -1949,7 +1917,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
     begin
       let opengoal = Cic.Meta(maxm,irl) in
       let proofterm = 
-        Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in
+        Equality.build_goal_proof newproof opengoal ty in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
           (curi,extended_metasenv,pbo,pty),goal in
diff --git a/helm/software/components/tactics/paramodulation/subst.ml b/helm/software/components/tactics/paramodulation/subst.ml
new file mode 100644 (file)
index 0000000..f738d2f
--- /dev/null
@@ -0,0 +1,215 @@
+(* cOpyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
+
+
+(******* CIC substitution ***************************************************)
+
+type cic_substitution = Cic.substitution
+let cic_apply_subst = CicMetaSubst.apply_subst
+let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
+let cic_ppsubst = CicMetaSubst.ppsubst
+let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
+let cic_flatten_subst subst =
+    List.map
+      (fun (i, (context, term, ty)) ->
+         let context = (* cic_apply_subst_context subst*) context in
+         let term = cic_apply_subst subst term in
+         let ty = cic_apply_subst subst ty in  
+         (i, (context, term, ty))) subst
+let rec cic_lookup_subst meta subst =
+  match meta with
+  | Cic.Meta (i, _) -> (
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
+      in cic_lookup_subst t subst 
+      with Not_found -> meta
+    )
+  | _ -> meta
+;;
+
+let cic_merge_subst_if_possible s1 s2 =
+  let already_in = Hashtbl.create 13 in
+  let rec aux acc = function
+    | ((i,_,x) as s)::tl ->
+        (try 
+          let x' = Hashtbl.find already_in i in
+          if x = x' then aux acc tl else None
+        with
+        | Not_found -> 
+            Hashtbl.add already_in i x;
+            aux (s::acc) tl)
+    | [] -> Some acc 
+  in  
+    aux [] (s1@s2)
+;;
+
+(******** NAIF substitution **************************************************)
+(* 
+ * naif version of apply subst; the local context of metas is ignored;
+ * we assume the substituted term must be lifted according to the nesting
+ * depth of the meta. 
+ * Alternatively, we could used implicit instead of metas 
+ *)
+
+type naif_substitution = (int * Cic.term) list 
+
+let naif_apply_subst subst term =
+ let rec aux k t =
+   match t with
+       Cic.Rel _ -> t
+     | Cic.Var (uri,exp_named_subst) -> 
+         let exp_named_subst' =
+           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+         in
+           Cic.Var (uri, exp_named_subst')
+    | Cic.Meta (i, l) -> 
+        (try
+          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+         with Not_found -> t)
+    | Cic.Sort _
+    | Cic.Implicit _ -> t
+    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
+    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
+    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
+    | Cic.Const (uri,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          if exp_named_subst' != exp_named_subst then
+            Cic.Const (uri, exp_named_subst')
+          else
+            t (* TODO: provare a mantenere il piu' possibile sharing *)
+    | Cic.MutInd (uri,typeno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          Cic.MutInd (uri,typeno,exp_named_subst')
+    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | Cic.MutCase (sp,i,outty,t,pl) ->
+        let pl' = List.map (aux k) pl in
+          Cic.MutCase (sp, i, aux k outty, aux k t, pl')
+    | Cic.Fix (i, fl) ->
+        let len = List.length fl in
+        let fl' =
+         List.map 
+           (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
+        in
+          Cic.Fix (i, fl')
+    | Cic.CoFix (i, fl) ->
+        let len = List.length fl in
+        let fl' =
+          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
+        in
+          Cic.CoFix (i, fl')
+in
+  aux 0 term
+;;
+
+(* naif version of apply_subst_metasenv: we do not apply the 
+substitution to the context *)
+
+let naif_apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, context, naif_apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.mem_assoc i subst))
+      metasenv)
+
+let naif_ppsubst names subst =
+  "{" ^ String.concat "; "
+    (List.map
+      (fun (idx, t) ->
+         Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
+    subst) ^ "}"
+;;
+
+let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
+
+let naif_flatten_subst subst = 
+  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+;;
+
+let rec naif_lookup_subst meta subst =
+  match meta with
+    | Cic.Meta (i, _) ->
+        (try
+          naif_lookup_subst (List.assoc i subst) subst
+        with
+            Not_found -> meta)
+    | _ -> meta
+;;
+
+let naif_merge_subst_if_possible s1 s2 =
+  let already_in = Hashtbl.create 13 in
+  let rec aux acc = function
+    | ((i,x) as s)::tl ->
+        (try 
+          let x' = Hashtbl.find already_in i in
+          if x = x' then aux acc tl else None
+        with
+        | Not_found -> 
+            Hashtbl.add already_in i x;
+            aux (s::acc) tl)
+    | [] -> Some acc 
+  in  
+    aux [] (s1@s2)
+;;
+
+(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
+
+type substitution = naif_substitution
+let apply_subst = naif_apply_subst
+let apply_subst_metasenv = naif_apply_subst_metasenv
+let ppsubst ?(names=[]) l = naif_ppsubst names l
+let buildsubst = naif_buildsubst
+let flatten_subst = naif_flatten_subst
+let lookup_subst = naif_lookup_subst
+
+(* filter out from metasenv the variables in substs *)
+let filter subst metasenv =
+  List.filter
+    (fun (m, _, _) ->
+         try let _ = List.find (fun (i, _) -> m = i) subst in false
+         with Not_found -> true)
+    metasenv
+;;
+
+let is_in_subst i subst = List.mem_assoc i subst;;
+  
+let merge_subst_if_possible = naif_merge_subst_if_possible;;
+
+let empty_subst = [];;
+
+let concat_substs x y = x @ y;;
+
diff --git a/helm/software/components/tactics/paramodulation/subst.mli b/helm/software/components/tactics/paramodulation/subst.mli
new file mode 100644 (file)
index 0000000..3bbf7d0
--- /dev/null
@@ -0,0 +1,43 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type substitution 
+
+val empty_subst : substitution
+val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst : ?names:(Cic.name option list) -> substitution -> string
+val buildsubst : 
+  int -> Cic.context -> Cic.term -> Cic.term -> substitution -> 
+    substitution
+val flatten_subst : substitution -> substitution 
+val lookup_subst : Cic.term -> substitution -> Cic.term
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
+val is_in_subst : int -> substitution -> bool
+val merge_subst_if_possible: 
+  substitution -> substitution -> 
+    substitution option
+val concat_substs: substitution -> substitution -> substitution
+