summaryrefslogtreecommitdiff
path: root/interp/modintern.ml
blob: f53d1796ef2c1c1dd1c75836f6dc3f2264598c29 (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id: modintern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)

open Pp
open Util
open Names
open Entries
open Libnames
open Topconstr
open Constrintern

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 (loc,qid) =
  try
    let mp = Nametab.locate_module qid in
      Dumpglob.dump_modref loc mp "modtype"; mp
  with
    | Not_found -> Modops.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 ->
	Modops.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 ->
    Modops.error_not_a_module_or_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 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
	MSEapply(me1,me2)
  | CMwith _ -> Modops.error_with_in_module ()


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
	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
      if not ismod2 then Modops.error_application_to_module_type ();
      (MSEapply (me1,me2), ismod1)
  | CMwith (me,decl) ->
      let me,ismod = interp_modexpr_or_modtype env me in
      let decl = transl_with_decl env decl in
      if ismod then Modops.error_with_in_module ();
      (MSEwith(me,decl), ismod)