Mercurial > urweb
comparison src/elab_env.sml @ 721:9864b64b1700
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 |