diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 268 |
1 files changed, 129 insertions, 139 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 4cccaaf8f..25ece5b8e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -22,10 +22,10 @@ let cases_predicate_names tml = | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,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 = Loc.tag ~loc @@ + match snd 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 @@ -59,46 +59,46 @@ let cast_type_eq eq t1 t2 = match t1, t2 with | 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) -> +let rec glob_constr_eq (_loc1, c1) (_loc2, 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)) -> +| GPatVar (b1, pat1), GPatVar (b2, pat2) -> (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (_, f1, arg1), GApp (_, f2, arg2) -> +| 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) -> +| 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) -> +| 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, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) -> +| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> +| 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) -> +| 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) -> +| 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) -> +| 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) -> +| 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) -> +| GCast (c1, t1), GCast (c2, t2) -> glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 | _ -> false @@ -109,7 +109,7 @@ and tomatch_tuple_eq (c1, p1) (c2, p2) = 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 -and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) = +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 @@ -137,80 +137,82 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with 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) -> +let map_glob_constr_left_to_right f = Loc.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,t,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,compt,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 (fun (loc,(idl,p,c)) -> (loc,(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 = Loc.with_unloc (function | GVar _ -> acc - | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) -> + | GApp (c,args) -> List.fold_left f (f acc c) args + | GLambda (_,_,b,c) | GProd (_,_,b,c) -> f (f acc b) c - | GLetIn (_,_,b,t,c) -> + | GLetIn (_,b,t,c) -> f (Option.fold_left f (f acc b) t) c - | GCases (_,_,rtntypopt,tml,pl) -> - let fold_pattern acc (_,idl,p,c) = f acc c in + | GCases (_,rtntypopt,tml,pl) -> + let fold_pattern acc (_,(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) () @@ -219,25 +221,25 @@ let same_id na id = match na with | Name id' -> Id.equal id id' 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) -> + let rec occur gt = Loc.with_unloc (function + | GVar (id') -> Id.equal id id' + | GApp (f,args) -> (occur f) || (List.exists occur args) + | GLambda (na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) - | GProd (loc,na,bk,ty,c) -> + | GProd (na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,t,c) -> + | GLetIn (na,b,t,c) -> (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> + | GCases (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) -> + | GLetTuple (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) -> + | GIf (c,rtntyp,b1,b2) -> occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> + | GRec (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)) @@ -249,11 +251,11 @@ let occur_glob_constr id = (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 + | GCast (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) + ) gt + 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 @@ -268,33 +270,33 @@ let add_name_to_ids set na = | Name id -> Id.Set.add id set 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) -> + let rec vars bounded vs = Loc.with_unloc @@ (function + | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs + | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args) + | GLambda (na,_,ty,c) | GProd (na,_,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c - | GLetIn (loc,na,b,ty,c) -> + | GLetIn (na,b,ty,c) -> let vs' = vars bounded vs b in let vs'' = Option.fold_left (vars bounded) vs' ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs'' c - | GCases (loc,sty,rtntypopt,tml,pl) -> + | GCases (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) -> + | GLetTuple (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) -> + | GIf (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) -> + | GRec (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 = @@ -312,11 +314,12 @@ let free_glob_vars = 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 + | GCast (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) = + and vars_pattern bounded vs (loc,(idl,p,c)) = let bounded' = List.fold_right Id.Set.add idl bounded in vars bounded' vs c @@ -332,7 +335,7 @@ let free_glob_vars = let glob_visible_short_qualid c = let rec aux acc = function - | GRef (_,c,_) -> + | _, 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 @@ -351,26 +354,26 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> + let rec vars bound = Loc.with_loc (fun ~loc -> 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) -> + fold_glob_constr vars bound (loc, c) + | GCases (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) -> + | GLetTuple (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) -> + | GIf (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) -> + | GRec (fk,idl,bl,tyl,bv) -> let bound = Array.fold_right Id.Set.add idl bound in let vars_fix i bound fid = let bound = @@ -388,9 +391,10 @@ let bound_glob_vars = 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 + | GApp _ | GCast _ as c -> fold_glob_constr vars bound (loc, c) + ) - and vars_pattern bound (loc,idl,p,c) = + and vars_pattern bound (loc,(idl,p,c)) = let bound = List.fold_right add_and_check_ident idl bound in vars bound c @@ -435,14 +439,14 @@ let rec map_case_pattern_binders f = Loc.map (function 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 ((loc,(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 loc,(il,r,rhs) let map_pattern_binders f tomatch branches = CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, @@ -452,29 +456,14 @@ 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 (loc,(il,cll,rhs)) : cases_clause = + loc , (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 (loc, _) = loc (**********************************************************************) (* Alpha-renaming *) @@ -506,73 +495,74 @@ 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 rec rename_glob_vars l = Loc.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,t,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,Option.map (rename_glob_vars l) t,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 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 (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(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 + (* XXX: This located use case should be improved. *) + | r -> snd @@ map_glob_constr (rename_glob_vars l) (loc, r) + ) (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) -> +let rec cases_pattern_of_glob_constr na = Loc.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 -> Loc.tag ~loc @@ PatVar (Name id) + | Anonymous -> PatVar (Name id) end - | GHole (loc,_,_,_) -> Loc.tag ~loc @@ PatVar na - | GRef (loc,ConstructRef cstr,_) -> - Loc.tag ~loc @@ PatCstr (cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> - Loc.tag ~loc @@ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GHole (_,_,_) -> PatVar na + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) + | GApp ((_loc, GRef (ConstructRef cstr,_)),l) -> + PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found + ) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux x = Loc.with_loc (fun ~loc -> function - | PatCstr (cstr,[],Anonymous) -> - GRef (loc,ConstructRef cstr,None) - | PatCstr (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_closed_cases_pattern_aux x = Loc.map_with_loc (fun ~loc -> function + | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) + | PatCstr (cstr,l,Anonymous) -> + let ref = Loc.tag ~loc @@ GRef (ConstructRef cstr,None) in + GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x |