Mercurial > urweb
changeset 71:6431b315a1e3
Elaborate efold
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 26 Jun 2008 11:09:30 -0400 |
| parents | 2e0f3b21fb85 |
| children | 0ee10f4d73cf |
| files | src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/cfold.lac tests/efold.lac |
| diffstat | 10 files changed, 76 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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 "<ERROR>" and p_exp env = p_exp' false env
--- 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
--- 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 =
--- 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)
--- 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)
--- 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
--- 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
--- 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
--- /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]