Mercurial > urweb

comparison src/elab_util.sml @ 448:85819353a84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First Unnest tests working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 15:58:55 -0400
parents b77863cd0be2
children 787d4931fb07
comparison
equal deleted inserted replaced
447:b77863cd0be2 448:85819353a84f
223 S.Return () 223 S.Return ()
224 else 224 else
225 S.Continue (c, ())} k () of 225 S.Continue (c, ())} k () of
226 S.Return _ => true 226 S.Return _ => true
227 | S.Continue _ => false 227 | S.Continue _ => false
228
229 fun foldB {kind, con, bind} ctx st c =
230 case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
231 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
232 bind = bind} ctx c st of
233 S.Continue (_, st) => st
234 | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
228 235
229 end 236 end
230 237
231 structure Exp = struct 238 structure Exp = struct
232 239
338 345
339 | ECase (e, pes, {disc, result}) => 346 | ECase (e, pes, {disc, result}) =>
340 S.bind2 (mfe ctx e, 347 S.bind2 (mfe ctx e,
341 fn e' => 348 fn e' =>
342 S.bind2 (ListUtil.mapfold (fn (p, e) => 349 S.bind2 (ListUtil.mapfold (fn (p, e) =>
343 S.map2 (mfe ctx e, 350 let
344 fn e' => (p, e'))) pes, 351 fun pb ((p, _), ctx) =
352 case p of
353 PWild => ctx
354 | PVar (x, t) => bind (ctx, RelE (x, t))
355 | PPrim _ => ctx
356 | PCon (_, _, _, NONE) => ctx
357 | PCon (_, _, _, SOME p) => pb (p, ctx)
358 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
359 pb (p, ctx)) ctx xps
360 in
361 S.map2 (mfe (pb (p, ctx)) e,
362 fn e' => (p, e'))
363 end) pes,
345 fn pes' => 364 fn pes' =>
346 S.bind2 (mfc ctx disc, 365 S.bind2 (mfc ctx disc,
347 fn disc' => 366 fn disc' =>
348 S.map2 (mfc ctx result, 367 S.map2 (mfc ctx result,
349 fn result' => 368 fn result' =>
428 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), 447 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
429 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), 448 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
430 bind = bind} ctx e () of 449 bind = bind} ctx e () of
431 S.Continue (e, ()) => e 450 S.Continue (e, ()) => e
432 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" 451 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
452
453 fun foldB {kind, con, exp, bind} ctx st e =
454 case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
455 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
456 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
457 bind = bind} ctx e st of
458 S.Continue (_, st) => st
459 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
433 460
434 end 461 end
435 462
436 structure Sgn = struct 463 structure Sgn = struct
437 464
886 913
887 } k () of 914 } k () of
888 S.Return x => SOME x 915 S.Return x => SOME x
889 | S.Continue _ => NONE 916 | S.Continue _ => NONE
890 917
918 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
919 case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)),
920 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
921 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
922 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
923 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
924 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
925 decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
926 bind = bind} ctx d st of
927 S.Continue x => x
928 | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
929
891 end 930 end
892 931
932 structure File = struct
933
934 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
935
936 and maxNameDecl (d, _) =
937 case d of
938 DCon (_, n, _, _) => n
939 | DDatatype (_, n, _, ns) =>
940 foldl (fn ((_, n', _), m) => Int.max (n', m))
941 n ns
942 | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
943 foldl (fn ((_, n', _), m) => Int.max (n', m))
944 (Int.max (n1, n2)) ns
945 | DVal (_, n, _, _) => n
946 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
947 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
948 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
949 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
950 | DConstraint _ => 0
951 | DClass (_, n, _) => n
952 | DExport _ => 0
953 | DTable (n, _, _, _) => n
954 | DSequence (n, _, _) => n
955 | DDatabase _ => 0
956
957 and maxNameStr (str, _) =
958 case str of
959 StrConst ds => maxName ds
960 | StrVar n => n
961 | StrProj (str, _) => maxNameStr str
962 | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
963 | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
964 | StrError => 0
965
966 and maxNameSgn (sgn, _) =
967 case sgn of
968 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
969 | SgnVar n => n
970 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
971 | SgnWhere (sgn, _, _) => maxNameSgn sgn
972 | SgnProj (n, _, _) => n
973 | SgnError => 0
974
975 and maxNameSgi (sgi, _) =
976 case sgi of
977 SgiConAbs (_, n, _) => n
978 | SgiCon (_, n, _, _) => n
979 | SgiDatatype (_, n, _, ns) =>
980 foldl (fn ((_, n', _), m) => Int.max (n', m))
981 n ns
982 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
983 foldl (fn ((_, n', _), m) => Int.max (n', m))
984 (Int.max (n1, n2)) ns
985 | SgiVal (_, n, _) => n
986 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
987 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
988 | SgiConstraint _ => 0
989 | SgiTable (n, _, _, _) => n
990 | SgiSequence (n, _, _) => n
991 | SgiClassAbs (_, n) => n
992 | SgiClass (_, n, _) => n
993
893 end 994 end
995
996 end