summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/ur/top.ur171
-rw-r--r--lib/ur/top.urs112
-rw-r--r--src/core.sml1
-rw-r--r--src/core_print.sml1
-rw-r--r--src/core_util.sml8
-rw-r--r--src/corify.sml1
-rw-r--r--src/elab.sml11
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml130
-rw-r--r--src/elab_err.sig7
-rw-r--r--src/elab_err.sml61
-rw-r--r--src/elab_ops.sig6
-rw-r--r--src/elab_ops.sml69
-rw-r--r--src/elab_print.sig2
-rw-r--r--src/elab_print.sml95
-rw-r--r--src/elab_util.sig38
-rw-r--r--src/elab_util.sml154
-rw-r--r--src/elaborate.sml241
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_print.sml1
-rw-r--r--src/expl_util.sml4
-rw-r--r--src/explify.sml2
-rw-r--r--src/monoize.sml1
-rw-r--r--src/reduce.sml16
-rw-r--r--src/reduce_local.sml2
-rw-r--r--src/source.sml9
-rw-r--r--src/source_print.sml26
-rw-r--r--src/termination.sml9
-rw-r--r--src/unnest.sml18
-rw-r--r--src/urweb.grm23
-rw-r--r--src/urweb.lex3
31 files changed, 736 insertions, 491 deletions
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index 58e99f3c..9016fd27 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -1,3 +1,12 @@
+(** Row folding *)
+
+con folder = K ==> fn r :: {K} =>
+ tf :: ({K} -> Type)
+ -> (nm :: Name -> v :: K -> r :: {K} -> tf r
+ -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+ -> tf [] -> tf r
+
+
fun not b = if b then False else True
con idT (t :: Type) = t
@@ -27,23 +36,23 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
(f : nm :: Name -> rest :: {Unit}
-> fn [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) =
+ (i : tr []) (r ::: {Unit}) (fold : folder r)=
fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
- (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
- [[nm] ~ rest] r =>
- f [nm] [rest] r.nm (acc (r -- nm)))
- (fn _ => i)
+ (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+ [[nm] ~ rest] r =>
+ f [nm] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
(f : nm :: Name -> rest :: {Unit}
-> fn [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) =
+ (i : tr []) (r ::: {Unit}) (fold : folder r) =
fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
- (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
- [[nm] ~ rest] r1 r2 =>
- f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
- (fn _ _ => i)
+ (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+ [[nm] ~ rest] r1 r2 =>
+ f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
(f : nm :: Name -> rest :: {Unit}
@@ -54,134 +63,46 @@ fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
<xml>{f [nm] [rest] v1 v2}{acc}</xml>)
<xml/>
-fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
- (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldR K (tf :: K -> Type) (tr :: {K} -> Type)
+ (f : nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {Type} => $(map tf r) -> tr r]
- (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest)
+ (i : tr []) (r ::: {K}) (fold : folder r) =
+ fold [fn r :: {K} => $(map tf r) -> tr r]
+ (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest)
[[nm] ~ rest] r =>
f [nm] [t] [rest] r.nm (acc (r -- nm)))
(fn _ => i)
-fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
- (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- (acc : _ -> tr rest) [[nm] ~ rest] r =>
- f [nm] [t] [rest] r.nm (acc (r -- nm)))
- (fn _ => i)
-
-fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
- (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r]
- (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
- (acc : _ -> tr rest) [[nm] ~ rest] r =>
- f [nm] [t] [rest] r.nm (acc (r -- nm)))
- (fn _ => i)
-
-fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
- (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type)
+ (f : nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r]
- (fn (nm :: Name) (t :: Type) (rest :: {Type})
- (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
- f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
- (fn _ _ => i)
-
-fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
- (tr :: {(Type * Type)} -> Type)
- (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
- f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
- (fn _ _ => i)
-
-fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
- (tr :: {(Type * Type * Type)} -> Type)
- (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) =
- fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r]
- (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
- (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
- f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
- (fn _ _ => i)
-
-fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
- (f : nm :: Name -> t :: Type -> rest :: {Type}
+ (i : tr []) (r ::: {K}) (fold : folder r) =
+ fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: K) (rest :: {K})
+ (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
+ f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldRX K (tf :: K -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
tf t -> xml ctx [] []) =
- foldTR [tf] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc =>
- <xml>{f [nm] [t] [rest] r}{acc}</xml>)
- <xml/>
-
-fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
- (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> xml ctx [] []) =
- foldT2R [tf] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] r acc =>
- <xml>{f [nm] [t] [rest] r}{acc}</xml>)
- <xml/>
-
-fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
- (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> xml ctx [] []) =
- foldT3R [tf] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
- [[nm] ~ rest] r acc =>
- <xml>{f [nm] [t] [rest] r}{acc}</xml>)
- <xml/>
+ foldR [tf] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+ <xml/>
-fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
- (f : nm :: Name -> t :: Type -> rest :: {Type}
+fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
tf1 t -> tf2 t -> xml ctx [] []) =
- foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest]
- r1 r2 acc =>
- <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
- <xml/>
-
-fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
- (ctx :: {Unit})
- (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> xml ctx [] []) =
- foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
- [[nm] ~ rest] r1 r2 acc =>
- <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
- <xml/>
-
-fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
- (ctx :: {Unit})
- (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> xml ctx [] []) =
- foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
- (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
- [[nm] ~ rest] r1 r2 acc =>
- <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
- <xml/>
+ foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest]
+ r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+ <xml/>
fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
(q : sql_query tables exps) [tables ~ exps]
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 49aad50c..d891c80d 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -1,3 +1,12 @@
+(** Row folding *)
+
+con folder = K ==> fn r :: {K} =>
+ tf :: ({K} -> Type)
+ -> (nm :: Name -> v :: K -> r :: {K} -> tf r
+ -> fn [[nm] ~ r] => tf ([nm = v] ++ r))
+ -> tf [] -> tf r
+
+
val not : bool -> bool
con idT = fn t :: Type => t
@@ -25,103 +34,46 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> fn [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> fn [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
-> (nm :: Name -> rest :: {Unit}
-> fn [[nm] ~ rest] =>
tf1 -> tf2 -> xml ctx [] [])
- -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+ -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
-val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
- -> (nm :: Name -> t :: Type -> rest :: {Type}
+val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {Type} -> $(map tf r) -> tr r
+ -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
-val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
- -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r
+val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
+ -> tr :: ({K} -> Type)
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr []
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
-val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
- -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
+val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] [])
+ -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
-val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
- -> tr :: ({Type} -> Type)
- -> (nm :: Name -> t :: Type -> rest :: {Type}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr []
- -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
-
-val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
- -> tr :: ({(Type * Type)} -> Type)
- -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {(Type * Type)}
- -> $(map tf1 r) -> $(map tf2 r) -> tr r
-
-val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
- -> tr :: ({(Type * Type * Type)} -> Type)
- -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {(Type * Type * Type)}
- -> $(map tf1 r) -> $(map tf2 r) -> tr r
-
-val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
- -> (nm :: Name -> t :: Type -> rest :: {Type}
+val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: K -> rest :: {K}
-> fn [[nm] ~ rest] =>
- tf t -> xml ctx [] [])
- -> r :: {Type} -> $(map tf r) -> xml ctx [] []
-
-val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
- -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> xml ctx [] [])
- -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
-
-val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
- -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf t -> xml ctx [] [])
- -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
-
-val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
- -> (nm :: Name -> t :: Type -> rest :: {Type}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> xml ctx [] [])
- -> r :: {Type}
- -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
-
-val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
- -> ctx :: {Unit}
- -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> xml ctx [] [])
- -> r :: {(Type * Type)}
- -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
-
-
-val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
- -> ctx :: {Unit}
- -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
- -> fn [[nm] ~ rest] =>
- tf1 t -> tf2 t -> xml ctx [] [])
- -> r :: {(Type * Type * Type)}
- -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
+ tf1 t -> tf2 t -> xml ctx [] [])
+ -> r ::: {K} -> folder r
+ -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
-> sql_query tables exps
diff --git a/src/core.sml b/src/core.sml
index d7a57493..a28d93dd 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -96,7 +96,6 @@ datatype exp' =
| EConcat of exp * con * exp * con
| ECut of exp * con * { field : con, rest : con }
| ECutMulti of exp * con * { rest : con }
- | EFold of kind
| ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/core_print.sml b/src/core_print.sml
index db8c3907..504773ab 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -342,7 +342,6 @@ fun p_exp' par env (e, _) =
string "---",
space,
p_con' true env c])
- | EFold _ => string "fold"
| ECase (e, pes, {disc, result}) =>
parenIf par (box [string "case",
diff --git a/src/core_util.sml b/src/core_util.sml
index e76da387..d5f8dd05 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -454,10 +454,6 @@ fun compare ((e1, _), (e2, _)) =
| (ECutMulti _, _) => LESS
| (_, ECutMulti _) => GREATER
- | (EFold _, EFold _) => EQUAL
- | (EFold _, _) => LESS
- | (_, EFold _) => GREATER
-
| (ECase (e1, pes1, _), ECase (e2, pes2, _)) =>
join (compare (e1, e2),
fn () => joinL (fn ((p1, e1), (p2, e2)) =>
@@ -609,10 +605,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.map2 (mfc ctx rest,
fn rest' =>
(ECutMulti (e', c', {rest = rest'}), loc))))
- | EFold k =>
- S.map2 (mfk k,
- fn k' =>
- (EFold k', loc))
| ECase (e, pes, {disc, result}) =>
S.bind2 (mfe ctx e,
diff --git a/src/corify.sml b/src/corify.sml
index c464e5a5..802baf66 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -592,7 +592,6 @@ fun corifyExp st (e, loc) =
{field = corifyCon st field, rest = corifyCon st rest}), loc)
| L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c,
{rest = corifyCon st rest}), loc)
- | L.EFold k => (L'.EFold (corifyKind k), loc)
| L.ECase (e, pes, {disc, result}) =>
(L'.ECase (corifyExp st e,
diff --git a/src/elab.sml b/src/elab.sml
index ec8a910a..9ec3793e 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -40,6 +40,9 @@ datatype kind' =
| KError
| KUnif of ErrorMsg.span * string * kind option ref
+ | KRel of int
+ | KFun of string * kind
+
withtype kind = kind' located
datatype explicitness =
@@ -62,6 +65,10 @@ datatype con' =
| CAbs of string * kind * con
| CDisjoint of auto_instantiate * con * con * con
+ | CKAbs of string * con
+ | CKApp of con * kind
+ | TKFun of string * con
+
| CName of string
| CRecord of kind * (con * con) list
@@ -106,12 +113,14 @@ datatype exp' =
| ECApp of exp * con
| ECAbs of explicitness * string * kind * exp
+ | EKAbs of string * exp
+ | EKApp of exp * kind
+
| ERecord of (con * exp * con) list
| EField of exp * con * { field : con, rest : con }
| EConcat of exp * con * exp * con
| ECut of exp * con * { field : con, rest : con }
| ECutMulti of exp * con * { rest : con }
- | EFold of kind
| ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 0b436106..10d11e3b 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -47,6 +47,10 @@ signature ELAB_ENV = sig
| Rel of int * 'a
| Named of int * 'a
+ val pushKRel : env -> string -> env
+ val lookupKRel : env -> int -> string
+ val lookupK : env -> string -> int option
+
val pushCRel : env -> string -> Elab.kind -> env
val lookupCRel : env -> int -> string * Elab.kind
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 53c934dd..083e7d55 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -45,8 +45,32 @@ exception UnboundNamed of int
exception SynUnif
+val liftKindInKind =
+ U.Kind.mapB {kind = fn bound => fn k =>
+ case k of
+ KRel xn =>
+ if xn < bound then
+ k
+ else
+ KRel (xn + 1)
+ | _ => k,
+ bind = fn (bound, _) => bound + 1}
+
+val liftKindInCon =
+ U.Con.mapB {kind = fn bound => fn k =>
+ case k of
+ KRel xn =>
+ if xn < bound then
+ k
+ else
+ KRel (xn + 1)
+ | _ => k,
+ con = fn _ => fn c => c,
+ bind = fn (bound, U.Con.RelK _) => bound + 1
+ | (bound, _) => bound}
+
val liftConInCon =
- U.Con.mapB {kind = fn k => k,
+ U.Con.mapB {kind = fn _ => fn k => k,
con = fn bound => fn c =>
case c of
CRel xn =>
@@ -56,13 +80,27 @@ val liftConInCon =
CRel (xn + 1)
(*| CUnif _ => raise SynUnif*)
| _ => c,
- bind = fn (bound, U.Con.Rel _) => bound + 1
+ bind = fn (bound, U.Con.RelC _) => bound + 1
| (bound, _) => bound}
val lift = liftConInCon 0
+val liftKindInExp =
+ U.Exp.mapB {kind = fn bound => fn k =>
+ case k of
+ KRel xn =>
+ if xn < bound then
+ k
+ else
+ KRel (xn + 1)
+ | _ => k,
+ con = fn _ => fn c => c,
+ exp = fn _ => fn e => e,
+ bind = fn (bound, U.Exp.RelK _) => bound + 1
+ | (bound, _) => bound}
+
val liftConInExp =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn bound => fn c =>
case c of
CRel xn =>
@@ -76,7 +114,7 @@ val liftConInExp =
| (bound, _) => bound}
val liftExpInExp =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn _ => fn c => c,
exp = fn bound => fn e =>
case e of
@@ -93,7 +131,7 @@ val liftExpInExp =
val liftExp = liftExpInExp 0
val subExpInExp =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn _ => fn c => c,
exp = fn (xn, rep) => fn e =>
case e of
@@ -203,6 +241,9 @@ fun printClasses cs = (print "Classes:\n";
print "\n")) cs)
type env = {
+ renameK : int SM.map,
+ relK : string list,
+
renameC : kind var' SM.map,
relC : (string * kind) list,
namedC : (string * kind * con option) IM.map,
@@ -234,6 +275,9 @@ fun newNamed () =
end
val empty = {
+ renameK = SM.empty,
+ relK = [],
+
renameC = SM.empty,
relC = [],
namedC = IM.empty,
@@ -261,12 +305,51 @@ fun liftClassKey ck =
| CkProj _ => ck
| CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2)
+fun pushKRel (env : env) x =
+ let
+ val renameK = SM.map (fn n => n+1) (#renameK env)
+ in
+ {renameK = SM.insert (renameK, x, 0),
+ relK = x :: #relK env,
+
+ renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
+ | x => x) (#renameC env),
+ relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
+ namedC = #namedC env,
+
+ datatypes = #datatypes env,
+ constructors = #constructors env,
+
+ classes = #classes env,
+
+ renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
+ | Named' (n, c) => Named' (n, c)) (#renameE env),
+ relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
+ namedE = #namedE env,
+
+ renameSgn = #renameSgn env,
+ sgn = #sgn env,
+
+ renameStr = #renameStr env,
+ str = #str env
+ }
+ end
+
+fun lookupKRel (env : env) n =
+ (List.nth (#relK env, n))
+ handle Subscript => raise UnboundRel n
+
+fun lookupK (env : env) x = SM.find (#renameK env, x)
+
fun pushCRel (env : env) x k =
let
val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
| x => x) (#renameC env)
in
- {renameC = SM.insert (renameC, x, Rel' (0, k)),
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = SM.insert (renameC, x, Rel' (0, k)),
relC = (x, k) :: #relC env,
namedC = #namedC env,
@@ -298,7 +381,10 @@ fun lookupCRel (env : env) n =
handle Subscript => raise UnboundRel n
fun pushCNamedAs (env : env) x n k co =
- {renameC = SM.insert (#renameC env, x, Named' (n, k)),
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = SM.insert (#renameC env, x, Named' (n, k)),
relC = #relC env,
namedC = IM.insert (#namedC env, n, (x, k, co)),
@@ -340,7 +426,10 @@ fun pushDatatype (env : env) n xs xncs =
let
val dk = U.classifyDatatype xncs
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -380,7 +469,10 @@ fun datatypeArgs (xs, _) = xs
fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
fun pushClass (env : env) n =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -468,7 +560,10 @@ fun pushERel (env : env) x t =
CM.insert (classes, f, class)
end
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -509,7 +604,10 @@ fun pushENamedAs (env : env) x n t =
CM.insert (classes, f, class)
end
in
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -552,7 +650,10 @@ fun lookupE (env : env) x =
| SOME (Named' x) => Named x
fun pushSgnNamedAs (env : env) x n sgis =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
@@ -868,7 +969,10 @@ fun enrichClasses env classes (m1, ms) sgn =
| _ => classes
fun pushStrNamedAs (env : env) x n sgn =
- {renameC = #renameC env,
+ {renameK = #renameK env,
+ relK = #relK env,
+
+ renameC = #renameC env,
relC = #relC env,
namedC = #namedC env,
diff --git a/src/elab_err.sig b/src/elab_err.sig
index d757572f..3b14406b 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -27,11 +27,16 @@
signature ELAB_ERR = sig
+ datatype kind_error =
+ UnboundKind of ErrorMsg.span * string
+
+ val kindError : ElabEnv.env -> kind_error -> unit
+
datatype kunify_error =
KOccursCheckFailed of Elab.kind * Elab.kind
| KIncompatible of Elab.kind * Elab.kind
- val kunifyError : kunify_error -> unit
+ val kunifyError : ElabEnv.env -> kunify_error -> unit
datatype con_error =
UnboundCon of ErrorMsg.span * string
diff --git a/src/elab_err.sml b/src/elab_err.sml
index e8d7ff68..8892674c 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -36,7 +36,7 @@ structure U = ElabUtil
open Print
structure P = ElabPrint
-val simplCon = U.Con.mapB {kind = fn k => k,
+val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
con = fn env => fn c =>
let
val c = (c, ErrorMsg.dummySpan)
@@ -46,25 +46,34 @@ val simplCon = U.Con.mapB {kind = fn k => k,
("c'", P.p_con env c')];*)
#1 c'
end,
- bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k
- | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE}
+ bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
+ | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE
+ | (env, _) => env}
val p_kind = P.p_kind
+
+datatype kind_error =
+ UnboundKind of ErrorMsg.span * string
+
+fun kindError env err =
+ case err of
+ UnboundKind (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound kind variable " ^ s)
datatype kunify_error =
KOccursCheckFailed of kind * kind
| KIncompatible of kind * kind
-fun kunifyError err =
+fun kunifyError env err =
case err of
KOccursCheckFailed (k1, k2) =>
eprefaces "Kind occurs check failed"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)]
+ [("Kind 1", p_kind env k1),
+ ("Kind 2", p_kind env k2)]
| KIncompatible (k1, k2) =>
eprefaces "Incompatible kinds"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)]
+ [("Kind 1", p_kind env k1),
+ ("Kind 2", p_kind env k2)]
fun p_con env c = P.p_con env (simplCon env c)
@@ -89,9 +98,9 @@ fun conError env err =
| WrongKind (c, k1, k2, kerr) =>
(ErrorMsg.errorAt (#2 c) "Wrong kind";
eprefaces' [("Constructor", p_con env c),
- ("Have kind", p_kind k1),
- ("Need kind", p_kind k2)];
- kunifyError kerr)
+ ("Have kind", p_kind env k1),
+ ("Need kind", p_kind env k2)];
+ kunifyError env kerr)
| DuplicateField (loc, s) =>
ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
| ProjBounds (c, n) =>
@@ -101,7 +110,7 @@ fun conError env err =
| ProjMismatch (c, k) =>
(ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
eprefaces' [("Constructor", p_con env c),
- ("Kind", p_kind k)])
+ ("Kind", p_kind env k)])
datatype cunify_error =
@@ -116,9 +125,9 @@ fun cunifyError env err =
case err of
CKind (k1, k2, kerr) =>
(eprefaces "Kind unification failure"
- [("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)];
- kunifyError kerr)
+ [("Kind 1", p_kind env k1),
+ ("Kind 2", p_kind env k2)];
+ kunifyError env kerr)
| COccursCheckFailed (c1, c2) =>
eprefaces "Constructor occurs check failed"
[("Con 1", p_con env c1),
@@ -133,7 +142,7 @@ fun cunifyError env err =
("Con 2", p_con env c2)]
| CKindof (k, c, expected) =>
eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")")
- [("Kind", p_kind k),
+ [("Kind", p_kind env k),
("Con", p_con env c)]
| CRecordFailure (c1, c2) =>
eprefaces "Can't unify record constructors"
@@ -267,9 +276,9 @@ fun sgnError env err =
(ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
("Need", p_sgn_item env sgi2),
- ("Kind 1", p_kind k1),
- ("Kind 2", p_kind k2)];
- kunifyError kerr)
+ ("Kind 1", p_kind env k1),
+ ("Kind 2", p_kind env k2)];
+ kunifyError env kerr)
| SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
(ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
eprefaces' [("Have", p_sgn_item env sgi1),
@@ -296,9 +305,9 @@ fun sgnError env err =
("Field", PD.string x)])
| WhereWrongKind (k1, k2, kerr) =>
(ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
- eprefaces' [("Have", p_kind k1),
- ("Need", p_kind k2)];
- kunifyError kerr)
+ eprefaces' [("Have", p_kind env k1),
+ ("Need", p_kind env k2)];
+ kunifyError env kerr)
| NotIncludable sgn =>
(ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
eprefaces' [("Signature", p_sgn env sgn)])
@@ -337,10 +346,10 @@ fun strError env err =
eprefaces' [("Signature", p_sgn env sgn)])
| NotType (k, (k1, k2, ue)) =>
(ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
- eprefaces' [("Kind", p_kind k),
- ("Subkind 1", p_kind k1),
- ("Subkind 2", p_kind k2)];
- kunifyError ue)
+ eprefaces' [("Kind", p_kind env k),
+ ("Subkind 1", p_kind env k1),
+ ("Subkind 2", p_kind env k2)];
+ kunifyError env ue)
| DuplicateConstructor (x, loc) =>
ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
| NotDatatype loc =>
diff --git a/src/elab_ops.sig b/src/elab_ops.sig
index 62af9638..7088bf06 100644
--- a/src/elab_ops.sig
+++ b/src/elab_ops.sig
@@ -27,6 +27,12 @@
signature ELAB_OPS = sig
+ val liftKindInKind : int -> Elab.kind -> Elab.kind
+ val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind
+
+ val liftKindInCon : int -> Elab.con -> Elab.con
+ val subKindInCon : int * Elab.kind -> Elab.con -> Elab.con
+
val liftConInCon : int -> Elab.con -> Elab.con
val subConInCon : int * Elab.con -> Elab.con -> Elab.con
val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index c3e9274c..60a7639d 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -32,8 +32,64 @@ open Elab
structure E = ElabEnv
structure U = ElabUtil
+fun liftKindInKind' by =
+ U.Kind.mapB {kind = fn bound => fn k =>
+ case k of
+ KRel xn =>
+ if xn < bound then
+ k
+ else
+ KRel (xn + by)
+ | _ => k,
+ bind = fn (bound, _) => bound + 1}
+
+fun subKindInKind' rep =
+ U.Kind.mapB {kind = fn (by, xn) => fn k =>
+ case k of
+ KRel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 (liftKindInKind' by 0 rep)
+ | GREATER => KRel (xn' - 1)
+ | LESS => k)
+ | _ => k,
+ bind = fn ((by, xn), _) => (by+1, xn+1)}
+
+val liftKindInKind = liftKindInKind' 1
+
+fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn)
+
+fun liftKindInCon by =
+ U.Con.mapB {kind = fn bound => fn k =>
+ case k of
+ KRel xn =>
+ if xn < bound then
+ k
+ else
+ KRel (xn + by)
+ | _ => k,
+ con = fn _ => fn c => c,
+ bind = fn (bound, U.Con.RelK _) => bound + 1
+ | (bound, _) => bound}
+
+fun subKindInCon' rep =
+ U.Con.mapB {kind = fn (by, xn) => fn k =>
+ case k of
+ KRel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 (liftKindInKind' by 0 rep)
+ | GREATER => KRel (xn' - 1)
+ | LESS => k)
+ | _ => k,
+ con = fn _ => fn c => c,
+ bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1)
+ | (st, _) => st}
+
+val liftKindInCon = liftKindInCon 1
+
+fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn)
+
fun liftConInCon by =
- U.Con.mapB {kind = fn k => k,
+ U.Con.mapB {kind = fn _ => fn k => k,
con = fn bound => fn c =>
case c of
CRel xn =>
@@ -43,11 +99,11 @@ fun liftConInCon by =
CRel (xn + by)
(*| CUnif _ => raise SynUnif*)
| _ => c,
- bind = fn (bound, U.Con.Rel _) => bound + 1
+ bind = fn (bound, U.Con.RelC _) => bound + 1
| (bound, _) => bound}
fun subConInCon' rep =
- U.Con.mapB {kind = fn k => k,
+ U.Con.mapB {kind = fn _ => fn k => k,
con = fn (by, xn) => fn c =>
case c of
CRel xn' =>
@@ -57,7 +113,7 @@ fun subConInCon' rep =
| LESS => c)
(*| CUnif _ => raise SynUnif*)
| _ => c,
- bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1)
+ bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
| (ctx, _) => ctx}
val liftConInCon = liftConInCon 1
@@ -205,6 +261,11 @@ fun hnormCon env (cAll as (c, loc)) =
| _ => default ()
end
| c1' => (CApp ((c1', loc), hnormCon env c2), loc))
+
+ | CKApp (c1, k) =>
+ (case hnormCon env c1 of
+ (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body)
+ | _ => cAll)
| CConcat (c1, c2) =>
(case (hnormCon env c1, hnormCon env c2) of
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 3d078576..41d72ca7 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -28,7 +28,7 @@
(* Pretty-printing Ur/Web *)
signature ELAB_PRINT = sig
- val p_kind : Elab.kind Print.printer
+ val p_kind : ElabEnv.env -> Elab.kind Print.printer
val p_explicitness : Elab.explicitness Print.printer
val p_con : ElabEnv.env -> Elab.con Print.printer
val p_pat : ElabEnv.env -> Elab.pat Print.printer
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 098c9259..a0e1a54a 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -38,25 +38,36 @@ structure E = ElabEnv
val debug = ref false
-fun p_kind' par (k, _) =
+fun p_kind' par env (k, _) =
case k of
KType => string "Type"
- | KArrow (k1, k2) => parenIf par (box [p_kind' true k1,
+ | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
space,
string "->",
space,
- p_kind k2])
+ p_kind env k2])
| KName => string "Name"
- | KRecord k => box [string "{", p_kind k, string "}"]
+ | KRecord k => box [string "{", p_kind env k, string "}"]
| KUnit => string "Unit"
| KTuple ks => box [string "(",
- p_list_sep (box [space, string "*", space]) p_kind ks,
+ p_list_sep (box [space, string "*", space]) (p_kind env) ks,
string ")"]
| KError => string "<ERROR>"
- | KUnif (_, _, ref (SOME k)) => p_kind' par k
+ | KUnif (_, _, ref (SOME k)) => p_kind' par env k
| KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
+ | KRel n => ((if !debug then
+ string (E.lookupKRel env n ^ "_" ^ Int.toString n)
+ else
+ string (E.lookupKRel env n))
+ handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
+ | KFun (x, k) => box [string x,
+ space,
+ string "-->",
+ space,
+ p_kind (E.pushKRel env x) k]
+
and p_kind k = p_kind' false k
fun p_explicitness e =
@@ -66,7 +77,7 @@ fun p_explicitness e =
fun p_con' par env (c, _) =
case c of
- TFun (t1, t2) => parenIf par (box [p_con' true env t1,
+ TFun (t1, t2) => parenIf true (box [p_con' true env t1,
space,
string "->",
space,
@@ -75,20 +86,22 @@ fun p_con' par env (c, _) =
space,
p_explicitness e,
space,
- p_kind k,
+ p_kind env k,
space,
string "->",
space,
p_con (E.pushCRel env x k) c])
- | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
- space,
- string "~",
- space,
- p_con env c2,
- space,
- string "=>",
- space,
- p_con env c3])
+ | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1,
+ space,
+ string (case ai of
+ Instantiate => "~"
+ | LeaveAlone => "~~"),
+ space,
+ p_con env c2,
+ space,
+ string "=>",
+ space,
+ p_con env c3])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
box [p_name env x,
@@ -134,7 +147,7 @@ fun p_con' par env (c, _) =
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=>",
space,
@@ -152,7 +165,7 @@ fun p_con' par env (c, _) =
space,
p_con env c]) xcs,
string "]::",
- p_kind k])
+ p_kind env k])
else
parenIf par (box [string "[",
p_list (fn (x, c) =>
@@ -181,8 +194,24 @@ fun p_con' par env (c, _) =
| CError => string "<ERROR>"
| CUnif (_, _, _, ref (SOME c)) => p_con' par env c
| CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
- p_kind k,
+ p_kind env k,
string ">"]
+
+ | CKAbs (x, c) => box [string x,
+ space,
+ string "==>",
+ space,
+ p_con (E.pushKRel env x) c]
+ | CKApp (c, k) => box [p_con env c,
+ string "[[",
+ p_kind env k,
+ string "]]"]
+ | TKFun (x, c) => box [string x,
+ space,
+ string "-->",
+ space,
+ p_con (E.pushKRel env x) c]
+
and p_con env = p_con' false env
@@ -286,7 +315,7 @@ fun p_exp' par env (e, _) =
space,
p_explicitness exp,
space,
- p_kind k,
+ p_kind env k,
space,
string "=>",
space,
@@ -377,8 +406,6 @@ fun p_exp' par env (e, _) =
space,
p_con' true env c])
- | EFold _ => string "fold"
-
| ECase (e, pes, _) => parenIf par (box [string "case",
space,
p_exp env e,
@@ -415,6 +442,16 @@ fun p_exp' par env (e, _) =
string "end"]
end
+ | EKAbs (x, e) => box [string x,
+ space,
+ string "==>",
+ space,
+ p_exp (E.pushKRel env x) e]
+ | EKApp (e, k) => box [p_exp env e,
+ string "[[",
+ p_kind env k,
+ string "]]"]
+
and p_exp env = p_exp' false env
and p_edecl env (dAll as (d, _)) =
@@ -478,14 +515,14 @@ fun p_sgn_item env (sgi, _) =
space,
string "::",
space,
- p_kind k]
+ p_kind env k]
| SgiCon (x, n, k, c) => box [string "con",
space,
p_named x n,
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=",
space,
@@ -540,14 +577,14 @@ fun p_sgn_item env (sgi, _) =
space,
string "::",
space,
- p_kind k]
+ p_kind env k]
| SgiClass (x, n, k, c) => box [string "class",
space,
p_named x n,
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=",
space,
@@ -627,7 +664,7 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=",
space,
@@ -719,7 +756,7 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
string "::",
space,
- p_kind k,
+ p_kind env k,
space,
string "=",
space,
diff --git a/src/elab_util.sig b/src/elab_util.sig
index f9988981..817f885f 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -30,17 +30,24 @@ signature ELAB_UTIL = sig
val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind
structure Kind : sig
+ val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
+ bind : 'context * string -> 'context}
+ -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB
val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder
-> (Elab.kind, 'state, 'abort) Search.mapfolder
val exists : (Elab.kind' -> bool) -> Elab.kind -> bool
+ val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
+ bind : 'context * string -> 'context}
+ -> 'context -> (Elab.kind -> Elab.kind)
end
structure Con : sig
datatype binder =
- Rel of string * Elab.kind
- | Named of string * int * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
- val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
bind : 'context * binder -> 'context}
-> ('context, Elab.con, 'state, 'abort) Search.mapfolderB
@@ -48,7 +55,7 @@ structure Con : sig
con : (Elab.con', 'state, 'abort) Search.mapfolder}
-> (Elab.con, 'state, 'abort) Search.mapfolder
- val mapB : {kind : Elab.kind' -> Elab.kind',
+ val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
con : 'context -> Elab.con' -> Elab.con',
bind : 'context * binder -> 'context}
-> 'context -> (Elab.con -> Elab.con)
@@ -58,7 +65,7 @@ structure Con : sig
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool} -> Elab.con -> bool
- val foldB : {kind : Elab.kind' * 'state -> 'state,
+ val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
con : 'context * Elab.con' * 'state -> 'state,
bind : 'context * binder -> 'context}
-> 'context -> 'state -> Elab.con -> 'state
@@ -66,12 +73,13 @@ end
structure Exp : sig
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
- val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
bind : 'context * binder -> 'context}
@@ -80,7 +88,7 @@ structure Exp : sig
con : (Elab.con', 'state, 'abort) Search.mapfolder,
exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
-> (Elab.exp, 'state, 'abort) Search.mapfolder
- val mapB : {kind : Elab.kind' -> Elab.kind',
+ val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
con : 'context -> Elab.con' -> Elab.con',
exp : 'context -> Elab.exp' -> Elab.exp',
bind : 'context * binder -> 'context}
@@ -89,7 +97,7 @@ structure Exp : sig
con : Elab.con' -> bool,
exp : Elab.exp' -> bool} -> Elab.exp -> bool
- val foldB : {kind : Elab.kind' * 'state -> 'state,
+ val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
con : 'context * Elab.con' * 'state -> 'state,
exp : 'context * Elab.exp' * 'state -> 'state,
bind : 'context * binder -> 'context}
@@ -98,12 +106,13 @@ end
structure Sgn : sig
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| Str of string * Elab.sgn
| Sgn of string * Elab.sgn
- val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
@@ -127,14 +136,15 @@ end
structure Decl : sig
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
| Str of string * Elab.sgn
| Sgn of string * Elab.sgn
- val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
@@ -168,7 +178,7 @@ structure Decl : sig
decl : Elab.decl' -> 'a option}
-> Elab.decl -> 'a option
- val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state,
+ val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state,
con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
diff --git a/src/elab_util.sml b/src/elab_util.sml
index f052a06d..be1c9459 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -43,44 +43,60 @@ structure S = Search
structure Kind = struct
-fun mapfold f =
+fun mapfoldB {kind, bind} =
let
- fun mfk k acc =
- S.bindP (mfk' k acc, f)
+ fun mfk ctx k acc =
+ S.bindP (mfk' ctx k acc, kind ctx)
- and mfk' (kAll as (k, loc)) =
+ and mfk' ctx (kAll as (k, loc)) =
case k of
KType => S.return2 kAll
| KArrow (k1, k2) =>
- S.bind2 (mfk k1,
+ S.bind2 (mfk ctx k1,
fn k1' =>
- S.map2 (mfk k2,
+ S.map2 (mfk ctx k2,
fn k2' =>
(KArrow (k1', k2'), loc)))
| KName => S.return2 kAll
| KRecord k =>
- S.map2 (mfk k,
+ S.map2 (mfk ctx k,
fn k' =>
(KRecord k', loc))
| KUnit => S.return2 kAll
| KTuple ks =>
- S.map2 (ListUtil.mapfold mfk ks,
+ S.map2 (ListUtil.mapfold (mfk ctx) ks,
fn ks' =>
(KTuple ks', loc))
| KError => S.return2 kAll
- | KUnif (_, _, ref (SOME k)) => mfk' k
+ | KUnif (_, _, ref (SOME k)) => mfk' ctx k
| KUnif _ => S.return2 kAll
+
+ | KRel _ => S.return2 kAll
+ | KFun (x, k) =>
+ S.map2 (mfk (bind (ctx, x)) k,
+ fn k' =>
+ (KFun (x, k'), loc))
in
mfk
end
+fun mapfold fk =
+ mapfoldB {kind = fn () => fk,
+ bind = fn ((), _) => ()} ()
+
+fun mapB {kind, bind} ctx k =
+ case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
+ bind = bind} ctx k () of
+ S.Continue (k, ()) => k
+ | S.Return _ => raise Fail "ElabUtil.Kind.mapB: Impossible"
+
fun exists f k =
case mapfold (fn k => fn () =>
if f k then
@@ -95,12 +111,13 @@ end
structure Con = struct
datatype binder =
- Rel of string * Elab.kind
- | Named of string * int * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
+ | NamedC of string * int * Elab.kind
fun mapfoldB {kind = fk, con = fc, bind} =
let
- val mfk = Kind.mapfold fk
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
fun mfc ctx c acc =
S.bindP (mfc' ctx c acc, fc ctx)
@@ -114,9 +131,9 @@ fun mapfoldB {kind = fk, con = fc, bind} =
fn c2' =>
(TFun (c1', c2'), loc)))
| TCFun (e, x, k, c) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
- S.map2 (mfc (bind (ctx, Rel (x, k))) c,
+ S.map2 (mfc (bind (ctx, RelC (x, k))) c,
fn c' =>
(TCFun (e, x, k', c'), loc)))
| CDisjoint (ai, c1, c2, c3) =>
@@ -142,16 +159,16 @@ fun mapfoldB {kind = fk, con = fc, bind} =
fn c2' =>
(CApp (c1', c2'), loc)))
| CAbs (x, k, c) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
- S.map2 (mfc (bind (ctx, Rel (x, k))) c,
+ S.map2 (mfc (bind (ctx, RelC (x, k))) c,
fn c' =>
(CAbs (x, k', c'), loc)))
| CName _ => S.return2 cAll
| CRecord (k, xcs) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
S.map2 (ListUtil.mapfold (fn (x, c) =>
S.bind2 (mfc ctx x,
@@ -169,9 +186,9 @@ fun mapfoldB {kind = fk, con = fc, bind} =
fn c2' =>
(CConcat (c1', c2'), loc)))
| CMap (k1, k2) =>
- S.bind2 (mfk k1,
+ S.bind2 (mfk ctx k1,
fn k1' =>
- S.map2 (mfk k2,
+ S.map2 (mfk ctx k2,
fn k2' =>
(CMap (k1', k2'), loc)))
@@ -190,17 +207,32 @@ fun mapfoldB {kind = fk, con = fc, bind} =
| CError => S.return2 cAll
| CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
| CUnif _ => S.return2 cAll
+
+ | CKAbs (x, c) =>
+ S.map2 (mfc (bind (ctx, RelK x)) c,
+ fn c' =>
+ (CKAbs (x, c'), loc))
+ | CKApp (c, k) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (CKApp (c', k'), loc)))
+ | TKFun (x, c) =>
+ S.map2 (mfc (bind (ctx, RelK x)) c,
+ fn c' =>
+ (TKFun (x, c'), loc))
in
mfc
end
fun mapfold {kind = fk, con = fc} =
- mapfoldB {kind = fk,
+ mapfoldB {kind = fn () => fk,
con = fn () => fc,
bind = fn ((), _) => ()} ()
fun mapB {kind, con, bind} ctx c =
- case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+ case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
bind = bind} ctx c () of
S.Continue (c, ()) => c
@@ -227,7 +259,7 @@ fun exists {kind, con} k =
| S.Continue _ => false
fun foldB {kind, con, bind} ctx st c =
- case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+ case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
bind = bind} ctx c st of
S.Continue (_, st) => st
@@ -238,20 +270,22 @@ end
structure Exp = struct
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
let
- val mfk = Kind.mapfold fk
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
fun bind' (ctx, b) =
let
val b' = case b of
- Con.Rel x => RelC x
- | Con.Named x => NamedC x
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
in
bind (ctx, b')
end
@@ -288,7 +322,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
fn c' =>
(ECApp (e', c'), loc)))
| ECAbs (expl, x, k, e) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
S.map2 (mfe (bind (ctx, RelC (x, k))) e,
fn e' =>
@@ -347,11 +381,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
fn rest' =>
(ECutMulti (e', c', {rest = rest'}), loc))))
- | EFold k =>
- S.map2 (mfk k,
- fn k' =>
- (EFold k', loc))
-
| ECase (e, pes, {disc, result}) =>
S.bind2 (mfe ctx e,
fn e' =>
@@ -406,6 +435,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
(ELet (des', e'), loc)))
end
+ | EKAbs (x, e) =>
+ S.map2 (mfe (bind (ctx, RelK x)) e,
+ fn e' =>
+ (EKAbs (x, e'), loc))
+ | EKApp (e, k) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.map2 (mfk ctx k,
+ fn k' =>
+ (EKApp (e', k'), loc)))
+
and mfed ctx (dAll as (d, loc)) =
case d of
EDVal vi =>
@@ -432,7 +472,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
end
fun mapfold {kind = fk, con = fc, exp = fe} =
- mapfoldB {kind = fk,
+ mapfoldB {kind = fn () => fk,
con = fn () => fc,
exp = fn () => fe,
bind = fn ((), _) => ()} ()
@@ -457,7 +497,7 @@ fun exists {kind, con, exp} k =
| S.Continue _ => false
fun mapB {kind, con, exp, bind} ctx e =
- case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+ case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
bind = bind} ctx e () of
@@ -465,7 +505,7 @@ fun mapB {kind, con, exp, bind} ctx e =
| S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
fun foldB {kind, con, exp, bind} ctx st e =
- case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+ case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
bind = bind} ctx e st of
@@ -477,7 +517,8 @@ end
structure Sgn = struct
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| Str of string * Elab.sgn
| Sgn of string * Elab.sgn
@@ -487,14 +528,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
fun bind' (ctx, b) =
let
val b' = case b of
- Con.Rel x => RelC x
- | Con.Named x => NamedC x
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
in
bind (ctx, b')
end
val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
- val kind = Kind.mapfold kind
+ val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
fun sgi ctx si acc =
S.bindP (sgi' ctx si acc, sgn_item ctx)
@@ -502,11 +544,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
and sgi' ctx (siAll as (si, loc)) =
case si of
SgiConAbs (x, n, k) =>
- S.map2 (kind k,
+ S.map2 (kind ctx k,
fn k' =>
(SgiConAbs (x, n, k'), loc))
| SgiCon (x, n, k, c) =>
- S.bind2 (kind k,
+ S.bind2 (kind ctx k,
fn k' =>
S.map2 (con ctx c,
fn c' =>
@@ -548,11 +590,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
fn c2' =>
(SgiConstraint (c1', c2'), loc)))
| SgiClassAbs (x, n, k) =>
- S.map2 (kind k,
+ S.map2 (kind ctx k,
fn k' =>
(SgiClassAbs (x, n, k'), loc))
| SgiClass (x, n, k, c) =>
- S.bind2 (kind k,
+ S.bind2 (kind ctx k,
fn k' =>
S.map2 (con ctx c,
fn c' =>
@@ -608,7 +650,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
end
fun mapfold {kind, con, sgn_item, sgn} =
- mapfoldB {kind = kind,
+ mapfoldB {kind = fn () => kind,
con = fn () => con,
sgn_item = fn () => sgn_item,
sgn = fn () => sgn,
@@ -627,7 +669,8 @@ end
structure Decl = struct
datatype binder =
- RelC of string * Elab.kind
+ RelK of string
+ | RelC of string * Elab.kind
| NamedC of string * int * Elab.kind
| RelE of string * Elab.con
| NamedE of string * Elab.con
@@ -636,13 +679,14 @@ datatype binder =
fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
let
- val mfk = Kind.mapfold fk
+ val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
fun bind' (ctx, b) =
let
val b' = case b of
- Con.Rel x => RelC x
- | Con.Named x => NamedC x
+ Con.RelK x => RelK x
+ | Con.RelC x => RelC x
+ | Con.NamedC x => NamedC x
in
bind (ctx, b')
end
@@ -651,7 +695,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
fun bind' (ctx, b) =
let
val b' = case b of
- Exp.RelC x => RelC x
+ Exp.RelK x => RelK x
+ | Exp.RelC x => RelC x
| Exp.NamedC x => NamedC x
| Exp.RelE x => RelE x
| Exp.NamedE x => NamedE x
@@ -663,7 +708,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
fun bind' (ctx, b) =
let
val b' = case b of
- Sgn.RelC x => RelC x
+ Sgn.RelK x => RelK x
+ | Sgn.RelC x => RelC x
| Sgn.NamedC x => NamedC x
| Sgn.Sgn x => Sgn x
| Sgn.Str x => Str x
@@ -760,7 +806,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
and mfd' ctx (dAll as (d, loc)) =
case d of
DCon (x, n, k, c) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
S.map2 (mfc ctx c,
fn c' =>
@@ -825,7 +871,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
| DSequence _ => S.return2 dAll
| DClass (x, n, k, c) =>
- S.bind2 (mfk k,
+ S.bind2 (mfk ctx k,
fn k' =>
S.map2 (mfc ctx c,
fn c' =>
@@ -849,7 +895,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
end
fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
- mapfoldB {kind = kind,
+ mapfoldB {kind = fn () => kind,
con = fn () => con,
exp = fn () => exp,
sgn_item = fn () => sgn_item,
@@ -938,7 +984,7 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
| S.Continue _ => NONE
fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
- case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)),
+ case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0c335603..54543ae9 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -61,7 +61,7 @@
exception KUnify' of kunify_error
- fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
+ fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
let
fun err f = raise KUnify' (f (k1All, k2All))
in
@@ -70,19 +70,27 @@
| (L'.KUnit, L'.KUnit) => ()
| (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
- (unifyKinds' d1 d2;
- unifyKinds' r1 r2)
+ (unifyKinds' env d1 d2;
+ unifyKinds' env r1 r2)
| (L'.KName, L'.KName) => ()
- | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
+ | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2
| (L'.KTuple ks1, L'.KTuple ks2) =>
- ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
+ ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2))
handle ListPair.UnequalLengths => err KIncompatible)
+ | (L'.KRel n1, L'.KRel n2) =>
+ if n1 = n2 then
+ ()
+ else
+ err KIncompatible
+ | (L'.KFun (x, k1), L'.KFun (_, k2)) =>
+ unifyKinds' (E.pushKRel env x) k1 k2
+
| (L'.KError, _) => ()
| (_, L'.KError) => ()
- | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
- | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
+ | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
+ | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
| (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
if r1 = r2 then
@@ -106,12 +114,12 @@
exception KUnify of L'.kind * L'.kind * kunify_error
- fun unifyKinds k1 k2 =
- unifyKinds' k1 k2
+ fun unifyKinds env k1 k2 =
+ unifyKinds' env k1 k2
handle KUnify' err => raise KUnify (k1, k2, err)
fun checkKind env c k1 k2 =
- unifyKinds k1 k2
+ unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
conError env (WrongKind (c, k1, k2, err))
@@ -172,16 +180,23 @@
end
- fun elabKind (k, loc) =
+ fun elabKind env (k, loc) =
case k of
L.KType => (L'.KType, loc)
- | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
+ | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
| L.KName => (L'.KName, loc)
- | L.KRecord k => (L'.KRecord (elabKind k), loc)
+ | L.KRecord k => (L'.KRecord (elabKind env k), loc)
| L.KUnit => (L'.KUnit, loc)
- | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
+ | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
| L.KWild => kunif loc
+ | L.KVar s => (case E.lookupK env s of
+ NONE =>
+ (kindError env (UnboundKind (loc, s));
+ kerror)
+ | SOME n => (L'.KRel n, loc))
+ | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc)
+
fun mapKind (dom, ran, loc)=
(L'.KArrow ((L'.KArrow (dom, ran), loc),
(L'.KArrow ((L'.KRecord dom, loc),
@@ -192,11 +207,31 @@
L'.KUnif (_, _, ref (SOME k)) => hnormKind k
| _ => kAll
+ open ElabOps
+ val hnormCon = D.hnormCon
+
+ fun elabConHead (c as (_, loc)) k =
+ let
+ fun unravel (k, c) =
+ case hnormKind k of
+ (L'.KFun (x, k'), _) =>
+ let
+ val u = kunif loc
+
+ val k'' = subKindInKind (0, u) k'
+ in
+ unravel (k'', (L'.CKApp (c, u), loc))
+ end
+ | _ => (c, k)
+ in
+ unravel (k, c)
+ end
+
fun elabCon (env, denv) (c, loc) =
case c of
L.CAnnot (c, k) =>
let
- val k' = elabKind k
+ val k' = elabKind env k
val (c', ck, gs) = elabCon (env, denv) c
in
checkKind env c' ck k';
@@ -215,13 +250,21 @@
| L.TCFun (e, x, k, t) =>
let
val e' = elabExplicitness e
- val k' = elabKind k
+ val k' = elabKind env k
val env' = E.pushCRel env x k'
val (t', tk, gs) = elabCon (env', D.enter denv) t
in
checkKind env t' tk ktype;
((L'.TCFun (e', x, k', t'), loc), ktype, gs)
end
+ | L.TKFun (x, t) =>
+ let
+ val env' = E.pushKRel env x
+ val (t', tk, gs) = elabCon (env', denv) t
+ in
+ checkKind env t' tk ktype;
+ ((L'.TKFun (x, t'), loc), ktype, gs)
+ end
| L.CDisjoint (c1, c2, c) =>
let
val (c1', k1, gs1) = elabCon (env, denv) c1
@@ -253,9 +296,17 @@
(conError env (UnboundCon (loc, s));
(cerror, kerror, []))
| E.Rel (n, k) =>
- ((L'.CRel n, loc), k, [])
+ let
+ val (c, k) = elabConHead (L'.CRel n, loc) k
+ in
+ (c, k, [])
+ end
| E.Named (n, k) =>
- ((L'.CNamed n, loc), k, []))
+ let
+ val (c, k) = elabConHead (L'.CNamed n, loc) k
+ in
+ (c, k, [])
+ end)
| L.CVar (m1 :: ms, s) =>
(case E.lookupStr env m1 of
NONE => (conError env (UnboundStrInCon (loc, m1));
@@ -292,7 +343,7 @@
let
val k' = case ko of
NONE => kunif loc
- | SOME k => elabKind k
+ | SOME k => elabKind env k
val env' = E.pushCRel env x k'
val (t', tk, gs) = elabCon (env', D.enter denv) t
in
@@ -300,6 +351,15 @@
(L'.KArrow (k', tk), loc),
gs)
end
+ | L.CKAbs (x, t) =>
+ let
+ val env' = E.pushKRel env x
+ val (t', tk, gs) = elabCon (env', denv) t
+ in
+ ((L'.CKAbs (x, t'), loc),
+ (L'.KFun (x, tk), loc),
+ gs)
+ end
| L.CName s =>
((L'.CName s, loc), kname, [])
@@ -392,7 +452,7 @@
| L.CWild k =>
let
- val k' = elabKind k
+ val k' = elabKind env k
in
(cunif (loc, k'), k', [])
end
@@ -431,8 +491,6 @@
exception SynUnif = E.SynUnif
- open ElabOps
-
type record_summary = {
fields : (L'.con * L'.con) list,
unifs : (L'.con * L'.con option ref) list,
@@ -499,7 +557,12 @@
| L'.CError => kerror
| L'.CUnif (_, k, _, _) => k
- val hnormCon = D.hnormCon
+ | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
+ | L'.CKApp (c, k) =>
+ (case hnormKind (kindof env c) of
+ (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
+ | k => raise CUnify' (CKindof (k, c, "kapp")))
+ | L'.TKFun _ => ktype
fun deConstraintCon (env, denv) c =
let
@@ -564,6 +627,10 @@
| L'.CError => false
| L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
+ | L'.CKAbs _ => false
+ | L'.CKApp _ => false
+ | L'.TKFun _ => false
+
fun unifyRecordCons (env, denv) (c1, c2) =
let
fun rkindof c =
@@ -578,7 +645,7 @@
val (r1, gs1) = recordSummary (env, denv) c1
val (r2, gs2) = recordSummary (env, denv) c2
in
- unifyKinds k1 k2;
+ unifyKinds env k1 k2;
unifySummaries (env, denv) (k1, r1, r2);
gs1 @ gs2
end
@@ -848,12 +915,13 @@
val (c2, gs2) = hnormCon (env, denv) c2
in
let
+ (*val () = prefaces "unifyCons'" [("old1", p_con env old1),
+ ("old2", p_con env old2),
+ ("c1", p_con env c1),
+ ("c2", p_con env c2)]*)
+
val gs3 = unifyCons'' (env, denv) c1 c2
in
- (*prefaces "unifyCons'" [("c1", p_con env old1),
- ("c2", p_con env old2),
- ("t", PD.string (LargeReal.toString (Time.toReal
- (Time.- (Time.now (), befor)))))];*)
gs1 @ gs2 @ gs3
end
handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
@@ -878,7 +946,7 @@
if expl1 <> expl2 then
err CExplicitness
else
- (unifyKinds d1 d2;
+ (unifyKinds env d1 d2;
let
val denv' = D.enter denv
(*val befor = Time.now ()*)
@@ -906,7 +974,7 @@
(unifyCons' (env, denv) d1 d2;
unifyCons' (env, denv) r1 r2)
| (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
- (unifyKinds k1 k2;
+ (unifyKinds env k1 k2;
unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
| (L'.CName n1, L'.CName n2) =>
@@ -954,6 +1022,19 @@
else
err CIncompatible
+ | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
+ (unifyKinds env dom1 dom2;
+ unifyKinds env ran1 ran2;
+ [])
+
+ | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
+ unifyCons' (E.pushKRel env x, denv) c1 c2
+ | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
+ (unifyKinds env k1 k2;
+ unifyCons' (env, denv) c1 c2)
+ | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
+ unifyCons' (E.pushKRel env x, denv) c1 c2
+
| (L'.CError, _) => []
| (_, L'.CError) => []
@@ -966,7 +1047,7 @@
if r1 = r2 then
[]
else
- (unifyKinds k1 k2;
+ (unifyKinds env k1 k2;
r1 := SOME c2All;
[])
@@ -983,11 +1064,6 @@
(r := SOME c1All;
[])
- | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
- (unifyKinds dom1 dom2;
- unifyKinds ran1 ran2;
- [])
-
| _ => err CIncompatible
end
@@ -1013,36 +1089,7 @@
P.Int _ => !int
| P.Float _ => !float
| P.String _ => !string
-
- fun recCons (k, nm, v, rest, loc) =
- (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
- rest), loc)
-
- fun foldType (dom, loc) =
- (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
- (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
- (L'.TCFun (L'.Explicit, "v", dom,
- (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
- (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
- (L'.CDisjoint (L'.Instantiate,
- (L'.CRecord
- ((L'.KUnit, loc),
- [((L'.CRel 2, loc),
- (L'.CUnit, loc))]), loc),
- (L'.CRel 0, loc),
- (L'.CApp ((L'.CRel 3, loc),
- recCons (dom,
- (L'.CRel 2, loc),
- (L'.CRel 1, loc),
- (L'.CRel 0, loc),
- loc)), loc)),
- loc)), loc)),
- loc)), loc)), loc),
- (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
- (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
- (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
- loc)), loc)), loc)
-
+
datatype constraint =
Disjoint of D.goal
| TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
@@ -1056,7 +1103,16 @@
val (t, gs) = hnormCon (env, denv) t
in
case t of
- (L'.TCFun (L'.Implicit, x, k, t'), _) =>
+ (L'.TKFun (x, t'), _) =>
+ let
+ val u = kunif loc
+
+ val t'' = subKindInCon (0, u) t'
+ val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc))
+ in
+ (e, t, enD gs @ gs')
+ end
+ | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
let
val u = cunif (loc, k)
@@ -1575,7 +1631,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
| L.ECAbs (expl, x, k, e) =>
let
val expl' = elabExplicitness expl
- val k' = elabKind k
+ val k' = elabKind env k
val env' = E.pushCRel env x k'
val (e', et, gs) = elabExp (env', D.enter denv) e
@@ -1584,6 +1640,15 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
(L'.TCFun (expl', x, k', et), loc),
gs)
end
+ | L.EKAbs (x, e) =>
+ let
+ val env' = E.pushKRel env x
+ val (e', et, gs) = elabExp (env', denv) e
+ in
+ ((L'.EKAbs (x, e'), loc),
+ (L'.TKFun (x, et), loc),
+ gs)
+ end
| L.EDisjoint (c1, c2, e) =>
let
@@ -1710,13 +1775,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
gs1 @ enD gs2 @ enD gs3 @ enD gs4)
end
- | L.EFold =>
- let
- val dom = kunif loc
- in
- ((L'.EFold dom, loc), foldType (dom, loc), [])
- end
-
| L.ECase (e, pes) =>
let
val (e', et, gs1) = elabExp (env, denv) e
@@ -1781,6 +1839,7 @@ and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) =
case e of
L.EAbs _ => true
| L.ECAbs (_, _, _, e) => allowable e
+ | L.EKAbs (_, e) => allowable e
| L.EDisjoint (_, _, e) => allowable e
| _ => false
@@ -1859,7 +1918,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
case sgi of
L.SgiConAbs (x, k) =>
let
- val k' = elabKind k
+ val k' = elabKind env k
val (env', n) = E.pushCNamed env x k' NONE
in
@@ -1870,7 +1929,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
let
val k' = case ko of
NONE => kunif loc
- | SOME k => elabKind k
+ | SOME k => elabKind env k
val (c', ck, gs') = elabCon (env, denv) c
val (env', n) = E.pushCNamed env x k' (SOME c')
@@ -1979,7 +2038,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
val (env', n) = E.pushENamed env x c'
val c' = normClassConstraint env c'
in
- (unifyKinds ck ktype
+ (unifyKinds env ck ktype
handle KUnify ue => strError env (NotType (ck, ue)));
([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
@@ -2027,7 +2086,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
| L.SgiClassAbs (x, k) =>
let
- val k = elabKind k
+ val k = elabKind env k
val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val (env, n) = E.pushCNamed env x k' NONE
val env = E.pushClass env n
@@ -2037,7 +2096,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
| L.SgiClass (x, k, c) =>
let
- val k = elabKind k
+ val k = elabKind env k
val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val (c', ck, gs) = elabCon (env, denv) c
val (env, n) = E.pushCNamed env x k' (SOME c')
@@ -2149,7 +2208,7 @@ and elabSgn (env, denv) (sgn, loc) =
| L'.SgnConst sgis =>
if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
x' = x andalso
- (unifyKinds k ck
+ (unifyKinds env k ck
handle KUnify x => sgnError env (WhereWrongKind x);
true)
| _ => false) sgis then
@@ -2355,7 +2414,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
fun found (x', n1, k1, co1) =
if x = x' then
let
- val () = unifyKinds k1 k2
+ val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
val env = E.pushCNamedAs env x n1 k1 co1
@@ -2606,7 +2665,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
fun found (x', n1, k1, co) =
if x = x' then
let
- val () = unifyKinds k1 k2
+ val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
@@ -2635,7 +2694,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
fun found (x', n1, k1, c1) =
if x = x' then
let
- val () = unifyKinds k1 k2
+ val () = unifyKinds env k1 k2
handle KUnify (k1, k2, err) =>
sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
@@ -2702,6 +2761,9 @@ fun positive self =
| CAbs _ => false
| CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+ | CKAbs _ => false
+ | TKFun _ => false
+
| CName _ => true
| CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
@@ -2728,6 +2790,9 @@ fun positive self =
| CAbs _ => false
| CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
+ | CKAbs _ => false
+ | TKFun _ => false
+
| CName _ => true
| CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
@@ -2777,6 +2842,9 @@ fun wildifyStr env (str, sgn) =
| L'.KUnif (_, _, ref (SOME k)) => decompileKind k
| L'.KUnif _ => NONE
+ | L'.KRel _ => NONE
+ | L'.KFun _ => NONE
+
fun decompileCon env (c, loc) =
case c of
L'.CRel i =>
@@ -2914,7 +2982,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
let
val k' = case ko of
NONE => kunif loc
- | SOME k => elabKind k
+ | SOME k => elabKind env k
val (c', ck, gs') = elabCon (env, denv) c
val (env', n) = E.pushCNamed env x k' (SOME c')
@@ -3047,6 +3115,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
case e of
L.EAbs _ => true
| L.ECAbs (_, _, _, e) => allowable e
+ | L.EKAbs (_, e) => allowable e
| L.EDisjoint (_, _, e) => allowable e
| _ => false
@@ -3264,7 +3333,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
| L.DClass (x, k, c) =>
let
- val k = elabKind k
+ val k = elabKind env k
val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
val (c', ck, gs') = elabCon (env, denv) c
val (env, n) = E.pushCNamed env x k' (SOME c')
diff --git a/src/expl.sml b/src/expl.sml
index c0d291b5..0101dd1f 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -93,7 +93,6 @@ datatype exp' =
| EConcat of exp * con * exp * con
| ECut of exp * con * { field : con, rest : con }
| ECutMulti of exp * con * { rest : con }
- | EFold of kind
| ECase of exp * (pat * exp) list * { disc : con, result : con }
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 7044bfa2..313fef5c 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -351,7 +351,6 @@ fun p_exp' par env (e, loc) =
string "---",
space,
p_con' true env c])
- | EFold _ => string "fold"
| EWrite e => box [string "write(",
p_exp env e,
diff --git a/src/expl_util.sml b/src/expl_util.sml
index a2b5f2f6..febf3586 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -311,10 +311,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.map2 (mfc ctx rest,
fn rest' =>
(ECutMulti (e', c', {rest = rest'}), loc))))
- | EFold k =>
- S.map2 (mfk k,
- fn k' =>
- (EFold k', loc))
| EWrite e =>
S.map2 (mfe ctx e,
diff --git a/src/explify.sml b/src/explify.sml
index a4eab0ba..5bce9268 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -107,8 +107,6 @@ fun explifyExp (e, loc) =
{field = explifyCon field, rest = explifyCon rest}), loc)
| L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c,
{rest = explifyCon rest}), loc)
- | L.EFold k => (L'.EFold (explifyKind k), loc)
-
| L.ECase (e, pes, {disc, result}) =>
(L'.ECase (explifyExp e,
map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
diff --git a/src/monoize.sml b/src/monoize.sml
index 898d3e61..96ef2c6a 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -2183,7 +2183,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
| L.EConcat _ => poly ()
| L.ECut _ => poly ()
| L.ECutMulti _ => poly ()
- | L.EFold _ => poly ()
| L.ECase (e, pes, {disc, result}) =>
let
diff --git a/src/reduce.sml b/src/reduce.sml
index 949b2a6d..77718b66 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -214,20 +214,6 @@ fun conAndExp (namedC, namedE) =
in
case #1 e of
ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
-
- | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) =>
- (case #1 c of
- CRecord (_, []) => i
- | CRecord (k, (nm, v) :: rest) =>
- let
- val rest = (CRecord (k, rest), loc)
- in
- exp (deKnown env)
- (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc),
- (ECApp (e, rest), loc)), loc)
- end
- | _ => (ECApp (e, c), loc))
-
| _ => (ECApp (e, c), loc)
end
@@ -334,8 +320,6 @@ fun conAndExp (namedC, namedE) =
| _ => default ()
end
- | EFold _ => all
-
| ECase (e, pes, {disc, result}) =>
let
fun patBinds (p, _) =
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
index 7de7d799..25b1023a 100644
--- a/src/reduce_local.sml
+++ b/src/reduce_local.sml
@@ -107,8 +107,6 @@ fun exp env (all as (e, loc)) =
| ECut (e, c, others) => (ECut (exp env e, c, others), loc)
| ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
- | EFold _ => all
-
| ECase (e, pes, others) =>
let
fun patBinds (p, _) =
diff --git a/src/source.sml b/src/source.sml
index d70d0f5d..e9531245 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -38,6 +38,9 @@ datatype kind' =
| KTuple of kind list
| KWild
+ | KFun of string * kind
+ | KVar of string
+
withtype kind = kind' located
datatype explicitness =
@@ -56,6 +59,9 @@ datatype con' =
| CAbs of string * kind option * con
| CDisjoint of con * con * con
+ | CKAbs of string * con
+ | TKFun of string * con
+
| CName of string
| CRecord of (con * con) list
@@ -119,12 +125,13 @@ datatype exp' =
| ECAbs of explicitness * string * kind * exp
| EDisjoint of con * con * exp
+ | EKAbs of string * exp
+
| ERecord of (con * exp) list
| EField of exp * con
| EConcat of exp * exp
| ECut of exp * con
| ECutMulti of exp * con
- | EFold
| EWild
diff --git a/src/source_print.sml b/src/source_print.sml
index 148157c2..f2420947 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -50,6 +50,13 @@ fun p_kind' par (k, _) =
p_list_sep (box [space, string "*", space]) p_kind ks,
string ")"]
+ | KVar x => string x
+ | KFun (x, k) => box [string x,
+ space,
+ string "-->",
+ space,
+ p_kind k]
+
and p_kind k = p_kind' false k
fun p_explicitness e =
@@ -156,6 +163,17 @@ fun p_con' par (c, _) =
| CProj (c, n) => box [p_con c,
string ".",
string (Int.toString n)]
+
+ | CKAbs (x, c) => box [string x,
+ space,
+ string "==>",
+ space,
+ p_con c]
+ | TKFun (x, c) => box [string x,
+ space,
+ string "-->",
+ space,
+ p_con c]
and p_con c = p_con' false c
@@ -273,8 +291,6 @@ fun p_exp' par (e, _) =
string "---",
space,
p_con' true c])
- | EFold => string "fold"
-
| ECase (e, pes) => parenIf par (box [string "case",
space,
p_exp e,
@@ -300,6 +316,12 @@ fun p_exp' par (e, _) =
newline,
string "end"]
+ | EKAbs (x, e) => box [string x,
+ space,
+ string "-->",
+ space,
+ p_exp e]
+
and p_exp e = p_exp' false e
and p_edecl (d, _) =
diff --git a/src/termination.sml b/src/termination.sml
index e89f329e..5dd95f46 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -190,6 +190,7 @@ fun declOk' env (d, loc) =
in
(p, ps, calls)
end
+ | EKApp (e, _) => combiner calls e
| _ =>
let
val (p, calls) = exp parent (penv, calls) e
@@ -239,6 +240,13 @@ fun declOk' env (d, loc) =
in
(Rabble, calls)
end
+ | EKApp _ => apps ()
+ | EKAbs (_, e) =>
+ let
+ val (_, calls) = exp parent (penv, calls) e
+ in
+ (Rabble, calls)
+ end
| ERecord xets =>
let
@@ -278,7 +286,6 @@ fun declOk' env (d, loc) =
in
(Rabble, calls)
end
- | EFold _ => (Rabble, calls)
| ECase (e, pes, _) =>
let
diff --git a/src/unnest.sml b/src/unnest.sml
index 8e363301..1d0c2388 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -37,7 +37,7 @@ structure U = ElabUtil
structure IS = IntBinarySet
fun liftExpInExp by =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn _ => fn c => c,
exp = fn bound => fn e =>
case e of
@@ -51,7 +51,7 @@ fun liftExpInExp by =
| (bound, _) => bound}
val subExpInExp =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn _ => fn c => c,
exp = fn (xn, rep) => fn e =>
case e of
@@ -65,7 +65,7 @@ val subExpInExp =
| ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
| (ctx, _) => ctx}
-val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
+val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
con = fn (cb, c, cvs) =>
case c of
CRel n =>
@@ -76,11 +76,11 @@ val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
| _ => cvs,
bind = fn (cb, b) =>
case b of
- U.Con.Rel _ => cb + 1
+ U.Con.RelC _ => cb + 1
| _ => cb}
0 IS.empty
-fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
+fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
con = fn ((cb, eb), c, st as (cvs, evs)) =>
case c of
CRel n =>
@@ -124,7 +124,7 @@ fun positionOf (x : int) ls =
end
fun squishCon cfv =
- U.Con.mapB {kind = fn k => k,
+ U.Con.mapB {kind = fn _ => fn k => k,
con = fn cb => fn c =>
case c of
CRel n =>
@@ -135,12 +135,12 @@ fun squishCon cfv =
| _ => c,
bind = fn (cb, b) =>
case b of
- U.Con.Rel _ => cb + 1
+ U.Con.RelC _ => cb + 1
| _ => cb}
0
fun squishExp (nr, cfv, efv) =
- U.Exp.mapB {kind = fn k => k,
+ U.Exp.mapB {kind = fn _ => fn k => k,
con = fn (cb, eb) => fn c =>
case c of
CRel n =>
@@ -169,7 +169,7 @@ type state = {
decls : (string * int * con * exp) list
}
-fun kind (k, st) = (k, st)
+fun kind (_, k, st) = (k, st)
fun exp ((ks, ts), e as old, st : state) =
case e of
diff --git a/src/urweb.grm b/src/urweb.grm
index d425caec..b6e4ce72 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -184,10 +184,10 @@ fun tagIn bt =
| LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
| EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR
| PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT
- | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS
+ | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS
| DATATYPE | OF
| TYPE | NAME
- | ARROW | LARROW | DARROW | STAR | SEMI
+ | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW
| FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE
| LET | IN
| STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL
@@ -327,6 +327,8 @@ fun tagIn bt =
%name Urweb
+%right KARROW
+%nonassoc DKARROW
%right SEMI
%nonassoc LARROW
%nonassoc IF THEN ELSE
@@ -575,6 +577,8 @@ kind : TYPE (KType, s (TYPEleft, TYPEright))
| KUNIT (KUnit, s (KUNITleft, KUNITright))
| UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright))
| LPAREN ktuple RPAREN (KTuple ktuple, s (LPARENleft, RPARENright))
+ | CSYMBOL (KVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+ | CSYMBOL KARROW kind (KFun (CSYMBOL, kind), s (CSYMBOLleft, kindright))
ktuple : kind STAR kind ([kind1, kind2])
| kind STAR ktuple (kind :: ktuple)
@@ -585,10 +589,12 @@ capps : cterm (cterm)
cexp : capps (capps)
| cexp ARROW cexp (TFun (cexp1, cexp2), s (cexp1left, cexp2right))
| SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright))
+ | CSYMBOL KARROW cexp (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
| cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))
| FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
+ | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright))
| LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
@@ -651,7 +657,7 @@ cargp : SYMBOL (fn (c, k) =>
((CAbs (SYMBOL, SOME kind, c), loc),
(KArrow (kind, k), loc))
end)
- | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) =>
+ | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) =>
let
val loc = s (LBRACKleft, RBRACKright)
in
@@ -716,6 +722,7 @@ eexp : eapps (eapps)
in
#1 (eargs (eexp, (CWild (KType, loc), loc)))
end)
+ | CSYMBOL DKARROW eexp (EKAbs (CSYMBOL, eexp), s (CSYMBOLleft, eexpright))
| eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright))
| eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright))
| eexp MINUSMINUSMINUS cexp (ECutMulti (eexp, cexp), s (eexpleft, cexpright))
@@ -851,6 +858,13 @@ eargp : SYMBOL (fn (e, t) =>
((EDisjoint (cexp1, cexp2, e), loc),
(CDisjoint (cexp1, cexp2, t), loc))
end)
+ | CSYMBOL (fn (e, t) =>
+ let
+ val loc = s (CSYMBOLleft, CSYMBOLright)
+ in
+ ((EKAbs (CSYMBOL, e), loc),
+ (TKFun (CSYMBOL, t), loc))
+ end)
eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
| LPAREN etuple RPAREN (let
@@ -895,7 +909,6 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
(EField (e, ident), loc))
(EVar (#1 path, #2 path, DontInfer), s (pathleft, pathright)) idents
end)
- | FOLD (EFold, s (FOLDleft, FOLDright))
| XML_BEGIN xml XML_END (let
val loc = s (XML_BEGINleft, XML_ENDright)
@@ -1070,7 +1083,7 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer)
()
else
ErrorMsg.errorAt pos "Begin and end tags don't match.";
- (EFold, pos))
+ (EWild, pos))
end)
| LBRACE eexp RBRACE (eexp)
| LBRACE LBRACK eexp RBRACK RBRACE (let
diff --git a/src/urweb.lex b/src/urweb.lex
index 29e07194..bb57f03d 100644
--- a/src/urweb.lex
+++ b/src/urweb.lex
@@ -247,7 +247,9 @@ notags = [^<{\n]+;
<INITIAL> "}" => (exitBrace ();
Tokens.RBRACE (pos yypos, pos yypos + size yytext));
+<INITIAL> "-->" => (Tokens.KARROW (pos yypos, pos yypos + size yytext));
<INITIAL> "->" => (Tokens.ARROW (pos yypos, pos yypos + size yytext));
+<INITIAL> "==>" => (Tokens.DKARROW (pos yypos, pos yypos + size yytext));
<INITIAL> "=>" => (Tokens.DARROW (pos yypos, pos yypos + size yytext));
<INITIAL> "++" => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext));
<INITIAL> "--" => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext));
@@ -291,7 +293,6 @@ notags = [^<{\n]+;
<INITIAL> "fun" => (Tokens.FUN (pos yypos, pos yypos + size yytext));
<INITIAL> "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext));
<INITIAL> "map" => (Tokens.MAP (pos yypos, pos yypos + size yytext));
-<INITIAL> "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext));
<INITIAL> "case" => (Tokens.CASE (pos yypos, pos yypos + size yytext));
<INITIAL> "if" => (Tokens.IF (pos yypos, pos yypos + size yytext));
<INITIAL> "then" => (Tokens.THEN (pos yypos, pos yypos + size yytext));
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-21 05:23:28 +0000