Mercurial > urweb

comparison src/core_env.sml @ 177:5d030ee143e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Case through corify
author Adam Chlipala <adamc@hcoop.net>
date Sat, 02 Aug 2008 11:15:32 -0400
parents 25b169416ea8
children d11754ffe252
comparison
equal deleted inserted replaced
176:33d4a8eea484 177:5d030ee143e2
60 type env = { 60 type env = {
61 relC : (string * kind) list, 61 relC : (string * kind) list,
62 namedC : (string * kind * con option) IM.map, 62 namedC : (string * kind * con option) IM.map,
63 63
64 datatypes : (string * (string * int * con option) list) IM.map, 64 datatypes : (string * (string * int * con option) list) IM.map,
65 constructors : (string * con option * int) IM.map,
65 66
66 relE : (string * con) list, 67 relE : (string * con) list,
67 namedE : (string * con * exp option * string) IM.map 68 namedE : (string * con * exp option * string) IM.map
68 } 69 }
69 70
70 val empty = { 71 val empty = {
71 relC = [], 72 relC = [],
72 namedC = IM.empty, 73 namedC = IM.empty,
73 74
74 datatypes = IM.empty, 75 datatypes = IM.empty,
76 constructors = IM.empty,
75 77
76 relE = [], 78 relE = [],
77 namedE = IM.empty 79 namedE = IM.empty
78 } 80 }
79 81
80 fun pushCRel (env : env) x k = 82 fun pushCRel (env : env) x k =
81 {relC = (x, k) :: #relC env, 83 {relC = (x, k) :: #relC env,
82 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 84 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
83 85
84 datatypes = #datatypes env, 86 datatypes = #datatypes env,
87 constructors = #constructors env,
85 88
86 relE = map (fn (x, c) => (x, lift c)) (#relE env), 89 relE = map (fn (x, c) => (x, lift c)) (#relE env),
87 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)} 90 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
88 91
89 fun lookupCRel (env : env) n = 92 fun lookupCRel (env : env) n =
93 fun pushCNamed (env : env) x n k co = 96 fun pushCNamed (env : env) x n k co =
94 {relC = #relC env, 97 {relC = #relC env,
95 namedC = IM.insert (#namedC env, n, (x, k, co)), 98 namedC = IM.insert (#namedC env, n, (x, k, co)),
96 99
97 datatypes = #datatypes env, 100 datatypes = #datatypes env,
101 constructors = #constructors env,
98 102
99 relE = #relE env, 103 relE = #relE env,
100 namedE = #namedE env} 104 namedE = #namedE env}
101 105
102 fun lookupCNamed (env : env) n = 106 fun lookupCNamed (env : env) n =
107 fun pushDatatype (env : env) x n xncs = 111 fun pushDatatype (env : env) x n xncs =
108 {relC = #relC env, 112 {relC = #relC env,
109 namedC = #namedC env, 113 namedC = #namedC env,
110 114
111 datatypes = IM.insert (#datatypes env, n, (x, xncs)), 115 datatypes = IM.insert (#datatypes env, n, (x, xncs)),
116 constructors = foldl (fn ((x, n, to), constructors) =>
117 IM.insert (constructors, n, (x, to, n)))
118 (#constructors env) xncs,
112 119
113 relE = #relE env, 120 relE = #relE env,
114 namedE = #namedE env} 121 namedE = #namedE env}
115 122
116 fun lookupDatatype (env : env) n = 123 fun lookupDatatype (env : env) n =
117 case IM.find (#datatypes env, n) of 124 case IM.find (#datatypes env, n) of
118 NONE => raise UnboundNamed n 125 NONE => raise UnboundNamed n
119 | SOME x => x 126 | SOME x => x
120 127
128 fun lookupConstructor (env : env) n =
129 case IM.find (#constructors env, n) of
130 NONE => raise UnboundNamed n
131 | SOME x => x
132
121 fun pushERel (env : env) x t = 133 fun pushERel (env : env) x t =
122 {relC = #relC env, 134 {relC = #relC env,
123 namedC = #namedC env, 135 namedC = #namedC env,
124 136
125 datatypes = #datatypes env, 137 datatypes = #datatypes env,
138 constructors = #constructors env,
126 139
127 relE = (x, t) :: #relE env, 140 relE = (x, t) :: #relE env,
128 namedE = #namedE env} 141 namedE = #namedE env}
129 142
130 fun lookupERel (env : env) n = 143 fun lookupERel (env : env) n =
134 fun pushENamed (env : env) x n t eo s = 147 fun pushENamed (env : env) x n t eo s =
135 {relC = #relC env, 148 {relC = #relC env,
136 namedC = #namedC env, 149 namedC = #namedC env,
137 150
138 datatypes = #datatypes env, 151 datatypes = #datatypes env,
152 constructors = #constructors env,
139 153
140 relE = #relE env, 154 relE = #relE env,
141 namedE = IM.insert (#namedE env, n, (x, t, eo, s))} 155 namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
142 156
143 fun lookupENamed (env : env) n = 157 fun lookupENamed (env : env) n =