X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=fcc0b953e70ad9f50c6dd3a8f144867bf1261fbb;hb=189cd88a0532779547e8c10ff6f78ca93aae363a;hp=2643ce843a6a0707404d031a516c550aa86cc41d;hpb=c5b3da2ed2b2dafd22cc50edb4ac5f1d402dfa94;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 2643ce843..fcc0b953e 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -10,6 +10,459 @@
       V_______________________________________________________________ *)
 
 (* $Id$ *)
+
+exception UnificationFailure of string Lazy.t;;
+exception Uncertain of string Lazy.t;;
+exception AssertFailure of string Lazy.t;;
+
+let (===) x y = Pervasives.compare x y = 0 ;;
+
+let uncert_exc metasenv subst context t1 t2 = 
+  Uncertain (lazy (
+  "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
+  " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
+;;
+
+let fail_exc metasenv subst context t1 t2 = 
+  UnificationFailure (lazy (
+  "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
+  " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
+;;
+
+let mk_appl hd tl =
+  match hd with
+  | NCic.Appl l -> NCic.Appl (l@tl)
+  | _ -> NCic.Appl (hd :: tl)
+;;
+
+let flexible l = 
+  List.exists 
+    (function 
+       | NCic.Meta _  
+       | NCic.Appl (NCic.Meta _::_) -> true
+       | _ -> false) l
+;;
+
+exception WrongShape;;
+
+let eta_reduce = 
+  let delift_if_not_occur body orig =
+    try 
+        NCicSubstitution.psubst ~avoid_beta_redexes:true
+          (fun () -> raise WrongShape) [()] body
+    with WrongShape -> orig
+  in
+  function
+  | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
+      delift_if_not_occur hd orig
+  | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
+    when HExtlib.list_last l = NCic.Rel 1 ->
+       let body = 
+         let args, _ = HExtlib.split_nth (List.length l - 1) l in
+         NCic.Appl (hd::args)
+       in
+       delift_if_not_occur body orig
+  | t -> t
+;;
+ 
+module C = NCic;;
+module Ref = NReference;;
+
+let indent = ref "";;
+let inside c = indent := !indent ^ String.make 1 c;;
+let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+
+let pp s = 
+ prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);; 
+
+(* let pp _ = ();; *)
+
+let rec beta_expand num test_eq_only swap metasenv subst context t arg =
+  let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
+   try
+    let metasenv, subst =
+     if swap then
+      unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
+     else
+      unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
+    in
+     (metasenv, subst), NCic.Rel (1 + n)
+   with Uncertain _ | UnificationFailure _ ->
+       match t' with
+       | NCic.Rel m as orig -> 
+           (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
+       (* andrea: in general, beta_expand can create badly typed
+        terms. This happens quite seldom in practice, UNLESS we
+        iterate on the local context. For this reason, we renounce
+        to iterate and just lift *)
+       | NCic.Meta (i,(shift,lc)) ->
+           (metasenv,subst), NCic.Meta (i,(shift+1,lc))
+       | NCic.Prod (name, src, tgt) as orig ->
+           let (metasenv, subst), src1 = aux (n,context,true) acc src in 
+           let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
+           let ms, tgt1 = aux k (metasenv, subst) tgt in 
+           if src == src1 && tgt == tgt1 then ms, orig else
+           ms, NCic.Prod (name, src1, tgt1)
+       | t -> 
+           NCicUntrusted.map_term_fold_a 
+             (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
+
+  in
+  let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
+  let fresh_name = "Hbeta" ^ string_of_int num in
+  let (metasenv,subst), t1 = 
+    aux (0, context, test_eq_only) (metasenv, subst) t in
+  let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
+  try 
+    ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
+    metasenv, subst, t2
+  with NCicTypeChecker.TypeCheckerFailure _ -> 
+    metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
+
+and beta_expand_many test_equality_only swap metasenv subst context t args =
+(*D*)  inside 'B'; try let rc =
+  pp (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
+     args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+  let _, subst, metasenv, hd =
+    List.fold_right
+      (fun arg (num,subst,metasenv,t) ->
+         let metasenv, subst, t =
+           beta_expand num test_equality_only swap metasenv subst context t arg
+         in
+           num+1,subst,metasenv,t)
+      args (1,subst,metasenv,t) 
+  in
+  pp ("Head syntesized by b-exp: " ^ 
+    NCicPp.ppterm ~metasenv ~subst ~context hd);
+    metasenv, subst, hd
+(*D*)  in outside (); rc with exn -> outside (); raise exn
+
+and instantiate test_eq_only metasenv subst context n lc t swap =
+(*D*)  inside 'I'; try let rc = 
+  let unify test_eq_only m s c t1 t2 = 
+    if swap then unify test_eq_only m s c t2 t1 
+    else unify test_eq_only m s c t1 t2
+  in
+  let ty_t = 
+    try NCicTypeChecker.typeof ~subst ~metasenv context t 
+    with NCicTypeChecker.TypeCheckerFailure msg -> 
+      prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+      prerr_endline (Lazy.force msg);
+      assert false
+  in
+  let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
+  let lty = NCicSubstitution.subst_meta lc ty in
+  pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+    ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t); 
+  let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
+  let (metasenv, subst), t = 
+    try NCicMetaSubst.delift metasenv subst context n lc t
+    with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
+    |    NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg)
+  in
+  (* Unifying the types may have already instantiated n. *)
+  try
+    let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
+    let oldt = NCicSubstitution.subst_meta lc oldt in
+    (* conjecture: always fail --> occur check *)
+    unify test_eq_only metasenv subst context oldt t
+  with NCicUtils.Subst_not_found _ -> 
+    (* by cumulativity when unify(?,Type_i) 
+     * we could ? := Type_j with j <= i... *)
+    let subst = (n, (name, ctx, t, ty)) :: subst in
+    pp ("?"^string_of_int n^" := "^NCicPp.ppterm
+      ~metasenv ~subst ~context:ctx t);
+    let metasenv = 
+      List.filter (fun (m,_) -> not (n = m)) metasenv 
+    in
+    metasenv, subst
+(*D*)  in outside(); rc with exn -> outside (); raise exn
+
+and unify test_eq_only metasenv subst context t1 t2 =
+(*D*) inside 'U'; try let rc =
+   let fo_unif test_eq_only metasenv subst t1 t2 =
+   (*D*) inside 'F'; try let rc = 
+     pp ("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2);
+     if t1 === t2 then
+       metasenv, subst
+     else
+       match (t1,t2) with
+       | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
+           if NCicEnvironment.universe_leq a b then metasenv, subst
+           else raise (fail_exc 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 (fail_exc metasenv subst context t1 t2)
+       | (C.Sort C.Prop,C.Sort (C.Type _)) -> 
+           if (not test_eq_only) then metasenv, subst
+           else raise (fail_exc 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 true metasenv subst context s1 s2 in
+           unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+       | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+           let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
+           let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
+           let context = (name1, C.Def (s1,ty1))::context in
+           unify test_eq_only metasenv subst context t1 t2
+
+       | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+          (try 
+           let l1 = NCicUtils.expand_local_context l1 in
+           let l2 = NCicUtils.expand_local_context l2 in
+           let metasenv, subst, to_restrict, _ =
+            List.fold_right2 
+             (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
+                try 
+                  let metasenv, subst = 
+                   unify test_eq_only metasenv subst context 
+                    (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
+                  in
+                  metasenv, subst, to_restrict, i-1  
+                with UnificationFailure _ | Uncertain _ ->
+                  metasenv, subst, i::to_restrict, i-1)
+             l1 l2 (metasenv, subst, [], List.length l1)
+           in
+           let metasenv, subst, _ = 
+             NCicMetaSubst.restrict metasenv subst n1 to_restrict
+           in
+             metasenv, subst
+          with 
+           | Invalid_argument _ -> assert false
+           | NCicMetaSubst.MetaSubstFailure msg ->
+              try 
+                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 test_eq_only metasenv subst context term1 term2
+              with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+       | C.Meta (n,lc), t -> 
+           (try 
+             let _,_,term,_ = NCicUtils.lookup_subst n subst in
+             let term = NCicSubstitution.subst_meta lc term in
+               unify test_eq_only metasenv subst context term t
+           with NCicUtils.Subst_not_found _-> 
+             instantiate test_eq_only metasenv subst context n lc t false)
+
+       | t, C.Meta (n,lc) -> 
+           (try 
+             let _,_,term,_ = NCicUtils.lookup_subst n subst in
+             let term = NCicSubstitution.subst_meta lc term in
+               unify test_eq_only metasenv subst context t term
+           with NCicUtils.Subst_not_found _-> 
+             instantiate test_eq_only metasenv subst context n lc t true)
+
+       | 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 test_eq_only metasenv subst context (mk_appl term args) t2
+
+       | _, 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 test_eq_only metasenv subst context t1 (mk_appl term args)
+
+       |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
+          NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+            (try
+              List.fold_left2 
+                (fun (metasenv, subst) t1 t2 ->
+                  unify test_eq_only metasenv subst context t1 t2)
+                (metasenv,subst) l1 l2
+            with Invalid_argument _ -> 
+              raise (fail_exc metasenv subst context t1 t2))
+
+       | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
+           (* we verify that none of the args is a Meta, 
+              since beta expanding w.r.t a metavariable makes no sense  *)
+              let metasenv, subst, beta_expanded =
+                beta_expand_many 
+                  test_eq_only false 
+                  metasenv subst context t2 args
+              in
+                unify test_eq_only metasenv subst context 
+                  (C.Meta (i,l)) beta_expanded 
+
+       | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
+              let metasenv, subst, beta_expanded =
+                beta_expand_many 
+                  test_eq_only true 
+                  metasenv subst context t1 args
+              in
+                unify test_eq_only metasenv subst context 
+                  beta_expanded (C.Meta (i,l))
+
+       (* 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)) 
+         when Ref.eq r1 r2 ->
+           let relevance = NCicEnvironment.get_relevance r1 in
+           let relevance = match r1 with
+             | Ref.Ref (_,Ref.Con (_,_,lno)) ->
+                 let _,relevance = HExtlib.split_nth lno relevance in
+                   HExtlib.mk_list false lno @ relevance
+             | _ -> relevance
+           in
+           let metasenv, subst, _ = 
+             try
+               List.fold_left2 
+                 (fun (metasenv, subst, relevance) t1 t2 ->
+                    let b, relevance = 
+                      match relevance with b::tl -> b,tl | _ -> true, [] in
+                    let metasenv, subst = 
+                      try unify test_eq_only metasenv subst context t1 t2
+                      with UnificationFailure _ | Uncertain _ when not b ->
+                        metasenv, subst
+                    in
+                      metasenv, subst, relevance)
+                 (metasenv, subst, relevance) tl1 tl2
+             with Invalid_argument _ -> 
+               raise (uncert_exc metasenv subst context t1 t2)
+           in 
+             metasenv, subst
+
+       | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+          C.Match (ref2,outtype2,term2,pl2)) ->
+	   let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
+	   let _,_,ty,_ = List.nth itl tyno in
+	   let rec remove_prods ~subst context ty = 
+             let ty = NCicReduction.whd ~subst context ty in
+             match ty with
+             | C.Sort _ -> ty
+	     | C.Prod (name,so,ta) -> 
+                   remove_prods ~subst ((name,(C.Decl so))::context) ta
+             | _ -> assert false
+           in
+           let is_prop = 
+             match remove_prods ~subst [] ty with
+             | C.Sort C.Prop -> true
+             | _ -> false 
+           in
+	   let rec remove_prods ~subst context ty = 
+             let ty = NCicReduction.whd ~subst context ty in
+             match ty with
+             | C.Sort _ -> ty
+	     | C.Prod (name,so,ta) -> 
+                   remove_prods ~subst ((name,(C.Decl so))::context) ta
+             | _ -> assert false
+           in
+           if not (Ref.eq ref1 ref2) then 
+             raise (uncert_exc metasenv subst context t1 t2) 
+           else
+             let metasenv, subst = 
+               unify test_eq_only metasenv subst context outtype1 outtype2 in
+             let metasenv, subst = 
+               try unify test_eq_only metasenv subst context term1 term2 
+               with UnificationFailure _ | Uncertain _ when is_prop -> 
+                 metasenv, subst
+             in
+             (try
+              List.fold_left2 
+               (fun (metasenv,subst) -> 
+                  unify test_eq_only metasenv subst context)
+               (metasenv, subst) pl1 pl2
+             with Invalid_argument _ -> 
+               raise (uncert_exc metasenv subst context t1 t2))
+       | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+       | _ -> raise (uncert_exc metasenv subst context t1 t2)
+    (*D*)  in outside(); rc with exn -> outside (); raise exn
+    in
+    let height_of = function
+     | NCic.Const (Ref.Ref (_,Ref.Def h)) 
+     | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) 
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) 
+     | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+     | _ -> 0
+    in
+    let put_in_whd m1 m2 =
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+      NCicReduction.reduce_machine ~delta:max_int ~subst context m2,
+      false (* not in normal form *)
+    in
+    let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = 
+      let h1 = height_of t1 in 
+      let h2 = height_of t2 in
+      let delta = 
+        if flexible [t1] then max 0 (h2 - 1) else
+        if flexible [t2] then max 0 (h1 - 1) else
+        if h1 = h2 then max 0 (h1 -1) else min h1 h2 
+      in
+      pp ("DELTA STEP TO: " ^ string_of_int delta);
+      let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+      let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+      if (m1' == m1 && m2' == m2 && delta > 0) then
+         (* if we have as heads a Fix of height n>m>0 and another term of height
+          * m, we set delta = m. The Fix may or may not reduce, depending on its
+          * rec argument. if no reduction was performed we decrease delta to m-1
+          * to reduce the other term *)
+         let delta = delta - 1 in
+         pp ("DELTA STEP TO: " ^ string_of_int delta);
+         let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in
+         let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in
+         m1', m2', (m1 == m1' && m2 == m2') || delta = 0
+      else m1', m2', delta = 0
+    in
+    let rec unif_machines metasenv subst = 
+      function
+      | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
+    (*D*) inside 'M'; try let rc =
+         pp ((if are_normal then "*" else " ") ^ " " ^
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
+           " === " ^ 
+           NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
+          let relevance = [] (* TO BE UNDERSTOOD 
+            match t1 with
+            | C.Const r -> NCicEnvironment.get_relevance r
+            | _ -> [] *) in
+          let unif_from_stack t1 t2 b metasenv subst =
+              try
+                let t1 = NCicReduction.from_stack t1 in
+                let t2 = NCicReduction.from_stack t2 in
+                unif_machines metasenv subst (put_in_whd t1 t2)
+              with UnificationFailure _ | Uncertain _ when not b ->
+                metasenv, subst
+          in
+          let rec check_stack l1 l2 r (metasenv, subst) =
+            match l1,l2,r with
+            | x1::tl1, x2::tl2, r::tr ->
+                check_stack tl1 tl2 tr 
+                  (unif_from_stack x1 x2 r metasenv subst)
+            | x1::tl1, x2::tl2, [] ->
+                check_stack tl1 tl2 [] 
+                  (unif_from_stack x1 x2 true metasenv subst)
+            | l1, l2, _ -> 
+                fo_unif test_eq_only metasenv subst
+                   (NCicReduction.unwind (k1,e1,t1,List.rev l1)) 
+                   (NCicReduction.unwind (k2,e2,t2,List.rev l2))
+          in
+        try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
+        with UnificationFailure _ | Uncertain _ when not are_normal ->
+(*
+          let delta = delta - 1 in 
+          let red = NCicReduction.reduce_machine ~delta ~subst context in
+*)
+          unif_machines metasenv subst (small_delta_step m1 m2)
+     (*D*)  in outside(); rc with exn -> outside (); raise exn
+     in
+     try fo_unif test_eq_only metasenv subst t1 t2
+     with UnificationFailure msg | Uncertain msg as exn -> 
+       try 
+         unif_machines metasenv subst 
+          (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
+       with 
+       | UnificationFailure _ -> raise (UnificationFailure msg)
+       | Uncertain _ -> raise exn
+(*D*)  in outside(); rc with exn -> outside (); raise exn
+;;
+
+let unify = 
+  indent := "";      
+  unify false;;
+
+
+
 (* 
 
 open Printf