Mercurial > urweb

comparison src/corify.sml @ 186:88d46972de53

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bool in Basis
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 18:53:20 -0400
parents 19ee24bffbc0
children 8e9f97508f0d
comparison
equal deleted inserted replaced
185:19ee24bffbc0 186:88d46972de53
60 60
61 val debug : t -> unit 61 val debug : t -> unit
62 62
63 val enter : t -> t 63 val enter : t -> t
64 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
65 val ffi : string -> L'.con SM.map -> string SM.map -> t 65 val ffi : string -> L'.con SM.map -> (string * L'.con option) SM.map -> t
66 66
67 datatype core_con = 67 datatype core_con =
68 CNormal of int 68 CNormal of int
69 | CFfi of string 69 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 70 val bindCon : t -> string -> int -> t * int
71 val lookupConById : t -> int -> int option 71 val lookupConById : t -> int -> int option
72 val lookupConByName : t -> string -> core_con 72 val lookupConByName : t -> string -> core_con
73 73
74 val bindConstructor : t -> string -> int -> L'.patCon -> t 74 val bindConstructor : t -> string -> int -> L'.patCon -> t
75 val lookupConstructorByNameOpt : t -> string -> L'.patCon option
75 val lookupConstructorByName : t -> string -> L'.patCon 76 val lookupConstructorByName : t -> string -> L'.patCon
76 val lookupConstructorById : t -> int -> L'.patCon 77 val lookupConstructorById : t -> int -> L'.patCon
77 78
78 datatype core_val = 79 datatype core_val =
79 ENormal of int 80 ENormal of int
98 vals : int SM.map, 99 vals : int SM.map,
99 strs : flattening SM.map, 100 strs : flattening SM.map,
100 funs : (string * int * L.str) SM.map} 101 funs : (string * int * L.str) SM.map}
101 | FFfi of {mod : string, 102 | FFfi of {mod : string,
102 vals : L'.con SM.map, 103 vals : L'.con SM.map,
103 constructors : string SM.map} 104 constructors : (string * L'.con option) SM.map}
104 105
105 type t = { 106 type t = {
106 cons : int IM.map, 107 cons : int IM.map,
107 constructors : L'.patCon IM.map, 108 constructors : L'.patCon IM.map,
108 vals : int IM.map, 109 vals : int IM.map,
255 fun lookupConstructorById ({constructors, ...} : t) n = 256 fun lookupConstructorById ({constructors, ...} : t) n =
256 case IM.find (constructors, n) of 257 case IM.find (constructors, n) of
257 NONE => raise Fail "Corify.St.lookupConstructorById" 258 NONE => raise Fail "Corify.St.lookupConstructorById"
258 | SOME x => x 259 | SOME x => x
259 260
261 fun lookupConstructorByNameOpt ({current, ...} : t) x =
262 case current of
263 FFfi {mod = m, constructors, ...} =>
264 (case SM.find (constructors, x) of
265 NONE => NONE
266 | SOME (n, to) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to}))
267 | FNormal {constructors, ...} =>
268 case SM.find (constructors, x) of
269 NONE => NONE
270 | SOME n => SOME n
271
260 fun lookupConstructorByName ({current, ...} : t) x = 272 fun lookupConstructorByName ({current, ...} : t) x =
261 case current of 273 case current of
262 FFfi {mod = m, constructors, ...} => 274 FFfi {mod = m, constructors, ...} =>
263 (case SM.find (constructors, x) of 275 (case SM.find (constructors, x) of
264 NONE => raise Fail "Corify.St.lookupConstructorByName [1]" 276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
265 | SOME n => L'.PConFfi {mod = m, datatyp = n, con = x}) 277 | SOME (n, to) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to})
266 | FNormal {constructors, ...} => 278 | FNormal {constructors, ...} =>
267 case SM.find (constructors, x) of 279 case SM.find (constructors, x) of
268 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" 280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
269 | SOME n => n 281 | SOME n => n
270 282
431 | L.EModProj (m, ms, x) => 443 | L.EModProj (m, ms, x) =>
432 let 444 let
433 val st = St.lookupStrById st m 445 val st = St.lookupStrById st m
434 val st = foldl St.lookupStrByName st ms 446 val st = foldl St.lookupStrByName st ms
435 in 447 in
436 case St.lookupValByName st x of 448 case St.lookupConstructorByNameOpt st x of
437 St.ENormal n => (L'.ENamed n, loc) 449 SOME (pc as L'.PConFfi {mod = m, datatyp, arg, ...}) =>
438 | St.EFfi (m, t) => 450 (case arg of
439 case t of 451 NONE => (L'.ECon (pc, NONE), loc)
440 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => 452 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
441 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) 453 (L'.ECon (pc, SOME (L'.ERel 0, loc)), loc)), loc))
442 | t as (L'.TFun _, _) => 454 | _ =>
443 let 455 case St.lookupValByName st x of
444 fun getArgs (all as (t, _), args) = 456 St.ENormal n => (L'.ENamed n, loc)
445 case t of 457 | St.EFfi (m, t) =>
446 L'.TFun (dom, ran) => getArgs (ran, dom :: args) 458 case t of
447 | _ => (all, rev args) 459 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
448 460 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
449 val (result, args) = getArgs (t, []) 461 | t as (L'.TFun _, _) =>
450 462 let
451 val (actuals, _) = foldr (fn (_, (actuals, n)) => 463 fun getArgs (all as (t, _), args) =
452 ((L'.ERel n, loc) :: actuals, 464 case t of
453 n + 1)) ([], 0) args 465 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
454 val app = (L'.EFfiApp (m, x, actuals), loc) 466 | _ => (all, rev args)
455 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => 467
456 ((L'.EAbs ("arg" ^ Int.toString n, 468 val (result, args) = getArgs (t, [])
457 t, 469
458 ran, 470 val (actuals, _) = foldr (fn (_, (actuals, n)) =>
459 abs), loc), 471 ((L'.ERel n, loc) :: actuals,
460 (L'.TFun (t, ran), loc), 472 n + 1)) ([], 0) args
461 n - 1)) (app, result, length args - 1) args 473 val app = (L'.EFfiApp (m, x, actuals), loc)
462 in 474 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
463 abs 475 ((L'.EAbs ("arg" ^ Int.toString n,
464 end 476 t,
465 | _ => (L'.EFfi (m, x), loc) 477 ran,
478 abs), loc),
479 (L'.TFun (t, ran), loc),
480 n - 1)) (app, result, length args - 1) args
481 in
482 abs
483 end
484 | _ => (L'.EFfi (m, x), loc)
466 end 485 end
467 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) 486 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
468 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) 487 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
469 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) 488 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
470 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) 489 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
628 end 647 end
629 648
630 | L.SgiDatatype (x, n, xnts) => 649 | L.SgiDatatype (x, n, xnts) =>
631 let 650 let
632 val (st, n') = St.bindCon st x n 651 val (st, n') = St.bindCon st x n
633 val (xnts, (st, cmap, conmap)) = 652 val (xnts, (ds', st, cmap, conmap)) =
634 ListUtil.foldlMap 653 ListUtil.foldlMap
635 (fn ((x', n, to), (st, cmap, conmap)) => 654 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
636 let 655 let
637 val st = St.bindConstructor st x' n
638 (L'.PConFfi {mod = m,
639 datatyp = x,
640 con = x'})
641 val st = St.bindConstructorVal st x' n
642
643 val dt = (L'.CNamed n', loc) 656 val dt = (L'.CNamed n', loc)
644 657
645 val (to, cmap) = 658 val to = Option.map (corifyCon st) to
659
660 val pc = L'.PConFfi {mod = m,
661 datatyp = x,
662 con = x',
663 arg = to}
664
665 val (cmap, d) =
646 case to of 666 case to of
647 NONE => (NONE, SM.insert (cmap, x', dt)) 667 NONE => (SM.insert (cmap, x', dt),
668 (L'.DVal (x', n, dt,
669 (L'.ECon (pc, NONE), loc),
670 ""), loc))
648 | SOME t => 671 | SOME t =>
649 let 672 let
650 val t = corifyCon st t 673 val tf = (L'.TFun (t, dt), loc)
674 val d = (L'.DVal (x', n, tf,
675 (L'.EAbs ("x", t, tf,
676 (L'.ECon (pc,
677 SOME (L'.ERel 0,
678 loc)),
679 loc)), loc), ""), loc)
651 in 680 in
652 (SOME t, SM.insert (cmap, x', 681 (SM.insert (cmap, x', tf), d)
653 (L'.TFun (t, dt), loc)))
654 end 682 end
655 683
656 val conmap = SM.insert (conmap, x', x) 684 val st = St.bindConstructor st x' n pc
685 (*val st = St.bindConstructorVal st x' n*)
686
687 val conmap = SM.insert (conmap, x', (x, to))
657 in 688 in
658 ((x', n, to), 689 ((x', n, to),
659 (st, cmap, conmap)) 690 (d :: ds', st, cmap, conmap))
660 end) (st, cmap, conmap) xnts 691 end) ([], st, cmap, conmap) xnts
661 in 692 in
662 ((L'.DDatatype (x, n', xnts), loc) :: ds, 693 (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds,
663 cmap, 694 cmap,
664 conmap, 695 conmap,
665 st) 696 st)
666 end 697 end
667 698