# HG changeset patch # User Adam Chlipala # Date 1214492970 14400 # Node ID 6431b315a1e34337bc4ba7bbd1e27bd46339d3f7 # Parent 2e0f3b21fb85077aea4fe3a86b6780262a17c546 Elaborate efold diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/elab.sml --- a/src/elab.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/elab.sml Thu Jun 26 11:09:30 2008 -0400 @@ -78,6 +78,7 @@ | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } + | EFold of kind | EError diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/elab_print.sml --- a/src/elab_print.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/elab_print.sml Thu Jun 26 11:09:30 2008 -0400 @@ -88,10 +88,11 @@ p_con' true env c] | CRel n => - if !debug then - string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) - else - string (#1 (E.lookupCRel env n)) + ((if !debug then + string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupCRel env n))) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) | CNamed n => ((if !debug then string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) @@ -248,7 +249,8 @@ box [p_exp' true env e, string ".", p_con' true env c] - + | EFold _ => string "fold" + | EError => string "" and p_exp env = p_exp' false env diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/elab_util.sml --- a/src/elab_util.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/elab_util.sml Thu Jun 26 11:09:30 2008 -0400 @@ -273,6 +273,11 @@ fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) + | EFold k => + S.map2 (mfk k, + fn k' => + (EFold k', loc)) + | EError => S.return2 eAll in mfe diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/elaborate.sml --- a/src/elaborate.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/elaborate.sml Thu Jun 26 11:09:30 2008 -0400 @@ -665,6 +665,15 @@ (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), (L'.CRecord (k, rest), loc)), loc)), loc) + | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') => + let + val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc) + in + hnormCon env + (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), + (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), + rest''), loc)), loc) + end | _ => cAll) | _ => cAll) | _ => cAll) @@ -674,6 +683,9 @@ (case (hnormCon env c1, hnormCon env c2) of ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) => (L'.CRecord (k, xcs1 @ xcs2), loc) + | ((L'.CRecord (_, []), _), c2') => c2' + | ((L'.CConcat (c11, c12), loc), c2') => + hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc) | _ => cAll) | _ => cAll @@ -758,6 +770,10 @@ | (L'.CConcat _, _) => isRecord () | (_, L'.CConcat _) => isRecord () + | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => + (unifyKinds dom1 dom2; + unifyKinds ran1 ran2) + | _ => err CIncompatible end @@ -804,6 +820,28 @@ | 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'.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), + (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) + fun typeof env (e, loc) = case e of L'.EPrim p => primType env p @@ -836,6 +874,7 @@ | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) | L'.EField (_, _, {field, ...}) => field + | L'.EFold dom => foldType (dom, loc) | L'.EError => cerror @@ -988,6 +1027,13 @@ checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft) end + + | L.EFold => + let + val dom = kunif () + in + ((L'.EFold dom, loc), foldType (dom, loc)) + end datatype decl_error = diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/explify.sml --- a/src/explify.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/explify.sml Thu Jun 26 11:09:30 2008 -0400 @@ -79,6 +79,7 @@ | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) + | L.EFold _ => raise Fail "Explify EFold" | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc) diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/lacweb.grm --- a/src/lacweb.grm Thu Jun 26 10:02:34 2008 -0400 +++ b/src/lacweb.grm Thu Jun 26 11:09:30 2008 -0400 @@ -249,6 +249,8 @@ | FLOAT (EPrim (Prim.Float FLOAT), s (FLOATleft, FLOATright)) | STRING (EPrim (Prim.String STRING), s (STRINGleft, STRINGright)) + | FOLD (EFold, s (FOLDleft, FOLDright)) + rexp : ([]) | ident EQ eexp ([(ident, eexp)]) | ident EQ eexp COMMA rexp ((ident, eexp) :: rexp) diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/source.sml --- a/src/source.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/source.sml Thu Jun 26 11:09:30 2008 -0400 @@ -93,6 +93,7 @@ | ERecord of (con * exp) list | EField of exp * con + | EFold withtype exp = exp' located diff -r 2e0f3b21fb85 -r 6431b315a1e3 src/source_print.sml --- a/src/source_print.sml Thu Jun 26 10:02:34 2008 -0400 +++ b/src/source_print.sml Thu Jun 26 11:09:30 2008 -0400 @@ -201,7 +201,7 @@ | EField (e, c) => box [p_exp' true e, string ".", p_con' true c] - + | EFold => string "fold" and p_exp e = p_exp' false e diff -r 2e0f3b21fb85 -r 6431b315a1e3 tests/cfold.lac --- a/tests/cfold.lac Thu Jun 26 10:02:34 2008 -0400 +++ b/tests/cfold.lac Thu Jun 26 11:09:30 2008 -0400 @@ -1,12 +1,15 @@ con currier = fold (fn nm => fn t => fn acc => t -> acc) {} -con greenCurry = currier [] +con greenCurryIngredients :: {Type} = [] +con greenCurry = currier greenCurryIngredients val greenCurry : greenCurry = {} -con redCurry = currier [A = int, B = string] +con redCurryIngredients = [A = int, B = string] +con redCurry = currier redCurryIngredients val redCurry : redCurry = fn x : int => fn y : string => {} -con yellowCurry = currier [A = string, B = int, C = float] +con yellowCurryIngredients = [A = string, B = int, C = float] +con yellowCurry = currier yellowCurryIngredients val yellowCurry : yellowCurry = fn x => fn y => fn z => {} val main = yellowCurry diff -r 2e0f3b21fb85 -r 6431b315a1e3 tests/efold.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/efold.lac Thu Jun 26 11:09:30 2008 -0400 @@ -0,0 +1,6 @@ +val currier : rs :: {Type} -> Cfold.currier rs = + fold [Cfold.currier] (fn nm :: Name => fn t :: Type => fn rest :: {Type} => fn acc => fn x => acc) {} + +val greenCurry : Cfold.greenCurry = currier [Cfold.greenCurryIngredients] +val redCurry : Cfold.redCurry = currier [Cfold.redCurryIngredients] +val yellowCurry : Cfold.yellowCurry = currier [Cfold.yellowCurryIngredients]