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.sml44
1 files changed, 37 insertions, 7 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 4c27c98d..897f481d 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -291,6 +291,7 @@ fun declBinds env (d, _) =
| DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
| DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
| DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+ | DConstraint _ => env
fun sgiBinds env (sgi, _) =
case sgi of
@@ -299,6 +300,7 @@ fun sgiBinds env (sgi, _) =
| SgiVal (x, n, t) => pushENamedAs env x n t
| SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
| SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
+ | SgiConstraint _ => env
fun sgnSeek f sgis =
let
@@ -308,13 +310,14 @@ fun sgnSeek f sgis =
| (sgi, _) :: sgis =>
case f sgi of
SOME v => SOME (v, (sgns, strs, cons))
- | NONE =>
- case sgi of
- SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
- | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
- | SgiVal _ => seek (sgis, sgns, strs, cons)
- | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
- | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
+ | NONE =>
+ case sgi of
+ SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+ | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
+ | SgiVal _ => seek (sgis, sgns, strs, cons)
+ | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
+ | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
+ | SgiConstraint _ => seek (sgis, sgns, strs, cons)
in
seek (sgis, IM.empty, IM.empty, IM.empty)
end
@@ -461,5 +464,32 @@ fun projectVal env {sgn, str, field} =
| SgnError => SOME (CError, ErrorMsg.dummySpan)
| _ => NONE
+fun sgnSeekConstraints (str, sgis) =
+ let
+ fun seek (sgis, sgns, strs, cons, acc) =
+ case sgis of
+ [] => acc
+ | (sgi, _) :: sgis =>
+ case sgi of
+ SgiConstraint (c1, c2) =>
+ let
+ val sub = sgnSubCon (str, (sgns, strs, cons))
+ in
+ seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
+ end
+ | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+ | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+ | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
+ | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
+ | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
+ in
+ seek (sgis, IM.empty, IM.empty, IM.empty, [])
+ end
+
+fun projectConstraints env {sgn, str} =
+ case #1 (hnormSgn env sgn) of
+ SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
+ | SgnError => SOME []
+ | _ => NONE
end