Mercurial > urweb
comparison src/mono_util.sml @ 198:ab86aa858e6c
'Option' datatype encoding
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 09 Aug 2008 19:23:31 -0400 |
parents | 890a61991263 |
children | 326fb4686f60 |
comparison
equal
deleted
inserted
replaced
197:b1b9bcfd8c42 | 198:ab86aa858e6c |
---|---|
26 *) | 26 *) |
27 | 27 |
28 structure MonoUtil :> MONO_UTIL = struct | 28 structure MonoUtil :> MONO_UTIL = struct |
29 | 29 |
30 open Mono | 30 open Mono |
31 | |
32 fun classifyDatatype xncs = | |
33 if List.all (fn (_, _, NONE) => true | _ => false) xncs then | |
34 Enum | |
35 else | |
36 Default | |
37 | 31 |
38 structure S = Search | 32 structure S = Search |
39 | 33 |
40 structure Typ = struct | 34 structure Typ = struct |
41 | 35 |
352 val ctx' = | 346 val ctx' = |
353 case #1 d' of | 347 case #1 d' of |
354 DDatatype (x, n, xncs) => | 348 DDatatype (x, n, xncs) => |
355 let | 349 let |
356 val ctx = bind (ctx, Datatype (x, n, xncs)) | 350 val ctx = bind (ctx, Datatype (x, n, xncs)) |
357 val t = (TDatatype (n, ref (classifyDatatype xncs, xncs)), #2 d') | 351 val t = (TDatatype (n, ref (ElabUtil.classifyDatatype xncs, xncs)), #2 d') |
358 in | 352 in |
359 foldl (fn ((x, n, to), ctx) => | 353 foldl (fn ((x, n, to), ctx) => |
360 let | 354 let |
361 val t = case to of | 355 val t = case to of |
362 NONE => t | 356 NONE => t |