From aff007d80f87128884c96a664bc88aec69107d85 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Sep 2009 14:50:57 +0000 Subject: [PATCH] some fixes here and there --- .../components/ng_refiner/nCicCoercion.ml | 19 ++++++-- .../components/ng_refiner/nCicRefiner.ml | 47 ++++++++++++++----- .../components/ng_tactics/nTactics.ml | 9 +++- 3 files changed, 59 insertions(+), 16 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index d168ba548..757041451 100644 --- 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 a33162947..5a6f1028f 100644 --- 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 0030fd75a..caa069a0d 100644 --- 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; -- 2.39.2