Mercurial > urweb

comparison src/elab_env.sml @ 677:81573f62d6c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Enforce termination of type class instances
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 15:54:04 -0400
parents 43430b7190f4
children f0224c7f12bb
comparison
equal deleted inserted replaced
676:e0c186464612 677:81573f62d6c3
180 join (Int.compare (m1, m2), 180 join (Int.compare (m1, m2),
181 fn () => join (joinL String.compare (ms1, ms2), 181 fn () => join (joinL String.compare (ms1, ms2),
182 fn () => String.compare (x1, x2))) 182 fn () => String.compare (x1, x2)))
183 end 183 end
184 184
185 structure CS = BinarySetFn(CK)
185 structure CM = BinaryMapFn(CK) 186 structure CM = BinaryMapFn(CK)
186 187
187 datatype class_key = 188 datatype class_key =
188 CkNamed of int 189 CkNamed of int
189 | CkRel of int 190 | CkRel of int
695 let 696 let
696 fun clauses (c, hyps) = 697 fun clauses (c, hyps) =
697 case #1 c of 698 case #1 c of
698 TFun (hyp, c) => 699 TFun (hyp, c) =>
699 (case class_pair_in hyp of 700 (case class_pair_in hyp of
700 NONE => NONE 701 SOME (p as (_, CkRel _)) => clauses (c, p :: hyps)
701 | SOME p => clauses (c, p :: hyps)) 702 | _ => NONE)
702 | _ => 703 | _ =>
703 case class_pair_in c of 704 case class_pair_in c of
704 NONE => NONE 705 NONE => NONE
705 | SOME (cn, ck) => 706 | SOME (cn, ck) =>
706 let 707 let
728 (SOME f1, SOME f2) => SOME (f2, Inclusion f1) 729 (SOME f1, SOME f2) => SOME (f2, Inclusion f1)
729 | _ => NONE) 730 | _ => NONE)
730 | _ => quantifiers (c, 0) 731 | _ => quantifiers (c, 0)
731 end 732 end
732 733
734 fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) =
735 let
736 fun search (f, fs) =
737 if f = init then
738 NONE
739 else if CS.member (fs, f) then
740 SOME fs
741 else
742 let
743 val fs = CS.add (fs, f)
744 in
745 case CM.find (classes, f) of
746 NONE => SOME fs
747 | SOME {inclusions = fs', ...} =>
748 CM.foldli (fn (f', _, fs) =>
749 case fs of
750 NONE => NONE
751 | SOME fs => search (f', fs)) (SOME fs) fs'
752 end
753 in
754 case search (f, CS.empty) of
755 SOME _ => CM.insert (inclusions, f, e)
756 | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle";
757 inclusions)
758 end
759
733 fun pushENamedAs (env : env) x n t = 760 fun pushENamedAs (env : env) x n t =
734 let 761 let
735 val classes = #classes env 762 val classes = #classes env
736 val classes = case rule_in t of 763 val classes = case rule_in t of
737 NONE => classes 764 NONE => classes
747 Normal (nvars, hyps, x) => 774 Normal (nvars, hyps, x) =>
748 {ground = KM.insert (#ground class, (x, nvars), (hyps, e)), 775 {ground = KM.insert (#ground class, (x, nvars), (hyps, e)),
749 inclusions = #inclusions class} 776 inclusions = #inclusions class}
750 | Inclusion f' => 777 | Inclusion f' =>
751 {ground = #ground class, 778 {ground = #ground class,
752 inclusions = CM.insert (#inclusions class, f', e)} 779 inclusions = inclusion (classes, f, #inclusions class, f', e)}
753 in 780 in
754 CM.insert (classes, f, class) 781 CM.insert (classes, f, class)
755 end 782 end
756 in 783 in
757 {renameK = #renameK env, 784 {renameK = #renameK env,
1111 (globalizeN n, 1138 (globalizeN n,
1112 globalize k)) hyps, e)), 1139 globalize k)) hyps, e)),
1113 inclusions = #inclusions class} 1140 inclusions = #inclusions class}
1114 | Inclusion f' => 1141 | Inclusion f' =>
1115 {ground = #ground class, 1142 {ground = #ground class,
1116 inclusions = CM.insert (#inclusions class, 1143 inclusions = inclusion (classes, cn,
1144 #inclusions class,
1117 globalizeN f', e)} 1145 globalizeN f', e)}
1118 in 1146 in
1119 CM.insert (classes, cn, class) 1147 CM.insert (classes, cn, class)
1120 end 1148 end
1121 in 1149 in
1144 (globalizeN n, 1172 (globalizeN n,
1145 globalize k)) hyps, e)), 1173 globalize k)) hyps, e)),
1146 inclusions = #inclusions class} 1174 inclusions = #inclusions class}
1147 | Inclusion f' => 1175 | Inclusion f' =>
1148 {ground = #ground class, 1176 {ground = #ground class,
1149 inclusions = CM.insert (#inclusions class, 1177 inclusions = inclusion (classes, cn,
1178 #inclusions class,
1150 globalizeN f', e)} 1179 globalizeN f', e)}
1151 in 1180 in
1152 CM.insert (classes, cn, class) 1181 CM.insert (classes, cn, class)
1153 end 1182 end
1154 in 1183 in