diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 745 |
1 files changed, 535 insertions, 210 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 51dfadac..0c5393cf 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -7,23 +7,111 @@ (************************************************************************) open Pp -open Errors +open CErrors 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 (vars1,vars2 as vars) t1 t2 = match t1, t2 with +| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) +| NApp (t1, a1), NApp (t2, a2) -> + (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) 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 vars) t1 t2 && + (eq_notation_constr vars) u1 u2 && b1 == b2 +| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 +| NProd (na1, t1, u1), NProd (na2, t2, u2) -> + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 +| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 +| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) 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 vars) 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 vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + in + Option.equal (eq_notation_constr vars) 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 vars) o1 o2 && + (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 +| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + (eq_notation_constr vars) t1 t2 && + Name.equal na1 na2 && + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) u1 u2 && + (eq_notation_constr vars) 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 vars) o1 o2 && + (eq_notation_constr vars) t1 t2 + in + Array.equal Id.equal ids1 ids2 && + Array.equal (List.equal eq) ts1 ts2 && + Array.equal (eq_notation_constr vars) us1 us2 && + Array.equal (eq_notation_constr vars) rs1 rs2 +| NSort s1, NSort s2 -> + 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 +| (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." + | Anonymous -> CErrors.error "This expression should be a simple identifier." | Name id -> id let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na @@ -36,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') +let subst_binder_type_vars l = function + | Evar_kinds.BinderType (Name id) -> + let id = + try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id + with Not_found -> id in + Evar_kinds.BinderType (Name id) + | e -> e + let rec subst_glob_vars l = function | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> @@ -48,6 +144,7 @@ let rec subst_glob_vars l = function try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) let ldots_var = Id.of_string ".." @@ -105,7 +202,6 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) | NHole (x, naming, arg) -> GHole (loc, x, naming, arg) - | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x,None) let glob_constr_of_notation_constr loc x = @@ -113,7 +209,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) @@ -143,96 +239,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 -| NPatVar p1, NPatVar p2 -> - Id.equal p1 p2 -| 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 _ | NPatVar _ | 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 -> @@ -240,7 +246,13 @@ let check_is_hole id = function GHole _ -> () | t -> strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") -let compare_recursive_parts found f (iterator,subc) = +let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' + +type recursive_pattern_kind = +| RecursiveTerms of bool (* associativity *) +| RecursiveBinders of glob_constr * glob_constr + +let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in let rec aux c1 c2 = match c1,c2 with @@ -261,18 +273,16 @@ let compare_recursive_parts found f (iterator,subc) = let x,y = if lassoc then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, Some lassoc) in + let () = diff := Some (x, y, RecursiveTerms lassoc) in true | Some _ -> false end | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) - check_is_hole x t_x; - check_is_hole y t_y; begin match !diff with | None -> - let () = diff := Some (x, y, None) in + let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in aux c term | Some _ -> false end @@ -286,29 +296,42 @@ let compare_recursive_parts found f (iterator,subc) = (* Here, we would need a loc made of several parts ... *) user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") - | Some (x,y,Some lassoc) -> - let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in + | Some (x,y,RecursiveTerms lassoc) -> + let newfound,x,y,lassoc = + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) + then + !found,x,y,lassoc + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) || + List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found) + then + !found,y,x,not lassoc + else + (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in let iterator = - f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator - else iterator) in + f' (if lassoc then iterator + else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,None) -> + | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in - let iterator = f iterator in + let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; + check_is_hole x t_x; + check_is_hole y t_y; NBinderList (x,y,iterator,f (Option.get !terminator)) else raise Not_found let notation_constr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in + let has_ltac = ref false in let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) - try compare_recursive_parts found aux' (split_at_recursive_part c) + try compare_recursive_parts found aux aux' (split_at_recursive_part c) with Not_found -> found := keepfound; match c with @@ -350,20 +373,20 @@ 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,naming,arg) -> NHole (w, naming, arg) + | GHole (_,w,naming,arg) -> + if arg != None then has_ltac := true; + NHole (w, naming, arg) | GRef (_,r,_) -> NRef r - | GPatVar (_,(_,n)) -> NPatVar n - | GEvar _ -> + | GEvar _ | GPatVar _ -> error "Existential variables not allowed in notations." in let t = aux a in (* Side effect *) - t, !found + t, !found, !has_ltac -let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' - -let check_variables nenv (found,foundrec,foundrecbinding) = +let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = + let injective = ref true in let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in let useless_vars = Id.Map.fold fold recvars Id.Set.empty in @@ -386,7 +409,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = error (Id.to_string x ^ " should not be bound in a recursive pattern of the right-hand side.") - else nenv.ninterp_only_parse <- true + else injective := false in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then @@ -406,13 +429,15 @@ let check_variables nenv (found,foundrec,foundrecbinding) = with Not_found -> check_bound x end | NtnInternTypeIdent -> check_bound x in - Id.Map.iter check_type vars + Id.Map.iter check_type vars; + !injective let notation_constr_of_glob_constr nenv a = - let a, found = notation_constr_and_vars_of_glob_constr a in - let () = check_variables nenv found in - a + let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in + let injective = check_variables_and_reversibility nenv found in + a, not has_ltac && injective +(**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = @@ -420,7 +445,6 @@ let notation_constr_of_constr avoiding t = let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } in notation_constr_of_glob_constr nenv t @@ -438,7 +462,7 @@ let rec subst_notation_constr subst bound raw = | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else - notation_constr_of_constr bound t + fst (notation_constr_of_constr bound t) | NVar _ -> raw @@ -526,7 +550,7 @@ let rec subst_notation_constr subst bound raw = if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') - | NPatVar _ | NSort _ -> raw + | NSort _ -> raw | NHole (knd, naming, solve) -> let nknd = match knd with @@ -548,7 +572,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 -> @@ -567,6 +592,18 @@ let abstract_return_type_context_notation_constr = abstract_return_type_context snd (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) +let is_term_meta id metas = + try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false + with Not_found -> false + +let is_onlybinding_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false + with Not_found -> false + +let is_bindinglist_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false + with Not_found -> false + exception No_match let rec alpha_var id1 id2 = function @@ -575,26 +612,231 @@ let rec alpha_var id1 id2 = function | _::idl -> alpha_var id1 id2 idl | [] -> Id.equal id1 id2 -let add_env alp (sigma,sigmalist,sigmabinders) var v = +let alpha_rename alpmetas v = + if alpmetas == [] then v + else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match + +let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = (* Check that no capture of binding variables occur *) - if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; + (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..." + with an actual term "fun z => ... z ..." when "x" is not bound in the + notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then + we keep (z,x) in alp, and we have to check that what the [v] which is bound + to [var] does not contain z *) + if not (Id.equal ldots_var var) && + List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match; + (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..." + with an actual term "fun z => ... z ..." when "x" is bound in the + notation and the name "x" cannot be changed to "z", e.g. because + used at another occurrence, as in "Notation "'lam' y , P & Q" := + ((fun y => P),(fun y => Q))". Then, we keep (z,y) in alpmetas, and we + have to check that "fun z => ... z ..." denotes the same term as + "fun x => ... x ... ?var ... x" up to alpha-conversion when [var] + is instantiated by [v]; + Currently, we fail, but, eventually, [x] in [v] could be replaced by [x], + and, in match_, when finding "x" in subterm, failing because of a capture, + and, in match_, when finding "z" in subterm, replacing it with "x", + and, in an even further step, being even more robust, independent of the order, so + that e.g. the notation for ex2 works on "x y |- ex2 (fun x => y=x) (fun y => x=y)" + by giving, say, "exists2 x0, y=x0 & x=x0", but this would typically require the + glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the + choice of exact variable be done there; but again, this would be a non-trivial + refinement *) + let v = alpha_rename alpmetas v in (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::sigma,sigmalist,sigmabinders) + ((var,v)::terms,onlybinders,termlists,binderlists) + +let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl = + if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match; + let vl = List.map (alpha_rename alpmetas) vl in + (terms,onlybinders,(var,vl)::termlists,binderlists) + +let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = + (* TODO: handle the case of multiple occs in different scopes *) + (terms,(var,v)::onlybinders,termlists,binderlists) + +let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = + (terms,onlybinders,termlists,(x,bl)::binderlists) + +let rec pat_binder_of_term = function + | GVar (loc, id) -> PatVar (loc, Name id) + | GApp (loc, GRef (_,ConstructRef cstr,_), l) -> + let nparams = Inductiveops.inductive_nparams (fst cstr) in + let _,l = List.chop nparams l in + PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous) + | _ -> raise No_match -let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = +let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try - let v' = Id.List.assoc var sigma in + let v' = Id.List.assoc var terms in match v, v' with - | GHole _, _ -> fullsigma + | GHole _, _ -> sigma | _, GHole _ -> - add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v + let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in + add_env alp sigma var v | _, _ -> - if glob_constr_eq v v' then fullsigma + if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma else raise No_match - with Not_found -> add_env alp fullsigma var v + with Not_found -> add_env alp sigma var v -let bind_binder (sigma,sigmalist,sigmabinders) x bl = - (sigma,sigmalist,(x,List.rev bl)::sigmabinders) +let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl = + try + let vl' = Id.List.assoc var termlists in + let unify_term v v' = + match v, v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in + let rec unify vl vl' = + match vl, vl' with + | [], [] -> [] + | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl' + | _ -> raise No_match in + let vl = unify vl vl' in + let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in + add_termlist_env alp sigma var vl + with Not_found -> add_termlist_env alp sigma var vl + +let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = + try + match Id.List.assoc var terms with + | GVar (_,id') -> + (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), + sigma + | _ -> anomaly (str "A term which can be a binder has to be a variable") + with Not_found -> + (* The matching against a term allowing to find the instance has not been found yet *) + (* If it will be a different name, we shall unfortunately fail *) + (* TODO: look at the consequences for alp *) + alp, add_env alp sigma var (GVar (Loc.ghost,id)) + +let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id = + try + let v' = Id.List.assoc var onlybinders in + match v' with + | Anonymous -> + (* Should not occur, since the term has to be bound upwards *) + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + add_binding_env alp sigma var (Name id) + | Name id' -> + if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match + with Not_found -> add_binding_env alp sigma var (Name id) + +let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = + try + let v' = Id.List.assoc var onlybinders in + match v, v' with + | Anonymous, _ -> alp, sigma + | _, Anonymous -> + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + alp, add_binding_env alp sigma var v + | Name id1, Name id2 -> + if Id.equal id1 id2 then alp,sigma + else (fst alp,(id1,id2)::snd alp),sigma + with Not_found -> alp, add_binding_env alp sigma var v + +let rec map_cases_pattern_name_left f = function + | PatVar (loc,na) -> PatVar (loc,f na) + | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na) + +let rec fold_cases_pattern_eq f x p p' = match p, p' with + | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na) + | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' -> + let x,l = fold_cases_pattern_list_eq f x l l' in + let x,na = f x na na' in + x, PatCstr (loc,c,l,na) + | _ -> failwith "Not equal" + +and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with + | [], [] -> x, [] + | p::pl, p'::pl' -> + let x, p = fold_cases_pattern_eq f x p p' in + let x, pl = fold_cases_pattern_list_eq f x pl pl' in + x, p :: pl + | _ -> assert false + +let rec cases_pattern_eq p1 p2 = match p1, p2 with +| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2 +| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 +| _ -> false + +let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl = + let bl = List.rev bl in + try + let bl' = Id.List.assoc var binderlists in + let unify_name alp na na' = + match na, na' with + | Anonymous, na' -> alp, na' + | na, Anonymous -> alp, na + | Name id, Name id' -> + if Id.equal id id' then alp, na' + else (fst alp,(id,id')::snd alp), na' in + let unify_pat alp p p' = + try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in + let unify_term alp v v' = + match v, v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in + let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in + let unify_binder alp b b' = + match b, b' with + | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) -> + let alp, na = unify_name alp na na' in + alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t') + | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) -> + let alp, na = unify_name alp na na' in + alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t') + | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) -> + let alp, p = unify_pat alp p p' in + alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t') + | _ -> raise No_match in + let rec unify alp bl bl' = + match bl, bl' with + | [], [] -> alp, [] + | b :: bl, b' :: bl' -> + let alp,b = unify_binder alp b b' in + let alp,bl = unify alp bl bl' in + alp, b :: bl + | _ -> raise No_match in + let alp, bl = unify alp bl bl' in + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + alp, add_bindinglist_env sigma var bl + with Not_found -> + alp, add_bindinglist_env sigma var bl + +let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl = + try + let bl' = Id.List.assoc var binderlists in + let unify_id id na' = + match na' with + | Anonymous -> Name (rename_var (snd alp) id) + | Name id' -> + if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in + let unify_pat p p' = + if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' + else raise No_match in + let unify_term_binder c b' = + match c, b' with + | GVar (_, id), (Inl na', bk', None, t') (* assum *) -> + (Inl (unify_id id na'), bk', None, t') + | c, (Inr p', bk', None, t') (* pattern *) -> + let p = pat_binder_of_term c in + (Inr (unify_pat p p'), bk', None, t') + | _ -> raise No_match in + let rec unify cl bl' = + match cl, bl' with + | [], [] -> [] + | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl' + | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl' + | _ -> raise No_match in + let bl = unify cl bl' in + let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in + add_bindinglist_env sigma var bl + with Not_found -> + anomaly (str "There should be a binder list bindings this list of terms") let match_fix_kind fk1 fk2 = match (fk1,fk2) with @@ -615,12 +857,16 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (_,Name id2) when Id.List.mem id2 (fst metas) -> - let rhs = match na1 with - | Name id1 -> GVar (Loc.ghost,id1) - | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - alp, bind_env alp sigma id2 rhs - | (Name id1,Name id2) -> (id1,id2)::alp,sigma + | (na1,Name id2) when is_onlybinding_meta id2 metas -> + bind_binding_env alp sigma id2 na1 + | (Name id1,Name id2) when is_term_meta id2 metas -> + (* We let the non-binding occurrence define the rhs and hence reason up to *) + (* alpha-conversion for the given occurrence of the name (see #4592)) *) + bind_term_as_binding_env alp sigma id2 id1 + | (Anonymous,Name id2) when is_term_meta id2 metas -> + (* We let the non-binding occurrence define the rhs *) + alp, sigma + | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -636,45 +882,69 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function + | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + when islambda && Id.equal p e -> + match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b | GLambda (_,na,bk,t,b) when islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b + match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b + | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)])) + when not islambda && Id.equal p e -> + match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b | GProd (_,(Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b + match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b + ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b | b -> (decls,b) -let remove_sigma x (sigmavar,sigmalist,sigmabinders) = - (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders) +let remove_sigma x (terms,onlybinders,termlists,binderlists) = + (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists) -let match_abinderlist_with_app match_fun metas sigma rest x iter termin = - let rec aux sigma acc rest = +let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) = + (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists) + +let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas + +let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas + +let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin = + let rec aux sigma bl rest = try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = Id.List.assoc ldots_var (pi1 sigma) in + let metas = add_ldots_var (add_meta_bindinglist y metas) in + let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in + let rest = Id.List.assoc ldots_var terms in let b = - match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false + match Id.List.assoc y binderlists with [b] -> b | _ ->assert false in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in - aux sigma (b::acc) rest - with No_match when not (List.is_empty acc) -> - acc, match_fun metas sigma rest termin in - let bl,sigma = aux sigma [] rest in - bind_binder sigma x bl + let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in + aux sigma (b::bl) rest + with No_match when not (List.is_empty bl) -> + bl, rest, sigma in + let bl,rest,sigma = aux sigma [] rest in + let alp,sigma = bind_bindinglist_env alp sigma x bl in + match_fun alp metas sigma rest termin + +let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas -let match_alist match_fun metas sigma rest x iter termin lassoc = +let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = let rec aux sigma acc rest = try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = Id.List.assoc ldots_var (pi1 sigma) in - let t = Id.List.assoc x (pi1 sigma) in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + let metas = add_ldots_var (add_meta_term y metas) in + let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in + let rest = Id.List.assoc ldots_var terms in + let t = Id.List.assoc y terms in + let sigma = remove_sigma y (remove_sigma ldots_var sigma) in aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in - let l,sigma = aux sigma [] rest in - (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) + let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in + let l = if lassoc then l else List.rev l in + if is_bindinglist_meta x metas then + (* This is a recursive pattern for both bindings and terms; it is *) + (* registered for binders *) + bind_bindinglist_as_term_env alp sigma x l + else + bind_termlist_env alp sigma x l let does_not_come_from_already_eta_expanded_var = (* This is hack to avoid looping on a rule with rhs of the form *) @@ -688,41 +958,67 @@ let does_not_come_from_already_eta_expanded_var = (* checked). *) function GVar _ -> false | _ -> true -let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = +let rec match_ inner u alp metas sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) - | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1 + | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1 + | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1 + | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1 (* Matching recursive notations for terms *) - | r1, NList (x,_,iter,termin,lassoc) -> - match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc + | r1, NList (x,y,iter,termin,lassoc) -> + match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc + + (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *) + | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e -> + let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in + | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)-> + let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) - match_in u alp metas (bind_binder sigma x decls) b termin - | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin + + (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *) + | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e -> + let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin + + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin) when na1 != Anonymous -> - let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in + let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) - match_in u alp metas (bind_binder sigma x decls) b termin + let alp,sigma = bind_bindinglist_env alp sigma x decls in + match_in u alp metas sigma b termin (* Matching recursive notations for binders: general case *) - | r, NBinderList (x,_,iter,termin) -> - match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin + | r, NBinderList (x,y,iter,termin) -> + match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])), + NLambda (Name id,_,b2) + when is_bindinglist_meta id metas -> + let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in + match_in u alp metas sigma b1 b2 + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) + when is_bindinglist_meta id metas -> + let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + match_in u alp metas sigma b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) - when Id.List.mem id blmetas && na != Anonymous -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + when is_bindinglist_meta id metas && na != Anonymous -> + let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in + match_in u alp metas sigma b1 b2 (* Matching compositionally *) - | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma + | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> 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 let f1,l1,f2,l2 = @@ -794,15 +1090,21 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = otherwise how to ensure it corresponds to a well-typed eta-expansion; we make an exception for types which are metavariables: this is useful e.g. to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *) - | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner -> - let id' = Namegen.next_ident_away id (free_glob_vars b1) in + | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner -> + let avoid = + free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in + let id' = Namegen.next_ident_away id avoid in let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma - | NVar id2 -> bind_env alp sigma id2 t1 + | NVar id2 -> bind_term_env alp sigma id2 t1 | _ -> assert false in - match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,t1)]) - (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 + let (alp,sigma) = + if is_bindinglist_meta id metas then + bind_bindinglist_env alp sigma id [(Inl (Name id'),Explicit,None,t1)] + else + match_names metas (alp,sigma) (Name id') na in + match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 | (GRec _ | GEvar _), _ | _,_ -> raise No_match @@ -823,14 +1125,20 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 +let term_of_binder = function + | Name id -> GVar (Loc.ghost,id) + | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) + +type glob_decl2 = + (name, cases_pattern) Util.union * Decl_kinds.binding_kind * + glob_constr option * glob_constr + let match_notation_constr u c (metas,pat) = - let test (_, (_, x)) = match x with NtnTypeBinderList -> false | _ -> true in - let vars = List.partition test metas in - let vars = (List.map fst (fst vars), List.map fst (snd vars)) in - let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in + let terms,binders,termlists,binderlists = + match_ false u ([],[]) metas ([],[],[],[]) c pat in (* Reorder canonically the substitution *) - let find x = - try Id.List.assoc x terms + let find_binder x = + try term_of_binder (Id.List.assoc x binders) with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) @@ -838,11 +1146,15 @@ let match_notation_constr u c (metas,pat) = List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> - ((find x, scl)::terms',termlists',binders') + let term = try Id.List.assoc x terms with Not_found -> raise No_match in + ((term, scl)::terms',termlists',binders') + | NtnTypeOnlyBinder -> + ((find_binder x, scl)::terms',termlists',binders') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(Id.List.assoc x binders,scl)::binders')) + let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in + (terms',termlists',(bl, scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) @@ -851,17 +1163,31 @@ let add_patterns_for_params ind l = let nparams = mib.Declarations.mind_nparams in Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l -let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = +let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = try - let vvar = Id.List.assoc var sigma in - if cases_pattern_eq v vvar then fullsigma else raise No_match + let vvar = Id.List.assoc var terms in + if cases_pattern_eq v vvar then sigma else raise No_match with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) - (var,v)::sigma,sigmalist,x + (var,v)::terms,x,termlists,y + +let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc = + let rec aux sigma acc rest = + try + let metas = add_ldots_var (add_meta_term y metas) in + let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in + let rest = Id.List.assoc ldots_var terms in + let t = Id.List.assoc y terms in + let sigma = remove_sigma y (remove_sigma ldots_var sigma) in + aux sigma (t::acc) rest + with No_match when not (List.is_empty acc) -> + acc, match_fun metas sigma rest termin in + let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in + (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) -let rec match_cases_pattern metas sigma a1 a2 = +let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = match (a1,a2) with - | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> sigma,(0,add_patterns_for_params (fst r1) largs) @@ -875,15 +1201,15 @@ let rec match_cases_pattern metas sigma a1 a2 = else let l1',more_args = Util.List.chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) - | r1, NList (x,_,iter,termin,lassoc) -> - (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) - (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[]) + | r1, NList (x,y,iter,termin,lassoc) -> + (match_cases_pattern_list (match_cases_pattern_no_more_args) + metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - |out,(_,[]) -> out - |_ -> raise No_match + | out,(_,[]) -> out + | _ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with @@ -904,16 +1230,15 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') + | NtnTypeOnlyBinder -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) let match_notation_constr_cases_pattern c (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in + let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in reorder_canonically_substitution terms termlists metas, more_args let match_notation_constr_ind_pattern ind args (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in + let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in reorder_canonically_substitution terms termlists metas, more_args |