diff options
| -rw-r--r-- | lib/ur/basis.urs | 31 | ||||
| -rw-r--r-- | lib/ur/top.ur | 30 | ||||
| -rw-r--r-- | lib/ur/top.urs | 52 | ||||
| -rw-r--r-- | src/core.sml | 2 | ||||
| -rw-r--r-- | src/core_print.sml | 2 | ||||
| -rw-r--r-- | src/core_util.sml | 10 | ||||
| -rw-r--r-- | src/corify.sml | 2 | ||||
| -rw-r--r-- | src/disjoint.sml | 33 | ||||
| -rw-r--r-- | src/elab.sml | 2 | ||||
| -rw-r--r-- | src/elab_ops.sml | 253 | ||||
| -rw-r--r-- | src/elab_print.sml | 2 | ||||
| -rw-r--r-- | src/elab_util.sml | 4 | ||||
| -rw-r--r-- | src/elaborate.sml | 176 | ||||
| -rw-r--r-- | src/elisp/urweb-defs.el | 4 | ||||
| -rw-r--r-- | src/elisp/urweb-mode.el | 2 | ||||
| -rw-r--r-- | src/expl.sml | 2 | ||||
| -rw-r--r-- | src/expl_print.sml | 2 | ||||
| -rw-r--r-- | src/expl_util.sml | 4 | ||||
| -rw-r--r-- | src/explify.sml | 2 | ||||
| -rw-r--r-- | src/monoize.sml | 2 | ||||
| -rw-r--r-- | src/reduce.sml | 13 | ||||
| -rw-r--r-- | src/source.sml | 2 | ||||
| -rw-r--r-- | src/source_print.sml | 2 | ||||
| -rw-r--r-- | src/urweb.grm | 4 | ||||
| -rw-r--r-- | src/urweb.lex | 1 |
25 files changed, 223 insertions, 416 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index b4a40fde..cd2468ba 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -120,31 +120,20 @@ con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type con sql_subset :: {{Type}} -> {{Type}} -> Type val sql_subset : keep_drop :: {({Type} * {Type})} -> sql_subset - (fold (fn nm (fields :: ({Type} * {Type})) - acc [[nm] ~ acc] - [fields.1 ~ fields.2] => - [nm = fields.1 ++ fields.2] - ++ acc) [] keep_drop) - (fold (fn nm (fields :: ({Type} * {Type})) - acc [[nm] ~ acc] => - [nm = fields.1] ++ acc) - [] keep_drop) + (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) + (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop) val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables val sql_query1 : tables ::: {{Type}} -> grouped ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} - -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = sql_table fields] ++ acc) - [] tables), + -> {From : $(map (fn fields :: {Type} => sql_table fields) tables), Where : sql_exp tables [] [] bool, GroupBy : sql_subset tables grouped, Having : sql_exp grouped tables [] bool, SelectFields : sql_subset grouped selectedFields, - SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp grouped tables [] t] - ++ acc) [] selectedExps) } + SelectExps : $(map (fn (t :: Type) => sql_exp grouped tables [] t) selectedExps) } -> sql_query1 tables selectedFields selectedExps type sql_relop @@ -291,8 +280,7 @@ val query : tables ::: {{Type}} -> exps ::: {Type} -> fn [tables ~ exps] => state ::: Type -> sql_query tables exps - -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> state -> transaction state) -> state @@ -306,17 +294,12 @@ val dml : dml -> transaction unit val insert : fields ::: {Type} -> sql_table fields - -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [] [] [] t] ++ acc) - [] fields) + -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) -> dml val update : unchanged ::: {Type} -> changed :: {Type} -> fn [changed ~ unchanged] => - $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [T = changed ++ unchanged] [] [] t] - ++ acc) - [] changed) + $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) -> sql_table (changed ++ unchanged) -> sql_exp [T = changed ++ unchanged] [] [] bool -> dml diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 35e8519b..58e99f3c 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -8,17 +8,7 @@ con fstTTT (t :: (Type * Type * Type)) = t.1 con sndTTT (t :: (Type * Type * Type)) = t.2 con thdTTT (t :: (Type * Type * Type)) = t.3 -con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] +con mapUT = fn f :: Type => map (fn _ :: Unit => f) con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -69,7 +59,7 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf r) -> tr r] + fold [fn r :: {Type} => $(map tf r) -> tr r] (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) @@ -80,7 +70,7 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] + 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))) @@ -91,7 +81,7 @@ fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r] + 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))) @@ -102,7 +92,7 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] + 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))) @@ -114,7 +104,7 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] + 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))) @@ -126,7 +116,7 @@ fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r] + 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))) @@ -195,8 +185,7 @@ fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx [] []) = query q (fn fs acc => return <xml>{acc}{f fs}</xml>) @@ -204,8 +193,7 @@ fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx [] [])) = query q (fn fs acc => diff --git a/lib/ur/top.urs b/lib/ur/top.urs index d6315b92..49aad50c 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -8,17 +8,7 @@ con fstTTT = fn t :: (Type * Type * Type) => t.1 con sndTTT = fn t :: (Type * Type * Type) => t.2 con thdTTT = fn t :: (Type * Type * Type) => t.3 -con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] +con mapUT = fn f :: Type => map (fn _ :: Unit => f) con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -53,19 +43,19 @@ val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r + -> tr [] -> r :: {Type} -> $(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)} -> $(mapT2T tf r) -> tr r + -> tr [] -> r :: {(Type * Type)} -> $(map tf 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)} -> $(mapT3T tf r) -> tr r + -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) @@ -73,7 +63,7 @@ val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] - -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r + -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) @@ -81,7 +71,7 @@ val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r + -> $(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) @@ -89,32 +79,32 @@ val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * T -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r + -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) - -> r :: {Type} -> $(mapTT tf r) -> 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)} -> $(mapT2T tf r) -> 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)} -> $(mapT3T tf r) -> 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} - -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit} @@ -122,7 +112,7 @@ val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) @@ -131,21 +121,19 @@ val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx [] []) -> transaction (xml ctx [] []) val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx [] [])) -> transaction (xml ctx [] []) @@ -155,20 +143,14 @@ val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} transaction (option $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables)) + ++ map (fn fields :: {Type} => $fields) tables)) val oneRow : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps -> fn [tables ~ exps] => transaction $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables) + ++ map (fn fields :: {Type} => $fields) tables) val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> sql_injectable (option t) diff --git a/src/core.sml b/src/core.sml index c6e0cfef..d7a57493 100644 --- a/src/core.sml +++ b/src/core.sml @@ -54,7 +54,7 @@ datatype con' = | CRecord of kind * (con * con) list | CConcat of con * con - | CFold of kind * kind + | CMap of kind * kind | CUnit diff --git a/src/core_print.sml b/src/core_print.sml index 405ae14e..db8c3907 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -138,7 +138,7 @@ fun p_con' par env (c, _) = string "++", space, p_con env c2]) - | CFold _ => string "fold" + | CMap _ => string "map" | CUnit => string "()" | CTuple cs => box [string "(", diff --git a/src/core_util.sml b/src/core_util.sml index a222dca4..e76da387 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -178,11 +178,11 @@ fun compare ((c1, _), (c2, _)) = | (CConcat _, _) => LESS | (_, CConcat _) => GREATER - | (CFold (d1, r1), CFold (d2, r2)) => + | (CMap (d1, r1), CMap (d2, r2)) => join (Kind.compare (d1, r2), fn () => Kind.compare (r1, r2)) - | (CFold _, _) => LESS - | (_, CFold _) => GREATER + | (CMap _, _) => LESS + | (_, CMap _) => GREATER | (CUnit, CUnit) => EQUAL | (CUnit, _) => LESS @@ -261,12 +261,12 @@ fun mapfoldB {kind = fk, con = fc, bind} = S.map2 (mfc ctx c2, fn c2' => (CConcat (c1', c2'), loc))) - | CFold (k1, k2) => + | CMap (k1, k2) => S.bind2 (mfk k1, fn k1' => S.map2 (mfk k2, fn k2' => - (CFold (k1', k2'), loc))) + (CMap (k1', k2'), loc))) | CUnit => S.return2 cAll diff --git a/src/corify.sml b/src/corify.sml index 2383ee03..c464e5a5 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -473,7 +473,7 @@ fun corifyCon st (c, loc) = | L.CRecord (k, xcs) => (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc) | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc) - | L.CFold (k1, k2) => (L'.CFold (corifyKind k1, corifyKind k2), loc) + | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc) | L.CUnit => (L'.CUnit, loc) | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc) 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 diff --git a/src/elab.sml b/src/elab.sml index 8e44c43c..ec8a910a 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -66,7 +66,7 @@ datatype con' = | CRecord of kind * (con * con) list | CConcat of con * con - | CFold of kind * kind + | CMap of kind * kind | CUnit diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 0648d704..c3e9274c 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -114,181 +114,98 @@ fun hnormCon env (cAll as (c, loc)) = ("sc", ElabPrint.p_con env sc)];*) sc end - | c1' as CApp (c', i) => + | c1' as CApp (c', f) => let fun default () = (CApp ((c1', loc), hnormCon env c2), loc) in case #1 (hnormCon env c') of - CApp (c', f) => - (case #1 (hnormCon env c') of - CFold ks => - (case #1 (hnormCon env c2) of - CRecord (_, []) => hnormCon env i - | CRecord (k, (x, c) :: rest) => - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc) - | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => - let - val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) - - (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc)*) - in - (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc) - end - | _ => - let - fun cunif () = - let - val r = ref NONE - in - (r, (CUnif (loc, (KType, loc), "_", r), loc)) - end - - val (nmR, nm) = cunif () - val (vR, v) = cunif () - val (rR, r) = cunif () - - val c = f - val c = (CApp (c, nm), loc) - val c = (CApp (c, v), loc) - val c = (CApp (c, r), loc) - fun unconstraint c = - case hnormCon env c of - (CDisjoint (_, _, _, c), _) => unconstraint c - | c => c - val c = unconstraint c - - fun tryDistributivity () = - let - fun distribute (c1, c2) = - let - val c = (CFold ks, loc) - val c = (CApp (c, f), loc) - val c = (CApp (c, i), loc) - - val c1 = (CApp (c, c1), loc) - val c2 = (CApp (c, c2), loc) - val c = (CConcat (c1, c2), loc) - in - hnormCon env c - end - in - case (hnormCon env i, hnormCon env c2, hnormCon env c) of - ((CRecord (_, []), _), - (CConcat (arg1, arg2), _), - (CConcat (c1, c2'), _)) => - (case (hnormCon env c1, hnormCon env c2') of - ((CRecord (_, [(nm', v')]), _), - (CUnif (_, _, _, rR'), _)) => - (case hnormCon env nm' of - (CUnif (_, _, _, nmR'), _) => - if nmR' = nmR andalso rR' = rR then - distribute (arg1, arg2) - else - default () - | _ => default ()) - | _ => default ()) - | _ => default () - end - - fun tryFusion () = - let - fun fuse (dom, new_v, r') = - let - val ran = #2 ks - - val f = (CApp (f, (CRel 2, loc)), loc) - val f = (CApp (f, new_v), loc) - val f = (CApp (f, (CRel 0, loc)), loc) - val f = (CAbs ("acc", ran, f), loc) - val f = (CAbs ("v", dom, f), loc) - val f = (CAbs ("nm", (KName, loc), f), loc) - - val c = (CFold (dom, ran), loc) - val c = (CApp (c, f), loc) - val c = (CApp (c, i), loc) - val c = (CApp (c, r'), loc) - in - hnormCon env c - end - in - case #1 (hnormCon env c2) of - CApp (f, r') => - (case #1 (hnormCon env f) of - CApp (f, inner_i) => - (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of - (CApp (f, inner_f), CRecord (_, [])) => - (case #1 (hnormCon env f) of - CFold (dom, _) => - let - val c = inner_f - val c = (CApp (c, nm), loc) - val c = (CApp (c, v), loc) - val c = (CApp (c, r), loc) - val c = unconstraint c - - (*val () = Print.prefaces "Onto something!" - [("c", ElabPrint.p_con env cAll), - ("c'", ElabPrint.p_con env c)]*) - - in - case #1 (hnormCon env c) of - CConcat (first, rest) => - (case (#1 (hnormCon env first), - #1 (hnormCon env rest)) of - (CRecord (_, [(nm', v')]), - CUnif (_, _, _, rR')) => - (case #1 (hnormCon env nm') of - CUnif (_, _, _, nmR') => - if rR' = rR andalso nmR' = nmR then - (nmR := SOME (CRel 2, loc); - vR := SOME (CRel 1, loc); - rR := SOME (CError, loc); - fuse (dom, v', r')) - else - tryDistributivity () - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity () - end - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity () - end - - in - (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) - case (hnormCon env i, unconstraint c) of - ((CRecord (_, []), _), - (CConcat (c1, c2'), _)) => - (case (hnormCon env c1, hnormCon env c2') of - ((CRecord (_, [(nm', v')]), _), - (CUnif (_, _, _, rR'), _)) => - (case (hnormCon env nm', hnormCon env v') of - ((CUnif (_, _, _, nmR'), _), - (CUnif (_, _, _, vR'), _)) => - if nmR' = nmR andalso vR' = vR andalso rR' = rR then - hnormCon env c2 - else - tryFusion () - | _ => tryFusion ()) - | _ => tryFusion ()) - | _ => tryFusion () - end) - | _ => default ()) + CMap (ks as (k1, k2)) => + (case #1 (hnormCon env c2) of + CRecord (_, []) => (CRecord (k2, []), loc) + | CRecord (_, (x, c) :: rest) => + hnormCon 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 + hnormCon env + (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, rest''), loc)), loc) + end + | _ => + let + fun unconstraint c = + case hnormCon env c of + (CDisjoint (_, _, _, c), _) => unconstraint c + | c => c + + fun tryDistributivity () = + case hnormCon 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 + hnormCon env c + end + | _ => default () + + fun tryFusion () = + case #1 (hnormCon env c2) of + CApp (f', r') => + (case #1 (hnormCon env f') of + CApp (f', inner_f) => + (case #1 (hnormCon env f') of + CMap (dom, _) => + let + 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 + hnormCon env c + end + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity () + + fun tryIdentity () = + let + fun cunif () = + let + val r = ref NONE + in + (r, (CUnif (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 + hnormCon env c2 + else + tryFusion () + | _ => tryFusion () + end + in + tryIdentity () + end) | _ => default () end | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) - + | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => diff --git a/src/elab_print.sml b/src/elab_print.sml index 0e6c9767..098c9259 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -167,7 +167,7 @@ fun p_con' par env (c, _) = string "++", space, p_con env c2]) - | CFold _ => string "fold" + | CMap _ => string "map" | CUnit => string "()" diff --git a/src/elab_util.sml b/src/elab_util.sml index 6e78907d..f052a06d 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -168,12 +168,12 @@ fun mapfoldB {kind = fk, con = fc, bind} = S.map2 (mfc ctx c2, fn c2' => (CConcat (c1', c2'), loc))) - | CFold (k1, k2) => + | CMap (k1, k2) => S.bind2 (mfk k1, fn k1' => S.map2 (mfk k2, fn k2' => - (CFold (k1', k2'), loc))) + (CMap (k1', k2'), loc))) | CUnit => S.return2 cAll diff --git a/src/elaborate.sml b/src/elaborate.sml index 39cb85b2..fa97bdf8 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -182,13 +182,10 @@ | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) | L.KWild => kunif loc - fun foldKind (dom, ran, loc)= - (L'.KArrow ((L'.KArrow ((L'.KName, loc), - (L'.KArrow (dom, - (L'.KArrow (ran, ran), loc)), loc)), loc), - (L'.KArrow (ran, - (L'.KArrow ((L'.KRecord dom, loc), - ran), loc)), loc)), loc) + fun mapKind (dom, ran, loc)= + (L'.KArrow ((L'.KArrow (dom, ran), loc), + (L'.KArrow ((L'.KRecord dom, loc), + (L'.KRecord ran, loc)), loc)), loc) fun hnormKind (kAll as (k, _)) = case k of @@ -355,13 +352,13 @@ ((L'.CConcat (c1', c2'), loc), k, D.prove env denv (c1', c2', loc) @ gs1 @ gs2) end - | L.CFold => + | L.CMap => let val dom = kunif loc val ran = kunif loc in - ((L'.CFold (dom, ran), loc), - foldKind (dom, ran, loc), + ((L'.CMap (dom, ran), loc), + mapKind (dom, ran, loc), []) end @@ -489,7 +486,7 @@ | L'.CRecord (k, _) => (L'.KRecord k, loc) | L'.CConcat (c, _) => kindof env c - | L'.CFold (dom, ran) => foldKind (dom, ran, loc) + | L'.CMap (dom, ran) => mapKind (dom, ran, loc) | L'.CUnit => (L'.KUnit, loc) @@ -504,41 +501,21 @@ val hnormCon = D.hnormCon - datatype con_summary = - Nil - | Cons - | Unknown - - fun compatible cs = - case cs of - (Unknown, _) => false - | (_, Unknown) => false - | (s1, s2) => s1 = s2 - - fun summarizeCon (env, denv) c = + fun deConstraintCon (env, denv) c = let val (c, gs) = hnormCon (env, denv) c in case #1 c of - L'.CRecord (_, []) => (Nil, gs) - | L'.CRecord (_, _ :: _) => (Cons, gs) - | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs) - | L'.CDisjoint (_, _, _, c) => + L'.CDisjoint (_, _, _, c) => let - val (s, gs') = summarizeCon (env, denv) c + val (c', gs') = deConstraintCon (env, denv) c in - (s, gs @ gs') + (c', gs @ gs') end - | _ => (Unknown, gs) + | _ => (c, gs) end - fun p_con_summary s = - Print.PD.string (case s of - Nil => "Nil" - | Cons => "Cons" - | Unknown => "Unknown") - - exception SummaryFailure + exception GuessFailure fun isUnitCon env (c, loc) = case c of @@ -574,7 +551,7 @@ | L'.CRecord _ => false | L'.CConcat _ => false - | L'.CFold _ => false + | L'.CMap _ => false | L'.CUnit => true @@ -720,14 +697,14 @@ fun isGuessable (other, fs) = let - val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure) + val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure) in List.all (fn (loc, env, denv, c1, c2) => case D.prove env denv (c1, c2, loc) of [] => true | _ => false) gs end - handle SummaryFailure => false + handle GuessFailure => false val (fs1, fs2, others1, others2) = case (fs1, fs2, others1, others2) of @@ -783,79 +760,68 @@ ("#2", p_summary env s2)]*) end - and guessFold (env, denv) (c1, c2, gs, ex) = + and guessMap (env, denv) (c1, c2, gs, ex) = let val loc = #2 c1 - fun unfold (dom, ran, f, i, r, c) = + fun unfold (dom, ran, f, r, c) = let - val nm = cunif (loc, (L'.KName, loc)) - val v = - case dom of - (L'.KUnit, _) => (L'.CUnit, loc) - | _ => cunif (loc, dom) - val rest = cunif (loc, (L'.KRecord dom, loc)) - val acc = (L'.CFold (dom, ran), loc) - val acc = (L'.CApp (acc, f), loc) - val acc = (L'.CApp (acc, i), loc) - val acc = (L'.CApp (acc, rest), loc) - - val (iS, gs3) = summarizeCon (env, denv) i - - val app = (L'.CApp (f, nm), loc) - val app = (L'.CApp (app, v), loc) - val app = (L'.CApp (app, acc), loc) - val (appS, gs4) = summarizeCon (env, denv) app - - val (cS, gs5) = summarizeCon (env, denv) c - in - (*prefaces "Summaries" [("iS", p_con_summary iS), - ("appS", p_con_summary appS), - ("cS", p_con_summary cS)];*) - - if compatible (iS, appS) then - raise ex - else if compatible (cS, iS) then + fun unfold (r, c) = let - (*val () = prefaces "Same?" [("i", p_con env i), - ("c", p_con env c)]*) - val gs6 = unifyCons (env, denv) i c - (*val () = TextIO.print "Yes!\n"*) - - val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) + val (c', gs1) = deConstraintCon (env, denv) c in - gs @ gs3 @ gs5 @ gs6 @ gs7 - end - else if compatible (cS, appS) then - let - (*val () = prefaces "Same?" [("app", p_con env app), - ("c", p_con env c), - ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*) - val gs6 = unifyCons (env, denv) app c - (*val () = TextIO.print "Yes!\n"*) - - val singleton = (L'.CRecord (dom, [(nm, v)]), loc) - val concat = (L'.CConcat (singleton, rest), loc) - (*val () = prefaces "Pre-crew" [("r", p_con env r), - ("concat", p_con env concat)]*) - val gs7 = unifyCons (env, denv) r concat - in - (*prefaces "The crew" [("nm", p_con env nm), - ("v", p_con env v), - ("rest", p_con env rest)];*) + case #1 c' of + L'.CRecord (_, []) => + let + val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) + in + gs1 @ gs2 + end + | L'.CRecord (_, [(x, v)]) => + let + val v' = case dom of + (L'.KUnit, _) => (L'.CUnit, loc) + | _ => cunif (loc, dom) + val gs2 = unifyCons (env, denv) v' (L'.CApp (f, v), loc) - gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 + val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc) + in + gs1 @ gs2 @ gs3 + end + | L'.CRecord (_, (x, v) :: rest) => + let + val r1 = cunif (loc, (L'.KRecord dom, loc)) + val r2 = cunif (loc, (L'.KRecord dom, loc)) + val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) + + val gs3 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)) + val gs4 = unfold (r2, (L'.CRecord (ran, rest), loc)) + in + gs1 @ gs2 @ gs3 @ gs4 + end + | L'.CConcat (c1', c2') => + let + val r1 = cunif (loc, (L'.KRecord dom, loc)) + val r2 = cunif (loc, (L'.KRecord dom, loc)) + val gs2 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) + + val gs3 = unfold (r1, c1') + val gs4 = unfold (r2, c2') + in + gs1 @ gs2 @ gs3 @ gs4 + end + | _ => raise ex end - else - raise ex + in + unfold (r, c) end handle _ => raise ex in case (#1 c1, #1 c2) of - (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) => - unfold (dom, ran, f, i, r, c2) - | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) => - unfold (dom, ran, f, i, r, c1) + (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) => + unfold (dom, ran, f, r, c2) + | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => + unfold (dom, ran, f, r, c1) | _ => raise ex end @@ -890,7 +856,7 @@ (Time.- (Time.now (), befor)))))];*) gs1 @ gs2 @ gs3 end - handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) + handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex) end and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = @@ -1017,7 +983,7 @@ (r := SOME c1All; []) - | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => + | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => (unifyKinds dom1 dom2; unifyKinds ran1 ran2; []) @@ -2740,7 +2706,7 @@ fun positive self = | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs | CConcat (c1, c2) => none c1 andalso none c2 - | CFold => true + | CMap => true | CUnit => true @@ -2766,7 +2732,7 @@ fun positive self = | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs | CConcat (c1, c2) => pos c1 andalso pos c2 - | CFold => true + | CMap => true | CUnit => true diff --git a/src/elisp/urweb-defs.el b/src/elisp/urweb-defs.el index 5551b7a2..e1382692 100644 --- a/src/elisp/urweb-defs.el +++ b/src/elisp/urweb-defs.el @@ -107,7 +107,7 @@ notion of \"the end of an outline\".") "if" "then" "else" "case" "of" "fn" "fun" "val" "and" "datatype" "type" "open" "include" urweb-module-head-syms - "con" "fold" "where" "extern" "constraint" "constraints" + "con" "map" "where" "extern" "constraint" "constraints" "table" "sequence" "class" "cookie") "Symbols starting an sexp.") @@ -192,7 +192,7 @@ for all symbols and in all lines starting with the given symbol." "The starters of new expressions.") (defconst urweb-exptrail-syms - '("if" "then" "else" "case" "of" "fn" "with" "fold")) + '("if" "then" "else" "case" "of" "fn" "with" "map")) (defconst urweb-pipeheads '("|" "of" "fun" "fn" "and" "datatype") diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el index 223006fc..e7615cc3 100644 --- a/src/elisp/urweb-mode.el +++ b/src/elisp/urweb-mode.el @@ -133,7 +133,7 @@ See doc for the variable `urweb-mode-info'." (defconst urweb-keywords-regexp (urweb-syms-re "and" "case" "class" "con" "constraint" "constraints" - "datatype" "else" "end" "extern" "fn" "fold" + "datatype" "else" "end" "extern" "fn" "map" "fun" "functor" "if" "include" "of" "open" "let" "in" "rec" "sequence" "sig" "signature" "cookie" diff --git a/src/expl.sml b/src/expl.sml index cce0fc22..c0d291b5 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -54,7 +54,7 @@ datatype con' = | CRecord of kind * (con * con) list | CConcat of con * con - | CFold of kind * kind + | CMap of kind * kind | CUnit diff --git a/src/expl_print.sml b/src/expl_print.sml index 2ce0c5e2..7044bfa2 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -149,7 +149,7 @@ fun p_con' par env (c, _) = string "++", space, p_con env c2]) - | CFold _ => string "fold" + | CMap _ => string "map" | CUnit => string "()" | CTuple cs => box [string "(", diff --git a/src/expl_util.sml b/src/expl_util.sml index d2073a23..a2b5f2f6 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -145,12 +145,12 @@ fun mapfoldB {kind = fk, con = fc, bind} = S.map2 (mfc ctx c2, fn c2' => (CConcat (c1', c2'), loc))) - | CFold (k1, k2) => + | CMap (k1, k2) => S.bind2 (mfk k1, fn k1' => S.map2 (mfk k2, fn k2' => - (CFold (k1', k2'), loc))) + (CMap (k1', k2'), loc))) | CUnit => S.return2 cAll diff --git a/src/explify.sml b/src/explify.sml index a10037ef..a4eab0ba 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -63,7 +63,7 @@ fun explifyCon (c, loc) = | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc) | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) - | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc) + | L.CMap (dom, ran) => (L'.CMap (explifyKind dom, explifyKind ran), loc) | L.CUnit => (L'.CUnit, loc) diff --git a/src/monoize.sml b/src/monoize.sml index 4efa2fea..898d3e61 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -206,7 +206,7 @@ fun monoType env = | L.CRecord _ => poly () | L.CConcat _ => poly () - | L.CFold _ => poly () + | L.CMap _ => poly () | L.CUnit => poly () | L.CTuple _ => poly () diff --git a/src/reduce.sml b/src/reduce.sml index b428c01f..949b2a6d 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -103,14 +103,13 @@ fun conAndExp (namedC, namedE) = CAbs (_, _, b) => con (KnownC c2 :: deKnown env) b - | CApp ((CApp ((CFold _, _), f), _), i) => + | CApp ((CMap (dom, ran), _), f) => (case #1 c2 of - CRecord (_, []) => i - | CRecord (k, (x, c) :: rest) => + CRecord (_, []) => (CRecord (ran, []), loc) + | CRecord (_, (x, c) :: rest) => con (deKnown env) - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp (c1, - (CRecord (k, rest), loc)), loc)), loc) + (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc) | _ => (CApp (c1, c2), loc)) | _ => (CApp (c1, c2), loc) @@ -130,7 +129,7 @@ fun conAndExp (namedC, namedE) = (CRecord (k, xcs1 @ xcs2), loc) | _ => (CConcat (c1, c2), loc) end - | CFold _ => all + | CMap _ => all | CUnit => all diff --git a/src/source.sml b/src/source.sml index a5c86f66..d70d0f5d 100644 --- a/src/source.sml +++ b/src/source.sml @@ -60,7 +60,7 @@ datatype con' = | CRecord of (con * con) list | CConcat of con * con - | CFold + | CMap | CUnit diff --git a/src/source_print.sml b/src/source_print.sml index d6568efe..148157c2 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -139,7 +139,7 @@ fun p_con' par (c, _) = string "++", space, p_con c2]) - | CFold => string "fold" + | CMap => string "map" | CUnit => string "()" diff --git a/src/urweb.grm b/src/urweb.grm index 5f2c0575..d425caec 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -184,7 +184,7 @@ 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 | FOLD | UNIT | KUNIT | CLASS + | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS | DATATYPE | OF | TYPE | NAME | ARROW | LARROW | DARROW | STAR | SEMI @@ -681,7 +681,7 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | path DOT INT (CProj ((CVar path, s (pathleft, pathright)), Int64.toInt INT), s (pathleft, INTright)) | UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright)) - | FOLD (CFold, s (FOLDleft, FOLDright)) + | MAP (CMap, s (MAPleft, MAPright)) | UNIT (CUnit, s (UNITleft, UNITright)) | LPAREN ctuplev RPAREN (CTuple ctuplev, s (LPARENleft, RPARENright)) diff --git a/src/urweb.lex b/src/urweb.lex index aef68ad1..29e07194 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -290,6 +290,7 @@ notags = [^<{\n]+; <INITIAL> "and" => (Tokens.AND (pos yypos, pos yypos + size yytext)); <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)); |