summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_err.sml25
-rw-r--r--src/elab_ops.sig1
-rw-r--r--src/elab_ops.sml175
-rw-r--r--tests/league.ur7
4 files changed, 192 insertions, 16 deletions
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 2bf059e6..1951d971 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -36,20 +36,6 @@ structure U = ElabUtil
open Print
structure P = ElabPrint
-val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
- con = fn env => fn c =>
- let
- val c = (c, ErrorMsg.dummySpan)
- val c' = ElabOps.hnormCon env c
- in
- (*prefaces "simpl" [("c", P.p_con env c),
- ("c'", P.p_con env c')];*)
- #1 c'
- end,
- bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
- | (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
- | (env, _) => env}
-
val p_kind = P.p_kind
datatype kind_error =
@@ -80,7 +66,7 @@ fun kunifyError env err =
[("Kind 1", p_kind env k1),
("Kind 2", p_kind env k2)]
-fun p_con env c = P.p_con env (simplCon env c)
+fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
datatype con_error =
UnboundCon of ErrorMsg.span * string
@@ -195,7 +181,14 @@ datatype exp_error =
| OutOfContext of ErrorMsg.span * (exp * con) option
| IllegalRec of string * exp
-val p_exp = P.p_exp
+val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
+ con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
+ exp = fn _ => fn e => e,
+ bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
+ | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
+ | (env, _) => env}
+
+fun p_exp env e = P.p_exp env (simplExp env e)
val p_pat = P.p_pat
fun expError env err =
diff --git a/src/elab_ops.sig b/src/elab_ops.sig
index ed4c7d68..97e4b602 100644
--- a/src/elab_ops.sig
+++ b/src/elab_ops.sig
@@ -40,6 +40,7 @@ signature ELAB_OPS = sig
val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
val hnormCon : ElabEnv.env -> Elab.con -> Elab.con
+ val reduceCon : ElabEnv.env -> Elab.con -> Elab.con
val identity : int ref
val distribute : int ref
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index dc9f69a4..dbefbe7d 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -324,4 +324,179 @@ fun hnormCon env (cAll as (c, loc)) =
| _ => cAll
+fun reduceCon env (cAll as (c, loc)) =
+ case c of
+ TFun (c1, c2) => (TFun (reduceCon env c1, reduceCon env c2), loc)
+ | TCFun (exp, x, k, c) => (TCFun (exp, x, k, reduceCon env c), loc)
+ | TRecord c => (TRecord (reduceCon env c), loc)
+ | TDisjoint (c1, c2, c3) => (TDisjoint (reduceCon env c1, reduceCon env c2, reduceCon env c3), loc)
+
+ | CRel _ => cAll
+ | CNamed xn =>
+ (case E.lookupCNamed env xn of
+ (_, _, SOME c') => reduceCon env c'
+ | _ => cAll)
+ | CModProj _ => cAll
+ | CApp (c1, c2) =>
+ let
+ val c1 = reduceCon env c1
+ val c2 = reduceCon env c2
+ fun default () = (CApp (c1, c2), loc)
+ in
+ case #1 c1 of
+ CAbs (x, k, cb) =>
+ ((reduceCon env (subConInCon (0, c2) cb))
+ handle SynUnif => default ())
+ | CApp (c', f) =>
+ let
+ val c' = reduceCon env c'
+ val f = reduceCon env f
+ in
+ case #1 c' of
+ CMap (ks as (k1, k2)) =>
+ (case #1 c2 of
+ CRecord (_, []) => (CRecord (k2, []), loc)
+ | CRecord (_, (x, c) :: rest) =>
+ reduceCon env
+ (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
+ | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+ let
+ val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+ in
+ reduceCon env
+ (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, rest''), loc)), loc)
+ end
+ | _ =>
+ let
+ fun unconstraint c =
+ case reduceCon env c of
+ (TDisjoint (_, _, c), _) => unconstraint c
+ | c => c
+
+ fun inc r = r := !r + 1
+
+ fun tryDistributivity () =
+ case reduceCon env c2 of
+ (CConcat (c1, c2), _) =>
+ let
+ val c = (CMap ks, loc)
+ val c = (CApp (c, f), loc)
+
+ val c1 = (CApp (c, c1), loc)
+ val c2 = (CApp (c, c2), loc)
+ val c = (CConcat (c1, c2), loc)
+ in
+ inc distribute;
+ reduceCon env c
+ end
+ | _ => default ()
+
+ fun tryFusion () =
+ case #1 (reduceCon env c2) of
+ CApp (f', r') =>
+ (case #1 (reduceCon env f') of
+ CApp (f', inner_f) =>
+ (case #1 (reduceCon env f') of
+ CMap (dom, _) =>
+ let
+ val inner_f = liftConInCon 0 inner_f
+ val f = liftConInCon 0 f
+
+ val f' = (CApp (inner_f, (CRel 0, loc)), loc)
+ val f' = (CApp (f, f'), loc)
+ val f' = (CAbs ("v", dom, f'), loc)
+
+ val c = (CMap (dom, k2), loc)
+ val c = (CApp (c, f'), loc)
+ val c = (CApp (c, r'), loc)
+ in
+ inc fuse;
+ reduceCon env c
+ end
+ | _ => tryDistributivity ())
+ | _ => tryDistributivity ())
+ | _ => tryDistributivity ()
+
+ fun tryIdentity () =
+ let
+ fun cunif () =
+ let
+ val r = ref (Unknown (fn _ => true))
+ in
+ (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
+ end
+
+ val (vR, v) = cunif ()
+
+ val c = (CApp (f, v), loc)
+ in
+ case unconstraint c of
+ (CUnif (_, _, _, _, vR'), _) =>
+ if vR' = vR then
+ (inc identity;
+ reduceCon env c2)
+ else
+ tryFusion ()
+ | _ => tryFusion ()
+ end
+ in
+ tryIdentity ()
+ end)
+ | _ => default ()
+ end
+ | _ => default ()
+ end
+ | CAbs (x, k, b) =>
+ let
+ val b = reduceCon (E.pushCRel env x k) b
+ fun default () = (CAbs (x, k, b), loc)
+ in
+ case #1 b of
+ CApp (f, (CRel 0, _)) =>
+ if occurs f then
+ default ()
+ else
+ reduceCon env (subConInCon (0, (CUnit, loc)) f)
+ | _ => default ()
+ end
+
+ | CKAbs (x, b) => (CKAbs (x, reduceCon (E.pushKRel env x) b), loc)
+ | CKApp (c1, k) =>
+ (case reduceCon env c1 of
+ (CKAbs (_, body), _) => reduceCon env (subKindInCon (0, k) body)
+ | c1 => (CKApp (c1, k), loc))
+ | TKFun (x, c) => (TKFun (x, reduceCon env c), loc)
+
+ | CName _ => cAll
+
+ | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (reduceCon env x, reduceCon env c)) xcs), loc)
+ | CConcat (c1, c2) =>
+ let
+ val c1 = reduceCon env c1
+ val c2 = reduceCon env c2
+ in
+ case (c1, c2) of
+ ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => (CRecord (k, xcs1 @ xcs2), loc)
+ | ((CRecord (_, []), _), _) => c2
+ | ((CConcat (c11, c12), loc), _) => reduceCon env (CConcat (c11, (CConcat (c12, c2), loc)), loc)
+ | (_, (CRecord (_, []), _)) => c1
+ | _ => (CConcat (c1, c2), loc)
+ end
+ | CMap _ => cAll
+
+ | CUnit => cAll
+
+ | CTuple cs => (CTuple (map (reduceCon env) cs), loc)
+ | CProj (c, n) =>
+ (case reduceCon env c of
+ (CTuple cs, _) => reduceCon env (List.nth (cs, n - 1))
+ | c => (CProj (c, n), loc))
+
+ | CError => cAll
+
+ | CUnif (nl, _, _, _, ref (Known c)) => reduceCon env (E.mliftConInCon nl c)
+ | CUnif _ => cAll
+
end
diff --git a/tests/league.ur b/tests/league.ur
new file mode 100644
index 00000000..7edd5f42
--- /dev/null
+++ b/tests/league.ur
@@ -0,0 +1,7 @@
+type team = string
+type league = string
+
+table team : { Id : team,
+ League : league }
+
+val foo:int = queryL(SELECT * FROM team)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 21:14:04 +0000