X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=c4534e8daf6f466430f1144abf40ed28ed3c691a;hb=79684e8bd0f54b5c88fff981366bd8c78dd0fbe9;hp=48d1eeb1caa491631052740f68c3c159dada558c;hpb=e869500069d11aadd7bbe8afddcdd9044d0b56a7;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 48d1eeb1c..c4534e8da 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -109,7 +109,7 @@ let rec typeof rdb | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty | C.Appl _ when skip_appl -> metasenv, subst, t, expty | _ -> - pp (lazy ( + pp (lazy ("forcing infty=expty: "^ (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^ (NCicPp.ppterm ~metasenv ~subst:[] ~context expty))); try @@ -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 ^ " ::exp:: " ^ + 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 -> @@ -317,7 +332,7 @@ let rec typeof rdb NCicTypeChecker.type_of_branch ~subst context leftno outtype cons ty_cons in pp (lazy ("TYPEOFBRANCH: " ^ - NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^ + NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::inf:: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_branch )); let metasenv, subst, p, _ = typeof_aux metasenv subst context (Some ty_branch) p in @@ -329,7 +344,7 @@ let rec typeof rdb metasenv, subst, C.Match (r, outtype, term, pl),resty | C.Match _ -> assert false in - pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ + pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " ::inf:: "^ NCicPp.ppterm ~metasenv ~subst ~context infty )); force_ty true true metasenv subst context orig t infty expty (*D*)in outside(); rc with exc -> outside (); raise exc @@ -348,7 +363,7 @@ and try_coercions rdb (NCicPp.ppterm ~metasenv ~subst ~context t) (NCicPp.ppterm ~metasenv ~subst ~context infty) (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) - | (metasenv, newterm, newtype, meta)::tl -> + | (_,metasenv, newterm, newtype, meta)::tl -> try pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context @@ -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,7 +462,14 @@ 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 - force_ty true false metasenv subst context orig_t res ty_he expty + 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)); + (* whatever the term is, we force the type. in case of ((Lambda..) ?...) + * the application may also be a lambda! *) + force_ty false false metasenv subst context orig_t res ty_he expty | NCic.Implicit `Vector::tl -> let has_some_more_pis x = match NCicReduction.whd ~subst context x with