]> matita.cs.unibo.it Git - helm.git/commitdiff
some fixed done in Orsay:
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 15 Jun 2006 09:37:49 +0000 (09:37 +0000)
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)

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

index 3bff5b57460bc4decc952b913a83f4c410fb4d29..2be5da0627d07d7c390ba622ea4d692ab6751c40 100644 (file)
@@ -223,7 +223,7 @@ let open_eq_ind args =
 
 let open_pred pred =
   match pred with 
-  | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) 
+  | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) 
      when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
   | _ -> prerr_endline (CicPp.ppterm pred); assert false   
 ;;
@@ -336,15 +336,16 @@ let contextualize uri ty left right t =
    * that is used only by the base case
    *
    * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
+   * ty_ctx is the type of ctx_d
    *)
-    let rec aux uri ty left right ctx_d = function
+    let rec aux uri ty left right ctx_d ctx_ty = function
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
         when LibraryObjects.is_sym_eq_URI uri_sym  ->
           let ty,l,r,p = open_sym ens tl in
-          mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+          mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
       | Cic.LetIn (name,body,rest) ->
           (* we should go in body *)
-          Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+          Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest)
       | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
         when LibraryObjects.is_eq_ind_URI uri_ind || 
              LibraryObjects.is_eq_ind_r_URI uri_ind ->
@@ -355,12 +356,13 @@ let contextualize uri ty left right t =
           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, ty2 = 
             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 m =  CicSubstitution.subst hole m in
             let ctx_c = CicSubstitution.subst hole ctx_c in
-            m, ctx_c          
+            let ty2 = CicSubstitution.subst hole ty2 in
+            m, ctx_c, ty2          
           in
           (* create the compound context and put the terms under it *)
           let ctx_dc = compose_contexts ctx_d ctx_c in
@@ -373,17 +375,17 @@ let contextualize uri ty left right t =
           (* 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 
+              aux uri ty2 c_what m ctx_d ctx_ty p1 
             else
-              mk_sym uri_sym ty d_m dc_what
-                (aux uri ty1 m c_what ctx_d p1)
+              mk_sym uri_sym ctx_ty d_m dc_what
+                (aux uri ty2 m c_what ctx_d ctx_ty 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)
+              mk_sym uri_sym ctx_ty dc_what dc_other
+                (aux uri ty1 what other ctx_dc ctx_ty p2)
             else
-              aux uri ty1 other what ctx_dc p2
+              aux uri ty1 other what ctx_dc ctx_ty 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 *)
@@ -392,10 +394,11 @@ let contextualize uri ty left right t =
               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)
+                (mk_sym uri_sym ctx_ty dc_what d_m p1),
+                (mk_sym uri_sym ctx_ty dc_other dc_what p2)
           in
-          mk_trans uri_trans ty a b c paeqb pbeqc
+          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
@@ -406,16 +409,16 @@ let contextualize uri ty left right t =
             let ctx_d = CicSubstitution.lift 1 ctx_d in
             put_in_ctx ctx_d (Cic.Rel 1)
           in
-          let lty = CicSubstitution.lift 1 ty in 
+          let lty = CicSubstitution.lift 1 ctx_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
+        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)
   in
-  aux uri ty left right hole t
+  aux uri ty left right hole ty t
 ;;
 
 let contextualize_rewrites t ty = 
@@ -729,9 +732,8 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-    (proof,se)
-  (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
-   se *)
+   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   se 
 ;;
 
 let refl_proof ty term = 
@@ -789,6 +791,7 @@ let meta_convertibility_aux table t1 t2 =
   let rec aux ((table_l, table_r) as table) t1 t2 =
     match t1, t2 with
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
+        let tl1, tl2 = [],[] in
         let m1_binding, table_l =
           try List.assoc m1 table_l, table_l
           with Not_found -> m2, (m1, m2)::table_l
index e72ed64dad3c37c9620a97ec7576784bf3cb80ae..925aab6e05d3663ba3d01eabca3cf11e43b16ac8 100644 (file)
@@ -728,6 +728,7 @@ let rec betaexpand_term
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->
+        let l = [] in
         let l', lifted_l =
           List.fold_right
             (fun arg (res, lifted_tl) ->
@@ -1057,11 +1058,23 @@ let superposition_left (metasenv, context, ugraph) table goal =
     Utils.compare_weights ~normalize:true
       (Utils.weight_of_term l) (Utils.weight_of_term r)
   in
-  let big,small,possmall = 
-    match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
-  in
-  let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-  List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+  
+  if c = Utils.Incomparable then
+    let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+    let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+    prerr_endline "ZZZ";
+    prerr_endline (string_of_int (List.length expansionsl));
+    prerr_endline (string_of_int (List.length expansionsr));
+    List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+    @
+    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+  else
+    let big,small,possmall = 
+      match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+    in
+    let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+    List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
 ;;
 
 (** demodulation, when the target is a goal *)
index 91fcee8a22833b645784a6e62ef03996e41d8f56..6004de44ceb29ef815daf390b824678aa8863ef3 100644 (file)
@@ -51,7 +51,7 @@ let rec check_irl start = function
 let rec is_simple_term = function
   | Cic.Appl ((Cic.Meta _)::_) -> false
   | Cic.Appl l -> List.for_all is_simple_term l
-  | Cic.Meta (i, l) -> check_irl 1 l
+  | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
   | Cic.Rel _ -> true
   | Cic.Const _ -> true
   | Cic.MutInd (_, _, []) -> true
index 1282ed27f1cd9f9726baccb892c06dd3c73ee6fb..fe63c7d669abed002c73b8876b60bba5abd0f834 100644 (file)
@@ -708,7 +708,6 @@ let backward_simplify env new' ?passive active =
       active, passive, newa, newp *)
 ;;
 
-
 let close env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
@@ -1202,6 +1201,17 @@ let check_if_goal_is_identity env = function
     when left = right && iseq uri ->
       let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
       Some (goalproof, reflproof, 0, Subst.empty_subst,m)
+  | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) 
+    when iseq uri ->
+    (let _,context,_ = env in
+    try 
+     let s,m,_ = 
+       Inference.unification m m context left right CicUniv.empty_ugraph 
+     in
+      let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in
+      let m = Subst.apply_subst_metasenv s m in
+      Some (goalproof, reflproof, 0, s,m)
+    with _ -> None)
   | _ -> None
 ;;                              
     
@@ -1270,10 +1280,16 @@ let infer_goal_set env active goals =
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
   let _,table,_ = build_table [current] in
+  let _,_,_,_,id = Equality.open_equality current in
   active_goals,
   List.fold_left 
     (fun acc g ->
       let new' = Indexing.superposition_left env table g in
+      if id = 2 then
+        begin
+        prerr_endline "XXXXXXX";
+        List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ;
+       end;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1288,6 +1304,7 @@ let size_of_goal_set_p (_,l) = List.length l;;
 let given_clause 
   ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
+  let names = names_of_context context in
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
     let now = Unix.gettimeofday () in
@@ -1339,13 +1356,18 @@ let given_clause
             ParamodulationFailure "No more passive"(*maybe this is a success! *)
           else
             begin
+              let goals = infer_goal_set env active goals in
+              let goals = infer_goal_set env active goals in
               let goals = infer_goal_set env active goals in
               let current, passive = select env goals passive in
+              let _,_,goaltype = List.hd (fst goals) in                
+              prerr_endline (Printf.sprintf  "Current goal = %s\n"
+                (CicPp.pp goaltype names));
               prerr_endline (Printf.sprintf  "Selected = %s\n"
                 (Equality.string_of_equality ~env current));
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
-                forward_simplify env (Positive, current) ~passive active 
+                forward_simplify env (Positive, current) (*~passive*) active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
@@ -1376,6 +1398,14 @@ let given_clause
                     | Some p, Some rp -> simplify (new' @ p @ rp) active passive
                   in
                   let active, passive, new' = simplify new' active passive in
+                  if iterno = 36 || iterno = 654 then
+                   begin 
+                     prerr_endline "...................";
+                     List.iter 
+                       (fun x -> prerr_endline (Equality.string_of_equality 
+~env:env x)) new';
+                     prerr_endline "FINE...................";
+                   end;
                   prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
@@ -1732,6 +1762,8 @@ let saturate
         let initial = Equality.add_subst subsumption_subst newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
+      let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+      let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
       (* ?? *)
       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
@@ -1750,7 +1782,10 @@ let saturate
                | None ->
                    [i,context,ty], (Cic.Meta(i,[]))::acc2, 
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
-          ([],[],[],None) proof_menv 
+          ([],[],[],None) 
+          (List.filter 
+          (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