|
adamc@2
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@2
|
2 * All rights reserved.
|
|
adamc@2
|
3 *
|
|
adamc@2
|
4 * Redistribution and use in source and binary forms, with or without
|
|
adamc@2
|
5 * modification, are permitted provided that the following conditions are met:
|
|
adamc@2
|
6 *
|
|
adamc@2
|
7 * - Redistributions of source code must retain the above copyright notice,
|
|
adamc@2
|
8 * this list of conditions and the following disclaimer.
|
|
adamc@2
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
|
adamc@2
|
10 * this list of conditions and the following disclaimer in the documentation
|
|
adamc@2
|
11 * and/or other materials provided with the distribution.
|
|
adamc@2
|
12 * - The names of contributors may not be used to endorse or promote products
|
|
adamc@2
|
13 * derived from this software without specific prior written permission.
|
|
adamc@2
|
14 *
|
|
adamc@2
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
|
adamc@2
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
|
adamc@2
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
|
adamc@2
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
|
adamc@2
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
|
adamc@2
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
|
adamc@2
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
|
adamc@2
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
|
adamc@2
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
|
adamc@2
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
|
adamc@2
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
|
adamc@2
|
26 *)
|
|
adamc@2
|
27
|
|
adamc@2
|
28 structure ElabEnv :> ELAB_ENV = struct
|
|
adamc@2
|
29
|
|
adamc@2
|
30 open Elab
|
|
adamc@2
|
31
|
|
adamc@2
|
32 structure IM = IntBinaryMap
|
|
adamc@2
|
33 structure SM = BinaryMapFn(struct
|
|
adamc@2
|
34 type ord_key = string
|
|
adamc@2
|
35 val compare = String.compare
|
|
adamc@2
|
36 end)
|
|
adamc@2
|
37
|
|
adamc@2
|
38 exception UnboundRel of int
|
|
adamc@2
|
39 exception UnboundNamed of int
|
|
adamc@2
|
40
|
|
adamc@2
|
41 datatype var' =
|
|
adamc@2
|
42 CRel' of int * kind
|
|
adamc@2
|
43 | CNamed' of int * kind
|
|
adamc@2
|
44
|
|
adamc@2
|
45 datatype var =
|
|
adamc@2
|
46 CNotBound
|
|
adamc@2
|
47 | CRel of int * kind
|
|
adamc@2
|
48 | CNamed of int * kind
|
|
adamc@2
|
49
|
|
adamc@2
|
50 type env = {
|
|
adamc@2
|
51 renameC : var' SM.map,
|
|
adamc@2
|
52 relC : (string * kind) list,
|
|
adamc@2
|
53 namedC : (string * kind) IM.map
|
|
adamc@2
|
54 }
|
|
adamc@2
|
55
|
|
adamc@2
|
56 val namedCounter = ref 0
|
|
adamc@2
|
57
|
|
adamc@2
|
58 val empty = {
|
|
adamc@2
|
59 renameC = SM.empty,
|
|
adamc@2
|
60 relC = [],
|
|
adamc@2
|
61 namedC = IM.empty
|
|
adamc@2
|
62 }
|
|
adamc@2
|
63
|
|
adamc@2
|
64 fun pushCRel (env : env) x k =
|
|
adamc@2
|
65 let
|
|
adamc@2
|
66 val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k)
|
|
adamc@2
|
67 | x => x) (#renameC env)
|
|
adamc@2
|
68 in
|
|
adamc@2
|
69 {renameC = SM.insert (renameC, x, CRel' (0, k)),
|
|
adamc@2
|
70 relC = (x, k) :: #relC env,
|
|
adamc@2
|
71 namedC = #namedC env}
|
|
adamc@2
|
72 end
|
|
adamc@2
|
73
|
|
adamc@2
|
74 fun lookupCRel (env : env) n =
|
|
adamc@2
|
75 (List.nth (#relC env, n))
|
|
adamc@2
|
76 handle Subscript => raise UnboundRel n
|
|
adamc@2
|
77
|
|
adamc@5
|
78 fun pushCNamedAs (env : env) x n k =
|
|
adamc@5
|
79 {renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
|
|
adamc@5
|
80 relC = #relC env,
|
|
adamc@5
|
81 namedC = IM.insert (#namedC env, n, (x, k))}
|
|
adamc@5
|
82
|
|
adamc@5
|
83 fun pushCNamed env x k =
|
|
adamc@2
|
84 let
|
|
adamc@2
|
85 val n = !namedCounter
|
|
adamc@2
|
86 in
|
|
adamc@2
|
87 namedCounter := n + 1;
|
|
adamc@5
|
88 (pushCNamedAs env x n k, n)
|
|
adamc@2
|
89 end
|
|
adamc@2
|
90
|
|
adamc@2
|
91 fun lookupCNamed (env : env) n =
|
|
adamc@2
|
92 case IM.find (#namedC env, n) of
|
|
adamc@2
|
93 NONE => raise UnboundNamed n
|
|
adamc@2
|
94 | SOME x => x
|
|
adamc@2
|
95
|
|
adamc@2
|
96 fun lookupC (env : env) x =
|
|
adamc@2
|
97 case SM.find (#renameC env, x) of
|
|
adamc@2
|
98 NONE => CNotBound
|
|
adamc@2
|
99 | SOME (CRel' x) => CRel x
|
|
adamc@2
|
100 | SOME (CNamed' x) => CNamed x
|
|
adamc@2
|
101
|
|
adamc@2
|
102 end
|
