Mercurial > urweb

comparison src/elab_env.sml @ 11:e97c6d335869

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple elaboration working
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 15:20:46 -0400
parents 14b533dbe6cc
children 6049e2193bf2
comparison
equal deleted inserted replaced
10:dde5c52e5e5e 11:e97c6d335869
48 | Named of int * 'a 48 | Named of int * 'a
49 49
50 type env = { 50 type env = {
51 renameC : kind 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 * con option) IM.map,
54 54
55 renameE : con var' SM.map, 55 renameE : con var' SM.map,
56 relE : (string * con) list, 56 relE : (string * con) list,
57 namedE : (string * con) IM.map 57 namedE : (string * con) IM.map
58 } 58 }
85 85
86 fun lookupCRel (env : env) n = 86 fun lookupCRel (env : env) n =
87 (List.nth (#relC env, n)) 87 (List.nth (#relC env, n))
88 handle Subscript => raise UnboundRel n 88 handle Subscript => raise UnboundRel n
89 89
90 fun pushCNamedAs (env : env) x n k = 90 fun pushCNamedAs (env : env) x n k co =
91 {renameC = SM.insert (#renameC env, x, Named' (n, k)), 91 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
92 relC = #relC env, 92 relC = #relC env,
93 namedC = IM.insert (#namedC env, n, (x, k)), 93 namedC = IM.insert (#namedC env, n, (x, k, co)),
94 94
95 renameE = #renameE env, 95 renameE = #renameE env,
96 relE = #relE env, 96 relE = #relE env,
97 namedE = #namedE env} 97 namedE = #namedE env}
98 98
99 fun pushCNamed env x k = 99 fun pushCNamed env x k co =
100 let 100 let
101 val n = !namedCounter 101 val n = !namedCounter
102 in 102 in
103 namedCounter := n + 1; 103 namedCounter := n + 1;
104 (pushCNamedAs env x n k, n) 104 (pushCNamedAs env x n k co, n)
105 end 105 end
106 106
107 fun lookupCNamed (env : env) n = 107 fun lookupCNamed (env : env) n =
108 case IM.find (#namedC env, n) of 108 case IM.find (#namedC env, n) of
109 NONE => raise UnboundNamed n 109 NONE => raise UnboundNamed n