Mercurial > urweb

comparison src/cjr_env.sml @ 181:31dfab1d4050

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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