Mercurial > urweb

comparison src/elab_env.sml @ 849:e571fb150a9f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix a bug in type class enrichment from substructures
author Adam Chlipala <adamc@hcoop.net>
date Tue, 16 Jun 2009 14:38:01 -0400
parents 7f871c03e3a1
children 6d9538ce94d8
comparison
equal deleted inserted replaced
848:e8594cfa3236 849:e571fb150a9f
1068 in 1068 in
1069 (SgnConst sgis, loc) 1069 (SgnConst sgis, loc)
1070 end 1070 end
1071 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" 1071 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
1072 1072
1073 fun manifest (m, ms, loc) =
1074 foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms
1075
1073 fun enrichClasses env classes (m1, ms) sgn = 1076 fun enrichClasses env classes (m1, ms) sgn =
1074 case #1 (hnormSgn env sgn) of 1077 case #1 (hnormSgn env sgn) of
1075 SgnConst sgis => 1078 SgnConst sgis =>
1076 let 1079 let
1077 val (classes, _, _, _) = 1080 val (classes, _, _, _) =
1087 1090
1088 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env) 1091 fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
1089 in 1092 in
1090 case #1 sgi of 1093 case #1 sgi of
1091 SgiStr (x, _, sgn) => 1094 SgiStr (x, _, sgn) =>
1092 (enrichClasses env classes (m1, ms @ [x]) sgn, 1095 let
1093 newClasses, 1096 val str = manifest (m1, ms, #2 sgi)
1094 sgiSeek (#1 sgi, fmap), 1097 val sgn' = sgnSubSgn (str, fmap) sgn
1095 env) 1098 in
1099 (enrichClasses env classes (m1, ms @ [x]) sgn',
1100 newClasses,
1101 sgiSeek (#1 sgi, fmap),
1102 env)
1103 end
1096 | SgiSgn (x, n, sgn) => 1104 | SgiSgn (x, n, sgn) =>
1097 (classes, 1105 (classes,
1098 newClasses, 1106 newClasses,
1099 fmap, 1107 fmap,
1100 pushSgnNamedAs env x n sgn) 1108 pushSgnNamedAs env x n sgn)