(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* QInd.equal env i1 i2) i1.cip_ind i2.cip_ind && i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq env (p1:constr_pattern) p2 = match p1, p2 with | PRef r1, PRef r2 -> QGlobRef.equal env r1 r2 | PVar v1, PVar v2 -> Id.equal v1 v2 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) -> Evar.equal ev1 ev2 && List.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) ctx1 ctx2 | PRel i1, PRel i2 -> Int.equal i1 i2 | PApp (t1, arg1), PApp (t2, arg2) -> constr_pattern_eq env t1 t2 && Array.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) arg1 arg2 | PSoApp (id1, arg1), PSoApp (id2, arg2) -> Id.equal id1 id2 && List.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) arg1 arg2 | PLambda (v1, t1, b1), PLambda (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq env t1 t2 && constr_pattern_eq env b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq env t1 t2 && constr_pattern_eq env b1 b2 | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> Name.equal v1 v2 && constr_pattern_eq env b1 b2 && Option.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) t1 t2 && constr_pattern_eq env c1 c2 | PSort s1, PSort s2 -> UnivGen.QualityOrSet.equal s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> constr_pattern_eq env t1 t2 && constr_pattern_eq env l1 l2 && constr_pattern_eq env r1 r2 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) -> case_info_pattern_eq env info1 info2 && Option.equal (fun (nas1, p1) (nas2, p2) -> Array.equal Name.equal nas1 nas2 && constr_pattern_eq env p1 p2) p1 p2 && constr_pattern_eq env r1 r2 && List.equal (fun p1 p2 -> pattern_eq env p1 p2) l1 l2 | PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq env f1 f2 | PCoFix (i1,f1), PCoFix (i2,f2) -> Int.equal i1 i2 && rec_declaration_eq env f1 f2 | PProj (p1, t1), PProj (p2, t2) -> QProjection.equal env p1 p2 && constr_pattern_eq env t1 t2 | PInt i1, PInt i2 -> Uint63.equal i1 i2 | PFloat f1, PFloat f2 -> Float64.equal f1 f2 | PString s1, PString s2 -> Pstring.equal s1 s2 | PArray (t1, def1, ty1), PArray (t2, def2, ty2) -> Array.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) t1 t2 && constr_pattern_eq env def1 def2 && constr_pattern_eq env ty1 ty2 | PExtra e, _ -> Util.Empty.abort e | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _ | PFloat _ | PString _ | PArray _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq env (i1, j1, p1) (i2, j2, p2) = Int.equal i1 i2 && Array.equal Name.equal j1 j2 && constr_pattern_eq env p1 p2 and rec_declaration_eq env (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && Array.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) c1 c2 && Array.equal (fun c1 c2 -> constr_pattern_eq env c1 c2) r1 r2 let rec occurn_pattern : 'a. _ -> 'a constr_pattern_r -> _ = fun (type a) n (p:a constr_pattern_r) -> match p with | PRel p -> Int.equal n p | PApp (f,args) -> (occurn_pattern n f) || (Array.exists (occurn_pattern n) args) | PProj (_,arg) -> occurn_pattern n arg | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) | PLetIn (na,b,t,c) -> Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t || (occurn_pattern (n+1) c) | PIf (c,c1,c2) -> (occurn_pattern n c) || (occurn_pattern n c1) || (occurn_pattern n c2) | PCase(_, p, c, br) -> Option.cata (fun (nas, p) -> occurn_pattern (Array.length nas + n) p) false p || (occurn_pattern n c) || (List.exists (fun (_, nas, p) -> occurn_pattern (Array.length nas + n) p) br) | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> List.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ | PString _ -> false | PFix (_,(_,tl,bl)) -> Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl | PCoFix (_,(_,tl,bl)) -> Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl | PArray (t,def,ty) -> Array.exists (occurn_pattern n) t || occurn_pattern n def || occurn_pattern n ty | PExtra _ -> false (* XXX dubious behaviour *) let noccurn_pattern n c = not (occurn_pattern n c) exception BoundPattern;; let rec head_pattern_bound (t:constr_pattern) = match t with | PProd (_,_,b) -> head_pattern_bound b | PLetIn (_,_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> GlobRef.VarRef id | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern | PCoFix _ | PInt _ | PFloat _ | PString _ | PArray _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") | PExtra e -> Util.Empty.abort e let mkPRef env gr = PRef (Environ.QGlobRef.canonize env gr) let pattern_of_constr ~broken env sigma t = let t = EConstr.Unsafe.to_constr t in let kind = if broken then Constr.kind else fun c -> EConstr.kind_upto sigma c in let rec pattern_of_constr env t = let open Context.Rel.Declaration in match kind t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id | Sort s -> PSort (EConstr.ESorts.quality_or_set sigma (EConstr.ESorts.make s)) | Cast (c,_,_) -> pattern_of_constr env c | LetIn (na,c,t,b) -> PLetIn (na.binder_name, pattern_of_constr env c,Some (pattern_of_constr env t), pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na.binder_name, pattern_of_constr env c, pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | Lambda (na,c,b) -> PLambda (na.binder_name, pattern_of_constr env c, pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match kind f with | Evar (evk,args) -> let EvarInfo evi = Evd.find sigma evk in (match snd (Evd.evar_source evi) with Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) | Const (sp,u) -> mkPRef env (GlobRef.ConstRef sp) | Ind (sp,u) -> mkPRef env (GlobRef.IndRef sp) | Construct (sp,u) -> mkPRef env (GlobRef.ConstructRef sp) | Proj (p, _, c) -> pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> let EvarInfo evi = Evd.find sigma evk in (match snd (Evd.evar_source evi) with | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) -> PMeta (Some id) | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) begin match Evd.existential_opt_value0 sigma ev with | Some v -> pattern_of_constr env v | None -> let ctxt = Evd.expand_existential sigma (EConstr.of_existential ev) in PEvar (evk,List.map (fun c -> pattern_of_constr env (EConstr.Unsafe.to_constr c)) ctxt) end | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) | Case (ci, u, pms, p0, iv, a, br0) -> let (ci, (p,_), iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in let pattern_of_ctx c (nas, c0) = let ctx, c = Term.decompose_lambda_n_decls (Array.length nas) c in let env = push_rel_context ctx env in let c = pattern_of_constr env c in (Array.map Context.binder_name nas, c) in let p = pattern_of_ctx p (fst p0) in let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; cip_extensible = false } in let branch_of_constr i c = let nas, c = pattern_of_ctx c br0.(i) in (i, nas, c) in PCase (cip, Some p, pattern_of_constr env a, Array.to_list (Array.mapi branch_of_constr br)) | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in PFix (lni,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | CoFix (ln,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | Int i -> PInt i | Float f -> PFloat f | String s -> PString s | Array (_u, t, def, ty) -> PArray (Array.map (pattern_of_constr env) t, pattern_of_constr env def, pattern_of_constr env ty) in pattern_of_constr env t let legacy_bad_pattern_of_constr env sigma c : constr_pattern = pattern_of_constr ~broken:true env sigma c let pattern_of_constr env sigma c = pattern_of_constr ~broken:false env sigma c (* To process patterns, we need a translation without typing at all. *) let map_pattern_with_binders_gen (type a b) g f fgen l : a constr_pattern_r -> b constr_pattern_r = function | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl) | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl) | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b) | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b) | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> let fold nas l = Array.fold_left (fun l na -> g na l) l nas in let map_branch (i, n, c) = (i, n, f (fold n l) c) in let po = Option.map (fun (nas, po) -> nas, (f (fold nas l) po)) po in PCase (ci,po,f l p, List.map map_branch pl) | PProj (p,pc) -> PProj (p, f l pc) | PFix (lni,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl)) | PCoFix (ln,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) | PArray (t,def,ty) -> PArray (Array.map (f l) t, f l def, f l ty) | PEvar (ev,ps) -> PEvar (ev, List.map (f l) ps) | PExtra x -> fgen l x (* Non recursive *) | (PVar _ | PRel _ | PRef _ | PSort _ | PMeta _ | PInt _ | PFloat _ | PString _ as x) -> x let map_pattern_with_binders (type a) g f l (p:a constr_pattern_r) : a constr_pattern_r = let fgen _ : a -> a constr_pattern_r = function | x -> PExtra x in map_pattern_with_binders_gen g f fgen l p let rec liftn_pattern k n = function | PRel i as x -> if i >= n then PRel (i+k) else x | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c let lift_pattern k = liftn_pattern k 1 let rec subst_pattern_gen : 'a. (_ -> 'a -> 'a) -> _ -> _ -> _ -> 'a constr_pattern_r -> 'a constr_pattern_r = fun (type a) gsubst env sigma subst (pat: a constr_pattern_r) -> match pat with | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else (match t with | None -> PRef ref' | Some t -> pattern_of_constr env sigma (EConstr.of_constr t.UVars.univ_abstracted_value)) | PVar _ | PEvar _ | PRel _ | PInt _ | PFloat _ | PString _ -> pat | PExtra g -> PExtra (gsubst subst g) | PProj (p,c) -> let p' = Projection.map (subst_mind subst) p in let c' = subst_pattern_gen gsubst env sigma subst c in if p' == p && c' == c then pat else PProj(p',c') | PApp (f,args) -> let f' = subst_pattern_gen gsubst env sigma subst f in let args' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> let args' = List.Smart.map (subst_pattern_gen gsubst env sigma subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> let c1' = subst_pattern_gen gsubst env sigma subst c1 in let c2' = subst_pattern_gen gsubst env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PLambda (name,c1',c2') | PProd (name,c1,c2) -> let c1' = subst_pattern_gen gsubst env sigma subst c1 in let c2' = subst_pattern_gen gsubst env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern_gen gsubst env sigma subst c1 in let t' = Option.Smart.map (subst_pattern_gen gsubst env sigma subst) t in let c2' = subst_pattern_gen gsubst env sigma subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> let c' = subst_pattern_gen gsubst env sigma subst c in let c1' = subst_pattern_gen gsubst env sigma subst c1 in let c2' = subst_pattern_gen gsubst env sigma subst c2 in if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in let map ((nas, typ) as t) = let typ' = subst_pattern_gen gsubst env sigma subst typ in if typ' == typ then t else (nas, typ') in let typ' = Option.Smart.map map typ in let c' = subst_pattern_gen gsubst env sigma subst c in let subst_branch ((i,n,c) as br) = let c' = subst_pattern_gen gsubst env sigma subst c in if c' == c then br else (i,n,c') in let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> let tl' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) tl in let bl' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> let tl' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) tl in let bl' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) | PArray (t,def,ty) -> let t' = Array.Smart.map (subst_pattern_gen gsubst env sigma subst) t in let def' = subst_pattern_gen gsubst env sigma subst def in let ty' = subst_pattern_gen gsubst env sigma subst ty in if def' == def && t' == t && ty' == ty then pat else PArray (t',def',ty') let subst_pattern env sigma subst p = subst_pattern_gen (fun _ e -> Util.Empty.abort e) env sigma subst p let subst_uninstantiated_pattern env sigma subst p = subst_pattern_gen Gensubst.constr_subst env sigma subst p let mkPLetIn na b t c = PLetIn(na,b,t,c) let mkPProd na t u = PProd(na,t,u) let mkPLambda na t b = PLambda(na,t,b) let mkPProd_or_LetIn (na,_,bo,t) c = match bo with | None -> mkPProd na t c | Some b -> mkPLetIn na b (Some t) c let mkPLambda_or_LetIn (na,_,bo,t) c = match bo with | None -> mkPLambda na t c | Some b -> mkPLetIn na b (Some t) c let it_mkPProd_or_LetIn x y = List.fold_left (fun c d -> mkPProd_or_LetIn d c) x y let it_mkPLambda_or_LetIn x y = List.fold_left (fun c d -> mkPLambda_or_LetIn d c) x y type 'a pat_interp_fun = Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> 'a -> Pattern.constr_pattern module InterpPatObj = struct type (_, 'g) t = 'g pat_interp_fun end module InterpPat = GenConstr.Register(InterpPatObj) let interp_pat = InterpPat.get let register_interp_pat = InterpPat.register let error_instantiate_pattern id l = let is = match l with | [_] -> "is" | _ -> "are" in user_err (str "Cannot substitute the term bound to " ++ Id.print id ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") let interp_pattern env sigma ist p = let fgen vars = function | GenConstr.Glb (tag, g) -> interp_pat tag env sigma ist g in let rec aux vars = function | PVar id as x -> (try let ctx,c = Id.Map.find id ist.Ltac_pretype.ltac_constrs in try let inst = List.map (fun id -> EConstr.mkRel (List.index Name.equal (Name id) vars)) ctx in let c = EConstr.Vars.substl inst c in pattern_of_constr env sigma c with Not_found (* List.index failed *) -> let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) | p -> map_pattern_with_binders_gen (fun id vars -> id :: vars) (fun vars p -> aux vars p) fgen vars p in aux [] p let err ?loc pp = user_err ?loc pp let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:CWarnings.CoreCategories.automation (fun () -> Pp.strbrk "Cast types are ignored in patterns") type meta_accu = | Metas of Id.Set.t ref | InCastType of Loc.t option let push_meta metas n = match metas with | Metas metas -> metas := Id.Set.add n !metas | InCastType loc -> CErrors.user_err ?loc Pp.(str "Cannot bind pattern variable in cast type:" ++ spc() ++ str "cast types are ignored in patterns.") let in_cast_type loc = function | Metas _ -> InCastType loc | InCastType _ as v -> (* We report the error with the loc of the outermost cast Alternatively we could use the loc of the meta, or the loc of the innermost cast. *) v let pat_of_raw env metas vars p = let rec pat_of_raw metas vars : _ -> _ constr_pattern_r = DAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) | GPatVar (Evar_kinds.FirstOrderPatVar n) -> push_meta metas n; PMeta (Some n) | GRef (gr,_) -> PRef (Environ.QGlobRef.canonize env gr) (* Hack to avoid rewriting a complete interpretation of patterns *) | GApp (c, cl) -> begin match DAst.get c with | GPatVar (Evar_kinds.SecondOrderPatVar n) -> push_meta metas n; PSoApp (n, List.map (pat_of_raw metas vars) cl) | _ -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) end | GProj ((p,_), cl, c) -> if Structures.PrimitiveProjections.mem p then let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in let p = Projection.make p false in PProj (p, pat_of_raw metas vars c) else PApp (PRef (GlobRef.ConstRef p), Array.map_of_list (pat_of_raw metas vars) (cl @ [c])) | GLambda (na,_,bk,c1,c2) -> Name.iter (fun n -> push_meta metas n) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GProd (na,_,bk,c1,c2) -> Name.iter (fun n -> push_meta metas n) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GLetIn (na,_,c1,t,c2) -> Name.iter (fun n -> push_meta metas n) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) | GSort gs -> (try PSort (Glob_ops.glob_sort_quality gs) with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern.")) | GHole _ -> PMeta None | GGenarg (GenConstr.Glb (tag, _) as g) -> let () = if not (InterpPat.mem tag) then let name = GenConstr.repr tag in user_err ?loc (str "This quotation is not supported in patterns (" ++ str name ++ str ").") in PExtra g | GCast (c,_,t) -> let () = (* Checks that there are no pattern variables in the type *) let _ : _ constr_pattern_r = pat_of_raw (in_cast_type t.loc metas) vars t in () in warn_cast_in_pattern ?loc (); pat_of_raw metas vars c | GIf (c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> let cip = { cip_style = LetStyle; cip_ind = None; cip_extensible = false } in let tags = Array.of_list nal (* Approximation which can be without let-ins... *) in PCase (cip, None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas (List.rev_append (Array.to_list tags) vars) c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind p = match DAst.get p with | PatCstr((ind,_),_,_) -> Some ind | _ -> None in let get_ind = function | {CAst.v=(_,[p],_)}::_ -> get_ind p | _ -> None in let ind_tags,ind = match indnames with | Some {CAst.v=(ind,nal)} -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in Some (Array.rev_of_list (na :: List.rev nal), pat_of_raw metas nvars p) | None, _ -> None | Some p, None -> match DAst.get p with | GHole _ -> None | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; cip_ind = ind; cip_extensible = ext } in (* Nota : when we have a non-trivial predicate, the inductive type is known. Same when we have at least one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) | GRec (GFix (ln,n), ids, decls, tl, cl) -> let get_struct_arg = function | Some n -> n | None -> err ?loc (Pp.str "\"struct\" annotation is expected.") (* TODO why can't the annotation be omitted? *) in let ln = Array.map get_struct_arg ln in let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in let names = Array.map (fun id -> Name id) ids in PFix ((ln,n), (names, tl, cl)) | GRec (GCoFix n, ids, decls, tl, cl) -> let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in let names = Array.map (fun id -> Name id) ids in PCoFix (n, (names, tl, cl)) | GInt i -> PInt i | GFloat f -> PFloat f | GString s -> PString s | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GArray _ -> err ?loc (Pp.str "Non supported pattern.")) and pat_of_glob_in_context metas vars decls c = let rec aux acc vars = function | (na,_,bk,b,t) :: decls -> let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in aux (decl::acc) (na::vars) decls | [] -> acc, pat_of_raw metas vars c in aux [] vars decls and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with | PatVar na -> Name.iter (fun n -> push_meta metas n) na; na | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] | {CAst.loc=loc';v=(_,[p], br)} :: brs -> begin match DAst.get p, DAst.get br, brs with | PatVar Anonymous, GHole _, [] -> true, [] (* ends with _ => _ *) | PatCstr((indsp,j),lv,_), _, _ -> let () = match ind with | Some sp when Ind.UserOrd.equal sp indsp -> () | _ -> err ?loc (Pp.str "All constructors must be in the same inductive type.") in if Int.Set.mem (j-1) indexes then err ?loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev_append lna vars in let tags = Array.of_list lna in let pat = pat_of_raw metas vars' br in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in ext, ((j-1, tags, pat) :: pats) | _ -> err ?loc:loc' (Pp.str "Non supported pattern.") end | {CAst.loc;v=(_,_,_)} :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs in pat_of_raw metas vars p let pattern_of_glob_constr env c = let metas = ref Id.Set.empty in let p = pat_of_raw env (Metas metas) [] c in (!metas, p)