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