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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Pp
open Util
open Names
open Entries
open Libnames
open Coqast
open Astterm
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
(*
(* Since module components are not put in the nametab we try to locate
the module prefix *)
exception BadRef
let lookup_qualid (modtype:bool) qid =
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
in
let rec find_module_prefix dir n =
if n<0 then raise Not_found;
let dir',dir'' = list_chop n dir in
let id',dir''' =
match dir'' with
| hd::tl -> hd,tl
| _ -> anomaly "This list should not be empty!"
in
let qid' = make_qualid dir' id' in
try
match Nametab.locate qid' with
| ModRef mp -> mp,dir'''
| _ -> raise BadRef
with
Not_found -> find_module_prefix dir (pred n)
in
try Nametab.locate qid
with Not_found ->
let (dir,id) = repr_qualid qid in
let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
let mp =
List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
in
if modtype then
ModTypeRef (make_ln mp (label_of_id id))
else
ModRef (MPdot (mp,label_of_id id))
*)
(* 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 binders qid =
try
let dir,id = repr_qualid qid in
(* dirpath in natural order *)
let idl = List.rev (id::repr_dirpath dir) in
let top_mp = MPbound (fst (List.assoc (List.hd idl) binders)) in
make_mp top_mp (List.tl idl)
with
Not_found -> Nametab.locate_module qid
let lookup_modtype binders qid =
try
let dir,id = repr_qualid qid in
(* dirpath in natural order *)
match List.rev (repr_dirpath dir) with
| hd::tl ->
let top_mp = MPbound (fst (List.assoc hd binders)) in
let mp = make_mp top_mp tl in
make_kn mp empty_dirpath (label_of_id id)
| [] -> raise Not_found
(* may-be a module, but not a module type!*)
with
Not_found -> Nametab.locate_modtype qid
let transl_with_decl binders = function
| Node(loc,"WITHMODULE",[id_ast;qid_ast]) ->
let id = match id_ast with
Nvar(_,id) -> id
| _ -> anomaly "Identifier AST expected"
in
let qid = match qid_ast with
| Node (loc, "QUALID", astl) ->
interp_qualid astl
| _ -> anomaly "QUALID expected"
in
With_Module (id,lookup_module binders qid)
| Node(loc,"WITHDEFINITION",[id_ast;cast]) ->
let id = match id_ast with
Nvar(_,id) -> id
| _ -> anomaly "Identifier AST expected"
in
let c = interp_constr Evd.empty (Global.env()) cast in
With_Definition (id,c)
| _ -> anomaly "Unexpected AST"
let rec transl_modtype binders = function
| Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with
| [Node (loc, "QUALID", astl)] ->
let qid = interp_qualid astl in begin
try
MTEident (lookup_modtype binders qid)
with
| Not_found ->
Modops.error_not_a_modtype (*loc*) (string_of_qualid qid)
end
| _ -> anomaly "QUALID expected"
end
| Node(loc,"MODTYPEWITH",[mty_ast;decl_ast]) ->
let mty = transl_modtype binders mty_ast in
let decl = transl_with_decl binders decl_ast in
MTEwith(mty,decl)
| _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only"
let transl_binder binders (idl,mty_ast) =
let mte = transl_modtype binders mty_ast in
let add_one binders id =
if List.mem_assoc id binders then
error "Two identical module binders..."
else
let mbid = make_mbid (Lib.module_dp()) (string_of_id id) in
(id,(mbid,mte))::binders
in
List.fold_left add_one binders idl
let transl_binders = List.fold_left transl_binder
let rec transl_modexpr binders = function
| Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with
| [Node (loc, "QUALID", astl)] ->
let qid = interp_qualid astl in begin
try
MEident (lookup_module binders qid)
with
| Not_found ->
Modops.error_not_a_module (*loc*) (string_of_qualid qid)
end
| _ -> anomaly "QUALID expected"
end
| Node(_,"MODEXPRAPP",[ast1;ast2]) ->
let me1 = transl_modexpr binders ast1 in
let me2 = transl_modexpr binders ast2 in
MEapply(me1,me2)
| Node(_,"MODEXPRAPP",_) ->
anomaly "transl_modexpr: MODEXPRAPP must have two arguments"
| _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..."
let interp_module_decl evd env args_ast mty_ast_o mexpr_ast_o =
let binders = transl_binders [] args_ast in
let mty_o = option_app (transl_modtype binders) mty_ast_o in
let mexpr_o = option_app (transl_modexpr binders) mexpr_ast_o in
(List.rev binders, mty_o, mexpr_o)
|
