some fixes here and there

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index d168ba5488d9ffa1ccf92311887ab05da4767cba..757041451bbe7978aeb30d0dcdaf88cdf35663d8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -12,7 +12,7 @@
 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
 
 let debug s = prerr_endline (Lazy.force s);;
-let debug _ = ();;
+(* let debug _ = ();; *)
 
 module COT : Set.OrderedType 
 with type t = string * NCic.term * int * int  * NCic.term *
@@ -98,10 +98,13 @@ let index_old_db odb (status : #status) =
 
 let look_for_coercion status metasenv subst context infty expty =
  let db_src,db_tgt = status#coerc_db in
-  match infty, expty with
+  match 
+    NCicUntrusted.apply_subst subst context infty, 
+    NCicUntrusted.apply_subst subst context expty 
+  with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
-  | _ ->
+  | infty, expty ->
 
     debug (lazy ("LOOK FOR COERCIONS: " ^ 
       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
@@ -122,6 +125,16 @@ let look_for_coercion status metasenv subst context infty expty =
           CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
         CoercionSet.empty tgt_class
     in
+
+    debug (lazy ("CANDIDATES SRC: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_src))));
+    debug (lazy ("CANDIDATES TGT: " ^ 
+      String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+        name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) 
+      (CoercionSet.elements set_tgt))));
+
     let candidates = CoercionSet.inter set_src set_tgt in
 
     debug (lazy ("CANDIDATES: " ^ 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index a3316294712c0fdffa0eafbcfddd18bb65ce7a6a..5a6f1028fdf9a4ad177a2483961a090096f8a697 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -126,10 +126,9 @@ let rec typeof rdb
   let rec typeof_aux metasenv subst context expty = 
     fun t as orig -> 
     (*D*)inside 'R'; try let rc = 
-    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
-    pp (lazy (if expty = None then "NONE" else "SOME"));
-    if (List.exists (fun (i,_) -> i=29) subst) then 
-      pp (lazy (NCicPp.ppsubst ~metasenv subst));
+    pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " expty= " ^
+       match expty with None -> "None" | Some e -> 
+       NCicPp.ppterm ~metasenv ~subst ~context e));
     let metasenv, subst, t, infty = 
     match t with
     | C.Rel n ->
@@ -202,7 +201,10 @@ let rec typeof rdb
        let (metasenv,subst), exp_ty_t = 
          match exp_s with 
          | Some exp_s -> 
-             (try NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t
+             (try 
+               pp(lazy("Force source to: "^NCicPp.ppterm ~metasenv ~subst
+                  ~context exp_s));
+               NCicUnification.unify rdb metasenv subst context s exp_s,exp_ty_t
              with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
                "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
                ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
@@ -234,13 +236,26 @@ let rec typeof rdb
        metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
     | C.Appl ((he as orig_he)::(_::_ as args)) ->
        let upto = match orig_he with C.Meta _ -> List.length args | _ -> 0 in
-       let metasenv, subst, he, ty_he = 
-         typeof_aux metasenv subst context None he in
-       let metasenv, subst, t, ty = 
-         eat_prods rdb ~localise force_ty metasenv subst context expty t
-          orig_he he ty_he args in
-       let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
-       metasenv, subst, t, ty
+       let hbr t = 
+         if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t 
+       in
+       let refine_appl () =
+         let metasenv, subst, he, ty_he = 
+            typeof_aux metasenv subst context None he in
+         let metasenv, subst, t, ty = 
+           eat_prods rdb ~localise force_ty metasenv subst context expty t
+            orig_he he ty_he args in
+         metasenv, subst, hbr t, ty
+       in
+       if args = [C.Implicit `Vector] && expty <> None then
+         (* we try here to expand the vector a 0 implicits, but we use
+          * the expected type *)
+         try
+           let metasenv, subst, he, ty_he = 
+              typeof_aux metasenv subst context expty he in
+           metasenv, subst, hbr he, ty_he
+         with Uncertain _ | RefineFailure _ -> refine_appl ()
+       else refine_appl ()
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
           outtype,(term as orig_term),pl) as orig ->
@@ -377,6 +392,9 @@ and try_coercions rdb
       | NCicUnification.UnificationFailure _ -> first exc tl
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
+  pp(lazy("try_coercion " ^ 
+    NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
+    NCicPp.ppterm ~metasenv ~subst ~context expty));
     first exc
       (NCicCoercion.look_for_coercion 
         rdb metasenv subst context infty expty)
@@ -444,6 +462,11 @@ and eat_prods rdb ~localise force_ty metasenv subst context expty orig_t orig_he
   let rec aux metasenv subst args_so_far he ty_he = function 
   | [] ->
      let res = NCicUntrusted.mk_appl he (List.rev args_so_far) in
+     pp(lazy("FORCE FINAL APPL: " ^ 
+       NCicPp.ppterm ~metasenv ~subst ~context res ^
+       " of type " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_he
+       ^ " to type " ^ match expty with None -> "None" | Some x -> 
+       NCicPp.ppterm ~metasenv ~subst ~context x));
       force_ty true false metasenv subst context orig_t res ty_he expty
   | NCic.Implicit `Vector::tl ->
       let has_some_more_pis x =

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 0030fd75abec375ef1cc06b0ab8d0da0c7206969..caa069a0d839697cdbfc36e8a0c155bccfed1b3c 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -434,7 +434,14 @@ let letin_tac ~where ~what:(_,_,w) name =
  ]
 ;;
 
-let apply_tac (s,n,t) = exact_tac (s,n,Ast.Appl [t; Ast.Implicit `Vector]);;
+let apply_tac (s,n,t) = 
+  let t = 
+    match t with
+    | Ast.AttributedTerm (_,Ast.Binder _) | Ast.Binder _ -> t
+    | _ -> Ast.Appl [t; Ast.Implicit `Vector]
+  in
+    exact_tac (s,n,t)
+;;
 
 type indtyinfo = {
         rightno: int;