summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml19
1 files changed, 19 insertions, 0 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 5b716730..720b19da 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -570,6 +570,25 @@ fun projectDatatype env {sgn, str, field} =
| SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
| _ => NONE
+fun projectConstructor env {sgn, str, field} =
+ case #1 (hnormSgn env sgn) of
+ SgnConst sgis =>
+ let
+ fun consider (n, xncs) =
+ ListUtil.search (fn (x, n', to) =>
+ if x <> field then
+ NONE
+ else
+ SOME (n', to, (CNamed n, #2 str))) xncs
+ in
+ case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs)
+ | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs)
+ | _ => NONE) sgis of
+ NONE => NONE
+ | SOME ((n, to, t), subs) => SOME (n, Option.map (sgnSubCon (str, subs)) to, sgnSubCon (str, subs) t)
+ end
+ | _ => NONE
+
fun projectVal env {sgn, str, field} =
case #1 (hnormSgn env sgn) of
SgnConst sgis =>