Mercurial > urweb
comparison src/cjr_env.sml @ 181:31dfab1d4050
Cjrize ECon
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 03 Aug 2008 11:17:33 -0400 |
parents | 25b169416ea8 |
children | d11754ffe252 |
comparison
equal
deleted
inserted
replaced
180:c7a5c8e0a0e0 | 181:31dfab1d4050 |
---|---|
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 datatypes : (string * (string * int * typ option) list) IM.map, | 41 datatypes : (string * (string * int * typ option) list) IM.map, |
42 constructors : (string * typ option * int) IM.map, | |
42 | 43 |
43 numRelE : int, | 44 numRelE : int, |
44 relE : (string * typ) list, | 45 relE : (string * typ) list, |
45 namedE : (string * typ) IM.map, | 46 namedE : (string * typ) IM.map, |
46 | 47 |
47 structs : (string * typ) list IM.map | 48 structs : (string * typ) list IM.map |
48 } | 49 } |
49 | 50 |
50 val empty = { | 51 val empty = { |
51 datatypes = IM.empty, | 52 datatypes = IM.empty, |
53 constructors = IM.empty, | |
52 | 54 |
53 numRelE = 0, | 55 numRelE = 0, |
54 relE = [], | 56 relE = [], |
55 namedE = IM.empty, | 57 namedE = IM.empty, |
56 | 58 |
57 structs = IM.empty | 59 structs = IM.empty |
58 } | 60 } |
59 | 61 |
60 fun pushDatatype (env : env) x n xncs = | 62 fun pushDatatype (env : env) x n xncs = |
61 {datatypes = IM.insert (#datatypes env, n, (x, xncs)), | 63 {datatypes = IM.insert (#datatypes env, n, (x, xncs)), |
64 constructors = foldl (fn ((x, n, to), constructors) => | |
65 IM.insert (constructors, n, (x, to, n))) | |
66 (#constructors env) xncs, | |
62 | 67 |
63 numRelE = #numRelE env, | 68 numRelE = #numRelE env, |
64 relE = #relE env, | 69 relE = #relE env, |
65 namedE = #namedE env, | 70 namedE = #namedE env, |
66 | 71 |
69 fun lookupDatatype (env : env) n = | 74 fun lookupDatatype (env : env) n = |
70 case IM.find (#datatypes env, n) of | 75 case IM.find (#datatypes env, n) of |
71 NONE => raise UnboundNamed n | 76 NONE => raise UnboundNamed n |
72 | SOME x => x | 77 | SOME x => x |
73 | 78 |
79 fun lookupConstructor (env : env) n = | |
80 case IM.find (#constructors env, n) of | |
81 NONE => raise UnboundNamed n | |
82 | SOME x => x | |
83 | |
74 fun pushERel (env : env) x t = | 84 fun pushERel (env : env) x t = |
75 {datatypes = #datatypes env, | 85 {datatypes = #datatypes env, |
86 constructors = #constructors env, | |
76 | 87 |
77 numRelE = #numRelE env + 1, | 88 numRelE = #numRelE env + 1, |
78 relE = (x, t) :: #relE env, | 89 relE = (x, t) :: #relE env, |
79 namedE = #namedE env, | 90 namedE = #namedE env, |
80 | 91 |
88 | 99 |
89 fun listERels (env : env) = #relE env | 100 fun listERels (env : env) = #relE env |
90 | 101 |
91 fun pushENamed (env : env) x n t = | 102 fun pushENamed (env : env) x n t = |
92 {datatypes = #datatypes env, | 103 {datatypes = #datatypes env, |
104 constructors = #constructors env, | |
93 | 105 |
94 numRelE = #numRelE env, | 106 numRelE = #numRelE env, |
95 relE = #relE env, | 107 relE = #relE env, |
96 namedE = IM.insert (#namedE env, n, (x, t)), | 108 namedE = IM.insert (#namedE env, n, (x, t)), |
97 | 109 |
102 NONE => raise UnboundNamed n | 114 NONE => raise UnboundNamed n |
103 | SOME x => x | 115 | SOME x => x |
104 | 116 |
105 fun pushStruct (env : env) n xts = | 117 fun pushStruct (env : env) n xts = |
106 {datatypes = #datatypes env, | 118 {datatypes = #datatypes env, |
119 constructors = #constructors env, | |
107 | 120 |
108 numRelE = #numRelE env, | 121 numRelE = #numRelE env, |
109 relE = #relE env, | 122 relE = #relE env, |
110 namedE = #namedE env, | 123 namedE = #namedE env, |
111 | 124 |