Mercurial > urweb

comparison src/elab_env.sml @ 9:14b533dbe6cc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added simple expression constructors to Elab
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 17:26:14 -0500
parents 258261a53842
children e97c6d335869
comparison
equal deleted inserted replaced
8:a455a9f85cc3 9:14b533dbe6cc
36 end) 36 end)
37 37
38 exception UnboundRel of int 38 exception UnboundRel of int
39 exception UnboundNamed of int 39 exception UnboundNamed of int
40 40
41 datatype var' = 41 datatype 'a var' =
42 CRel' of int * kind 42 Rel' of int * 'a
43 | CNamed' of int * kind 43 | Named' of int * 'a
44 44
45 datatype var = 45 datatype 'a var =
46 CNotBound 46 NotBound
47 | CRel of int * kind 47 | Rel of int * 'a
48 | CNamed of int * kind 48 | Named of int * 'a
49 49
50 type env = { 50 type env = {
51 renameC : var' SM.map, 51 renameC : kind var' SM.map,
52 relC : (string * kind) list, 52 relC : (string * kind) list,
53 namedC : (string * kind) IM.map 53 namedC : (string * kind) IM.map,
54
55 renameE : con var' SM.map,
56 relE : (string * con) list,
57 namedE : (string * con) IM.map
54 } 58 }
55 59
56 val namedCounter = ref 0 60 val namedCounter = ref 0
57 61
58 val empty = { 62 val empty = {
59 renameC = SM.empty, 63 renameC = SM.empty,
60 relC = [], 64 relC = [],
61 namedC = IM.empty 65 namedC = IM.empty,
66
67 renameE = SM.empty,
68 relE = [],
69 namedE = IM.empty
62 } 70 }
63 71
64 fun pushCRel (env : env) x k = 72 fun pushCRel (env : env) x k =
65 let 73 let
66 val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k) 74 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
67 | x => x) (#renameC env) 75 | x => x) (#renameC env)
68 in 76 in
69 {renameC = SM.insert (renameC, x, CRel' (0, k)), 77 {renameC = SM.insert (renameC, x, Rel' (0, k)),
70 relC = (x, k) :: #relC env, 78 relC = (x, k) :: #relC env,
71 namedC = #namedC env} 79 namedC = #namedC env,
80
81 renameE = #renameE env,
82 relE = #relE env,
83 namedE = #namedE env}
72 end 84 end
73 85
74 fun lookupCRel (env : env) n = 86 fun lookupCRel (env : env) n =
75 (List.nth (#relC env, n)) 87 (List.nth (#relC env, n))
76 handle Subscript => raise UnboundRel n 88 handle Subscript => raise UnboundRel n
77 89
78 fun pushCNamedAs (env : env) x n k = 90 fun pushCNamedAs (env : env) x n k =
79 {renameC = SM.insert (#renameC env, x, CNamed' (n, k)), 91 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
80 relC = #relC env, 92 relC = #relC env,
81 namedC = IM.insert (#namedC env, n, (x, k))} 93 namedC = IM.insert (#namedC env, n, (x, k)),
94
95 renameE = #renameE env,
96 relE = #relE env,
97 namedE = #namedE env}
82 98
83 fun pushCNamed env x k = 99 fun pushCNamed env x k =
84 let 100 let
85 val n = !namedCounter 101 val n = !namedCounter
86 in 102 in
93 NONE => raise UnboundNamed n 109 NONE => raise UnboundNamed n
94 | SOME x => x 110 | SOME x => x
95 111
96 fun lookupC (env : env) x = 112 fun lookupC (env : env) x =
97 case SM.find (#renameC env, x) of 113 case SM.find (#renameC env, x) of
98 NONE => CNotBound 114 NONE => NotBound
99 | SOME (CRel' x) => CRel x 115 | SOME (Rel' x) => Rel x
100 | SOME (CNamed' x) => CNamed x 116 | SOME (Named' x) => Named x
117
118 fun pushERel (env : env) x t =
119 let
120 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
121 | x => x) (#renameE env)
122 in
123 {renameC = #renameC env,
124 relC = #relC env,
125 namedC = #namedC env,
126
127 renameE = SM.insert (renameE, x, Rel' (0, t)),
128 relE = (x, t) :: #relE env,
129 namedE = #namedE env}
130 end
131
132 fun lookupERel (env : env) n =
133 (List.nth (#relE env, n))
134 handle Subscript => raise UnboundRel n
135
136 fun pushENamedAs (env : env) x n t =
137 {renameC = #renameC env,
138 relC = #relC env,
139 namedC = #namedC env,
140
141 renameE = SM.insert (#renameE env, x, Named' (n, t)),
142 relE = #relE env,
143 namedE = IM.insert (#namedE env, n, (x, t))}
144
145 fun pushENamed env x t =
146 let
147 val n = !namedCounter
148 in
149 namedCounter := n + 1;
150 (pushENamedAs env x n t, n)
151 end
152
153 fun lookupENamed (env : env) n =
154 case IM.find (#namedE env, n) of
155 NONE => raise UnboundNamed n
156 | SOME x => x
157
158 fun lookupE (env : env) x =
159 case SM.find (#renameE env, x) of
160 NONE => NotBound
161 | SOME (Rel' x) => Rel x
162 | SOME (Named' x) => Named x
101 163
102 end 164 end