update in basic_2 and static_2

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 8476119ad081c24489559e5e2e566ea0318f13bb..705d80cd451611015abcd374639959408ac91e11 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -301,7 +301,7 @@ let rec typeof rdb
        let hbr t = 
          if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t 
        in
-       let refine_appl () =
+       let refine_appl metasenv subst args =
          let metasenv, subst, he, ty_he = 
             typeof_aux metasenv subst context None he in
          let metasenv, subst, t, ty = 
@@ -316,8 +316,53 @@ let rec typeof rdb
            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 ()
+         with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
+       else
+        (* CSC: whd can be useful on he too... *)
+        (match he with
+            C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
+             match
+              HExtlib.map_option (NCicReduction.whd ~subst context) expty
+             with
+                Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
+                when NUri.eq uri1 uri2 ->
+                (try
+                 let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys ref in
+                 let leftexpargs,_ = HExtlib.split_nth leftno expargs in
+                  let rec instantiate metasenv subst revargs args =
+                   function
+                     [] ->
+                      (* some checks are re-done here, but it would be complex
+                         to avoid them (e.g. we did not check yet that the
+                         constructor is a constructor for that inductive type)*)
+                      refine_appl metasenv subst ((List.rev revargs)@args)
+                   | (exparg::expargs) as allexpargs ->
+                      match args with
+                         [] -> raise (Failure "Not enough args")
+                       | (C.Implicit `Vector::args) as allargs ->
+                          (try
+                            instantiate metasenv subst revargs args allexpargs
+                           with
+                              Sys.Break as exn -> raise exn
+                            | _ ->
+                             instantiate metasenv subst revargs
+                              (C.Implicit `Term :: allargs) allexpargs)
+                       | arg::args ->
+                          let metasenv,subst,arg,_ =
+                           typeof_aux metasenv subst context None arg in
+                          let metasenv,subst =
+                           NCicUnification.unify rdb metasenv subst context
+                            arg exparg
+                          in
+                           instantiate metasenv subst(arg::revargs) args expargs
+                  in
+                   instantiate metasenv subst [] args leftexpargs 
+                with
+                 | Sys.Break as exn -> raise exn
+                 | _ ->
+                    refine_appl metasenv subst args (* to try coercions *))
+              | _ -> refine_appl metasenv subst args)
+          | _ -> refine_appl metasenv subst args)
    | 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 ->
@@ -993,13 +1038,15 @@ let relocalise old_localise dt t add =
 ;;
 
 let undebruijnate inductive ref t rev_fl =
+  let len = List.length rev_fl in 
   NCicSubstitution.psubst (fun x -> x) 
-   (List.rev (HExtlib.list_mapi 
+   (HExtlib.list_mapi 
       (fun (_,_,rno,_,_,_) i -> 
+         let i = len - i - 1 in
          NCic.Const 
            (if inductive then NReference.mk_fix i rno ref
             else NReference.mk_cofix i ref))
-      rev_fl))
+      rev_fl)
     t
 ;; 
 
@@ -1128,6 +1175,29 @@ let typeof_obj
                     metasenv,subst,item1::context
                 ) (metasenv,subst,tys) sx_context_ty_rev sx_context_te_rev
               with Invalid_argument "List.fold_left2" -> assert false in
+             let metasenv, subst =
+                let rec aux context (metasenv,subst) = function
+                  | NCic.Meta _ -> metasenv, subst
+                  | NCic.Implicit _ -> metasenv, subst
+                  | NCic.Appl (NCic.Rel i :: args) as t
+                      when i > List.length context - len ->
+                      let lefts, _ = HExtlib.split_nth leftno args in
+                      let ctxlen = List.length context in
+                      let (metasenv, subst), _ = 
+                        List.fold_left
+                        (fun ((metasenv, subst),l) arg ->
+                          NCicUnification.unify rdb 
+                           ~test_eq_only:true metasenv subst context arg 
+                             (NCic.Rel (ctxlen - len - l)), l+1
+                          )
+                        ((metasenv, subst), 0) lefts
+                      in
+                      metasenv, subst
+                  | t -> NCicUtils.fold (fun e c -> e::c) context aux
+                  (metasenv,subst) t
+                in
+               aux context (metasenv,subst) te
+             in
              let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in
               (match
                 NCicReduction.whd ~subst context con_sort,