Mercurial > urweb

comparison src/core_env.sml @ 168:25b169416ea8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Storing datatype constructors in type references past monoize
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 15:43:17 -0400
parents 80192edca30d
children 5d030ee143e2
comparison
equal deleted inserted replaced
167:2be573fec9a6 168:25b169416ea8
59 59
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,
65
64 relE : (string * con) list, 66 relE : (string * con) list,
65 namedE : (string * con * exp option * string) IM.map 67 namedE : (string * con * exp option * string) IM.map
66 } 68 }
67 69
68 val empty = { 70 val empty = {
69 relC = [], 71 relC = [],
70 namedC = IM.empty, 72 namedC = IM.empty,
71 73
74 datatypes = IM.empty,
75
72 relE = [], 76 relE = [],
73 namedE = IM.empty 77 namedE = IM.empty
74 } 78 }
75 79
76 fun pushCRel (env : env) x k = 80 fun pushCRel (env : env) x k =
77 {relC = (x, k) :: #relC env, 81 {relC = (x, k) :: #relC env,
78 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 82 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
83
84 datatypes = #datatypes env,
79 85
80 relE = map (fn (x, c) => (x, lift c)) (#relE env), 86 relE = map (fn (x, c) => (x, lift c)) (#relE env),
81 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)} 87 namedE = IM.map (fn (x, c, eo, s) => (x, lift c, eo, s)) (#namedE env)}
82 88
83 fun lookupCRel (env : env) n = 89 fun lookupCRel (env : env) n =
86 92
87 fun pushCNamed (env : env) x n k co = 93 fun pushCNamed (env : env) x n k co =
88 {relC = #relC env, 94 {relC = #relC env,
89 namedC = IM.insert (#namedC env, n, (x, k, co)), 95 namedC = IM.insert (#namedC env, n, (x, k, co)),
90 96
97 datatypes = #datatypes env,
98
91 relE = #relE env, 99 relE = #relE env,
92 namedE = #namedE env} 100 namedE = #namedE env}
93 101
94 fun lookupCNamed (env : env) n = 102 fun lookupCNamed (env : env) n =
95 case IM.find (#namedC env, n) of 103 case IM.find (#namedC env, n) of
96 NONE => raise UnboundNamed n 104 NONE => raise UnboundNamed n
97 | SOME x => x 105 | SOME x => x
98 106
107 fun pushDatatype (env : env) x n xncs =
108 {relC = #relC env,
109 namedC = #namedC env,
110
111 datatypes = IM.insert (#datatypes env, n, (x, xncs)),
112
113 relE = #relE env,
114 namedE = #namedE env}
115
116 fun lookupDatatype (env : env) n =
117 case IM.find (#datatypes env, n) of
118 NONE => raise UnboundNamed n
119 | SOME x => x
120
99 fun pushERel (env : env) x t = 121 fun pushERel (env : env) x t =
100 {relC = #relC env, 122 {relC = #relC env,
101 namedC = #namedC env, 123 namedC = #namedC env,
124
125 datatypes = #datatypes env,
102 126
103 relE = (x, t) :: #relE env, 127 relE = (x, t) :: #relE env,
104 namedE = #namedE env} 128 namedE = #namedE env}
105 129
106 fun lookupERel (env : env) n = 130 fun lookupERel (env : env) n =
108 handle Subscript => raise UnboundRel n 132 handle Subscript => raise UnboundRel n
109 133
110 fun pushENamed (env : env) x n t eo s = 134 fun pushENamed (env : env) x n t eo s =
111 {relC = #relC env, 135 {relC = #relC env,
112 namedC = #namedC env, 136 namedC = #namedC env,
137
138 datatypes = #datatypes env,
113 139
114 relE = #relE env, 140 relE = #relE env,
115 namedE = IM.insert (#namedE env, n, (x, t, eo, s))} 141 namedE = IM.insert (#namedE env, n, (x, t, eo, s))}
116 142
117 fun lookupENamed (env : env) n = 143 fun lookupENamed (env : env) n =
122 fun declBinds env (d, loc) = 148 fun declBinds env (d, loc) =
123 case d of 149 case d of
124 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) 150 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
125 | DDatatype (x, n, xncs) => 151 | DDatatype (x, n, xncs) =>
126 let 152 let
153 val env = pushDatatype env x n xncs
127 val env = pushCNamed env x n (KType, loc) NONE 154 val env = pushCNamed env x n (KType, loc) NONE
128 in 155 in
129 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE "" 156 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) NONE ""
130 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "") 157 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc) NONE "")
131 env xncs 158 env xncs