- Added a swap parameter to the unification procedure

- Fixed a bug in the metavariable restriction algorithm, which resulted in bad
  metavariable local contexts.

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index ce0021d3d660d322b5cc1cf2466a2a5e93ffe066..549f06f85b57845c97737b609855b5b95fd016cc 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -133,27 +133,33 @@ let rec force_does_not_occur metasenv subst restrictions t =
          NCicUtils.Subst_not_found _ ->
           (* we ignore the subst since restrict will take care of already
            * instantiated/restricted metavariabels *)
-          let (metasenv,subst as ms), restrictions_for_n, l' =
-            let l = NCicUtils.expand_local_context lc in
-         
-            let ms, _, restrictions_for_n, l =
+          let l = NCicUtils.expand_local_context lc in
+          let sl = List.map (NCicSubstitution.lift shift) l in 
+          let (metasenv,subst as ms), _, restrictions_for_n, l' =
              List.fold_right
                (fun t (ms, i, restrictions_for_n, l) ->
                  try 
-                   let ms, t = aux (k-shift) ms t in
+              (*pp (lazy ("L'ORLO DELLA FOSSA: k= " ^ string_of_int k ^ " shift=" ^
+               string_of_int shift ^ " t=" ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
+                   let ms, t = aux k ms t in
+              (*pp (lazy ("LA FOSSA: " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] t));*)
                    ms, i-1, restrictions_for_n, t::l
                  with Occur ->
                    ms, i-1, i::restrictions_for_n, l)
-               l (ms, List.length l, [], [])
-            in
-                
-             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
+               sl (ms, List.length l, [], [])
           in
           if restrictions_for_n = [] then
-            ms, if l = l' then orig else NCic.Meta (n, l')
+            ms, if sl = l' then orig else (
+                (*pp (lazy ("FINITO: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[]
+                  ~context:[] (NCic.Meta (n,pack_lc (0, NCic.Ctx l')))));*)
+              NCic.Meta (n, pack_lc (0, NCic.Ctx l'))
+            )
           else
+            let l' = pack_lc (0, NCic.Ctx l') in
+            let _ = pp (lazy ("restrictions for n are:" ^ String.concat "," (List.map string_of_int restrictions_for_n))) in
             let metasenv, subst, newmeta, more_restricted = 
               restrict metasenv subst n restrictions_for_n in
+            let _ = pp (lazy ("more restricted: " ^String.concat "," (List.map string_of_int more_restricted))) in
             let l' = purge_restricted restrictions more_restricted l' in
               (metasenv, subst), NCic.Meta (newmeta, l'))
     | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
@@ -162,6 +168,8 @@ let rec force_does_not_occur metasenv subst restrictions t =
 
 and force_does_not_occur_in_context metasenv subst restrictions = function
   | name, NCic.Decl t as orig ->
+      (* pp (lazy ("CCC: hd is" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t ^
+      "\nCCC: restrictions are:" ^ String.concat "," (List.map string_of_int restrictions)));*)
       let (metasenv, subst), t' =
         force_does_not_occur metasenv subst restrictions t in
       metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
@@ -234,6 +242,9 @@ and restrict metasenv subst i (restrictions as orig) =
         let reloc_irl = 
           mk_perforated_irl 0 (List.length ctx) restrictions in
         let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
+         (* pp (lazy ("BBB: dopo1 \n" ^  NCicPp.ppsubst ~metasenv [subst_entry]));
+          pp (lazy ("BBB: dopo2 \n" ^  NCicPp.ppsubst ~metasenv (subst_entry::subst)));
+          pp (lazy ("BBB: dopo metasenv\n" ^  NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         List.map 
           (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 0f73dbc5c9e5f0fd268010092448dbce9c5b9e48..805ea859f8beef8be33eb03d123b850f37a5c48e 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -288,7 +288,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
          ~unify:(fun m s c t1 t2 -> 
            let ind = !indent in
            let res = 
-                   try Some (unify rdb test_eq_only m s c t1 t2 )
+             try Some (unify rdb test_eq_only m s c t1 t2 false)
              with UnificationFailure _ | Uncertain _ -> None
            in
            indent := ind; res) 
@@ -308,7 +308,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
       let oldt = NCicSubstitution.subst_meta lc oldt in
       let t = NCicSubstitution.subst_meta lc t in
       (* conjecture: always fail --> occur check *)
-      unify rdb test_eq_only metasenv subst context t oldt
+      unify rdb test_eq_only metasenv subst context t oldt false
     with NCicUtils.Subst_not_found _ -> 
       move_to_subst n (attrs,cc,t,ty) metasenv subst
   in
@@ -348,7 +348,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
             ppterm ~metasenv ~subst ~context ty ^ "=<=" ^
             ppterm ~metasenv ~subst ~context ty_t)); 
           let metasenv, subst = 
-            unify rdb false metasenv subst context ty_t ty in
+            unify rdb false metasenv subst context ty_t ty false in
           delift_to_subst test_eq_only n lc (attrs,cc,ty) t
            context metasenv subst
        | _ -> assert false)
@@ -361,7 +361,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
               NCicMetaSubst.delift 
                ~unify:(fun m s c t1 t2 -> 
                  let ind = !indent in
-                 let res = try Some (unify rdb test_eq_only m s c t1 t2 )
+                 let res = try Some (unify rdb test_eq_only m s c t1 t2 false )
                    with UnificationFailure _ | Uncertain _ -> None
                  in
                  indent := ind; res)
@@ -381,20 +381,24 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
           ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
           ppterm ~metasenv ~subst ~context ty_t)); 
         let metasenv, subst = 
-          unify rdb false metasenv subst context ty_t lty
+          unify rdb false metasenv subst context ty_t lty false
         in
         delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv
          subst)
  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
 
-and unify rdb test_eq_only metasenv subst context t1 t2 =
+and unify rdb test_eq_only metasenv subst context t1 t2 swap =
  (*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
     (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+     pp (lazy("  " ^ ppterm ~metasenv ~subst ~context t1 ^ 
+          (if swap then " ==>?== " 
+           else " ==<?==" ) ^ 
          ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
          ~subst metasenv));
-     pp (lazy("  " ^ ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
+     pp (lazy("  " ^ ppterm ~metasenv ~subst:[] ~context t1 ^
+          (if swap then " ==>??== " 
+           else " ==<??==" ) ^ 
          ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
          ~subst metasenv));
      if t1 === t2 then
@@ -415,25 +419,29 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
        | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
            prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
            assert false 
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
+       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
+           let a, b = if swap then b,a else a,b in
            if NCicEnvironment.universe_leq a b then metasenv, subst
            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
        | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
            if NCicEnvironment.universe_eq a b then metasenv, subst
            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
-       | (C.Sort C.Prop,C.Sort (C.Type _)) -> 
+       | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
+           if (not test_eq_only) then metasenv, subst
+           else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+       | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
            if (not test_eq_only) then metasenv, subst
            else raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
 
        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           let metasenv, subst = unify rdb true metasenv subst context s1 s2 in
-           unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+           let metasenv, subst = unify rdb true metasenv subst context s1 s2 swap in
+           unify rdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
-           let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 in
-           let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 in
+           let metasenv,subst=unify rdb test_eq_only metasenv subst context ty1 ty2 swap in
+           let metasenv,subst=unify rdb test_eq_only metasenv subst context s1 s2 swap in
            let context = (name1, C.Def (s1,ty1))::context in
-           unify rdb test_eq_only metasenv subst context t1 t2
+           unify rdb test_eq_only metasenv subst context t1 t2 swap
 
        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
           (try 
@@ -444,8 +452,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
              (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
                 try 
                   let metasenv, subst = 
-                   unify rdb test_eq_only metasenv subst context 
+                   unify rdb (*test_eq_only*) true metasenv subst context
                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
+                     swap
                   in
                   metasenv, subst, to_restrict, i-1  
                 with UnificationFailure _ | Uncertain _ ->
@@ -465,7 +474,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
                 let term1 = NCicSubstitution.subst_meta lc1 term in
                 let term2 = NCicSubstitution.subst_meta lc2 term in
-                  unify rdb test_eq_only metasenv subst context term1 term2
+                  unify rdb test_eq_only metasenv subst context term1 term2 swap
               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 
        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
@@ -473,12 +482,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
             (try
               List.fold_left2 
                 (fun (metasenv, subst) t1 t2 ->
-                  unify rdb test_eq_only metasenv subst context t1 t2)
+                  unify rdb (*test_eq_only*) true metasenv subst context t1 
+                    t2 swap)
                 (metasenv,subst) l1 l2
             with Invalid_argument _ -> 
               raise (UnificationFailure (mk_msg metasenv subst context t1 t2)))
        
-       | _, NCic.Meta (n, _) when is_locked n subst ->
+       | _, NCic.Meta (n, _) when is_locked n subst && not swap->
            (let (metasenv, subst), i = 
               match NCicReduction.whd ~subst context t1 with
               | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
@@ -487,7 +497,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                     (NCicTypeChecker.typeof ~metasenv ~subst context meta)
                  in
                    unify rdb test_eq_only metasenv subst context 
-                    (C.Meta (i,l)) lambda_Mj,
+                    (C.Meta (i,l)) lambda_Mj false,
                    i
               | NCic.Meta (i,_) -> (metasenv, subst), i
               | _ ->
@@ -518,36 +528,30 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                 let subst = List.filter (fun (j,_) -> j <> i) subst in
                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
               with Not_found -> assert false))
-
-       | C.Meta (n,lc), t when List.mem_assoc n subst -> 
-          let _,_,term,_ = NCicUtils.lookup_subst n subst in
-          let term = NCicSubstitution.subst_meta lc term in
-            unify rdb test_eq_only metasenv subst context term t
+       | NCic.Meta (n, _), _ when is_locked n subst && swap ->
+           unify rdb test_eq_only metasenv subst context t2 t1 false
 
        | t, C.Meta (n,lc) when List.mem_assoc n subst -> 
           let _,_,term,_ = NCicUtils.lookup_subst n subst in
           let term = NCicSubstitution.subst_meta lc term in
-            unify rdb test_eq_only metasenv subst context t term
-
-       | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
-            let _,_,term,_ = NCicUtils.lookup_subst i subst in
-            let term = NCicSubstitution.subst_meta l term in
-              unify rdb test_eq_only metasenv subst context 
-                (mk_appl ~upto:(List.length args) term args) t2
+            unify rdb test_eq_only metasenv subst context t term swap
+       | C.Meta (n,_), _ when List.mem_assoc n subst -> 
+            unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
 
        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
             let _,_,term,_ = NCicUtils.lookup_subst i subst in
             let term = NCicSubstitution.subst_meta l term in
               unify rdb test_eq_only metasenv subst context t1 
-                (mk_appl ~upto:(List.length args) term args)
+                (mk_appl ~upto:(List.length args) term args) swap
+       | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
+            unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
 
        | C.Meta (n,lc), t -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
-            (NCicReduction.head_beta_reduce ~subst t) false
-
+            (NCicReduction.head_beta_reduce ~subst t) swap
        | t, C.Meta (n,lc) -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
-           (NCicReduction.head_beta_reduce ~subst t) true
+           (NCicReduction.head_beta_reduce ~subst t) (not swap)
 
        | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
           let metasenv, lambda_Mj =
@@ -557,13 +561,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
           let metasenv, subst = 
            try
             unify rdb test_eq_only metasenv subst context 
-              (C.Meta (i,l)) lambda_Mj
+              (C.Meta (i,l)) lambda_Mj swap
            with UnificationFailure msg | Uncertain msg when not norm2->
             (* failure: let's try again argument vs argument *)
             raise (KeepReducing msg)
           in
           let metasenv, subst = 
-            unify rdb test_eq_only metasenv subst context t1 t2 
+            unify rdb test_eq_only metasenv subst context t1 t2 swap
           in
           (try
             let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
@@ -571,29 +575,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
             let subst = List.filter (fun (j,_) -> j <> i) subst in
             metasenv, ((i, (name, ctx, term, ty)) :: subst)
           with Not_found -> assert false)
-
-       | _, NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
-         let metasenv, lambda_Mj =
-           lambda_intros rdb metasenv subst context (List.length args)
-             (NCicTypeChecker.typeof ~metasenv ~subst context meta)
-         in
-         let metasenv, subst =
-          try
-           unify rdb test_eq_only metasenv subst context 
-            lambda_Mj (C.Meta (i,l))
-          with UnificationFailure msg | Uncertain msg when not norm1 ->
-           (* failure: let's try again argument vs argument *)
-           raise (KeepReducing msg)
-         in
-         let metasenv, subst = 
-           unify rdb test_eq_only metasenv subst context t1 t2 
-         in
-         (try
-           let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-           let term = eta_reduce subst term in
-           let subst = List.filter (fun (j,_) -> j <> i) subst in
-           metasenv, ((i, (name, ctx, term, ty)) :: subst)
-         with Not_found -> assert false)
+       | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
+           unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
 
        (* processing this case here we avoid a useless small delta step *)
        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
@@ -607,6 +590,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                       match relevance with b::tl -> b,tl | _ -> true, [] in
                     let metasenv, subst = 
                       try unify rdb test_eq_only metasenv subst context t1 t2
+                            swap
                       with UnificationFailure _ | Uncertain _ when not b ->
                         metasenv, subst
                     in
@@ -642,16 +626,16 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
              raise (Uncertain (mk_msg metasenv subst context t1 t2))
            else
              let metasenv, subst = 
-              unify rdb test_eq_only metasenv subst context outtype1 outtype2 in
+              unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
              let metasenv, subst = 
-               try unify rdb test_eq_only metasenv subst context term1 term2 
+               try unify rdb test_eq_only metasenv subst context term1 term2 swap
                with UnificationFailure _ | Uncertain _ when is_prop -> 
                  metasenv, subst
              in
              (try
               List.fold_left2 
-               (fun (metasenv,subst) -> 
-                  unify rdb test_eq_only metasenv subst context)
+               (fun (metasenv,subst) t1 t2 -> 
+                  unify rdb test_eq_only metasenv subst context t1 t2 swap)
                (metasenv, subst) pl1 pl2
              with Invalid_argument _ -> assert false)
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
@@ -692,7 +676,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               let metasenv,subst = 
                 List.fold_left 
                   (fun (metasenv, subst) (x,y) ->
-                     unify rdb test_eq_only metasenv subst context x y)
+                     unify rdb test_eq_only metasenv subst context x y false)
                   (metasenv, subst) premises
               in
               pp(lazy("FUNZIONA!"));
@@ -824,7 +808,7 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
       ~unify:(fun m s c t1 t2 -> 
          let ind = !indent in
          let res = 
-           try Some (unify rdb false m s c t1 t2 )
+           try Some (unify rdb false m s c t1 t2 false)
            with UnificationFailure _ | Uncertain _ -> None
          in
          indent := ind; res)
@@ -837,9 +821,9 @@ and delift_type_wrt_terms rdb metasenv subst context t args =
 ;;
 
 
-let unify rdb ?(test_eq_only=false) = 
+let unify rdb ?(test_eq_only=false) ?(swap=false) metasenv subst context t1 t2= 
   indent := "";      
-  unify rdb test_eq_only;;
+  unify rdb test_eq_only metasenv subst context t1 t2 swap;;
 
 let fix_sorts m s =
   fix m s true false (UnificationFailure (lazy "no sup"))

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 954f56e58ee86a895acdd0b074cab1525cfcc492..4296102184017bff35f9afa84a7ceff5ea97de1c 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -18,6 +18,7 @@ exception AssertFailure of string Lazy.t;;
 val unify :
   #NRstatus.status ->
   ?test_eq_only:bool -> (* default: false *)
+  ?swap:bool -> (* default: false *)
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term ->
    NCic.metasenv * NCic.substitution