From 0369aa83a42ed4730ed1946b02365760817f6ea2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Jul 2009 15:36:18 +0000 Subject: [PATCH] 1) Some more work for vector implicits. 2) Vector implicits can be used only in argument position. --- .../ng_disambiguation/nCicDisambiguate.ml | 2 +- .../components/ng_refiner/nCicRefiner.ml | 27 +++++++++---------- 2 files changed, 14 insertions(+), 15 deletions(-) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index b044b51d9..357f9e539 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -364,7 +364,7 @@ let interpretate_term_and_interpretate_term_option | Some (CicNotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation - | Some CicNotationPt.Implicit `Vector -> assert false + | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector | Some term -> aux ~localize loc context term in (fun ~context -> aux ~localize:true HExtlib.dummy_floc context), diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 2b648d857..a227e918e 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -36,16 +36,18 @@ let wrap_exc msg = function | e -> raise e ;; -let exp_implicit metasenv context expty = +let exp_implicit ~localise metasenv context expty t = let foo x = match expty with Some t -> `WithType t | None -> x in function | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term) | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type) | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term) + | `Vector -> + raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^ + "can only be used in argument position"))) | _ -> assert false ;; - let check_allowed_sort_elimination rdb localise r orig = let mkapp he arg = match he with @@ -145,8 +147,10 @@ let rec typeof rdb NCicPp.ppterm ~subst ~metasenv ~context t))) | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0)) | C.Implicit infos -> - let metasenv,_,t,ty = exp_implicit metasenv context expty infos in - metasenv, subst, t, ty + let metasenv,_,t,ty = + exp_implicit ~localise metasenv context expty t infos + in + metasenv, subst, t, ty | C.Meta (n,l) as t -> let ty = try @@ -228,15 +232,11 @@ let rec typeof rdb let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in 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 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 - metasenv subst context orig_he he ty_he args - in + eat_prods rdb ~localise metasenv subst context 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 | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) @@ -436,12 +436,11 @@ and guess_name subst ctx ty = with NCicUtils.Subst_not_found _ -> aux 'M') | _ -> aux 'H' -and eat_prods rdb - ~localise metasenv subst context orig_he he ty_he args -= +and eat_prods rdb ~localise metasenv subst context orig_he he ty_he args = (*D*)inside 'E'; try let rc = let rec aux metasenv subst args_so_far he ty_he = function - | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he + | [] ->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he + | NCic.Implicit `Vector::tl -> assert false | arg::tl -> match NCicReduction.whd ~subst context ty_he with | C.Prod (_,s,t) -> -- 2.39.2