Mercurial > urweb

comparison src/cjr_env.sml @ 166:a991431b77eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of unurlify for datatypes
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 14:28:44 -0400
parents e52dfb1e6b19
children 25b169416ea8
comparison
equal deleted inserted replaced
165:e52dfb1e6b19 166:a991431b77eb
36 exception UnboundNamed of int 36 exception UnboundNamed of int
37 exception UnboundF of int 37 exception UnboundF of int
38 exception UnboundStruct of int 38 exception UnboundStruct of int
39 39
40 type env = { 40 type env = {
41 namedT : (string * typ option) IM.map, 41 datatypes : (string * (string * int * typ option) list) IM.map,
42 42
43 numRelE : int, 43 numRelE : int,
44 relE : (string * typ) list, 44 relE : (string * typ) list,
45 namedE : (string * typ) IM.map, 45 namedE : (string * typ) IM.map,
46 46
47 structs : (string * typ) list IM.map 47 structs : (string * typ) list IM.map
48 } 48 }
49 49
50 val empty = { 50 val empty = {
51 namedT = IM.empty, 51 datatypes = IM.empty,
52 52
53 numRelE = 0, 53 numRelE = 0,
54 relE = [], 54 relE = [],
55 namedE = IM.empty, 55 namedE = IM.empty,
56 56
57 structs = IM.empty 57 structs = IM.empty
58 } 58 }
59 59
60 fun pushTNamed (env : env) x n co = 60 fun pushDatatype (env : env) x n xncs =
61 {namedT = IM.insert (#namedT env, n, (x, co)), 61 {datatypes = IM.insert (#datatypes env, n, (x, xncs)),
62 62
63 numRelE = #numRelE env, 63 numRelE = #numRelE env,
64 relE = #relE env, 64 relE = #relE env,
65 namedE = #namedE env, 65 namedE = #namedE env,
66 66
67 structs = #structs env} 67 structs = #structs env}
68 68
69 fun lookupTNamed (env : env) n = 69 fun lookupDatatype (env : env) n =
70 case IM.find (#namedT env, n) of 70 case IM.find (#datatypes env, n) of
71 NONE => raise UnboundNamed n 71 NONE => raise UnboundNamed n
72 | SOME x => x 72 | SOME x => x
73 73
74 fun pushERel (env : env) x t = 74 fun pushERel (env : env) x t =
75 {namedT = #namedT env, 75 {datatypes = #datatypes env,
76 76
77 numRelE = #numRelE env + 1, 77 numRelE = #numRelE env + 1,
78 relE = (x, t) :: #relE env, 78 relE = (x, t) :: #relE env,
79 namedE = #namedE env, 79 namedE = #namedE env,
80 80
87 fun countERels (env : env) = #numRelE env 87 fun countERels (env : env) = #numRelE env
88 88
89 fun listERels (env : env) = #relE env 89 fun listERels (env : env) = #relE env
90 90
91 fun pushENamed (env : env) x n t = 91 fun pushENamed (env : env) x n t =
92 {namedT = #namedT env, 92 {datatypes = #datatypes env,
93 93
94 numRelE = #numRelE env, 94 numRelE = #numRelE env,
95 relE = #relE env, 95 relE = #relE env,
96 namedE = IM.insert (#namedE env, n, (x, t)), 96 namedE = IM.insert (#namedE env, n, (x, t)),
97 97
101 case IM.find (#namedE env, n) of 101 case IM.find (#namedE env, n) of
102 NONE => raise UnboundNamed n 102 NONE => raise UnboundNamed n
103 | SOME x => x 103 | SOME x => x
104 104
105 fun pushStruct (env : env) n xts = 105 fun pushStruct (env : env) n xts =
106 {namedT = #namedT env, 106 {datatypes = #datatypes env,
107 107
108 numRelE = #numRelE env, 108 numRelE = #numRelE env,
109 relE = #relE env, 109 relE = #relE env,
110 namedE = #namedE env, 110 namedE = #namedE env,
111 111
118 118
119 fun declBinds env (d, loc) = 119 fun declBinds env (d, loc) =
120 case d of 120 case d of
121 DDatatype (x, n, xncs) => 121 DDatatype (x, n, xncs) =>
122 let 122 let
123 val env = pushTNamed env x n NONE 123 val env = pushDatatype env x n xncs
124 in 124 in
125 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TNamed n, loc) 125 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (TDatatype n, loc)
126 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TNamed n, loc)), loc)) 126 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (TDatatype n, loc)), loc))
127 env xncs 127 env xncs
128 end 128 end
129 | DStruct (n, xts) => pushStruct env n xts 129 | DStruct (n, xts) => pushStruct env n xts
130 | DVal (x, n, t, _) => pushENamed env x n t 130 | DVal (x, n, t, _) => pushENamed env x n t
131 | DFun (fx, n, args, ran, _) => 131 | DFun (fx, n, args, ran, _) =>