diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /plugins/funind/glob_termops.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[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 <unknown> 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 <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
Diffstat (limited to 'plugins/funind/glob_termops.ml')
| -rw-r--r-- | plugins/funind/glob_termops.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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 -> |