summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 15:54:05 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-02-24 15:54:05 -0500
commitd4452116d68b41b3c829d830f3fa9f2a275e36ec (patch)
tree8cf095234a22fcd203ed7252682e6db13796cf59
parenta52243a4a456ec4525c5e35351c458dcc4395aad (diff)
Folder generation for functors
Diffstat
-rw-r--r--demo/crud1.ur6
-rw-r--r--demo/crud2.ur4
-rw-r--r--demo/metaform1.ur1
-rw-r--r--demo/metaform2.ur1
-rw-r--r--src/elaborate.sml124
5 files changed, 63 insertions, 73 deletions
diff --git a/demo/crud1.ur b/demo/crud1.ur
index 65140035..3849e822 100644
--- a/demo/crud1.ur
+++ b/demo/crud1.ur
@@ -9,10 +9,4 @@ open Crud.Make(struct
B = Crud.string "B",
C = Crud.float "C",
D = Crud.bool "D"}
-
- val fl = Folder.cons [#A] [_] !
- (Folder.cons [#B] [_] !
- (Folder.cons [#C] [_] !
- (Folder.cons [#D] [_] !
- Folder.nil)))
end)
diff --git a/demo/crud2.ur b/demo/crud2.ur
index f7adf29b..1db376d4 100644
--- a/demo/crud2.ur
+++ b/demo/crud2.ur
@@ -31,8 +31,4 @@ open Crud.Make(struct
Inject = _
}
}
-
- val fl = Folder.cons [#Nam] [_] !
- (Folder.cons [#Ready] [_] !
- Folder.nil)
end)
diff --git a/demo/metaform1.ur b/demo/metaform1.ur
index 2f3356fa..c6a4664d 100644
--- a/demo/metaform1.ur
+++ b/demo/metaform1.ur
@@ -1,4 +1,3 @@
open Metaform.Make(struct
val names = {A = "Tic", B = "Tac", C = "Toe"}
- val fl = Folder.cons [#A] [()] ! (Folder.cons [#B] [()] ! (Folder.cons [#C] [()] ! Folder.nil))
end)
diff --git a/demo/metaform2.ur b/demo/metaform2.ur
index 87d40b18..430a42f0 100644
--- a/demo/metaform2.ur
+++ b/demo/metaform2.ur
@@ -1,6 +1,5 @@
structure MM = Metaform.Make(struct
val names = {X = "x", Y = "y"}
- val fl = Folder.cons [#X] [()] ! (Folder.cons [#Y] [()] ! Folder.nil)
end)
fun diversion () = return <xml><body>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5d4d9843..c55593b4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1057,10 +1057,18 @@
datatype constraint =
Disjoint of D.goal
| TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
- | Folder of E.env * L'.con * L'.exp option ref * ErrorMsg.span
val enD = map Disjoint
+ fun isClassOrFolder env cl =
+ E.isClass env cl
+ orelse case hnormCon env cl of
+ (L'.CKApp (cl, _), _) =>
+ (case hnormCon env cl of
+ (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r
+ | _ => false)
+ | _ => false
+
fun elabHead (env, denv) infer (e as (_, loc)) t =
let
fun unravel (t, e) =
@@ -1091,7 +1099,7 @@
val cl = hnormCon env cl
in
if infer <> L.TypesOnly then
- if E.isClass env cl then
+ if isClassOrFolder env cl then
let
val r = ref NONE
val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
@@ -1099,21 +1107,7 @@
(e, t, TypeClass (env, dom, r, loc) :: gs)
end
else
- case hnormCon env cl of
- (L'.CKApp (cl, _), _) =>
- (case hnormCon env cl of
- (L'.CModProj (top_n, [], "folder"), _) =>
- if top_n = !top_r then
- let
- val r = ref NONE
- val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
- in
- (e, t, Folder (env, x, r, loc) :: gs)
- end
- else
- default ()
- | _ => default ())
- | _ => default ()
+ default ()
else
default ()
end
@@ -2849,11 +2843,10 @@ fun wildifyStr env (str, sgn) =
in
case #1 t of
L'.CApp (f, _) =>
- if E.isClass env' f then
+ if isClassOrFolder env' f then
(neededC, constraints, SS.add (neededV, x))
else
default ()
-
| _ => default ()
end
@@ -2863,18 +2856,19 @@ fun wildifyStr env (str, sgn) =
end)
(SM.empty, [], SS.empty, env) sgis
- val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
- case d of
- L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
- handle NotFound =>
- needed)
- | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
- handle NotFound => needed)
- | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
- handle NotFound => needed)
- | L.DOpen _ => (SM.empty, SS.empty)
- | _ => needed)
- (neededC, neededV) ds
+ val (neededC, neededV) =
+ foldl (fn ((d, _), needed as (neededC, neededV)) =>
+ case d of
+ L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
+ handle NotFound =>
+ needed)
+ | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
+ handle NotFound => needed)
+ | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
+ handle NotFound => needed)
+ | L.DOpen _ => (SM.empty, SS.empty)
+ | _ => needed)
+ (neededC, neededV) ds
val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
case (decompileCon env' c1, decompileCon env' c2) of
@@ -3534,8 +3528,7 @@ fun elabFile basis topStr topSgn env file =
case E.resolveClass env c of
SOME e => r := SOME e
| NONE => expError env (Unresolvable (loc, c))
- end
- | Folder _ => raise Fail "Unresolved folder in top.ur") gs
+ end) gs
val () = subSgn env' topSgn' topSgn
@@ -3583,38 +3576,47 @@ fun elabFile basis topStr topSgn env file =
("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
| TypeClass (env, c, r, loc) =>
let
+ fun default () = expError env (Unresolvable (loc, c))
+
val c = normClassKey env c
in
case E.resolveClass env c of
SOME e => r := SOME e
- | NONE => expError env (Unresolvable (loc, c))
- end
- | Folder (env, c, r, loc) =>
- let
- val c = hnormCon env c
- in
- case #1 c of
- L'.CRecord (k, xcs) =>
- let
- val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
- val e = (L'.EKApp (e, k), loc)
-
- val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
- let
- val e = (L'.EModProj (top_n, ["Folder"], "cons"), loc)
- val e = (L'.EKApp (e, k), loc)
- val e = (L'.ECApp (e, (L'.CRecord (k, xcs), loc)), loc)
- val e = (L'.ECApp (e, x), loc)
- val e = (L'.ECApp (e, c), loc)
- val e = (L'.EApp (e, folder), loc)
- in
- (e, (x, c) :: xcs)
- end)
- (e, []) xcs
- in
- r := SOME folder
- end
- | _ => expError env (Unresolvable (loc, c))
+ | NONE =>
+ case #1 (hnormCon env c) of
+ L'.CApp (f, x) =>
+ (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
+ (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
+ (case #1 (hnormCon env f) of
+ L'.CModProj (top_n', [], "folder") =>
+ if top_n' = top_n then
+ let
+ val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
+ val e = (L'.EKApp (e, k), loc)
+
+ val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
+ let
+ val e = (L'.EModProj (top_n, ["Folder"],
+ "cons"), loc)
+ val e = (L'.EKApp (e, k), loc)
+ val e = (L'.ECApp (e,
+ (L'.CRecord (k, xcs),
+ loc)), loc)
+ val e = (L'.ECApp (e, x), loc)
+ val e = (L'.ECApp (e, c), loc)
+ val e = (L'.EApp (e, folder), loc)
+ in
+ (e, (x, c) :: xcs)
+ end)
+ (e, []) xcs
+ in
+ r := SOME folder
+ end
+ else
+ default ()
+ | _ => default ())
+ | _ => default ())
+ | _ => default ()
end) gs;
(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 18:58:20 +0000