snapshot

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 3f2f43df09d30d1449ec0ea2828be8b1276c0c0b..5062353cd1662876da66f1135265deffc0cbe910 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -196,8 +196,25 @@ and restrict metasenv subst i restrictions =
 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
    otherwise the occur check does not make sense in case of unification
    of ?n with ?n *)
-let delift metasenv subst context n l t =
-  let rec aux k (metasenv, subst as ms) = function
+let delift ~unify metasenv subst context n l t =
+  let unify_list = 
+    match l with
+    | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
+    | shift, NCic.Ctx l -> fun metasenv subst context k t ->
+       HExtlib.list_findopt
+        (fun li i ->
+          let li = NCicSubstitution.lift (k+shift) li in
+          match unify metasenv subst context li t with
+          | Some (metasenv,subst) -> 
+              Some ((metasenv, subst), NCic.Rel (i+1+k))
+          | None -> None)
+        l
+  in
+  let rec aux k (metasenv, subst as ms) t = 
+   match unify_list metasenv subst context k t with
+   | Some x -> x
+   | None -> 
+    match t with 
     | NCic.Rel n as t when n <= k -> ms, t
     | NCic.Rel n -> 
         (try
@@ -219,7 +236,8 @@ let delift metasenv subst context n l t =
             (NCicPp.ppterm ~context ~metasenv ~subst t))))
     | NCic.Meta (i,l1) as orig ->
         (try
-           let _,_,t,_ = NCicUtils.lookup_subst i subst in
+           let tag,_,t,_ = NCicUtils.lookup_subst i subst in
+           (match tag with None -> () | Some tag -> prerr_endline tag);
            aux k ms (NCicSubstitution.subst_meta l1 t)
          with NCicUtils.Subst_not_found _ ->
            if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli
index 033ea1b1b4f53682a419a5856380f1a46ee912bd..293e3a01f0b3d456a0110fd4daafe573fe0375a2 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.mli
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli
@@ -43,6 +43,8 @@ val restrict :
  * in the term (for occur check).
  *)
 val delift : 
+  unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
+    NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   int -> NCic.local_context -> NCic.term ->
     (NCic.metasenv * NCic.substitution) * NCic.term

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 7871d86e92052728a1828627783c0c83642fec24..8c5dcae76d0d700e5a93156faa32bdb5eae66ba0 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -309,7 +309,7 @@ let rec typeof hdb
       let resty = C.Appl (outtype::arguments@[term]) in
       let resty = NCicReduction.head_beta_reduce ~subst resty in
       metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
-    | C.Match _ as orig -> assert false
+    | C.Match _ -> assert false
     in
     pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
          NCicPp.ppterm ~metasenv ~subst ~context infty ));
@@ -586,7 +586,7 @@ let typeof_obj hdb
        uri, height, metasenv, subst, 
          C.Fixpoint (inductive, fl, attr)
 
-  | C.Inductive (ind, leftno, itl, attr) ->  assert false
+  | C.Inductive (_ind, _leftno, _itl, _attr) ->  assert false
 (*
   (* let's check if the arity of the inductive types are well formed *)
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 55ccca12a0c79dc16fc84180af3dab442dc66bb3..f23116b636d765a6460978e175da0377f0c34615 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -98,66 +98,21 @@ let fix_sorts swap metasenv subst context meta t =
     aux () t
 ;;
 
-let rec beta_expand hdb 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 hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
-     else
-      unify hdb 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 hdb test_equality_only swap metasenv subst context t args =
-(* (*D*)  inside 'B'; try let rc = *)
-  pp (lazy (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 hdb num test_equality_only swap metasenv subst context t arg
-         in
-           num+1,subst,metasenv,t)
-      args (1,subst,metasenv,t) 
-  in
-  pp (lazy ("Head syntesized by b-exp: " ^ 
-    NCicPp.ppterm ~metasenv ~subst ~context hd));
-    metasenv, subst, hd
-(* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
+let rec beta_expand_many metasenv subst context t args =
+ let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in
+ let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in
+ let rec mk_lambda context n = function
+   | [] -> 
+       let metasenv, _, bo, _ = 
+         NCicMetaSubst.mk_meta metasenv context (`WithType tty) in
+       metasenv, bo
+   | ty::tail -> 
+       let name = "HBeta"^string_of_int n in
+       let ty = NCicSubstitution.lift n ty in
+       let metasenv, bo = mk_lambda ((name,NCic.Decl ty)::context) (n+1) tail in
+       metasenv, NCic.Lambda (name, ty, bo)
+ in
+   mk_lambda context 0 argsty
 
 and instantiate hdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
@@ -214,7 +169,16 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap =
          pp (lazy(string_of_int n ^ " := 111 = "^
            NCicPp.ppterm ~metasenv ~subst ~context t));
   let (metasenv, subst), t = 
-    try NCicMetaSubst.delift metasenv subst context n lc t
+    try 
+      NCicMetaSubst.delift 
+       ~unify:(fun m s c t1 t2 -> 
+         let ind = !indent in
+         let res = 
+           try Some (unify test_eq_only m s c t1 t2 )
+           with UnificationFailure _ | Uncertain _ -> None
+         in
+         indent := ind; res) 
+       metasenv subst context n lc t
     with NCicMetaSubst.Uncertain msg -> 
          pp (lazy ("delift fails: " ^ Lazy.force msg));
          raise (Uncertain msg)
@@ -355,22 +319,26 @@ and unify hdb test_eq_only 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 hdb 
-                  test_eq_only false 
-                  metasenv subst context t2 args
+              let metasenv, beta_expanded =
+                beta_expand_many metasenv subst context t2 args
               in
+              let metasenv, subst = 
                 unify hdb test_eq_only metasenv subst context 
-                  (C.Meta (i,l)) beta_expanded 
+                  (C.Meta (i,l)) beta_expanded
+              in
+              
+              (* .... eta_reduce ?i ... *)
+                unify hdb test_eq_only metasenv subst context t1 t2 
 
        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
-              let metasenv, subst, beta_expanded =
-                beta_expand_many hdb 
-                  test_eq_only true 
-                  metasenv subst context t1 args
+              let metasenv, beta_expanded =
+                beta_expand_many metasenv subst context t1 args
               in
+              let metasenv, subst =
                 unify hdb test_eq_only metasenv subst context 
-                  beta_expanded (C.Meta (i,l))
+                 beta_expanded (C.Meta (i,l))
+              in
+                unify hdb test_eq_only metasenv subst context t1 t2 
 
        (* 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))