From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- plugins/funind/glob_termops.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins/funind/glob_termops.ml') diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 01e607412..66b9897d0 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -193,14 +193,14 @@ let rec alpha_pat excluded (loc, pat) = match pat with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then let new_id = Namegen.next_ident_away id excluded in - (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded), + (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) - else (Loc.tag ~loc pat),excluded,Id.Map.empty + else (Loc.tag ?loc pat),excluded,Id.Map.empty | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with @@ -218,7 +218,7 @@ let rec alpha_pat excluded (loc, pat) = ([],new_excluded,map) patl in - (Loc.tag ~loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -255,7 +255,7 @@ let raw_get_pattern_id pat acc = let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded (loc, rt) = - let new_rt = Loc.tag ~loc @@ + let new_rt = Loc.tag ?loc @@ match rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt | GLambda(Anonymous,k,t,b) -> @@ -445,7 +445,7 @@ let rec pattern_to_term pt = Loc.with_unloc (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern (loc, rt) = Loc.tag ~loc @@ + let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@ match rt with | GRef _ -> rt | GVar id when Id.compare id x_id == 0 -> Loc.obj term @@ -605,7 +605,7 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term (loc, rt) = Loc.tag ~loc @@ + let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@ match rt with | GRef _ -> rt | GVar _ -> rt @@ -673,7 +673,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map (loc, rt) = - Loc.tag ~loc @@ + Loc.tag ?loc @@ match rt with | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt | GVar id -> -- cgit v1.2.3