summaryrefslogtreecommitdiff
path: root/src/elab_util.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-29 17:30:34 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-29 17:30:34 -0400
commit210946aa1857eebde9b16a782cf293a83d2be008 (patch)
tree0304d9c5614cecb6cec0fe974de29dc18a71ad15 /src/elab_util.sml
parent994008d519cd6a065e00d3e5e6b36434eef8b7dd (diff)
Shorter, more focused error messages about undetermined unification variables
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r--src/elab_util.sml26
1 files changed, 26 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index fd8163c2..bf0185b1 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -1235,6 +1235,32 @@ and maxNameSgi (sgi, _) =
| SgiConstraint _ => 0
| SgiClassAbs (_, n, _) => n
| SgiClass (_, n, _, _) => n
+
+fun findDecl pred file =
+ let
+ fun decl d =
+ let
+ val r = case #1 d of
+ DStr (_, _, _, s) => str s
+ | _ => NONE
+ in
+ case r of
+ NONE => if pred d then SOME d else NONE
+ | _ => r
+ end
+
+ and str s =
+ case #1 s of
+ StrConst ds => ListUtil.search decl ds
+ | StrFun (_, _, _, _, s) => str s
+ | StrApp (s1, s2) =>
+ (case str s1 of
+ NONE => str s2
+ | r => r)
+ | _ => NONE
+ in
+ ListUtil.search decl file
+ end
end