(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Errors.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 let rec cases_pattern_fold_map loc g e = function | PatVar (_,na) -> let e',na' = g e na in e', PatVar (loc,na') | PatCstr (_,cstr,patl,na) -> let e',na' = g e na in let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') let rec subst_glob_vars l = function | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> let id = try match List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GLambda (loc,Name id,bk,t,c) -> let id = try match 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) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) 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) | 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 let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in subst_glob_vars outerl it | NBinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in let innerl = [(ldots_var,t);(x,GVar(loc,y))] in let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in subst_glob_vars outerl it | NLambda (na,ty,c) -> let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) | NLetIn (na,b,c) -> let e',na = g e na in GLetIn (loc,na,f e b,f e' c) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with | None -> e',None | Some (ind,nal) -> let e',nal' = List.fold_right (fun na (e',nal) -> let e',na' = g e' na in e',na'::nal) nal (e',[]) in e',Some (loc,ind,nal') in let e',na' = g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') | NLetTuple (nal,(na,po),b,c) -> let e',nal = List.fold_map g e nal in let e'',na = g e na in GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) | NIf (c,(na,po),b1,b2) -> let e',na = g e na in GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_map (to_id g) e idl in GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) | NSort x -> GSort (loc,x) | NHole x -> GHole (loc,x) | NPatVar n -> GPatVar (loc,(false,n)) | NRef x -> GRef (loc,x) let glob_constr_of_notation_constr loc x = let rec aux () 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) let add_name r = function Anonymous -> () | Name id -> add_id r id let split_at_recursive_part c = let sub = ref None in let rec aux = function | GApp (loc0,GVar(loc,v),c::l) when Id.equal v ldots_var -> begin match !sub with | None -> let () = sub := Some c in begin match l with | [] -> GVar (loc, ldots_var) | _ :: _ -> GApp (loc0, GVar (loc, ldots_var), l) end | Some _ -> (* Not narrowed enough to find only one recursive part *) raise Not_found end | c -> map_glob_constr aux c in let outer_iterator = aux c in match !sub with | None -> (* No recursive pattern found *) raise Not_found | Some c -> match outer_iterator with | 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) -> 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 subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> user_err_loc (loc_of_glob_constr 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 diff = ref None in let terminator = ref None in let rec aux c1 c2 = match c1,c2 with | GVar(_,v), term when Id.equal v ldots_var -> (* We found the pattern *) assert (match !terminator with None -> true | Some _ -> false); terminator := Some term; true | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when Id.equal v ldots_var -> (* We found the pattern, but there are extra arguments *) (* (this allows e.g. alternative (recursive) notation of application) *) assert (match !terminator with None -> true | Some _ -> false); terminator := Some term; List.for_all2eq aux l1 l2 | GVar (_,x), GVar (_,y) when not (Id.equal x y) -> (* We found the position where it differs *) let lassoc = match !terminator with None -> false | Some _ -> true in 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 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 aux c term | Some _ -> false end | _ -> compare_glob_constr aux (add_name found) c1 c2 in if aux iterator subc then match !diff with | None -> let loc1 = loc_of_glob_constr iterator in let loc2 = loc_of_glob_constr (Option.get !terminator) in (* 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 let iterator = f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator else iterator) in (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,None) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f iterator in (* found have been collected by compare_constr *) found := newfound; 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 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) with Not_found -> found := keepfound; match c with | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) user_err_loc (loc,"", str "Cannot find where the recursive pattern starts.") | c -> aux' c and aux' = function | GVar (_,id) -> add_id found id; NVar id | GApp (_,g,args) -> NApp (aux g, List.map aux args) | 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) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in NCases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; Option.iter (fun (_,_,nl) -> List.iter (add_name found) nl) x; (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml, List.map f eqnl) | GLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; NLetTuple (nal,(na,Option.map aux po),aux b,aux c) | GIf (loc,c,(na,po),b1,b2) -> add_name found na; NIf (aux c,(na,Option.map aux po),aux b1,aux b2) | GRec (_,fk,idl,dll,tl,bl) -> Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk != Explicit then error "Binders marked as implicit not allowed in notations."; add_name found na; (na,Option.map aux oc,aux b))) dll in 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) -> NHole w | GRef (_,r) -> NRef r | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> error "Existential variables not allowed in notations." in let t = aux a in (* Side effect *) t, !found let rec list_rev_mem_assoc x = function | [] -> false | (_,x')::l -> Id.equal x x' || list_rev_mem_assoc x l let check_variables vars recvars (found,foundrec,foundrecbinding) = let useless_vars = List.map snd recvars in let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in let check_recvar x = if List.mem x found then errorlabstrm "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in List.iter (fun (x,y) -> check_recvar x; check_recvar y) (foundrec@foundrecbinding); let check_bound x = if not (List.mem x found) then if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding then error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.") else error ((Id.to_string x)^" is unbound in the right-hand side.") in let check_pair s x y where = if not (List.mem (x,y) where) then errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type (x,typ) = match typ with | NtnInternTypeConstr -> begin try check_pair "term" x (List.assoc x recvars) foundrec with Not_found -> check_bound x end | NtnInternTypeBinder -> begin try check_pair "binding" x (List.assoc x recvars) foundrecbinding with Not_found -> check_bound x end | NtnInternTypeIdent -> check_bound x in List.iter check_type vars let notation_constr_of_glob_constr vars recvars a = let a,found = notation_constr_and_vars_of_glob_constr a in check_variables vars recvars found; a (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with | PatVar _ -> pat | PatCstr (loc,((kn,i),j),cpl,n) -> let kn' = subst_ind 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) let rec subst_notation_constr subst bound raw = match raw with | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else notation_constr_of_constr bound t | NVar _ -> raw | NApp (r,rl) -> let r' = subst_notation_constr subst bound r and rl' = List.smartmap (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') | NList (id1,id2,r1,r2,b) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NList (id1,id2,r1',r2',b) | NLambda (n,r1,r2) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NLambda (n,r1',r2') | NProd (n,r1,r2) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NProd (n,r1',r2') | NBinderList (id1,id2,r1,r2) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NBinderList (id1,id2,r1',r2') | NLetIn (n,r1,r2) -> let r1' = subst_notation_constr subst bound r1 and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else NLetIn (n,r1',r2') | NCases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt and rl' = List.smartmap (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 if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl and branches' = List.smartmap (fun (cpl,r as branch) -> let cpl' = List.smartmap (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) branches in if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & rl' == rl && branches' == branches then raw else NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> let po' = Option.smartmap (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> let po' = Option.smartmap (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else NIf (c',(na,po'),b1',b2') | NRec (fk,idl,dll,tl,bl) -> let dll' = Array.smartmap (List.smartmap (fun (na,oc,b as x) -> let oc' = Option.smartmap (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in let tl' = Array.smartmap (subst_notation_constr subst bound) tl in let bl' = Array.smartmap (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') | NPatVar _ | NSort _ -> raw | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> let ref',t = subst_global subst ref in if ref' == ref then raw else NHole (Evar_kinds.InternalHole) | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ |Evar_kinds.CasesType |Evar_kinds.InternalHole |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') 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 *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> let nal = List.flatten (List.map (fun (_,(na,t)) -> match t with Some x -> (pi x)@[na] | None -> [na]) tml) in List.fold_right mklam nal rtn) rtno let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,nal) -> nal) (fun na c -> GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole),c)) let abstract_return_type_context_notation_constr = abstract_return_type_context snd (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) exception No_match let rec alpha_var id1 id2 = function | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2 | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1 | _::idl -> alpha_var id1 id2 idl | [] -> Id.equal id1 id2 let compare_var v1 v2 = match v1, v2 with | GHole _, _ -> (true,true) | _, GHole _ -> (false,false) | _, _ -> (true,Pervasives.(=) v1 v2 (** FIXME *)) let add_env alp (sigma,sigmalist,sigmabinders) 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; (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::sigma,sigmalist,sigmabinders) let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = try let v' = List.assoc var sigma in match v, v' with | GHole _, _ -> fullsigma | _, GHole _ -> add_env alp (List.remove_assoc var sigma,sigmalist,sigmabinders) var v | _, _ -> if Pervasives.(=) v v' then fullsigma (** FIXME *) else raise No_match with Not_found -> add_env alp fullsigma var v let bind_binder (sigma,sigmalist,sigmabinders) x bl = (sigma,sigmalist,(x,List.rev bl)::sigmabinders) let match_fix_kind fk1 fk2 = match (fk1,fk2) with | GCoFix n1, GCoFix n2 -> Int.equal n1 n2 | GFix (nl1,n1), GFix (nl2,n2) -> let test (n1, _) (n2, _) = match n1, n2 with | _, None -> true | Some id1, Some id2 -> Int.equal id1 id2 | _ -> false in Int.equal n1 n2 && Array.for_all2 test nl1 nl2 | _ -> false let match_opt f sigma t1 t2 = match (t1,t2) with | None, None -> sigma | Some t1, Some t2 -> f sigma t1 t2 | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (_,Name id2) when List.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (Loc.ghost,id1) | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match let rec match_cases_pattern_binders metas acc pat1 pat2 = match (pat1,pat2) with | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2 | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> List.fold_left2 (match_cases_pattern_binders metas) (match_names metas acc na1 na2) patl1 patl2 | _ -> raise No_match let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function | GLambda (_,na,bk,t,b) when islambda -> match_iterated_binders islambda ((na,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 | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = (List.remove_assoc x sigmavar,sigmalist,sigmabinders) let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in let rest = List.assoc ldots_var (pi1 sigma) in let b = match List.assoc x (pi3 sigma) 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 match_alist match_fun metas sigma rest x 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 = List.assoc ldots_var (pi1 sigma) in let t = List.assoc x (pi1 sigma) in let sigma = remove_sigma x (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 does_not_come_from_already_eta_expanded_var = (* This is hack to avoid looping on a rule with rhs of the form *) (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) (* "F (fun x => H x)" and "H x" is recursively matched against the same *) (* rule, giving "H (fun x' => x x')" and so on. *) (* Ideally, we would need the type of the expression to know which of *) (* the arguments applied to it can be eta-expanded without looping. *) (* The following test is then an approximation of what can be done *) (* optimally (whether other looping situations can occur remains to be *) (* checked). *) function GVar _ -> false | _ -> true let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) | r1, NVar id2 when List.mem id2 tmetas -> bind_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 (* 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 (* 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) when na1 != Anonymous -> let (decls,b) = match_iterated_binders false [(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 (* 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 (* Matching individual binders as part of a recursive pattern *) | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) when List.mem id blmetas && na != Anonymous -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) | GVar (_,id1), NVar id2 when alpha_var id1 id2 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 = if n1 < n2 then let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 else if n1 > n2 then let l11,l12 = List.chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) (match_in u alp metas sigma f1 f2) l1 l2 | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) && Int.equal (List.length eqnl1) (List.length eqnl2) -> let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in let sigma = try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' with Option.Heterogeneous -> raise No_match in let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when Int.equal (List.length nal1) (List.length nal2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in let sigma = match_in u alp metas sigma b1 b2 in let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_in u alp metas sigma c1 c2 | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2) when match_fix_kind fk1 fk2 && Int.equal (Array.length idl1) (Array.length idl2) && Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2 -> let alp,sigma = Array.fold_left2 (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) -> let sigma = match_in u alp metas (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2 in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in let sigma = Array.fold_left2 (match_in u alp metas) sigma tl1 tl2 in let alp,sigma = Array.fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> match_in u alp metas sigma c1 c2 | GSort (_,GType _), NSort (GType None) when not u -> sigma | GSort (_,s1), NSort s2 when glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma (* On the fly eta-expansion so as to use notations of the form "exists x, P x" for "ex P"; ensure at least one constructor is consumed to avoid looping; expects type not given because don't know 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 let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id')) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_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 | (GRec _ | GEvar _), _ | _,_ -> raise No_match and match_in u = match_ true u and match_hd u = match_ false u and match_binders u alp metas na1 na2 sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in match_in u alp metas sigma b1 b2 and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) let (alp,sigma) = List.fold_left2 (match_cases_pattern_binders metas) (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 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 (* Reorder canonically the substitution *) let find x = try List.assoc x terms with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) GVar (Loc.ghost,x) in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> ((find x, scl)::terms',termlists',binders') | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> (terms',termlists',(List.assoc x binders,scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) let add_patterns_for_params ind l = let mib,_ = Global.lookup_inductive ind in 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 = try let vvar = List.assoc var sigma in if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *) with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) (var,v)::sigma,sigmalist,x let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | r1, NVar id2 when List.mem 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) | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then raise No_match 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,[]) | _ -> 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 let match_ind_pattern metas sigma ind pats a2 = match a2 with | NRef (IndRef r2) when eq_ind ind r2 -> sigma,(0,pats) | NApp (NRef (IndRef r2),l2) when eq_ind ind r2 -> let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats then raise No_match else let l1',more_args = Util.List.chop le2 pats in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) |_ -> raise No_match let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists') | NtnTypeConstrList -> (terms',(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 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 reorder_canonically_substitution terms termlists metas, more_args