diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 12b256c45..4984bfc38 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -55,6 +55,7 @@ let ldots_var = Id.of_string ".." let glob_constr_of_notation_constr_with_binders loc g f e = function | NVar id -> GVar (loc,id) | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) + | NProj (p,c) -> GProj (loc,p,f e c) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in @@ -106,7 +107,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | NSort x -> GSort (loc,x) | NHole (x, arg) -> GHole (loc, x, arg) | NPatVar n -> GPatVar (loc,(false,n)) - | NRef x -> GRef (loc,x) + | NRef x -> GRef (loc,x,None) let glob_constr_of_notation_constr loc x = let rec aux () x = @@ -146,9 +147,10 @@ let split_at_recursive_part c = let on_true_do b f c = if b then (f c; b) else b let compare_glob_constr f add t1 t2 = match t1,t2 with - | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 + | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2 | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 + | GProj (_,p1,c1), GProj (_, p2, c2) -> eq_constant p1 p2 && f c1 c2 | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> on_true_do (f ty1 ty2 && f c1 c2) add na1 @@ -164,7 +166,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | _,(GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | (GRef _ | GVar _ | GApp _ | GProj _ | GLambda _ | GProd _ | GHole _ | GSort _ | GLetIn _), _ -> false @@ -259,6 +261,7 @@ let notation_constr_and_vars_of_glob_constr a = and aux' = function | GVar (_,id) -> add_id found id; NVar id | GApp (_,g,args) -> NApp (aux g, List.map aux args) + | GProj (_,p,c) -> NProj (p, aux c) | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) @@ -288,7 +291,7 @@ let notation_constr_and_vars_of_glob_constr a = | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) | GSort (_,s) -> NSort s | GHole (_,w,arg) -> NHole (w, arg) - | GRef (_,r) -> NRef r + | GRef (_,r,_) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> error "Existential variables not allowed in notations." @@ -365,7 +368,7 @@ let rec subst_pat subst pat = match pat with | PatVar _ -> pat | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_ind subst kn + let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) @@ -385,6 +388,12 @@ let rec subst_notation_constr subst bound raw = if r' == r && rl' == rl then raw else NApp(r',rl') + | NProj (p,c) -> + let p' = subst_constant subst p in + let c' = subst_notation_constr subst bound c in + if p == p' && c == c' then raw else + NProj (p',c') + | NList (id1,id2,r1,r2,b) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in @@ -421,7 +430,7 @@ let rec subst_notation_constr subst bound raw = (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> - let indkn' = subst_ind subst indkn in + let indkn' = subst_mind subst indkn in if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl @@ -658,7 +667,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = (* Matching compositionally *) | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma - | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma + | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma | GApp (loc,f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in |