Mercurial > urweb

comparison src/cjrize.sml @ 808:d8f58d488cfb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Pathcheck
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:55:15 -0400
parents fa2019a63ea4
children 81fce435e255
comparison
equal deleted inserted replaced
807:61a1f5c5ae2c 808:d8f58d488cfb
481 | L.ERecv _ => raise Fail "Cjrize ERecv" 481 | L.ERecv _ => raise Fail "Cjrize ERecv"
482 | L.ESleep _ => raise Fail "Cjrize ESleep" 482 | L.ESleep _ => raise Fail "Cjrize ESleep"
483 483
484 fun cifyDecl ((d, loc), sm) = 484 fun cifyDecl ((d, loc), sm) =
485 case d of 485 case d of
486 L.DDatatype (x, n, xncs) => 486 L.DDatatype _ => raise Fail "Cjrize DDatatype"
487 (*L.DDatatype (x, n, xncs) =>
487 let 488 let
488 val dk = ElabUtil.classifyDatatype xncs 489 val dk = ElabUtil.classifyDatatype xncs
489 val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) => 490 val (xncs, sm) = ListUtil.foldlMap (fn ((x, n, to), sm) =>
490 case to of 491 case to of
491 NONE => ((x, n, NONE), sm) 492 NONE => ((x, n, NONE), sm)
495 in 496 in
496 ((x, n, SOME t), sm) 497 ((x, n, SOME t), sm)
497 end) sm xncs 498 end) sm xncs
498 in 499 in
499 (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm) 500 (SOME (L'.DDatatype (dk, x, n, xncs), loc), NONE, sm)
500 end 501 end*)
501 502
502 | L.DVal (x, n, t, e, _) => 503 | L.DVal (x, n, t, e, _) =>
503 let 504 let
504 val (t, sm) = cifyTyp (t, sm) 505 val (t, sm) = cifyTyp (t, sm)
505 506