diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 186 |
1 files changed, 94 insertions, 92 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5b49ebcbd9..b4cf6e9430 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -12,15 +12,103 @@ open Util open Names open Nameops open Globnames +open Decl_kinds open Misctypes open Glob_term open Glob_ops open Mod_subst open Notation_term -open Decl_kinds (**********************************************************************) -(* Re-interpret a notation as a glob_constr, taking care of binders *) +(* Utilities *) + +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 + | 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 + | 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 + | GProd (_,na1,bk1,ty1,c1), GProd (_,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 + | GHole _, GHole _ -> true + | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> + on_true_do (f b1 b2 && f c1 c2) add na1 + | (GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ + | _,(GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) + -> error "Unsupported construction in recursive notations." + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | GHole _ | GSort _ | GLetIn _), _ + -> false + +let rec eq_notation_constr t1 t2 = match t1, t2 with +| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NVar id1, NVar id2 -> Id.equal id1 id2 +| NApp (t1, a1), NApp (t2, a2) -> + eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 +| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 && b1 == b2 +| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NProd (na1, t1, u1), NProd (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) + let eqpat (p1, t1) (p2, t2) = + List.equal cases_pattern_eq p1 p2 && + eq_notation_constr t1 t2 + in + let eqf (t1, (na1, o1)) (t2, (na2, o2)) = + let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in + eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + in + Option.equal eq_notation_constr o1 o2 && + List.equal eqf r1 r2 && + List.equal eqpat p1 p2 +| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + List.equal Name.equal nas1 nas2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + eq_notation_constr t1 t2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr u1 u2 && + eq_notation_constr r1 r2 +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) + let eq (na1, o1, t1) (na2, o2, t2) = + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 + in + Array.equal Id.equal ids1 ids2 && + Array.equal (List.equal eq) ts1 ts2 && + Array.equal eq_notation_constr us1 us2 && + Array.equal eq_notation_constr rs1 rs2 +| NSort s1, NSort s2 -> + Miscops.glob_sort_eq s1 s2 +| NCast (t1, c1), NCast (t2, c2) -> + eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 +| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NCast _), _ -> false + +(**********************************************************************) +(* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function | Anonymous -> Errors.error "This expression should be a simple identifier." @@ -112,7 +200,7 @@ let glob_constr_of_notation_constr loc x = glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x -(****************************************************************************) +(******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) @@ -142,94 +230,6 @@ let split_at_recursive_part c = | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, 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 - | 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 - | 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 - | GProd (_,na1,bk1,ty1,c1), GProd (_,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 - | GHole _, GHole _ -> true - | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 && f c1 c2) add na1 - | (GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ - | _,(GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ - | GHole _ | GSort _ | GLetIn _), _ - -> false - -let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 - -let rec eq_notation_constr t1 t2 = match t1, t2 with -| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Id.equal id1 id2 -| NApp (t1, a1), NApp (t2, a2) -> - eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) -| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 && b1 == b2 -| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 -| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) - let eqpat (p1, t1) (p2, t2) = - List.equal cases_pattern_eq p1 p2 && - eq_notation_constr t1 t2 - in - let eqf (t1, (na1, o1)) (t2, (na2, o2)) = - let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in - eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 - in - Option.equal eq_notation_constr o1 o2 && - List.equal eqf r1 r2 && - List.equal eqpat p1 p2 -| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> - List.equal Name.equal nas1 nas2 && - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 -| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - eq_notation_constr t1 t2 && - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr u1 u2 && - eq_notation_constr r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) - let eq (na1, o1, t1) (na2, o2, t2) = - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 - in - Array.equal Id.equal ids1 ids2 && - Array.equal (List.equal eq) ts1 ts2 && - Array.equal eq_notation_constr us1 us2 && - Array.equal eq_notation_constr rs1 rs2 -| NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 -| NCast (t1, c1), NCast (t2, c2) -> - eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 -| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ - | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false - - let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> @@ -409,6 +409,7 @@ let notation_constr_of_glob_constr nenv a = let () = check_variables nenv found in a +(**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = @@ -544,7 +545,8 @@ let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in (metas,subst_notation_constr subst bound pat) -(* Pattern-matching glob_constr and notation_constr *) +(**********************************************************************) +(* Pattern-matching a [glob_constr] against a [notation_constr] *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> |