diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 54065e8b35..6422e184b5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -92,9 +92,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Uint63.equal i1 i2 | NFloat f1, NFloat f2 -> Float64.equal f1 f2 +| NArray(t1,def1,ty1), NArray(t2,def2,ty2) -> + Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2 + && eq_notation_constr vars ty1 ty2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false + | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -249,6 +252,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat | NRef x -> GRef (x,None) | NInt i -> GInt i | NFloat f -> GFloat f + | NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -472,6 +476,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = if arg != None then has_ltac := true; NHole (w, naming, arg) | GRef (r,_) -> NRef r + | GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -675,6 +680,14 @@ let rec subst_notation_constr subst bound raw = let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') + | NArray (t,def,ty) -> + let def' = subst_notation_constr subst bound def + and t' = Array.Smart.map (subst_notation_constr subst bound) t + and ty' = subst_notation_constr subst bound ty + in + if def' == def && t' == t && ty' == ty then raw else + NArray(t',def',ty') + 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) @@ -1254,9 +1267,16 @@ 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 + | GArray(_u,t,def,ty), NArray(nt,ndef,nty) -> + if Int.equal (Array.length t) (Array.length nt) then + let sigma = match_in u alp metas sigma def ndef in + let sigma = match_in u alp metas sigma ty nty in + Array.fold_left2 (match_in u alp metas) sigma t nt + else raise No_match + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _ | GInt _ | GFloat _), _ -> raise No_match + | GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match and match_in u = match_ true u |