diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-12 20:11:01 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:19 +0200 |
| commit | 846b74275511bd89c2f3abe19245133050d2199c (patch) | |
| tree | 24e4c838d440e7ce6104bca95c8eb4b7baa321ec /interp/modintern.ml | |
| parent | e57074289193b0f0184f3c7143d8ab7e0edd5112 (diff) | |
[constrexpr] Make patterns use Loc.located for location information
This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.
Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.
Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.
`git grep 'Loc.t \*'` gives an overview of the remaining work to do.
We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index d4ade7058..166711659 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -65,17 +65,16 @@ let transl_with_decl env = function let ctx = Evd.evar_context_universe_context ectx in WithDef (fqid,(c,ctx)) -let loc_of_module = function - | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc +let loc_of_module (l, _) = l (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind = function +let rec interp_module_ast env kind (loc, m) = match m with | CMident qid -> - let (mp,kind) = lookup_module_or_modtype kind qid in + let (mp,kind) = lookup_module_or_modtype kind (loc,qid) in (MEident mp, kind) - | CMapply (_,me1,me2) -> + | CMapply (me1,me2) -> let me1',kind1 = interp_module_ast env kind me1 in let me2',kind2 = interp_module_ast env ModAny me2 in let mp2 = match me2' with @@ -85,7 +84,7 @@ let rec interp_module_ast env kind = function if kind2 == ModType then error_application_to_module_type (loc_of_module me2); (MEapply (me1',mp2), kind1) - | CMwith (loc,me,decl) -> + | CMwith (me,decl) -> let me,kind = interp_module_ast env kind me in if kind == Module then error_incorrect_with_in_module loc; let decl = transl_with_decl env decl in |