diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 489 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 37 | ||||
| -rw-r--r-- | interp/constrextern.ml | 19 | ||||
| -rw-r--r-- | interp/constrextern.mli | 13 | ||||
| -rw-r--r-- | interp/constrintern.ml | 45 | ||||
| -rw-r--r-- | interp/declare.ml | 44 | ||||
| -rw-r--r-- | interp/declare.mli | 6 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.ml | 4 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 12 | ||||
| -rw-r--r-- | interp/interp.mllib | 6 | ||||
| -rw-r--r-- | interp/modintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 35 | ||||
| -rw-r--r-- | interp/reserve.ml | 6 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 7 | ||||
| -rw-r--r-- | interp/topconstr.ml | 300 | ||||
| -rw-r--r-- | interp/topconstr.mli | 41 |
17 files changed, 561 insertions, 507 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 771c137344..8b78a91b5b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -9,6 +9,7 @@ open Pp open Util open Names +open Nameops open Libnames open Constrexpr open Misctypes @@ -72,22 +73,22 @@ let rec cases_pattern_expr_eq p1 p2 = Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(r1), CPatAtom(r2) -> - Option.equal eq_reference r1 r2 + Option.equal eq_reference r1 r2 | CPatOr a1, CPatOr a2 -> - List.equal cases_pattern_expr_eq a1 a2 + List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> String.equal n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 | CPatPrim i1, CPatPrim i2 -> - prim_token_eq i1 i2 + prim_token_eq i1 i2 | CPatRecord l1, CPatRecord l2 -> - let equal (r1, e1) (r2, e2) = - eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 - in - List.equal equal l1 l2 + let equal (r1, e1) (r2, e2) = + eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + in + List.equal equal l1 l2 | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> - String.equal s1 s2 && cases_pattern_expr_eq e1 e2 + String.equal s1 s2 && cases_pattern_expr_eq e1 e2 | _ -> false and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) = @@ -103,79 +104,79 @@ let eq_universes u1 u2 = let rec constr_expr_eq e1 e2 = if CAst.(e1.v == e2.v) then true else match CAst.(e1.v, e2.v) with - | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 - | CFix(id1,fl1), CFix(id2,fl2) -> + | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 + | CFix(id1,fl1), CFix(id2,fl2) -> eq_located Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 - | CCoFix(id1,fl1), CCoFix(id2,fl2) -> + | CCoFix(id1,fl1), CCoFix(id2,fl2) -> eq_located Id.equal id1 id2 && List.equal cofix_expr_eq fl1 fl2 - | CProdN(bl1,a1), CProdN(bl2,a2) -> + | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> + | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> + | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 - | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> + | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && eq_reference r1 r2 && List.equal constr_expr_eq al1 al2 - | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> + | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && constr_expr_eq e1 e2 && List.equal args_eq al1 al2 - | CRecord l1, CRecord l2 -> - let field_eq (r1, e1) (r2, e2) = - eq_reference r1 r2 && constr_expr_eq e1 e2 - in - List.equal field_eq l1 l2 - | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> + | CRecord l1, CRecord l2 -> + let field_eq (r1, e1) (r2, e2) = + eq_reference r1 r2 && constr_expr_eq e1 e2 + in + List.equal field_eq l1 l2 + | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> (** Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 - | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_located Name.equal) n1 n2 && - Option.equal (eq_located Name.equal) m1 m2 && - Option.equal constr_expr_eq e1 e2 && - constr_expr_eq t1 t2 && - constr_expr_eq b1 b2 - | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> - constr_expr_eq e1 e2 && - Option.equal (eq_located Name.equal) n1 n2 && - Option.equal constr_expr_eq r1 r2 && - constr_expr_eq t1 t2 && - constr_expr_eq f1 f2 - | CHole _, CHole _ -> true - | CPatVar i1, CPatVar i2 -> - Id.equal i1 i2 - | CEvar (id1, c1), CEvar (id2, c2) -> - Id.equal id1 id2 && List.equal instance_eq c1 c2 - | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 - | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) -> - constr_expr_eq a1 a2 && + | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> + List.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_located Name.equal) m1 m2 && + Option.equal constr_expr_eq e1 e2 && + constr_expr_eq t1 t2 && constr_expr_eq b1 b2 - | CCast(a1,CastCoerce), CCast(a2, CastCoerce) -> - constr_expr_eq a1 a2 - | CNotation(n1, s1), CNotation(n2, s2) -> + | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> + constr_expr_eq e1 e2 && + Option.equal (eq_located Name.equal) n1 n2 && + Option.equal constr_expr_eq r1 r2 && + constr_expr_eq t1 t2 && + constr_expr_eq f1 f2 + | CHole _, CHole _ -> true + | CPatVar i1, CPatVar i2 -> + Id.equal i1 i2 + | CEvar (id1, c1), CEvar (id2, c2) -> + Id.equal id1 id2 && List.equal instance_eq c1 c2 + | CSort s1, CSort s2 -> + Miscops.glob_sort_eq s1 s2 + | CCast(t1,c1), CCast(t2,c2) -> + constr_expr_eq t1 t2 && cast_expr_eq c1 c2 + | CNotation(n1, s1), CNotation(n2, s2) -> String.equal n1 n2 && constr_notation_substitution_eq s1 s2 - | CPrim i1, CPrim i2 -> - prim_token_eq i1 i2 - | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && - Option.equal abstraction_kind_eq ak1 ak2 && - constr_expr_eq e1 e2 - | CDelimiters(s1,e1), CDelimiters(s2,e2) -> - String.equal s1 s2 && - constr_expr_eq e1 e2 - | _ -> false + | CPrim i1, CPrim i2 -> + prim_token_eq i1 i2 + | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> + binding_kind_eq bk1 bk2 && + Option.equal abstraction_kind_eq ak1 ak2 && + constr_expr_eq e1 e2 + | CDelimiters(s1,e1), CDelimiters(s2,e2) -> + String.equal s1 s2 && + constr_expr_eq e1 e2 + | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ + | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ + | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ + | CGeneralization _ | CDelimiters _), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && @@ -209,19 +210,19 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = constr_expr_eq b1 b2 and recursion_order_expr_eq r1 r2 = match r1, r2 with -| CStructRec, CStructRec -> true -| CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 -| CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> - constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 -| _ -> false + | CStructRec, CStructRec -> true + | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 + | CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> + constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 + | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 -| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) - List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 -| _ -> false + | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> + (** Don't care about the [binder_kind] *) + List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 + | _ -> false and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = List.equal constr_expr_eq e1 e2 && @@ -231,6 +232,16 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = and instance_eq (x1,c1) (x2,c2) = Id.equal x1 x2 && constr_expr_eq c1 c2 +and cast_expr_eq c1 c2 = match c1, c2 with +| CastConv t1, CastConv t2 +| CastVM t1, CastVM t2 +| CastNative t1, CastNative t2 -> constr_expr_eq t1 t2 +| CastCoerce, CastCoerce -> true +| CastConv _, _ +| CastVM _, _ +| CastNative _, _ +| CastCoerce, _ -> false + let constr_loc c = CAst.(c.loc) let cases_pattern_expr_loc cp = CAst.(cp.loc) @@ -245,6 +256,270 @@ let local_binders_loc bll = match bll with | [] -> None | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) +(** Folds and maps *) + +(* Legacy functions *) +let down_located f (_l, x) = f x +let located_fold_left f x (_l, y) = f x y + +let is_constructor id = + try Globnames.isConstructRef + (Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id))) + with Not_found -> false + +let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with + | CPatRecord l -> + List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l + | CPatAlias (pat,id) -> f id a + | CPatOr (patl) -> + List.fold_left (cases_pattern_fold_names f) a patl + | CPatCstr (_,patl1,patl2) -> + List.fold_left (cases_pattern_fold_names f) + (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 + | CPatNotation (_,(patl,patll),patl') -> + List.fold_left (cases_pattern_fold_names f) + (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' + | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat + | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a + | CPatPrim _ | CPatAtom _ -> a + | CPatCast ({CAst.loc},_) -> + CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" + (Pp.strbrk "Casts are not supported here.") + +let ids_of_pattern = + cases_pattern_fold_names Id.Set.add Id.Set.empty + +let ids_of_pattern_list = + List.fold_left + (located_fold_left + (List.fold_left (cases_pattern_fold_names Id.Set.add))) + Id.Set.empty + +let ids_of_cases_indtype p = + cases_pattern_fold_names Id.Set.add Id.Set.empty p + +let ids_of_cases_tomatch tms = + List.fold_right + (fun (_, ona, indnal) l -> + Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) + indnal + (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) + tms Id.Set.empty + +let rec fold_constr_expr_binders g f n acc b = function + | (nal,bk,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (Name.fold_right g) nal n in + f n (fold_constr_expr_binders g f n' acc b l) t + | [] -> + f n acc b + +let rec fold_local_binders g f n acc b = function + | CLocalAssum (nal,bk,t)::l -> + let nal = snd (List.split nal) in + let n' = List.fold_right (Name.fold_right g) nal n in + f n (fold_local_binders g f n' acc b l) t + | CLocalDef ((_,na),c,t)::l -> + Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t + | CLocalPattern (_,(pat,t))::l -> + let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in + Option.fold_left (f n) acc t + | [] -> + f n acc b + +let fold_constr_expr_with_binders g f n acc = CAst.with_val (function + | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l + | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) + | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l + | CLetIn (na,a,t,b) -> + f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b + | CCast (a,CastCoerce) -> f n acc a + | CNotation (_,(l,ll,bll)) -> + (* The following is an approximation: we don't know exactly if + an ident is binding nor to which subterms bindings apply *) + let acc = List.fold_left (f n) acc (l@List.flatten ll) in + List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll + | CGeneralization (_,_,c) -> f n acc c + | CDelimiters (_,a) -> f n acc a + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> + acc + | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l + | CCases (sty,rtnpo,al,bl) -> + let ids = ids_of_cases_tomatch al in + let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in + let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in + List.fold_right (fun (loc,(patl,rhs)) acc -> + let ids = ids_of_pattern_list patl in + f (Id.Set.fold g ids n) acc rhs) bl acc + | CLetTuple (nal,(ona,po),b,c) -> + let n' = List.fold_right (down_located (Name.fold_right g)) nal n in + f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c + | CIf (c,(ona,po),b1,b2) -> + let acc = f n (f n (f n acc b1) b2) c in + Option.fold_left + (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po + | CFix (_,l) -> + let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in + List.fold_right (fun (_,(_,o),lb,t,c) acc -> + fold_local_binders g f n' + (fold_local_binders g f n acc t lb) c lb) l acc + | CCoFix (_,_) -> + Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc + ) + +let free_vars_of_constr_expr c = + let rec aux bdvars l = function + | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c + in aux [] Id.Set.empty c + +let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) + +(* Used in correctness and interface *) +let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e + +let map_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_local_binders f g e bl = + (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let h (e,bl) = function + CLocalAssum(nal,k,ty) -> + (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) + | CLocalDef((loc,na),c,ty) -> + (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + | CLocalPattern (loc,(pat,t)) -> + let ids = ids_of_pattern pat in + (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in + let (e,rbl) = List.fold_left h (e,[]) bl in + (e, List.rev rbl) + +let map_constr_expr_with_binders g f e = CAst.map (function + | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) + | CApp ((p,a),l) -> + CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) + | CProdN (bl,b) -> + let (e,bl) = map_binders f g e bl in CProdN (bl,f e b) + | CLambdaN (bl,b) -> + let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) + | CLetIn (na,a,t,b) -> + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) + | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CNotation (n,(l,ll,bll)) -> + (* This is an approximation because we don't know what binds what *) + CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, + List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) + | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) + | CDelimiters (s,a) -> CDelimiters (s,f e a) + | CHole _ | CEvar _ | CPatVar _ | CSort _ + | CPrim _ | CRef _ as x -> x + | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l) + | CCases (sty,rtnpo,a,bl) -> + let bl = List.map (fun (loc,(patl,rhs)) -> + let ids = ids_of_pattern_list patl in + (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in + let ids = ids_of_cases_tomatch a in + let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in + CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) + | CLetTuple (nal,(ona,po),b,c) -> + let e' = List.fold_right (down_located (Name.fold_right g)) nal e in + let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in + CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) + | CIf (c,(ona,po),b1,b2) -> + let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in + CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) + | CFix (id,dl) -> + CFix (id,List.map (fun (id,n,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + (* Note: fix names should be inserted before the arguments... *) + let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,n,bl',t',d')) dl) + | CCoFix (id,dl) -> + CCoFix (id,List.map (fun (id,bl,t,d) -> + let (e',bl') = map_local_binders f g e bl in + let t' = f e' t in + let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in + let d' = f e'' d in + (id,bl',t',d')) dl) + ) + +(* Used in constrintern *) +let rec replace_vars_constr_expr l = function + | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> + (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) + | c -> map_constr_expr_with_binders Id.Map.remove + replace_vars_constr_expr l c + +(* Returns the ranges of locs of the notation that are not occupied by args *) +(* and which are then occupied by proper symbols of the notation (or spaces) *) + +let locs_of_notation ?loc locs ntn = + let unloc loc = Option.cata Loc.unloc (0,0) loc in + let (bl, el) = unloc loc in + let locs = List.map unloc locs in + let rec aux pos = function + | [] -> if Int.equal pos el then [] else [(pos,el)] + | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l + in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) + +let ntn_loc ?loc (args,argslist,binderslist) = + locs_of_notation ?loc + (List.map constr_loc (args@List.flatten argslist)@ + List.map local_binders_loc binderslist) + +let patntn_loc ?loc (args,argslist) = + locs_of_notation ?loc + (List.map cases_pattern_expr_loc (args@List.flatten argslist)) + +let error_invalid_pattern_notation ?loc () = + CErrors.user_err ?loc (str "Invalid notation for pattern.") + +(* Interpret the index of a recursion order annotation *) +let split_at_annot bl na = + let names = List.map snd (names_of_local_assums bl) in + match na with + | None -> + begin match names with + | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.") + | _ -> ([], bl) + end + | Some (loc, id) -> + let rec aux acc = function + | CLocalAssum (bls, k, t) as x :: rest -> + let test (_, na) = match na with + | Name id' -> Id.equal id id' + | Anonymous -> false + in + let l, r = List.split_when test bls in + begin match r with + | [] -> aux (x :: acc) rest + | _ -> + let ans = match l with + | [] -> acc + | _ -> CLocalAssum (l, k, t) :: acc + in + (List.rev ans, CLocalAssum (r, k, t) :: rest) + end + | CLocalDef ((_,na),_,_) as x :: rest -> + if Name.equal (Name id) na then + CErrors.user_err ?loc + (Id.print id ++ str" must be a proper parameter and not a local definition.") + else + aux (x :: acc) rest + | CLocalPattern (_,_) :: rest -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") + | [] -> + CErrors.user_err ?loc + (str "No parameter named " ++ Id.print id ++ str".") + in aux [] bl + (** Pseudo-constructors *) let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None) @@ -265,38 +540,40 @@ let add_name_in_env env n = | Anonymous -> env | Name id -> id :: env -let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) () +let fresh_var env c = + Namegen.next_ident_away (Id.of_string "pat") + (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env) let expand_binders ?loc mkC bl c = let rec loop ?loc bl c = match bl with | [] -> ([], c) | b :: bl -> - match b with - | CLocalDef ((loc1,_) as n, oty, b) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = add_name_in_env env n in - (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) - | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let env = List.fold_left add_name_in_env env nl in - (env, mkC ?loc (nl,bk,t) c) - | CLocalAssum ([],_,_) -> loop ?loc bl c - | CLocalPattern (loc1, (p, ty)) -> - let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in - let ni = Hook.get fresh_var env c in - let id = (loc1, Name ni) in - let ty = match ty with - | Some ty -> ty - | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) - in - let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in - let c = CAst.make ?loc @@ - CCases - (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) - in - (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) + match b with + | CLocalDef ((loc1,_) as n, oty, b) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let env = add_name_in_env env n in + (env, CAst.make ?loc @@ CLetIn (n,oty,b,c)) + | CLocalAssum ((loc1,_)::_ as nl, bk, t) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let env = List.fold_left add_name_in_env env nl in + (env, mkC ?loc (nl,bk,t) c) + | CLocalAssum ([],_,_) -> loop ?loc bl c + | CLocalPattern (loc1, (p, ty)) -> + let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in + let ni = fresh_var env c in + let id = (loc1, Name ni) in + let ty = match ty with + | Some ty -> ty + | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None) + in + let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in + let c = CAst.make ?loc @@ + CCases + (LetPatternStyle, None, [(e,None,None)], + [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + in + (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in let (_, c) = loop ?loc bl c in c @@ -309,24 +586,34 @@ let mkCLambdaN ?loc bll c = let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in expand_binders ?loc mk bll c -(* Deprecated *) -let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c -let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c - let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> - CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" - (str "This expression should be a simple identifier.") + CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id) | { CAst.loc; _ } -> CErrors.user_err ?loc - ~hdr:"coerce_to_id" - (str "This expression should be a simple identifier.") + ~hdr:"coerce_to_id" + (str "This expression should be a simple identifier.") let coerce_to_name = function | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id) | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous) | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") + +let asymmetric_patterns = ref (false) +let _ = Goptions.declare_bool_option { + Goptions.optdepr = false; + Goptions.optname = "no parameters in constructors"; + Goptions.optkey = ["Asymmetric";"Patterns"]; + Goptions.optread = (fun () -> !asymmetric_patterns); + Goptions.optwrite = (fun a -> asymmetric_patterns:=a); +} + +(************************************************************************) +(* Deprecated *) +let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c +let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7bd275e510..3ecb3d3212 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -56,11 +56,11 @@ val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_exp (** @deprecated variant of mkCLambdaN *) val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr +[@@ocaml.deprecated "deprecated variant of mkCLambdaN"] (** @deprecated variant of mkCProdN *) val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr - -val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t +[@@ocaml.deprecated "deprecated variant of mkCProdN"] (** {6 Destructors}*) @@ -83,3 +83,36 @@ val names_of_local_binders : local_binder_expr list -> Name.t located list val names_of_local_assums : local_binder_expr list -> Name.t located list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) + +(** { 6 Folds and maps } *) + +(** Used in typeclasses *) +val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> + ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b + +(** Used in correctness and interface; absence of var capture not guaranteed + in pattern-matching clauses and in binders of the form [x,y:T(x)] *) + +val map_constr_expr_with_binders : + (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> + 'a -> constr_expr -> constr_expr + +val replace_vars_constr_expr : + Id.t Id.Map.t -> constr_expr -> constr_expr + +(** Specific function for interning "in indtype" syntax of "match" *) +val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t + +val free_vars_of_constr_expr : constr_expr -> Id.Set.t +val occur_var_constr_expr : Id.t -> constr_expr -> bool + +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list + +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list + +(** For cases pattern parsing errors *) +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a + +(** Placeholder for global option, should be moved to a parameter *) +val asymmetric_patterns : bool ref diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1cf8f196d..e1df24f717 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -21,7 +21,6 @@ open CAst open Constrexpr open Constrexpr_ops open Notation_ops -open Topconstr open Glob_term open Glob_ops open Pattern @@ -185,18 +184,8 @@ let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f -(* XXX: Where to put this in the library? Util maybe? *) -let protect_ref r nf f x = - let old_ref = !r in - r := nf !r; - try let res = f x in r := old_ref; res - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - r := old_ref; - Exninfo.iraise reraise - let without_specific_symbols l = - protect_ref inactive_notations_table + Flags.with_modified_ref inactive_notations_table (fun tbl -> IRuleSet.(union (of_list l) tbl)) (**********************************************************************) @@ -424,7 +413,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in - if !Topconstr.asymmetric_patterns then + if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -456,7 +445,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -472,7 +461,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.asymmetric_patterns then l2 + let l2' = if !asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d980b1995f..51b06580e8 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -60,6 +60,19 @@ val set_extern_reference : val get_extern_reference : unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) +(** WARNING: The following functions are evil due to + side-effects. Think of the following case as used in the printer: + + without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c + + vs + + without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c + + which one is wrong? We should turn this kind of state into an + explicit argument. +*) + (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a0a749bfb3..977146b2fe 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -24,7 +24,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Topconstr open Nametab open Notation open Inductiveops @@ -122,7 +121,7 @@ type internalization_error = exception InternalizationError of internalization_error Loc.located let explain_variable_capture id id' = - pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++ + Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++ strbrk ": cannot interpret both of them with the same type" let explain_illegal_metavariable = @@ -132,12 +131,12 @@ let explain_not_a_constructor ref = str "Unknown constructor: " ++ pr_reference ref let explain_unbound_fix_name is_cofix id = - str "The name" ++ spc () ++ pr_id id ++ + str "The name" ++ spc () ++ Id.print id ++ spc () ++ str "is not bound in the corresponding" ++ spc () ++ str (if is_cofix then "co" else "") ++ str "fixpoint definition" let explain_non_linear_pattern id = - str "The variable " ++ pr_id id ++ str " is bound several times in pattern" + str "The variable " ++ Id.print id ++ str " is bound several times in pattern" let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ @@ -163,7 +162,7 @@ let error_parameter_not_implicit ?loc = "they must be replaced by '_'.") let error_ldots_var ?loc = - user_err ?loc (str "Special token " ++ pr_id ldots_var ++ + user_err ?loc (str "Special token " ++ Id.print ldots_var ++ str " is for use in the Notation command.") (**********************************************************************) @@ -263,13 +262,13 @@ let pr_scope_stack = function let error_inconsistent_scope ?loc id scopes1 scopes2 = user_err ?loc ~hdr:"set_var_scope" - (pr_id id ++ str " is here used in " ++ + (Id.print id ++ str " is here used in " ++ pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) let error_expect_binder_notation_type ?loc id = user_err ?loc - (pr_id id ++ + (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") let set_var_scope ?loc id istermvar env ntnvars = @@ -365,7 +364,7 @@ let check_hidden_implicit_parameters ?loc id impls = | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++ strbrk "a parameter of the inductive type; bound variables in " ++ strbrk "the type of a constructor shall use a different name.") @@ -534,8 +533,9 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na + let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in + let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in + (renaming,env), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -743,11 +743,18 @@ let string_of_ty = function let gvar (loc, id) us = match us with | None -> DAst.make ?loc @@ GVar id | Some _ -> - user_err ?loc (str "Variable " ++ pr_id id ++ + user_err ?loc (str "Variable " ++ Id.print id ++ str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = - (* Is [id] an inductive type potentially with implicit *) + (* Is [id] a notation variable *) + if Id.Map.mem id ntnvars then + begin + if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars; + gvar (loc,id) us, [], [], [] + end + else + (* Is [id] registered with implicit arguments *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map @@ -760,19 +767,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then gvar (loc,id) us, [], [], [] - (* Is [id] a notation variable *) - else if Id.Map.mem id ntnvars - then - (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], []) - (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var + (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc else gvar (loc,id) us, [], [], [] else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err ?loc ~hdr:"intern_var" - (str "variable " ++ pr_id id ++ str " should be bound to a term.") + (str "variable " ++ Id.print id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) let _ = Context.Named.lookup id namedctx in @@ -1570,9 +1573,9 @@ let extract_explicit_arg imps args = | ExplByName id -> if not (exists_implicit_name id imps) then user_err ?loc - (str "Wrong argument name: " ++ pr_id id ++ str "."); + (str "Wrong argument name: " ++ Id.print id ++ str "."); if Id.Map.mem id eargs then - user_err ?loc (str "Argument name " ++ pr_id id + user_err ?loc (str "Argument name " ++ Id.print id ++ str " occurs more than once."); id | ExplByPos (p,_id) -> @@ -1990,7 +1993,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (let (id,(loc,_)) = Id.Map.choose eargs in user_err ?loc (str "Not enough non implicit \ arguments to accept the argument bound to " ++ - pr_id id ++ str".")); + Id.print id ++ str".")); [] | ([], rargs) -> assert (Id.Map.is_empty eargs); diff --git a/interp/declare.ml b/interp/declare.ml index 0cc4d0fcaa..1b4645aff6 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -14,7 +14,6 @@ open Util open Names open Libnames open Globnames -open Nameops open Constr open Declarations open Entries @@ -46,7 +45,7 @@ let cache_variable ((sp,_),o) = | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then - alreadydeclared (pr_id id ++ str " already exists"); + alreadydeclared (Id.print id ++ str " already exists"); let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> @@ -107,7 +106,7 @@ type constant_declaration = Safe_typing.private_constants constant_entry * logic (* section (if Remark or Fact) is needed to access a construction *) let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then - alreadydeclared (pr_id (basename sp) ++ str " already exists"); + alreadydeclared (Id.print (basename sp) ++ str " already exists"); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); add_constant_kind con obj.cst_kind @@ -132,7 +131,7 @@ let exists_name id = let check_exists sp = let id = basename sp in - if exists_name id then alreadydeclared (pr_id id ++ str " already exists") + if exists_name id then alreadydeclared (Id.print id ++ str " already exists") let cache_constant ((sp,kn), obj) = let id = basename sp in @@ -204,12 +203,9 @@ let declare_constant_common id cst = update_tables c; c +let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = - let univs = - if poly then Polymorphic_const_entry univs - else Monomorphic_const_entry univs - in + ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -262,9 +258,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let declare_definition ?(internal=UserIndividualRequest) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - ?(poly=false) id ?types (body,ctx) = + id ?types (body,univs) = let cb = - definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body + definition_entry ?types ~univs ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -341,7 +337,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_record = None; mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty; + mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; }) @@ -407,11 +403,11 @@ let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition.") - | [id] -> pr_id id ++ str " is recursively defined" ++ + | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are recursively defined" ++ match indexes with | Some a -> spc () ++ str "(decreasing respectively on " ++ @@ -422,21 +418,21 @@ let fixpoint_message indexes l = let cofixpoint_message l = Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") - | [id] -> pr_id id ++ str " is corecursively defined" - | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ + | [id] -> Id.print id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are corecursively defined")) let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") let assumption_message id = (* Changing "assumed" to "declared", "assuming" referring more to the type of the object than to the name of the object (see discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") (** Global universe names, in a different summary *) @@ -458,16 +454,16 @@ let declare_universe_context poly ctx = Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) (* Discharged or not *) -type universe_decl = polymorphic * (Id.t * Univ.Level.t) list +type universe_decl = polymorphic * Universes.universe_binders let cache_universes (p, l) = let glob = Global.global_universe_names () in let glob', ctx = - List.fold_left (fun ((idl,lid),ctx) (id, lev) -> + Id.Map.fold (fun id lev ((idl,lid),ctx) -> ((Id.Map.add id (p, lev) idl, Univ.LMap.add lev id lid), Univ.ContextSet.add_universe lev ctx)) - (glob, Univ.ContextSet.empty) l + l (glob, Univ.ContextSet.empty) in cache_universe_context (p, ctx); Global.set_global_universe_names glob' @@ -488,9 +484,9 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.map (fun (l, id) -> + List.fold_left (fun acc (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in - (id, lev)) l + Id.Map.add id lev acc) Id.Map.empty l in Lib.add_anonymous_leaf (input_universes (poly, l)) @@ -527,7 +523,7 @@ let do_constraint poly l = let names, _ = Global.global_universe_names () in try loc, Id.Map.find id names with Not_found -> - user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id) + user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id) in let in_section = Lib.sections_are_opened () in let () = diff --git a/interp/declare.mli b/interp/declare.mli index 9b3194dec5..d50d37368c 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -42,7 +42,7 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.UContext.t -> + ?univs:Entries.constant_universes_entry -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry (** [declare_constant id cd] declares a global declaration @@ -56,8 +56,8 @@ val declare_constant : val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> - constr Univ.in_universe_context_set -> Constant.t + ?local:bool -> Id.t -> ?types:constr -> + constr Entries.in_constant_universes_entry -> Constant.t (** Since transparent constants' side effects are globally declared, we * need that *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 13ed65056d..0197cf9ae2 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -72,7 +72,7 @@ open Decl_kinds let type_of_logical_kind = function | IsDefinition def -> (match def with - | Definition -> "def" + | Definition | Let -> "def" | Coercion -> "coe" | SubClass -> "subclass" | CanonicalStructure -> "canonstruc" diff --git a/interp/impargs.ml b/interp/impargs.ml index 72d22db4d9..3105214d5e 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -10,8 +10,6 @@ open CErrors open Util open Names open Globnames -open Nameops -open Term open Constr open Reduction open Declarations @@ -344,7 +342,7 @@ let check_correct_manual_implicits autoimps l = | ExplByName id,(b,fi,forced) -> if not forced then user_err - (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") + (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then user_err diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cae67c3e70..519f2480ba 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -29,11 +29,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id ++ str + ((Id.print id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id++str" is already declared as a generalizable identifier")) + ((Id.print id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -80,7 +80,7 @@ let is_freevar ids env x = let ungeneralizable loc id = user_err ?loc ~hdr:"Generalization" - (str "Unbound and ungeneralizable variable " ++ pr_id id) + (str "Unbound and ungeneralizable variable " ++ Id.print id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -94,8 +94,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c - | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names l = @@ -152,7 +152,7 @@ let combine_params avoid fn applied needed = | Anonymous -> false in if not (List.exists is_id needed) then - user_err ?loc (str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ?loc (str "Wrong argument name: " ++ Id.print id); true | _ -> false) applied in diff --git a/interp/interp.mllib b/interp/interp.mllib index e3500cfeac..bb22cf468d 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,13 +1,13 @@ Tactypes Stdarg Genintern -Constrexpr_ops Notation_ops -Ppextend Notation -Dumpglob Syntax_def Smartlocate +Constrexpr_ops +Ppextend +Dumpglob Topconstr Reserve Impargs diff --git a/interp/modintern.ml b/interp/modintern.ml index 08657936ee..3eb91d8cd7 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,7 +62,7 @@ let transl_with_decl env = function WithMod (fqid,lookup_module qid) | CWith_Definition ((_,fqid),c) -> let c, ectx = interp_constr env (Evd.from_env env) c in - let ctx = Evd.evar_context_universe_context ectx in + let ctx = UState.context ectx in WithDef (fqid,(c,ctx)) let loc_of_module l = l.CAst.loc diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0967d21f01..20492e38c8 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -239,7 +239,7 @@ let subtract_loc loc1 loc2 = let check_is_hole id t = match DAst.get t with GHole _ -> () | _ -> user_err ?loc:(loc_of_glob_constr t) - (strbrk "In recursive notation with binders, " ++ pr_id id ++ + (strbrk "In recursive notation with binders, " ++ Id.print id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -400,7 +400,7 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - user_err (pr_id x ++ + user_err (Id.print x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -419,8 +419,8 @@ let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - user_err (strbrk "in the right-hand side, " ++ pr_id x ++ - str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ + user_err (strbrk "in the right-hand side, " ++ Id.print x ++ + str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = match typ with @@ -838,7 +838,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v | 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' + if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' else raise No_match in let unify_term_binder c = DAst.(map (fun b' -> match DAst.get c, b' with @@ -980,6 +980,19 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc = else bind_termlist_env alp sigma x l +let match_cast match_fun sigma c1 c2 = + match c1, c2 with + | CastConv t1, CastConv t2 + | CastVM t1, CastVM t2 + | CastNative t1, CastNative t2 -> + match_fun sigma t1 t2 + | CastCoerce, CastCoerce -> + sigma + | CastConv _, _ + | CastVM _, _ + | CastNative _, _ + | CastCoerce, _ -> raise No_match + let does_not_come_from_already_eta_expanded_var glob = (* 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 *) @@ -1125,11 +1138,8 @@ let rec match_ inner u alp metas sigma a1 a2 = 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 + | GCast(t1, c1), NCast(t2, c2) -> + match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match @@ -1157,8 +1167,9 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 - | (GRec _ | GEvar _), _ - | _,_ -> raise No_match + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ + | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ + | GCast _), _ -> raise No_match and match_in u = match_ true u diff --git a/interp/reserve.ml b/interp/reserve.ml index dc0f60dcf2..22c5a2f5e5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -87,12 +87,12 @@ let in_reserved : Id.t * notation_constr -> obj = let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_reserved_type" - ((pr_id id ++ str + ((Id.print id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try let _ = Id.Map.find id !reserve_table in user_err ?loc ~hdr:"declare_reserved_type" - ((pr_id id++str" is already bound to a type")) + ((Id.print id++str" is already bound to a type")) with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) @@ -102,7 +102,7 @@ let declare_reserved_type idl t = let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table let constr_key c = - try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c)))) + try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c)))) with Not_found -> Oth let revert_reserved_type t = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 84c6f4ef30..98e507309f 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,16 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CErrors open Util open Pp +open CErrors open Names open Libnames -open Notation_term open Libobject open Lib -open Nameops open Nametab +open Notation_term (* Syntactic definitions. *) @@ -31,7 +30,7 @@ let add_syntax_constant kn c onlyparse = let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then user_err ~hdr:"cache_syntax_constant" - (pr_id (basename sp) ++ str " already exists"); + (Id.print (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 7a3c83ff96..ecfb766ff4 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,294 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i*) -open Pp -open CErrors -open Util -open Names -open Nameops -open Libnames -open Misctypes -open Constrexpr open Constrexpr_ops -(*i*) - -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - -(**********************************************************************) -(* Miscellaneous *) - -let error_invalid_pattern_notation ?loc () = - user_err ?loc (str "Invalid notation for pattern.") - -(* Legacy functions *) -let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y - -(**********************************************************************) -(* Functions on constr_expr *) - -let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false - -let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with - | CPatRecord l -> - List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (pat,id) -> f id a - | CPatOr (patl) -> - List.fold_left (cases_pattern_fold_names f) a patl - | CPatCstr (_,patl1,patl2) -> - List.fold_left (cases_pattern_fold_names f) - (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,(patl,patll),patl') -> - List.fold_left (cases_pattern_fold_names f) - (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' - | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a - | CPatPrim _ | CPatAtom _ -> a - | CPatCast ({CAst.loc},_) -> - CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" - (Pp.strbrk "Casts are not supported here.") - -let ids_of_pattern = - cases_pattern_fold_names Id.Set.add Id.Set.empty - -let ids_of_pattern_list = - List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) - Id.Set.empty - -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - -let ids_of_cases_tomatch tms = - List.fold_right - (fun (_, ona, indnal) l -> - Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) - indnal - (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) - tms Id.Set.empty - -let rec fold_constr_expr_binders g f n acc b = function - | (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_constr_expr_binders g f n' acc b l) t - | [] -> - f n acc b - -let rec fold_local_binders g f n acc b = function - | CLocalAssum (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_local_binders g f n' acc b l) t - | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t - | CLocalPattern (_,(pat,t))::l -> - let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in - Option.fold_left (f n) acc t - | [] -> - f n acc b - -let fold_constr_expr_with_binders g f n acc = CAst.with_val (function - | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l - | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) - | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (na,a,t,b) -> - f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b - | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bll)) -> - (* The following is an approximation: we don't know exactly if - an ident is binding nor to which subterms bindings apply *) - let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll - | CGeneralization (_,_,c) -> f n acc c - | CDelimiters (_,a) -> f n acc a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> - acc - | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l - | CCases (sty,rtnpo,al,bl) -> - let ids = ids_of_cases_tomatch al in - let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in - let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in - List.fold_right (fun (loc,(patl,rhs)) acc -> - let ids = ids_of_pattern_list patl in - f (Id.Set.fold g ids n) acc rhs) bl acc - | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (Name.fold_right g)) nal n in - f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c - | CIf (c,(ona,po),b1,b2) -> - let acc = f n (f n (f n acc b1) b2) c in - Option.fold_left - (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po - | CFix (_,l) -> - let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> - fold_local_binders g f n' - (fold_local_binders g f n acc t lb) c lb) l acc - | CCoFix (_,_) -> - Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc - ) - -let free_vars_of_constr_expr c = - let rec aux bdvars l = function - | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l - | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c - in aux [] Id.Set.empty c - -let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) - -(* Interpret the index of a recursion order annotation *) - -let split_at_annot bl na = - let names = List.map snd (names_of_local_assums bl) in - match na with - | None -> - begin match names with - | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") - | _ -> ([], bl) - end - | Some (loc, id) -> - let rec aux acc = function - | CLocalAssum (bls, k, t) as x :: rest -> - let test (_, na) = match na with - | Name id' -> Id.equal id id' - | Anonymous -> false - in - let l, r = List.split_when test bls in - begin match r with - | [] -> aux (x :: acc) rest - | _ -> - let ans = match l with - | [] -> acc - | _ -> CLocalAssum (l, k, t) :: acc - in - (List.rev ans, CLocalAssum (r, k, t) :: rest) - end - | CLocalDef ((_,na),_,_) as x :: rest -> - if Name.equal (Name id) na then - user_err ?loc - (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.") - else - aux (x :: acc) rest - | CLocalPattern (_,_) :: rest -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") - | [] -> - user_err ?loc - (str "No parameter named " ++ Nameops.pr_id id ++ str".") - in aux [] bl - -(* Used in correctness and interface *) - -let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e - -let map_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_local_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) = function - CLocalAssum(nal,k,ty) -> - (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) - | CLocalDef((loc,na),c,ty) -> - (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) - | CLocalPattern (loc,(pat,t)) -> - let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_constr_expr_with_binders g f e = CAst.map (function - | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) - | CApp ((p,a),l) -> - CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) - | CProdN (bl,b) -> - let (e,bl) = map_binders f g e bl in CProdN (bl,f e b) - | CLambdaN (bl,b) -> - let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) - | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bll)) -> - (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, - List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) - | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) - | CDelimiters (s,a) -> CDelimiters (s,f e a) - | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CPrim _ | CRef _ as x -> x - | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l) - | CCases (sty,rtnpo,a,bl) -> - let bl = List.map (fun (loc,(patl,rhs)) -> - let ids = ids_of_pattern_list patl in - (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in - let ids = ids_of_cases_tomatch a in - let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in - CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) - | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (Name.fold_right g)) nal e in - let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) - | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) - | CFix (id,dl) -> - CFix (id,List.map (fun (id,n,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - (* Note: fix names should be inserted before the arguments... *) - let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,n,bl',t',d')) dl) - | CCoFix (id,dl) -> - CCoFix (id,List.map (fun (id,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,bl',t',d')) dl) - ) - -(* Used in constrintern *) -let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> - (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) - | c -> map_constr_expr_with_binders Id.Map.remove - replace_vars_constr_expr l c - -(* Returns the ranges of locs of the notation that are not occupied by args *) -(* and which are then occupied by proper symbols of the notation (or spaces) *) - -let locs_of_notation ?loc locs ntn = - let unloc loc = Option.cata Loc.unloc (0,0) loc in - let (bl, el) = unloc loc in - let locs = List.map unloc locs in - let rec aux pos = function - | [] -> if Int.equal pos el then [] else [(pos,el)] - | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l - in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) - -let ntn_loc ?loc (args,argslist,binderslist) = - locs_of_notation ?loc - (List.map constr_loc (args@List.flatten argslist)@ - List.map local_binders_loc binderslist) - -let patntn_loc ?loc (args,argslist) = - locs_of_notation ?loc - (List.map cases_pattern_expr_loc (args@List.flatten argslist)) +let asymmetric_patterns = asymmetric_patterns +let error_invalid_pattern_notation = error_invalid_pattern_notation +let split_at_annot = split_at_annot +let ntn_loc = ntn_loc +let patntn_loc = patntn_loc +let map_constr_expr_with_binders = map_constr_expr_with_binders +let fold_constr_expr_with_binders = fold_constr_expr_with_binders +let ids_of_cases_indtype = ids_of_cases_indtype +let occur_var_constr_expr = occur_var_constr_expr +let free_vars_of_constr_expr = free_vars_of_constr_expr +let replace_vars_constr_expr = replace_vars_constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 922f879558..9fc02461e0 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -10,40 +10,43 @@ open Loc open Names open Constrexpr -(** Topconstr *) - +(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *) val asymmetric_patterns : bool ref +[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] (** Utilities on constr_expr *) +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] + +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list +[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"] +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list +[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"] + +(** For cases pattern parsing errors *) +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a +[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"] -val replace_vars_constr_expr : - Id.t Id.Map.t -> constr_expr -> constr_expr +(*************************************************************************) +val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr +[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] val free_vars_of_constr_expr : constr_expr -> Id.Set.t +[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] + val occur_var_constr_expr : Id.t -> constr_expr -> bool +[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"] (** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - -val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"] (** Used in typeclasses *) - val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b - -(** Used in correctness and interface; absence of var capture not guaranteed - in pattern-matching clauses and in binders of the form [x,y:T(x)] *) +[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"] val map_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr - -val ntn_loc : - ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -val patntn_loc : - ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list - -(** For cases pattern parsing errors *) - -val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a +[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"] |