diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 727 |
1 files changed, 361 insertions, 366 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818..eda45f3d 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,33 +1,46 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util +open CAst open Names open Nameops open Globnames open Misctypes open Glob_term +open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) -let cases_pattern_loc = function - PatVar(loc,_) -> loc - | PatCstr(loc,_,_,_) -> loc +let cases_pattern_loc c = c.CAst.loc + +let alias_of_pat pat = DAst.with_val (function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) pat + +let set_pat_alias id = DAst.map (function + | PatVar Anonymous -> PatVar (Name id) + | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id) + | pat -> assert false) let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] - | (tm,(na,Some (_,_,nal))) -> na::nal) tml) + | (tm,(na,Some {v=(_,nal)})) -> na::nal) tml) -let mkGApp loc p t = - match p with - | GApp (loc,f,l) -> GApp (loc,f,l@[t]) - | _ -> GApp (loc,p,[t]) +let mkGApp ?loc p t = DAst.make ?loc @@ + match DAst.get p with + | GApp (f,l) -> GApp (f,l@[t]) + | _ -> GApp (p,[t]) let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp1 = Option.map f obd in @@ -35,367 +48,280 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = (na,k,comp1,comp2) let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Decl_kinds.Explicit, Decl_kinds.Explicit -> true -| Decl_kinds.Implicit, Decl_kinds.Implicit -> true -| _ -> false + | Decl_kinds.Explicit, Decl_kinds.Explicit -> true + | Decl_kinds.Implicit, Decl_kinds.Implicit -> true + | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false let case_style_eq s1 s2 = match s1, s2 with -| LetStyle, LetStyle -> true -| IfStyle, IfStyle -> true -| LetPatternStyle, LetPatternStyle -> true -| MatchStyle, MatchStyle -> true -| RegularStyle, RegularStyle -> true -| _ -> false - -let rec cases_pattern_eq p1 p2 = match p1, p2 with -| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2 -| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && - Name.equal na1 na2 -| _ -> false + | LetStyle, LetStyle -> true + | IfStyle, IfStyle -> true + | LetPatternStyle, LetPatternStyle -> true + | MatchStyle, MatchStyle -> true + | RegularStyle, RegularStyle -> true + | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false + +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with + | PatVar na1, PatVar na2 -> Name.equal na1 na2 + | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 + | (PatVar _ | PatCstr _), _ -> false let cast_type_eq eq t1 t2 = match t1, t2 with -| CastConv t1, CastConv t2 -> eq t1 t2 -| CastVM t1, CastVM t2 -> eq t1 t2 -| CastCoerce, CastCoerce -> true -| CastNative t1, CastNative t2 -> eq t1 t2 -| _ -> false - -let rec glob_constr_eq c1 c2 = match c1, c2 with -| GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2 -| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2 -| GEvar (_, id1, arg1), GEvar (_, id2, arg2) -> - Id.equal id1 id2 && - List.equal instance_eq arg1 arg2 -| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) -> - (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (_, f1, arg1), GApp (_, f2, arg2) -> - glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 -| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> - case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && - List.equal tomatch_tuple_eq tp1 tp2 && - List.equal cases_clause_eq cl1 cl2 -| GLetTuple (_, na1, (n1, p1), c1, t1), GLetTuple (_, na2, (n2, p2), c2, t2) -> - List.equal Name.equal na1 na2 && Name.equal n1 n2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GIf (_, m1, (pat1, p1), c1, t1), GIf (_, m2, (pat2, p2), c2, t2) -> - glob_constr_eq m1 m2 && Name.equal pat1 pat2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GRec (_, kn1, id1, decl1, c1, t1), GRec (_, kn2, id2, decl2, c2, t2) -> - fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && - Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 && - Array.equal glob_constr_eq c1 c2 && - Array.equal glob_constr_eq t1 t2 -| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2 -| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 -| GCast (_, c1, t1), GCast (_, c2, t2) -> - glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 -| _ -> false - -and tomatch_tuple_eq (c1, p1) (c2, p2) = - let eqp (_, i1, na1) (_, i2, na2) = + | CastConv t1, CastConv t2 -> eq t1 t2 + | CastVM t1, CastVM t2 -> eq t1 t2 + | CastCoerce, CastCoerce -> true + | CastNative t1, CastNative t2 -> eq t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + +let matching_var_kind_eq k1 k2 = match k1, k2 with +| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 +| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2 +| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false + +let tomatch_tuple_eq f (c1, p1) (c2, p2) = + let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in - glob_constr_eq c1 c2 && eq_pred p1 p2 + f c1 c2 && eq_pred p1 p2 -and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) = - List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && - glob_constr_eq c1 c2 +and cases_clause_eq f {CAst.v=(id1, p1, c1)} {CAst.v=(id2, p2, c2)} = + List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2 -and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) = +let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - Option.equal glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 - -and fix_kind_eq k1 k2 = match k1, k2 with -| GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a1 -| GCoFix i1, GCoFix i2 -> Int.equal i1 i2 -| _ -> false - -and fix_recursion_order_eq o1 o2 = match o1, o2 with -| GStructRec, GStructRec -> true -| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2 -| GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2 -| _ -> false - -and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && glob_constr_eq c1 c2 - -let map_glob_constr_left_to_right f = function - | GApp (loc,g,args) -> + Option.equal f c1 c2 && f t1 t2 + +let fix_recursion_order_eq f o1 o2 = match o1, o2 with + | GStructRec, GStructRec -> true + | GWfRec c1, GWfRec c2 -> f c1 c2 + | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> + f c1 c2 && Option.equal f o1 o2 + | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false + +let fix_kind_eq f k1 k2 = match k1, k2 with + | GFix (a1, i1), GFix (a2, i2) -> + let eq (i1, o1) (i2, o2) = + Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 + in + Int.equal i1 i2 && Array.equal eq a1 a1 + | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 + | (GFix _ | GCoFix _), _ -> false + +let instance_eq f (x1,c1) (x2,c2) = + Id.equal x1 x2 && f c1 c2 + +let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with + | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GVar id1, GVar id2 -> Id.equal id1 id2 + | GEvar (id1, arg1), GEvar (id2, arg2) -> + Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 + | GApp (f1, arg1), GApp (f2, arg2) -> + f f1 f2 && List.equal f arg1 arg2 + | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> + Name.equal na1 na2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2 + | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> + case_style_eq st1 st2 && Option.equal f c1 c2 && + List.equal (tomatch_tuple_eq f) tp1 tp2 && + List.equal (cases_clause_eq f) cl1 cl2 + | GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> + List.equal Name.equal na1 na2 && Name.equal n1 n2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> + f m1 m2 && Name.equal pat1 pat2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && + Array.equal f c1 c2 && Array.equal f t1 t2 + | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 + | GCast (c1, t1), GCast (c2, t2) -> + f c1 c2 && cast_type_eq f t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + +let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c + +let map_glob_constr_left_to_right f = DAst.map (function + | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in - GApp (loc,comp1,comp2) - | GLambda (loc,na,bk,ty,c) -> + GApp (comp1,comp2) + | GLambda (na,bk,ty,c) -> let comp1 = f ty in let comp2 = f c in - GLambda (loc,na,bk,comp1,comp2) - | GProd (loc,na,bk,ty,c) -> + GLambda (na,bk,comp1,comp2) + | GProd (na,bk,ty,c) -> let comp1 = f ty in let comp2 = f c in - GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,c) -> + GProd (na,bk,comp1,comp2) + | GLetIn (na,b,t,c) -> let comp1 = f b in + let compt = Option.map f t in let comp2 = f c in - GLetIn (loc,na,comp1,comp2) - | GCases (loc,sty,rtntypopt,tml,pl) -> + GLetIn (na,comp1,compt,comp2) + | GCases (sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in - let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in - GCases (loc,sty,comp1,comp2,comp3) - | GLetTuple (loc,nal,(na,po),b,c) -> + let comp3 = Util.List.map_left (CAst.map (fun (idl,p,c) -> (idl,p,f c))) pl in + GCases (sty,comp1,comp2,comp3) + | GLetTuple (nal,(na,po),b,c) -> let comp1 = Option.map f po in let comp2 = f b in let comp3 = f c in - GLetTuple (loc,nal,(na,comp1),comp2,comp3) - | GIf (loc,c,(na,po),b1,b2) -> + GLetTuple (nal,(na,comp1),comp2,comp3) + | GIf (c,(na,po),b1,b2) -> let comp1 = Option.map f po in let comp2 = f b1 in let comp3 = f b2 in - GIf (loc,f c,(na,comp1),comp2,comp3) - | GRec (loc,fk,idl,bl,tyl,bv) -> + GIf (f c,(na,comp1),comp2,comp3) + | GRec (fk,idl,bl,tyl,bv) -> let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in let comp2 = Array.map f tyl in let comp3 = Array.map f bv in - GRec (loc,fk,idl,comp1,comp2,comp3) - | GCast (loc,c,k) -> + GRec (fk,idl,comp1,comp2,comp3) + | GCast (c,k) -> let comp1 = f c in let comp2 = Miscops.map_cast_type f k in - GCast (loc,comp1,comp2) + GCast (comp1,comp2) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x + ) let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = function +let fold_glob_constr f acc = DAst.with_val (function | GVar _ -> acc - | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> + | GApp (c,args) -> List.fold_left f (f acc c) args + | GLambda (_,_,b,c) | GProd (_,_,b,c) -> f (f acc b) c - | GCases (_,_,rtntypopt,tml,pl) -> - let fold_pattern acc (_,idl,p,c) = f acc c in + | GLetIn (_,b,t,c) -> + f (Option.fold_left f (f acc b) t) c + | GCases (_,rtntypopt,tml,pl) -> + let fold_pattern acc {CAst.v=(idl,p,c)} = f acc c in List.fold_left fold_pattern (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml)) pl - | GLetTuple (_,_,rtntyp,b,c) -> + | GLetTuple (_,rtntyp,b,c) -> f (f (fold_return_type f acc rtntyp) b) c - | GIf (_,c,rtntyp,b1,b2) -> + | GIf (c,rtntyp,b1,b2) -> f (f (f (fold_return_type f acc rtntyp) c) b1) b2 - | GRec (_,_,_,bl,tyl,bv) -> + | GRec (_,_,bl,tyl,bv) -> let acc = Array.fold_left (List.fold_left (fun acc (na,k,bbd,bty) -> f (Option.fold_left f acc bbd) bty)) acc bl in Array.fold_left f (Array.fold_left f acc tyl) bv - | GCast (_,c,k) -> + | GCast (c,k) -> let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc + ) -let iter_glob_constr f = fold_glob_constr (fun () -> f) () +let fold_return_type_with_binders f g v acc (na,tyopt) = + Option.fold_left (f (Name.fold_right g na v)) acc tyopt -let same_id na id = match na with -| Anonymous -> false -| Name id' -> Id.equal id id' +let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function + | GVar _ -> acc + | GApp (c,args) -> List.fold_left (f v) (f v acc c) args + | GLambda (na,_,b,c) | GProd (na,_,b,c) -> + f (Name.fold_right g na v) (f v acc b) c + | GLetIn (na,b,t,c) -> + f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c + | GCases (_,rtntypopt,tml,pl) -> + let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in + let fold_tomatch (v',acc) (tm,(na,onal)) = + ((if rtntypopt = None then v' else + Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal), + f v acc tm) in + let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in + let acc = Option.fold_left (f v') acc rtntypopt in + List.fold_left fold_pattern acc pl + | GLetTuple (nal,rtntyp,b,c) -> + f (List.fold_right (Name.fold_right g) nal v) + (f v (fold_return_type_with_binders f g v acc rtntyp) b) c + | GIf (c,rtntyp,b1,b2) -> + f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 + | GRec (_,idl,bll,tyl,bv) -> + let v' = Array.fold_right g idl v in + let f' i acc fid = + let v,acc = + List.fold_left + (fun (v,acc) (na,k,bbd,bty) -> + (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (v,acc) + bll.(i) in + f v' (f v acc tyl.(i)) (bv.(i)) in + Array.fold_left_i f' acc idl + | GCast (c,k) -> + let acc = match k with + | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + f v acc c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc)) + +let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let rec occur = function - | GVar (loc,id') -> Id.equal id id' - | GApp (loc,f,args) -> (occur f) || (List.exists occur args) - | GLambda (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GProd (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,c) -> - (occur b) || (not (same_id na id) && (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> - (occur_option rtntypopt) - || (List.exists (fun (tm,_) -> occur tm) tml) - || (List.exists occur_pattern pl) - | GLetTuple (loc,nal,rtntyp,b,c) -> - occur_return_type rtntyp id - || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c)) - | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> - not (Array.for_all4 (fun fid bl ty bd -> - let rec occur_fix = function - [] -> not (occur ty) && (Id.equal fid id || not(occur bd)) - | (na,k,bbd,bty)::bl -> - not (occur bty) && - (match bbd with - Some bd -> not (occur bd) - | _ -> true) && - (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in - occur_fix bl) - idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) || (match k with CastConv t - | CastVM t | CastNative t -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - - and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c) - - and occur_option = function None -> false | Some p -> occur p - - and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt - - in occur - - -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set + let rec occur barred acc c = match DAst.get c with + | GVar id' -> Id.equal id id' + | _ -> + (* [g] looks if [id] appears in a binding position, in which + case, we don't have to look in the corresponding subterm *) + let g id' barred = barred || Id.equal id id' in + let f barred acc c = acc || not barred && occur false acc c in + fold_glob_constr_with_binders g f barred acc c in + occur false false let free_glob_vars = - let rec vars bounded vs = function - | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs - | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> - let vs' = vars bounded vs ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bounded vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in - List.fold_left (vars_pattern bounded) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 b in - let bounded' = List.fold_left add_name_to_ids bounded nal in - vars bounded' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 c in - let vs3 = vars bounded vs2 b1 in - vars bounded vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bounded' = Array.fold_right Id.Set.add idl bounded in - let vars_fix i vs fid = - let vs1,bounded1 = - List.fold_left - (fun (vs,bounded) (na,k,bbd,bty) -> - let vs' = vars_option bounded vs bbd in - let vs'' = vars bounded vs' bty in - let bounded' = add_name_to_ids bounded na in - (vs'',bounded') - ) - (vs,bounded') - bl.(i) - in - let vs2 = vars bounded1 vs1 tyl.(i) in - vars bounded1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bounded vs (loc,idl,p,c) = - let bounded' = List.fold_right Id.Set.add idl bounded in - vars bounded' vs c - - and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p - - and vars_return_type bounded vs (na,tyopt) = - let bounded' = add_name_to_ids bounded na in - vars_option bounded' vs tyopt - in + let rec vars bound vs c = match DAst.get c with + | GVar id' -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in - Id.Set.elements vs + vs let glob_visible_short_qualid c = - let rec aux acc = function - | GRef (_,c,_) -> + let rec aux acc c = match DAst.get c with + | GRef (c,_) -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in - if DirPath.is_empty dir then id :: acc else acc - | c -> + if DirPath.is_empty dir then Id.Set.add id acc else acc + | _ -> fold_glob_constr aux acc c - in aux [] c + in aux Id.Set.empty c let warn_variable_collision = let open Pp in CWarnings.create ~name:"variable-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variables of name " ++ pr_id name) + strbrk "Collision between bound variables of name " ++ Id.print name) let add_and_check_ident id set = if Id.Set.mem id set then warn_variable_collision id; Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c -> - let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let bound = vars_option bound rtntypopt in - let bound = - List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in - List.fold_left vars_pattern bound pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound b in - let bound = List.fold_right (name_fold add_and_check_ident) nal bound in - vars bound c - | GIf (loc,c,rtntyp,b1,b2) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound c in - let bound = vars bound b1 in - vars bound b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound = Array.fold_right Id.Set.add idl bound in - let vars_fix i bound fid = - let bound = - List.fold_left - (fun bound (na,k,bbd,bty) -> - let bound = vars_option bound bbd in - let bound = vars bound bty in - name_fold add_and_check_ident na bound - ) - bound - bl.(i) - in - let bound = vars bound tyl.(i) in - vars bound bv.(i) - in - Array.fold_left_i vars_fix bound idl - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound c - - and vars_pattern bound (loc,idl,p,c) = - let bound = List.fold_right add_and_check_ident idl bound in - vars bound c - - and vars_option bound = function None -> bound | Some p -> vars bound p - - and vars_return_type bound (na,tyopt) = - let bound = name_fold add_and_check_ident na bound in - vars_option bound tyopt + let rec vars bound = + fold_glob_constr_with_binders + (fun id () -> bound := add_and_check_ident id !bound) + (fun () () -> vars bound) + () () in fun rt -> - vars Id.Set.empty rt + let bound = ref Id.Set.empty in + vars bound rt; + !bound (** Mapping of names in binders *) @@ -405,37 +331,38 @@ let bound_glob_vars = probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) -let map_inpattern_binders f ((loc,id,nal) as x) = +let map_inpattern_binders f ({loc;v=(id,nal)} as x) = let r = CList.smartmap f nal in if r == nal then x - else loc,id,r + else CAst.make ?loc (id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = function - | PatVar (loc,na) as x -> +let rec map_case_pattern_binders f = DAst.map (function + | PatVar na as x -> let r = f na in if r == na then x - else PatVar (loc,r) - | PatCstr (loc,c,ps,na) as x -> + else PatVar r + | PatCstr (c,ps,na) as x -> let rna = f na in let rps = CList.smartmap (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x - else PatCstr(loc,c,rps,rna) + else PatCstr(c,rps,rna) + ) -let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause = +let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = (* spiwack: not sure if I must do something with the list of idents. It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x - else loc,il,r,rhs + else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, @@ -445,41 +372,28 @@ let map_pattern_binders f tomatch branches = let map_tomatch f (c,pp) : tomatch_tuple = f c , pp -let map_cases_branch f (loc,il,cll,rhs) : cases_clause = - loc , il , cll , f rhs +let map_cases_branch f = + CAst.map (fun (il,cll,rhs) -> (il , cll , f rhs)) let map_pattern f tomatch branches = List.map (fun tm -> map_tomatch f tm) tomatch, List.map (fun br -> map_cases_branch f br) branches -let loc_of_glob_constr = function - | GRef (loc,_,_) -> loc - | GVar (loc,_) -> loc - | GEvar (loc,_,_) -> loc - | GPatVar (loc,_) -> loc - | GApp (loc,_,_) -> loc - | GLambda (loc,_,_,_,_) -> loc - | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_) -> loc - | GCases (loc,_,_,_,_) -> loc - | GLetTuple (loc,_,_,_,_) -> loc - | GIf (loc,_,_,_,_) -> loc - | GRec (loc,_,_,_,_,_) -> loc - | GSort (loc,_) -> loc - | GHole (loc,_,_,_) -> loc - | GCast (loc,_,_) -> loc +let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) +exception UnsoundRenaming + let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l -let test_id l id = if collide_id l id then raise Not_found -let test_na l na = name_iter (test_id l) na +let test_id l id = if collide_id l id then raise UnsoundRenaming +let test_na l na = Name.iter (test_id l) na let update_subst na l = let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in - let l' = name_fold Id.List.remove_assoc na l in - name_fold + let l' = Name.fold_right Id.List.remove_assoc na l in + Name.fold_right (fun id _ -> if in_range id l' then let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in @@ -487,8 +401,6 @@ let update_subst na l = else na,l) na (na,l) -exception UnsoundRenaming - let rename_var l id = try let id' = Id.List.assoc id l in @@ -499,77 +411,160 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l = function - | GVar (loc,id) as r -> +let force c = DAst.make ?loc:c.CAst.loc (DAst.get c) + +let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function + | GVar id as r -> let id' = rename_var l id in - if id == id' then r else GVar (loc,id') - | GRef (_,VarRef id,_) as r -> + if id == id' then r else GVar id' + | GRef (VarRef id,_) as r -> if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else r - | GProd (loc,na,bk,t,c) -> + | GProd (na,bk,t,c) -> let na',l' = update_subst na l in - GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLambda (loc,na,bk,t,c) -> + GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLambda (na,bk,t,c) -> let na',l' = update_subst na l in - GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLetIn (loc,na,b,c) -> + GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLetIn (na,b,t,c) -> let na',l' = update_subst na l in - GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + GLetIn (na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) - | GCases (loc,ci,po,tomatchl,cls) -> + | GCases (ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = - test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in + test_na l na; Option.iter (fun {v=(_,nal)} -> List.iter (test_na l) nal) ino in let test_clause idl = List.iter (test_id l) idl in let po = Option.map (rename_glob_vars l) po in let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in - let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in - GCases (loc,ci,po,tomatchl,cls) - | GLetTuple (loc,nal,(na,po),c,b) -> + let cls = Util.List.map_left (CAst.map (fun (idl,p,c) -> test_clause idl; (idl,p,rename_glob_vars l c))) cls in + GCases (ci,po,tomatchl,cls) + | GLetTuple (nal,(na,po),c,b) -> List.iter (test_na l) (na::nal); - GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po), + GLetTuple (nal,(na,Option.map (rename_glob_vars l) po), rename_glob_vars l c,rename_glob_vars l b) - | GIf (loc,c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) -> test_na l na; - GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), + GIf (rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), rename_glob_vars l b1,rename_glob_vars l b2) - | GRec (loc,k,idl,decls,bs,ts) -> + | GRec (k,idl,decls,bs,ts) -> Array.iter (test_id l) idl; - GRec (loc,k,idl, + GRec (k,idl, Array.map (List.map (fun (na,k,bbd,bty) -> test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - | r -> map_glob_constr (rename_glob_vars l) r + | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c) + ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) -> +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + +let rec cases_pattern_of_glob_constr na = DAst.map (function + | GVar id -> begin match na with | Name _ -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found - | Anonymous -> PatVar (loc,Name id) + | Anonymous -> PatVar (Name id) + end + | GHole (_,_,_) -> PatVar na + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) + | GApp (c, l) -> + begin match DAst.get c with + | GRef (ConstructRef cstr,_) -> + PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | _ -> raise Not_found end - | GHole (loc,_,_,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr,_) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous -> + (* A canonical encoding of aliases *) + DAst.get (cases_pattern_of_glob_constr na' b) | _ -> raise Not_found + ) + +open Declarations +open Term +open Context + +(* Keep only patterns which are not bound to a local definitions *) +let drop_local_defs typi args = + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | [], [] -> [] + | Rel.Declaration.LocalDef _ :: decls, pat :: args -> + begin + match DAst.get pat with + | PatVar Anonymous -> aux decls args + | _ -> raise Not_found (* The pattern is used, one cannot drop it *) + end + | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) args + +let add_patterns_for_params_remove_local_defs (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + let l = + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in + drop_local_defs typi l in + Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l + +let add_alias ?loc na c = + match na with + | Anonymous -> c + | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id)) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux = function - | PatCstr (loc,cstr,[],Anonymous) -> - GRef (loc,ConstructRef cstr,None) - | PatCstr (loc,cstr,l,Anonymous) -> - let ref = GRef (loc,ConstructRef cstr,None) in - GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) +let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function + | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) + | PatCstr (cstr,l,na) -> + let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in + let l = add_patterns_for_params_remove_local_defs cstr l in + add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l)) + | PatVar (Name id) when not isclosed -> + GVar id + | PatVar Anonymous when not isclosed -> + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) | _ -> raise Not_found + ) x -let glob_constr_of_closed_cases_pattern = function - | PatCstr (loc,cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) +let glob_constr_of_closed_cases_pattern p = match DAst.get p with + | PatCstr (cstr,l,na) -> + let loc = p.CAst.loc in + na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found + +let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p + +(**********************************************************************) +(* Interpreting ltac variables *) + +open Pp +open CErrors + +let ltac_interp_name { ltac_idents ; ltac_genargs } = function + | Anonymous -> Anonymous + | Name id as n -> + try Name (Id.Map.find id ltac_idents) + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str"Ltac variable"++spc()++ Id.print id ++ + spc()++str"is not bound to an identifier."++spc()++ + str"It cannot be used in a binder.") + else n + +let empty_lvar : ltac_var_map = { + ltac_constrs = Id.Map.empty; + ltac_uconstrs = Id.Map.empty; + ltac_idents = Id.Map.empty; + ltac_genargs = Id.Map.empty; +} |