Very serious bug fixed in unification, but the fix is very ugly.

Explanation: we have reduced the case ? x1 .. xn to the case
?[x1,...,xn] by mean of lambda-abstractions. However, these need to be
typed. The way we used to type them was with non-dependent types. Thus they
failed in almost all dependent cases (like rewrite).

This fix seems to work and uses a few lines of code, but it requires a call
to the unifier which is VEEERY bad.

Debugging prints still to be removed.

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8872cbc9b576f855a8f65334addc871864e3bc6c..2b648d85781a0f6cc8ce407eb9322a14f02d4df8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -745,4 +745,6 @@ let typeof_obj
       uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
 ;;
 
+NCicUnification.set_refiner_typeof typeof;;
+
 (* vim:set foldmethod=marker: *)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 13ddac96d9be7e7995ae4ddc1b1aa105e6d701c6..71203b3a5dccdf2b3c5207677f2df501c6eb4084 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -15,6 +15,11 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+let refiner_typeof =
+ ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);;
+let set_refiner_typeof f = refiner_typeof := f
+;;
+
 let (===) x y = Pervasives.compare x y = 0 ;;
 
 let uncert_exc metasenv subst context t1 t2 = 
@@ -80,7 +85,12 @@ 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 outside () =
+ try
+  indent := String.sub !indent 0 (String.length !indent -1)
+ with
+  Invalid_argument _ -> indent := "??"; ()
+;;
 
 let pp s = 
   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
@@ -89,8 +99,8 @@ let pp s =
 let ppcontext = NCicPp.ppcontext;;
 let ppmetasenv = NCicPp.ppmetasenv;;
 
-(*let ppcontext ~metasenv ~subst context = "...";;
-let ppmetasenv ~subst metasenv = "...";;*)
+let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "...";;
+let ppmetasenv ~subst:_subst _metasenv = "...";;
 
 let pp _ = ();;
 
@@ -121,24 +131,51 @@ let is_locked n subst =
    with NCicUtils.Subst_not_found _ -> false
 ;;
 
+let rec mk_irl =
+ function
+    0 -> []
+  | n -> NCic.Rel n :: mk_irl (n-1)
+;;
 
-let rec lambda_intros metasenv subst context t args =
+let rec lambda_intros rdb 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 argsty =
+  List.map
+  (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in
+ let context_of_args = context in
+ let mk_appl = function [] -> assert false | [t] -> t | l -> NCic.Appl l in
+ let rec mk_lambda metasenv subst context n processed_args = function
+   | [] ->
        let metasenv, _, bo, _ = 
          NCicMetaSubst.mk_meta metasenv context 
            (`WithType (NCicSubstitution.lift n tty))
        in
-       metasenv, bo
-   | ty::tail -> 
+       metasenv, subst, bo
+   | (arg,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)
+       let metasenv,_,instance,_ =
+        NCicMetaSubst.mk_meta metasenv context_of_args `Term in
+       let meta_applied = mk_appl (instance::List.rev processed_args) in
+let metasenv,subst,_,_ =
+ !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None
+in
+prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty);
+prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args);
+prerr_endline (NCicPp.ppmetasenv metasenv ~subst);
+       let metasenv,subst =
+        unify rdb true metasenv subst context_of_args meta_applied ty in
+prerr_endline "UNIFY FINITA";
+       let telescopic_ty = NCicSubstitution.lift n instance in
+       let telescopic_ty =
+        mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in
+prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty);
+       let metasenv, subst, bo =
+        mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1)
+         (arg::processed_args) tail
+       in
+        metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
  in
-   mk_lambda context 0 argsty
+   mk_lambda metasenv subst context 0 [] argsty
 
 and instantiate rdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
@@ -314,9 +351,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               | NCic.Appl (NCic.Meta (i,l)::args) when
                   not (NCicMetaSubst.flexible subst args) 
                 ->
-                 let metasenv, lambda_Mj =
-                   lambda_intros metasenv subst context t1 args
+                 let metasenv, subst, lambda_Mj =
+                   lambda_intros rdb metasenv subst context t1 args
                  in
+prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj);
                    unify rdb test_eq_only metasenv subst context 
                     (C.Meta (i,l)) lambda_Mj,
                    i
@@ -395,8 +433,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
          not (NCicMetaSubst.flexible subst args) ->
            (* we verify that none of the args is a Meta, 
               since beta expanding w.r.t a metavariable makes no sense  *)
-              let metasenv, lambda_Mj =
-                lambda_intros metasenv subst context t1 args
+              let metasenv, subst, lambda_Mj =
+                lambda_intros rdb metasenv subst context t1 args
               in
               let metasenv, subst = 
                 unify rdb test_eq_only metasenv subst context 
@@ -414,8 +452,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
 
        | _, NCic.Appl (NCic.Meta (i,l)::args) when 
          not(NCicMetaSubst.flexible subst args) ->
-              let metasenv, lambda_Mj =
-                lambda_intros metasenv subst context t2 args
+              let metasenv, subst, lambda_Mj =
+                lambda_intros rdb metasenv subst context t2 args
               in
               let metasenv, subst =
                 unify rdb test_eq_only metasenv subst context 

diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index a6ddfaeed2009b04f95c9c37dd3b3d5a1886b2b6..47a59d4f2a88021c83e8c960de893aa71efbdafb 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -15,6 +15,13 @@ exception UnificationFailure of string Lazy.t;;
 exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
+val set_refiner_typeof:
+ (NRstatus.status ->
+   ?localise:(NCic.term -> Stdpp.location) ->
+   NCic.metasenv -> NCic.substitution -> NCic.context ->
+   NCic.term -> NCic.term option -> (* term, expected type *)
+     NCic.metasenv * NCic.substitution * NCic.term * NCic.term) -> unit
+
 val unify :
   #NRstatus.status ->
   ?test_eq_only:bool -> (* default: false *)