Mercurial > urweb

comparison src/elab_env.sml @ 721:9864b64b1700

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Classes as optional arguments to Basis.tag
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 14:19:15 -0400
parents acb8537f58f0
children 059074c8d2fc
comparison
equal deleted inserted replaced
720:acb8537f58f0 721:9864b64b1700
897 in 897 in
898 CModProj (m1, ms, nx) 898 CModProj (m1, ms, nx)
899 end) 899 end)
900 | _ => c 900 | _ => c
901 901
902 fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c = 902 fun sgnS_con' (m1, ms', (sgns, strs, cons)) =
903 case c of 903 U.Con.map {kind = fn x => x,
904 CModProj (m1, ms, x) => 904 con = fn c =>
905 (case IM.find (strs, m1) of 905 case c of
906 NONE => c 906 CModProj (m1, ms, x) =>
907 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x)) 907 (case IM.find (strs, m1) of
908 | CNamed n => 908 NONE => c
909 (case IM.find (cons, n) of 909 | SOME m1x => CModProj (m1, ms' @ m1x :: ms, x))
910 NONE => c 910 | CNamed n =>
911 | SOME nx => CModProj (m1, ms', nx)) 911 (case IM.find (cons, n) of
912 | CApp (c1, c2) => CApp ((sgnS_con' arg (#1 c1), #2 c1), 912 NONE => c
913 (sgnS_con' arg (#1 c2), #2 c2)) 913 | SOME nx => CModProj (m1, ms', nx))
914 | _ => c 914 | _ => c}
915 915
916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn = 916 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
917 case sgn of 917 case sgn of
918 SgnProj (m1, ms, x) => 918 SgnProj (m1, ms, x) =>
919 (case IM.find (strs, m1) of 919 (case IM.find (strs, m1) of
1024 (case rule_in c of 1024 (case rule_in c of
1025 NONE => default () 1025 NONE => default ()
1026 | SOME (cn, nvs, cs, c) => 1026 | SOME (cn, nvs, cs, c) =>
1027 let 1027 let
1028 val loc = #2 c 1028 val loc = #2 c
1029 fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc) 1029 val globalize = sgnS_con' (m1, ms, fmap)
1030 1030
1031 val nc = 1031 val nc =
1032 case cn of 1032 case cn of
1033 ClNamed f => IM.find (newClasses, f) 1033 ClNamed f => IM.find (newClasses, f)
1034 | _ => NONE 1034 | _ => NONE