X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=423c33d8eea5f61f50140270165dee062d617b3d;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=705d80cd451611015abcd374639959408ac91e11;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 705d80cd4..423c33d8e 100644
--- 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 metasenv subst args =
+       let refine_appl () =
          let metasenv, subst, he, ty_he = 
             typeof_aux metasenv subst context None he in
          let metasenv, subst, t, ty = 
@@ -316,53 +316,8 @@ 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 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)
+         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 ->
@@ -466,18 +421,9 @@ and try_coercions rdb
   ~localise 
   metasenv subst context t orig_t infty expty perform_unification exc 
 =
-  let cs_subst = NCicSubstitution.subst ~avoid_beta_redexes:true in
-  try 
-    pp (lazy "WWW: trying coercions -- preliminary unification");
-    let metasenv, subst = 
-      NCicUnification.unify rdb metasenv subst context infty expty
-    in metasenv, subst, t, expty
-  with
-  | exn ->
   (* we try with a coercion *)
   let rec first exc = function
-  | [] ->   
-      pp (lazy "WWW: no more coercions!");      
+  | [] ->         
       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (NCicPp.ppterm ~metasenv ~subst ~context t)
@@ -512,332 +458,7 @@ and try_coercions rdb
       with 
       | NCicUnification.UnificationFailure _ -> first exc tl
       | NCicUnification.Uncertain _ as exc -> first exc tl
-  in
-  
-  try 
-    pp (lazy "WWW: trying coercions -- inner check");
-    match infty, expty, t with
-    | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
-        (*{{{*) pp (lazy "CASE");
-        (* {{{ helper functions *)
-        let get_cl_and_left_p refit outty =
-          match refit with
-          | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
-             let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
-             let _, _, ty, cl = List.nth itl tyno in
-             let constructorsno = List.length cl in
-              let count_pis t =
-                let rec aux ctx t = 
-                  match NCicReduction.whd ~subst ~delta:max_int ctx t with
-                  | NCic.Prod (name,src,tgt) ->
-                      let ctx = (name, (NCic.Decl src)) :: ctx in
-                      1 + aux ctx tgt
-                  | _ -> 0
-                in
-                  aux [] t
-              in
-              let rec skip_lambda_delifting t n =
-                match t,n with
-                | _,0 -> t
-                | NCic.Lambda (_,_,t),n ->
-                    pp (lazy ("WWW: failing term? "^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[] t)); 
-                    skip_lambda_delifting
-                      (* substitute dangling indices with a dummy *)
-                      (NCicSubstitution.subst (NCic.Sort NCic.Prop) t) (n - 1)
-                | _ -> assert false
-              in
-              let get_l_r_p n = function
-                | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
-                | NCic.Lambda (_,NCic.Appl 
-                    (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
-                    HExtlib.split_nth n args
-                | _ -> assert false
-              in
-              let pis = count_pis ty in
-              let rno = pis - leftno in
-              let t = skip_lambda_delifting outty rno in
-              let left_p, _ = get_l_r_p leftno t in
-              let instantiate_with_left cl =
-                List.map 
-                  (fun ty -> 
-                    List.fold_left 
-                      (fun t p -> match t with
-                        | NCic.Prod (_,_,t) ->
-                            cs_subst p t
-                        | _-> assert false)
-                      ty left_p) 
-                  cl 
-              in
-              let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
-              cl, left_p, leftno, rno
-          | _ -> raise exn
-        in
-        let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
-          match t,n with
-          | _,0 ->
-            let rec mkr n = function 
-              | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
-            in
-            pp (lazy ("input replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
-            let bo =
-            NCicRefineUtil.replace_lifting
-              ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence)
-              ~context:ctx
-              ~what:(matched::right_p)
-              ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
-              ~where:bo
-            in
-            pp (lazy ("output replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
-            bo
-          | NCic.Lambda (name, src, tgt),_ ->
-              NCic.Lambda (name, src,
-               keep_lambdas_and_put_expty 
-                ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift 1 bo)
-                (List.map (NCicSubstitution.lift 1) right_p) (NCicSubstitution.lift 1 matched) (n-1))
-          | _ -> assert false
-        in
-        (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
-        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
-        let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
-        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
-        let add_params 
-          metasenv subst context cty outty mty m i 
-        =
-          let rec aux context outty par j mty m = function
-            | NCic.Prod (name, src, tgt) ->
-                let t,k = 
-                  aux 
-                    ((name, NCic.Decl src) :: context)
-                    (NCicSubstitution.lift 1 outty) (NCic.Rel j::par) (j+1) 
-                    (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt
-                in
-                NCic.Prod (name, src, t), k
-            | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
-                let k = 
-                  let k = NCic.Const(Ref.mk_constructor i r) in
-                  NCicUntrusted.mk_appl k par
-                in
-                (* the type has no parameters, so kty = mty
-                let kty = 
-                  try NCicTypechecker.typeof ~subst ~metasenv context k
-                  with NCicTypeChecker.TypeCheckerFailure _ -> assert false
-                in *)
-                NCic.Prod ("p", 
-                 NCic.Appl [eq; mty; m; mty; k],
-                 (NCicSubstitution.lift 1
-                  (NCicReduction.head_beta_reduce ~delta:max_int 
-                   (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
-            | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
-                let left_p,right_p = HExtlib.split_nth leftno pl in
-                let has_rights = right_p <> [] in
-                let k = 
-                  let k = NCic.Const(Ref.mk_constructor i r) in
-                  NCicUntrusted.mk_appl k (left_p@par)
-                in
-                let right_p = 
-                  try match 
-                    NCicTypeChecker.typeof ~subst ~metasenv context k
-                  with
-                  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
-                      snd (HExtlib.split_nth leftno args)
-                  | _ -> assert false
-                  with NCicTypeChecker.TypeCheckerFailure _-> assert false
-                in
-                let orig_right_p =
-                  match mty with
-                  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
-                      snd (HExtlib.split_nth leftno args)
-                  | _ -> assert false
-                in
-                List.fold_right2 
-                  (fun x y (tacc,pacc) ->
-                    let xty = 
-          	    try NCicTypeChecker.typeof ~subst ~metasenv context x
-                      with NCicTypeChecker.TypeCheckerFailure _ -> assert false
-                    in
-                    let yty = 
-          	    try NCicTypeChecker.typeof ~subst ~metasenv context y
-                      with NCicTypeChecker.TypeCheckerFailure _ -> assert false
-                    in
-                    NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
-                     NCicSubstitution.lift 1 tacc), (xty,x,yty,y)::pacc) 
-                  (orig_right_p @ [m]) (right_p @ [k]) 
-                  (NCicReduction.head_beta_reduce ~delta:max_int
-                      (NCicUntrusted.mk_appl outty (right_p@[k])), [])  
-
-  (*              if has_rights then
-                  NCicReduction.head_beta_reduce ~delta:max_int
-                    (NCic.Appl (outty ::right_p @ [k])),k
-                else
-                  NCic.Prod ("p", 
-                   NCic.Appl [eq; mty; m; k],
-                   (NCicSubstitution.lift 1
-                    (NCicReduction.head_beta_reduce ~delta:max_int 
-                     (NCic.Appl (outty ::right_p @ [k]))))),k*)
-            | _ -> assert false
-          in
-            aux context outty [] 1 mty m cty
-        in
-        let add_lambda_for_refl_m pbo eqs cty =
-          (* k lives in the right context *)
-          (* if rno <> 0 then pbo else *)
-          let rec aux = function 
-            | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) ->
-                NCic.Lambda (name,src,
-                (aux (bo,ty)))
-            | t,_ -> snd (List.fold_right
-                (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n,
-                  NCic.Appl [eq; xty; x; yty; y],
-                  NCicSubstitution.lift 1 acc)) eqs (1,t))
-                (*NCic.Lambda ("p",
-                  NCic.Appl [eq; mty; m; k],NCicSubstitution.lift 1 t)*)
-          in
-          aux (pbo,cty)
-        in
-        let add_pi_for_refl_m context new_outty mty m lno rno =
-          (*if rno <> 0 then new_outty else*)
-            let rec aux context mty m = function
-              | NCic.Lambda (name, src, tgt) ->
-                  let context = (name, NCic.Decl src)::context in
-                  NCic.Lambda (name, src, aux context (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt)
-              | t -> 
-                  let lhs =
-                    match mty with
-                    | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
-                    | _ -> [m]
-                  in
-                  let rhs = 
-                    List.map (fun x -> NCic.Rel x) 
-                      (List.rev (HExtlib.list_seq 1 (rno+2))) in
-                  List.fold_right2
-                    (fun x y acc ->
-                      let xty = 
-    		    try NCicTypeChecker.typeof ~subst ~metasenv context x
-                        with NCicTypeChecker.TypeCheckerFailure _ -> assert false
-                      in
-                      let yty = 
-    		    try NCicTypeChecker.typeof ~subst ~metasenv context y
-                        with NCicTypeChecker.TypeCheckerFailure _ -> assert false
-                      in
-                      NCic.Prod
-                      ("_", NCic.Appl [eq;xty;x;yty;y],
-                       (NCicSubstitution.lift 1 acc)))
-                    lhs rhs t
-  (*                NCic.Prod 
-                    ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
-                    NCicSubstitution.lift 1 t)*)
-            in
-              aux context mty m new_outty
-        in (* }}} end helper functions *)
-        (* constructors types with left params already instantiated *)
-        let outty = NCicUntrusted.apply_subst subst context outty in
-        let cl, left_p, leftno,rno = 
-          get_cl_and_left_p r outty
-        in
-        let right_p, mty = 
-          try
-            match 
-              NCicTypeChecker.typeof ~subst ~metasenv context m
-            with
-            | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty
-            | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty ->
-                snd (HExtlib.split_nth leftno args), mty
-            | _ -> assert false
-          with NCicTypeChecker.TypeCheckerFailure _ -> 
-             raise (AssertFailure(lazy "already ill-typed matched term"))
-        in
-        let mty = NCicUntrusted.apply_subst subst context mty in
-        let outty = NCicUntrusted.apply_subst subst context outty in
-        let expty = NCicUntrusted.apply_subst subst context expty in
-        let new_outty =
-         keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
-        in
-        pp 
-          (lazy ("CASE: new_outty: " ^ NCicPp.ppterm 
-           ~context ~metasenv ~subst new_outty));
-        let _,pl,subst,metasenv = 
-          List.fold_right2
-            (fun cty pbo (i, acc, s, menv) -> 
-               pp (lazy ("begin iteration"));
-              (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
-               *   (new_)outty right_par (K_i left_par k_par) *)
-               let infty_pbo, _ = 
-                 add_params menv s context cty outty mty m i in
-               pp 
-                (lazy ("CASE: infty_pbo: "^ NCicPp.ppterm
-                 ~context ~metasenv ~subst infty_pbo));
-               let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
-                 add_params menv s context cty new_outty mty m i in
-               pp 
-                (lazy ("CASE: expty_pbo: "^ NCicPp.ppterm
-                 ~context ~metasenv ~subst expty_pbo));
-               let pbo = add_lambda_for_refl_m pbo eqs cty in
-               pp 
-                 (lazy ("CASE: pbo: " ^ NCicPp.ppterm
-                 ~context ~metasenv ~subst pbo));
-               let metasenv, subst, pbo, _ =
-                 try_coercions rdb ~localise menv s context pbo 
-          	 orig_t (*??*) infty_pbo expty_pbo perform_unification exc
-               in
-               pp 
-                 (lazy ("CASE: pbo2: " ^ NCicPp.ppterm 
-                 ~context ~metasenv ~subst pbo));
-               (i-1, pbo::acc, subst, metasenv))
-            cl pl (List.length pl, [], subst, metasenv)
-        in
-        (*let metasenv, subst = 
-          try 
-            NCicUnification.unify rdb metasenv subst context outty new_outty 
-          with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
-        in*)
-        let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
-        pp (lazy ("CASE: new_outty: " ^ (NCicPp.ppterm 
-           ~metasenv ~subst ~context new_outty)));
-        let right_tys = 
-          List.map 
-            (fun t -> NCicTypeChecker.typeof ~subst ~metasenv context t) right_p in
-        let eqs = 
-          List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty]) 
-            (right_p@[m]) in
-        let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) 
-        in
-        metasenv, subst, t, expty (*}}}*)
-    | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> 
-        let rec mk_fresh_name ctx firstch n =
-          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
-          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
-          else mk_fresh_name ctx firstch (n+1)
-        in
-        (*{{{*) pp (lazy "LAM");
-        pp (lazy ("LAM: t = " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
-        let name_con = mk_fresh_name context 'c' 0
-          (*FreshNamesGenerator.mk_fresh_name 
-            ~subst metasenv context ~typ:src2 Cic.Anonymous*)
-        in
-        let context_src2 = ((name_con, NCic.Decl src2) :: context) in
-        (* contravariant part: the argument of f:src->ty *)
-        let metasenv, subst, rel1, _ = 
-          try_coercions rdb ~localise metasenv subst context_src2
-           (NCic.Rel 1) orig_t (NCicSubstitution.lift 1 src2) 
-           (NCicSubstitution.lift 1 src) perform_unification exc
-        in
-        (* covariant part: the result of f(c x); x:src2; (c x):src *)
-        let name_t, bo = 
-          match t with
-          | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from 2 1 bo)
-          | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift 1 t) [rel1]
-        in
-        (* we fix the possible dependency problem in the source ty *)
-        let ty = cs_subst rel1 (NCicSubstitution.lift_from 2 1 ty) in
-        let metasenv, subst, bo, _ = 
-          try_coercions rdb ~localise metasenv subst context_src2
-            bo orig_t ty ty2 perform_unification exc
-        in
-        let coerced = NCic.Lambda (name_t,src2, bo) in
-        pp (lazy ("LAM: coerced = " ^ NCicPp.ppterm ~metasenv ~subst ~context coerced));
-        metasenv, subst, coerced, expty (*}}}*)
-    | _ -> raise exc
-  with exc2 ->    
+  in 
   pp(lazy("try_coercion " ^ 
     NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
     NCicPp.ppterm ~metasenv ~subst ~context expty));
@@ -1038,15 +659,13 @@ 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) 
-   (HExtlib.list_mapi 
+   (List.rev (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
 ;; 
 
@@ -1175,29 +794,6 @@ 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,