From 8327f190c80287003048eaa10857d0f081b551bb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 28 May 2009 12:40:55 -0400 Subject: Fix EDLet elab_util bug --- lib/ur/list.ur | 70 +++++++++++++++++++++++++++--------------------------- lib/ur/listPair.ur | 2 +- src/elab_util.sml | 35 ++++++++++++++------------- src/unnest.sml | 8 ++++--- 4 files changed, 59 insertions(+), 56 deletions(-) diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 90729f5c..8493f2f5 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -1,38 +1,38 @@ datatype t = datatype Basis.list -val show (a ::: Type) (_ : show a) = - let - fun show' (ls : list a) = - case ls of - [] => "[]" - | x :: ls => show x ^ " :: " ^ show' ls - in - mkShow show' - end +val show = fn [a] (_ : show a) => + let + fun show' (ls : list a) = + case ls of + [] => "[]" + | x :: ls => show x ^ " :: " ^ show' ls + in + mkShow show' + end -val rev (a ::: Type) = - let - fun rev' acc (ls : list a) = - case ls of - [] => acc - | x :: ls => rev' (x :: acc) ls - in - rev' [] - end +val rev = fn [a] => + let + fun rev' acc (ls : list a) = + case ls of + [] => acc + | x :: ls => rev' (x :: acc) ls + in + rev' [] + end -val revAppend (a ::: Type) = - let - fun ra (ls : list a) acc = - case ls of - [] => acc - | x :: ls => ra ls (x :: acc) - in - ra - end +val revAppend = fn [a] => + let + fun ra (ls : list a) acc = + case ls of + [] => acc + | x :: ls => ra ls (x :: acc) + in + ra + end -fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 +fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2 -fun mp (a ::: Type) (b ::: Type) f = +fun mp [a] [b] f = let fun mp' acc ls = case ls of @@ -42,7 +42,7 @@ fun mp (a ::: Type) (b ::: Type) f = mp' [] end -fun mapPartial (a ::: Type) (b ::: Type) f = +fun mapPartial [a] [b] f = let fun mp' acc ls = case ls of @@ -54,7 +54,7 @@ fun mapPartial (a ::: Type) (b ::: Type) f = mp' [] end -fun mapX (a ::: Type) (ctx ::: {Unit}) f = +fun mapX [a] [ctx ::: {Unit}] f = let fun mapX' ls = case ls of @@ -64,7 +64,7 @@ fun mapX (a ::: Type) (ctx ::: {Unit}) f = mapX' end -fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f = +fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f = let fun mapM' acc ls = case ls of @@ -74,7 +74,7 @@ fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f = mapM' [] end -fun filter (a ::: Type) f = +fun filter [a] f = let fun fil acc ls = case ls of @@ -84,7 +84,7 @@ fun filter (a ::: Type) f = fil [] end -fun exists (a ::: Type) f = +fun exists [a] f = let fun ex ls = case ls of @@ -98,7 +98,7 @@ fun exists (a ::: Type) f = ex end -fun foldlMap (a ::: Type) (b ::: Type) (c ::: Type) f = +fun foldlMap [a] [b] [c] f = let fun fold ls' st ls = case ls of diff --git a/lib/ur/listPair.ur b/lib/ur/listPair.ur index 9a56f75a..a46cf187 100644 --- a/lib/ur/listPair.ur +++ b/lib/ur/listPair.ur @@ -1,4 +1,4 @@ -fun mapX (a ::: Type) (b ::: Type) (ctx ::: {Unit}) f = +fun mapX [a] [b] [ctx ::: {Unit}] f = let fun mapX' ls1 ls2 = case (ls1, ls2) of diff --git a/src/elab_util.sml b/src/elab_util.sml index c2101ae3..8082cb1e 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -438,29 +438,30 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | ELet (des, e, t) => let - val (des, ctx) = foldl (fn (ed, (des, ctx)) => - let - val ctx' = - case #1 ed of - EDVal (p, _, _) => doVars (p, ctx) - | EDValRec vis => - foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis - in - (S.bind2 (des, - fn des' => - S.map2 (mfed ctx ed, - fn ed' => des' @ [ed'])), - ctx') - end) + val (des, ctx') = foldl (fn (ed, (des, ctx)) => + let + val ctx' = + case #1 ed of + EDVal (p, _, _) => doVars (p, ctx) + | EDValRec vis => + foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) + ctx vis + in + (S.bind2 (des, + fn des' => + S.map2 (mfed ctx ed, + fn ed' => ed' :: des')), + ctx') + end) (S.return2 [], ctx) des in S.bind2 (des, fn des' => - S.bind2 (mfe ctx e, + S.bind2 (mfe ctx' e, fn e' => S.map2 (mfc ctx t, fn t' => - (ELet (des', e', t'), loc)))) + (ELet (rev des', e', t'), loc)))) end | EKAbs (x, e) => @@ -479,7 +480,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = EDVal (p, t, e) => S.bind2 (mfc ctx t, fn t' => - S.map2 (mfe (doVars (p, ctx)) e, + S.map2 (mfe ctx e, fn e' => (EDVal (p, t', e'), loc))) | EDValRec vis => diff --git a/src/unnest.sml b/src/unnest.sml index 3dfa741d..e0245c6f 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -241,10 +241,12 @@ fun exp ((ks, ts), e as old, st : state) = end) (IS.empty, IS.empty) vis - (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n") - val () = app (fn (x, t) => + (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) + (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) + (*val () = app (fn (x, t) => Print.prefaces "Var" [("x", Print.PD.string x), - ("t", ElabPrint.p_con E.empty t)]) ts*) + ("t", ElabPrint.p_con E.empty t)]) ts + val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*) val cfv = IS.foldl (fn (x, cfv) => let -- cgit v1.2.3