diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 62 | ||||
| -rw-r--r-- | interp/interp.mllib | 4 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 24 |
3 files changed, 57 insertions, 33 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index cc4655315..fde5a11f1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -531,21 +531,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = let rec aux (terms,binderopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with - | NVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = Id.Map.find id terms in - intern {env with tmp_scope = scopt; - scopes = subscopes @ env.scopes} a - with Not_found -> - try - GVar (loc, Id.Map.find id renaming) - with Not_found -> - (* Happens for local notation joint with inductive/fixpoint defs *) - GVar (loc,id) - end + | NVar id -> subst_var subst' (renaming, env) id | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -558,11 +544,34 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = List.fold_right fold (if lassoc then List.rev l else l) termin with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation")) - | NHole (Evar_kinds.BinderType (Name id as na)) -> - let na = - try snd (coerce_to_name (fst (Id.Map.find id terms))) - with Not_found -> na in - GHole (loc,Evar_kinds.BinderType na,None) + | NHole (knd, arg) -> + let knd = match knd with + | Evar_kinds.BinderType (Name id as na) -> + let na = + try snd (coerce_to_name (fst (Id.Map.find id terms))) + with Not_found -> na + in + Evar_kinds.BinderType na + | _ -> knd + in + let arg = match arg with + | None -> None + | Some arg -> + let open Tacexpr in + let open Genarg in + let mk_env id (c, (tmp_scope, subscopes)) accu = + let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in + let gc = intern nenv c in + let c = ConstrMayEval (Genredexpr.ConstrTerm (gc, Some c)) in + ((loc, id), c) :: accu + in + let bindings = Id.Map.fold mk_env terms [] in + let body = TacArg (loc, TacGeneric arg) in + let tac = TacLetIn (false, bindings, body) in + let arg = in_gen (glbwit Constrarg.wit_tactic) tac in + Some arg + in + GHole (loc, knd, arg) | NBinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -586,6 +595,19 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = | t -> glob_constr_of_notation_constr_with_binders loc (traverse_binder subst) (aux subst') subinfos t + and subst_var (terms, binderopt) (renaming, env) id = + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = Id.Map.find id terms in + intern {env with tmp_scope = scopt; + scopes = subscopes @ env.scopes} a + with Not_found -> + try + GVar (loc, Id.Map.find id renaming) + with Not_found -> + (* Happens for local notation joint with inductive/fixpoint defs *) + GVar (loc,id) in aux (terms,None) infos c let split_by_type ids = diff --git a/interp/interp.mllib b/interp/interp.mllib index 7f14fe42b..c9a031526 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,5 @@ +Stdarg +Constrarg Genintern Constrexpr_ops Notation_ops @@ -16,5 +18,3 @@ Constrextern Coqlib Discharge Declare -Stdarg -Constrarg diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ce9deb0db..57fc15f8e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -104,7 +104,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) - | NHole x -> GHole (loc, x, None) + | NHole (x, arg) -> GHole (loc, x, arg) | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x) @@ -287,7 +287,7 @@ let notation_constr_and_vars_of_glob_constr a = NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s - | GHole (_,w,_) -> NHole w + | GHole (_,w,arg) -> NHole (w, arg) | GRef (_,r) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> @@ -465,14 +465,16 @@ let rec subst_notation_constr subst bound raw = | NPatVar _ | NSort _ -> raw - | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - NHole (Evar_kinds.InternalHole) - | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ - |Evar_kinds.CasesType |Evar_kinds.InternalHole - |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar - |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw + | NHole (knd, solve) -> + let nknd = match knd with + | Evar_kinds.ImplicitArg (ref, i, b) -> + let nref, _ = subst_global subst ref in + if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) + | _ -> knd + in + let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + if nsolve == solve && nknd = knd then raw + else NHole (nknd, nsolve) | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in @@ -500,7 +502,7 @@ let abstract_return_type_context_glob_constr = let abstract_return_type_context_notation_constr = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, None),c)) exception No_match |