summaryrefslogtreecommitdiff
path: root/src/disjoint.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 15:33:20 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-21 15:33:20 -0500
commitc40cb1851bc27f0a0a99648be21dacb821b65ed9 (patch)
tree6ec268a6e7aaa927f41c76e354e78ca55585f69a /src/disjoint.sml
parent9f20d9299eab7caab6421860b6a54f831af73921 (diff)
"Hello world" compiles, after replacing type-level fold with map
Diffstat (limited to 'src/disjoint.sml')
-rw-r--r--src/disjoint.sml33
1 files changed, 2 insertions, 31 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index c6a8d50f..81023972 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -213,37 +213,8 @@ fun decomposeRow (env, denv) c =
("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
case #1 (#1 (hnormCon (env, denv) c)) of
CApp (
- (CApp (
- (CApp ((CFold (dom, ran), _), f), _),
- i), _),
- r) =>
- let
- val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
- val (env', v) = E.pushCNamed env' "v" dom NONE
- val (env', st) = E.pushCNamed env' "st" ran NONE
-
- val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
- (CUnit, loc))]), loc),
- (CNamed st, loc))
-
- val c' = (CApp (f, (CNamed nm, loc)), loc)
- val c' = (CApp (c', (CNamed v, loc)), loc)
- val c' = (CApp (c', (CNamed st, loc)), loc)
- val (ps, gs'') = decomposeRow (env', denv') c'
-
- fun covered p =
- case p of
- Unknown _ => false
- | Piece p =>
- case p of
- (NameN n, []) => n = nm
- | (RowN n, []) => n = st
- | _ => false
-
- val ps = List.filter (not o covered) ps
- in
- decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
- end
+ (CApp ((CMap _, _), _), _),
+ r) => decomposeRow' (r, (acc, gs))
| _ => default ()
end
in