comparison src/corify.sml @ 162:06a98129b23f

Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 7420fa18d657
children 80192edca30d
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
382 let 382 let
383 val (st, n) = St.bindCon st x n 383 val (st, n) = St.bindCon st x n
384 in 384 in
385 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 385 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
386 end 386 end
387 | L.DDatatype _ => raise Fail "Corify DDatatype"
388 | L.DDatatypeImp _ => raise Fail "Corify DDatatypeImp"
387 | L.DVal (x, n, t, e) => 389 | L.DVal (x, n, t, e) =>
388 let 390 let
389 val (st, n) = St.bindVal st x n 391 val (st, n) = St.bindVal st x n
390 val s = 392 val s =
391 if String.isPrefix "wrap_" x then 393 if String.isPrefix "wrap_" x then
566 end 568 end
567 569
568 fun maxName ds = foldl (fn ((d, _), n) => 570 fun maxName ds = foldl (fn ((d, _), n) =>
569 case d of 571 case d of
570 L.DCon (_, n', _, _) => Int.max (n, n') 572 L.DCon (_, n', _, _) => Int.max (n, n')
573 | L.DDatatype (_, n', _) => Int.max (n, n')
574 | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n')
571 | L.DVal (_, n', _, _) => Int.max (n, n') 575 | L.DVal (_, n', _, _) => Int.max (n, n')
572 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis 576 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
573 | L.DSgn (_, n', _) => Int.max (n, n') 577 | L.DSgn (_, n', _) => Int.max (n, n')
574 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) 578 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
575 | L.DFfiStr (_, n', _) => Int.max (n, n') 579 | L.DFfiStr (_, n', _) => Int.max (n, n')