diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 8 | ||||
| -rw-r--r-- | interp/constrextern.ml | 3 | ||||
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 19 |
4 files changed, 34 insertions, 4 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7cc8de85d2..da04d8786b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 = | CDelimiters(s1,e1), CDelimiters(s2,e2) -> String.equal s1 s2 && constr_expr_eq e1 e2 + | CProj(p1,c1), CProj(p2,c2) -> + eq_reference p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _), _ -> false + | CGeneralization _ | CDelimiters _ | CProj _), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && @@ -365,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + | CProj (_,c) -> + f n acc c ) let free_vars_of_constr_expr c = @@ -446,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) + | CProj (p,c) -> + CProj (p, f e c) ) (* Used in constrintern *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1330b3741e..4f7d537d3f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -908,6 +908,9 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, Miscops.map_cast_type (extern_typ scopes vars) c') + | GProj (p, c) -> + let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in + CProj (pr, sub_extern inctx scopes vars c) ) r' and extern_typ (_,scopes) = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 61b33aa415..8e99435dbc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1869,7 +1869,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) - ) + | CProj (pr, c) -> + match intern_reference pr with + | ConstRef p -> + DAst.make ?loc @@ GProj (Projection.make p false, intern env c) + | _ -> + raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) + ) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 20492e38c8..326d05cba6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 +| NProj (p1, c1), NProj (p2, c2) -> + Projection.equal p1 p2 && eq_notation_constr vars c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false + | NRec _ | NSort _ | NCast _ | NProj _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) + | NProj (p,c) -> GProj (p, f e c) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a = if arg != None then has_ltac := true; NHole (w, naming, arg) | GRef (r,_) -> NRef r + | GProj (p, c) -> NProj (p, aux c) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw = let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') + | NProj (p, c) -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_notation_constr subst bound c in + if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c') + + let subst_interpretation subst (metas,pat) = let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) @@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 + | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 -> + match_in u alp metas sigma t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _), _ -> raise No_match + | GCast _ | GProj _ ), _ -> raise No_match and match_in u = match_ true u |