1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Entries
open Libnames
open Constrexpr
open Constrintern
type module_internalization_error =
| NotAModuleNorModtype of string
| IncorrectWithInModule
| IncorrectModuleApplication
exception ModuleInternalizationError of module_internalization_error
(*
val error_declaration_not_path : module_struct_entry -> 'a
val error_not_a_functor : module_struct_entry -> 'a
val error_not_equal : module_path -> module_path -> 'a
oval error_not_a_modtype_loc : loc -> string -> 'a
val error_not_a_module_loc : loc -> string -> 'a
val error_not_a_module_or_modtype_loc : loc -> string -> 'a
val error_with_in_module : unit -> 'a
val error_application_to_module_type : unit -> 'a
*)
let error_not_a_modtype_loc loc s =
Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
let error_not_a_module_loc loc s =
Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s))
let error_not_a_module_nor_modtype_loc loc s =
Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
let error_incorrect_with_in_module loc =
Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
let error_application_to_module_type loc =
Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
(* Search for the head of [qid] in [binders].
If found, returns the module_path/kernel_name created from the dirpath
and the basename. Searches Nametab otherwise.
*)
let lookup_module (loc,qid) =
try
let mp = Nametab.locate_module qid in
Dumpglob.dump_modref loc mp "modtype"; mp
with
| Not_found -> error_not_a_module_loc loc (string_of_qualid qid)
let lookup_modtype (loc,qid) =
try
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref loc mp "mod"; mp
with
| Not_found ->
error_not_a_modtype_loc loc (string_of_qualid qid)
let lookup_module_or_modtype (loc,qid) =
try
let mp = Nametab.locate_module qid in
Dumpglob.dump_modref loc mp "modtype"; (mp,true)
with Not_found -> try
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref loc mp "mod"; (mp,false)
with Not_found ->
error_not_a_module_nor_modtype_loc loc (string_of_qualid qid)
let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
With_Module (fqid,lookup_module qid)
| CWith_Definition ((_,fqid),c) ->
With_Definition (fqid,interp_constr Evd.empty env c)
let loc_of_module = function
| CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
let check_module_argument_is_path me' = function
| CMident _ -> ()
| (CMapply (loc,_,_) | CMwith (loc,_,_)) ->
Loc.raise loc
(Modops.ModuleTypingError (Modops.ApplicationToNotPath me'))
let rec interp_modexpr env = function
| CMident qid ->
MSEident (lookup_module qid)
| CMapply (_,me1,me2) ->
let me1' = interp_modexpr env me1 in
let me2' = interp_modexpr env me2 in
check_module_argument_is_path me2' me2;
MSEapply(me1',me2')
| CMwith (loc,_,_) -> error_incorrect_with_in_module loc
let rec interp_modtype env = function
| CMident qid ->
MSEident (lookup_modtype qid)
| CMapply (_,mty1,me) ->
let mty' = interp_modtype env mty1 in
let me' = interp_modexpr env me in
check_module_argument_is_path me' me;
MSEapply(mty',me')
| CMwith (_,mty,decl) ->
let mty = interp_modtype env mty in
let decl = transl_with_decl env decl in
MSEwith(mty,decl)
let rec interp_modexpr_or_modtype env = function
| CMident qid ->
let (mp,ismod) = lookup_module_or_modtype qid in
(MSEident mp, ismod)
| CMapply (_,me1,me2) ->
let me1',ismod1 = interp_modexpr_or_modtype env me1 in
let me2',ismod2 = interp_modexpr_or_modtype env me2 in
check_module_argument_is_path me2' me2;
if not ismod2 then error_application_to_module_type (loc_of_module me2);
(MSEapply (me1',me2'), ismod1)
| CMwith (loc,me,decl) ->
let me,ismod = interp_modexpr_or_modtype env me in
let decl = transl_with_decl env decl in
if ismod then error_incorrect_with_in_module loc;
(MSEwith(me,decl), ismod)
|
