From b1d29df128dd1fa879e24f0eb3f5cdc1b74e16b7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 3 Jun 2010 13:04:37 -0400 Subject: Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize --- lib/ur/basis.urs | 2 +- lib/ur/string.ur | 10 ++- src/compiler.sig | 10 ++- src/compiler.sml | 6 +- src/core_print.sml | 11 +++- src/elab_env.sig | 1 + src/elab_env.sml | 9 +++ src/elab_print.sml | 11 +++- src/elab_util.sml | 32 ++++++++- src/especialize.sml | 7 +- src/expl_print.sml | 11 +++- src/monoize.sml | 7 +- src/reduce.sml | 32 +++++++++ src/reduce_local.sml | 179 +++++++++++++++++++++++++++++++++++++++++++-------- src/unnest.sml | 16 ++++- 15 files changed, 295 insertions(+), 49 deletions(-) diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 19983cd2..f2dffd38 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -79,7 +79,7 @@ val strsub : string -> int -> char val strsuffix : string -> int -> string val strchr : string -> char -> option string val strindex : string -> char -> option int -val strcspn : string -> string -> option int +val strcspn : string -> string -> int val substring : string -> int -> int -> string val str1 : char -> string diff --git a/lib/ur/string.ur b/lib/ur/string.ur index f19ce174..f7781e01 100644 --- a/lib/ur/string.ur +++ b/lib/ur/string.ur @@ -11,7 +11,15 @@ val suffix = Basis.strsuffix val index = Basis.strindex val atFirst = Basis.strchr -fun mindex {Haystack = s, Needle = chs} = Basis.strcspn s chs +fun mindex {Haystack = s, Needle = chs} = + let + val n = Basis.strcspn s chs + in + if n >= length s then + None + else + Some n + end fun substring s {Start = start, Len = len} = Basis.substring s start len diff --git a/src/compiler.sig b/src/compiler.sig index 16207e8b..7e3e8ffc 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -129,10 +129,14 @@ signature COMPILER = sig val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform val toShakey : (string, Core.file) transform - val toUnpoly : (string, Core.file) transform - val toSpecialize : (string, Core.file) transform + val toUnpoly : (string, Core.file) transform + val toSpecialize : (string, Core.file) transform val toShake4 : (string, Core.file) transform - val toEspecialize2 : (string, Core.file) transform + val toEspecialize2 : (string, Core.file) transform + val toShake4' : (string, Core.file) transform + val toUnpoly2 : (string, Core.file) transform + val toShake4'' : (string, Core.file) transform + val toEspecialize3 : (string, Core.file) transform val toReduce2 : (string, Core.file) transform val toShake5 : (string, Core.file) transform val toMarshalcheck : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 1d15367f..dcc1e5b3 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1013,8 +1013,12 @@ val toSpecialize = transform specialize "specialize" o toUnpoly val toShake4 = transform shake "shake4" o toSpecialize val toEspecialize2 = transform especialize "especialize2" o toShake4 +val toShake4' = transform shake "shake4'" o toEspecialize2 +val toUnpoly2 = transform unpoly "unpoly2" o toShake4' +val toShake4'' = transform shake "shake4'" o toUnpoly2 +val toEspecialize3 = transform especialize "especialize3" o toShake4'' -val toReduce2 = transform reduce "reduce2" o toEspecialize2 +val toReduce2 = transform reduce "reduce2" o toEspecialize3 val toShake5 = transform shake "shake5" o toReduce2 diff --git a/src/core_print.sml b/src/core_print.sml index fd0556e6..f18ea4b9 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -233,12 +233,19 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/elab_env.sig b/src/elab_env.sig index a5b8751a..769fea58 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -118,6 +118,7 @@ signature ELAB_ENV = sig val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn val patBinds : env -> Elab.pat -> env + val patBindsN : Elab.pat -> int exception Bad of Elab.con * Elab.con diff --git a/src/elab_env.sml b/src/elab_env.sml index dd050c9e..bb34c345 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1512,6 +1512,15 @@ fun patBinds env (p, loc) = | PCon (_, _, _, SOME p) => patBinds env p | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps +fun patBindsN (p, _) = + case p of + PWild => 0 + | PVar _ => 1 + | PPrim _ => 0 + | PCon (_, _, _, NONE) => 0 + | PCon (_, _, _, SOME p) => patBindsN p + | PRecord xps => foldl (fn ((_, p, _), n) => patBindsN p + n) 0 xps + fun edeclBinds env (d, loc) = case d of EDVal (p, _, _) => patBinds env p diff --git a/src/elab_print.sml b/src/elab_print.sml index 86448659..42a0a107 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -252,12 +252,19 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/elab_util.sml b/src/elab_util.sml index 8345e3f3..ec6c51ba 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -429,8 +429,10 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | PRecord xps => foldl (fn ((_, p, _), ctx) => pb (p, ctx)) ctx xps in - S.map2 (mfe (pb (p, ctx)) e, - fn e' => (p, e')) + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfe (pb (p', ctx)) e, + fn e' => (p', e'))) end) pes, fn pes' => S.bind2 (mfc ctx disc, @@ -482,6 +484,32 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn k' => (EKApp (e', k'), loc))) + and mfp ctx (pAll as (p, loc)) = + case p of + PWild => S.return2 pAll + | PVar (x, t) => + S.map2 (mfc ctx t, + fn t' => + (PVar (x, t'), loc)) + | PPrim _ => S.return2 pAll + | PCon (dk, pc, args, po) => + S.bind2 (ListUtil.mapfold (mfc ctx) args, + fn args' => + S.map2 ((case po of + NONE => S.return2 NONE + | SOME p => S.map2 (mfp ctx p, SOME)), + fn po' => + (PCon (dk, pc, args', po'), loc))) + | PRecord xps => + S.map2 (ListUtil.mapfold (fn (x, p, c) => + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfc ctx c, + fn c' => + (x, p', c')))) xps, + fn xps' => + (PRecord xps', loc)) + and mfed ctx (dAll as (d, loc)) = case d of EDVal (p, t, e) => diff --git a/src/especialize.sml b/src/especialize.sml index 7d129b8b..3fa3ea1d 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2009, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -278,7 +278,7 @@ fun specialize' (funcs, specialized) file = NONE => default () | SOME (f, xs) => case IM.find (#funcs st, f) of - NONE => default () + NONE => ((*print ("No find: " ^ Int.toString f ^ "\n");*) default ()) | SOME {name, args, body, typ, tag} => let val (xs, st) = ListUtil.foldlMap (fn (e, st) => exp (env, e, st)) st xs @@ -415,6 +415,8 @@ fun specialize' (funcs, specialized) file = (body', typ') fvs val mns = !mayNotSpec (*val () = mayNotSpec := SS.add (mns, name)*) + (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*) + val body' = ReduceLocal.reduceExp body' (*val () = Print.preface ("PRE", CorePrint.p_exp CoreEnv.empty body')*) val (body', st) = exp (env, body', st) val () = mayNotSpec := mns @@ -424,7 +426,6 @@ fun specialize' (funcs, specialized) file = e' fvs val e' = foldl (fn (arg, e) => (EApp (e, arg), loc)) e' xs - (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*) (*val () = Print.prefaces "Brand new" [("e'", CorePrint.p_exp CoreEnv.empty e'), ("e", CorePrint.p_exp CoreEnv.empty e), diff --git a/src/expl_print.sml b/src/expl_print.sml index 15838729..c953350c 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -234,12 +234,19 @@ fun p_pat' par env (p, _) = | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/monoize.sml b/src/monoize.sml index e2377bae..d43002cb 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2737,7 +2737,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.EFfi ("Basis", "tag"), - _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), + _), (L.CRecord (_, attrsGiven), _)), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), class), _), attrs), _), tag), _), @@ -2768,7 +2768,10 @@ fun monoExp (env, st, fm) (all as (e, loc)) = val (attrs, fm) = monoExp (env, st, fm) attrs val attrs = case #1 attrs of L'.ERecord xes => xes - | _ => raise Fail "Non-record attributes!" + | _ => map (fn ((L.CName x, _), t) => (x, (L'.EField (attrs, x), loc), monoType env t) + | (c, t) => (E.errorAt loc "Non-constant field name for HTML tag attribute"; + Print.eprefaces' [("Name", CorePrint.p_con env c)]; + ("", (L'.EField (attrs, ""), loc), monoType env t))) attrsGiven val attrs = if List.exists (fn ("Link", _, _) => true diff --git a/src/reduce.sml b/src/reduce.sml index b2911a5f..963863e8 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -65,6 +65,18 @@ val dangling = CoreUtil.Exp.RelE _ => n + 1 | _ => n} +val cdangling = + CoreUtil.Exp.existsB {kind = fn _ => false, + con = fn (n, c) => + case c of + CRel n' => n' >= n + | _ => false, + exp = fn _ => false, + bind = fn (n, b) => + case b of + CoreUtil.Exp.RelC _ => n + 1 + | _ => n} + datatype env_item = UnknownK | KnownK of kind @@ -86,6 +98,15 @@ val edepth' = foldl (fn (UnknownE, n) => n + 1 | (Lift (_, _, n'), n) => n + n' | (_, n) => n) 0 +val cdepth = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (_, n) => n) 0 + +val cdepth' = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (Lift (_, n', _), n) => n + n' + | (_, n) => n) 0 + type env = env_item list fun ei2s ei = @@ -344,6 +365,11 @@ fun kindConAndExp (namedC, namedE) = raise Fail "!") else ()*) + (*val () = if cdangling (cdepth env) all then + Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("env", Print.PD.string (e2s env))] + else + ()*) val r = case e of EPrim _ => all @@ -636,6 +662,12 @@ fun kindConAndExp (namedC, namedE) = raise Fail "!!") else ();*) + (*if cdangling (cdepth' (deKnown env)) r then + (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("r", CorePrint.p_exp CoreEnv.empty r)]; + raise Fail "!!") + else + ();*) r end in diff --git a/src/reduce_local.sml b/src/reduce_local.sml index 4c5ab52e..43317b9e 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -43,11 +43,15 @@ datatype env_item = Unknown | Known of exp - | Lift of int + | UnknownC + | KnownC of con + + | Lift of int * int type env = env_item list val deKnown = List.filter (fn Known _ => false + | KnownC _ => false | _ => true) datatype result = Yes of env | No | Maybe @@ -120,39 +124,140 @@ fun match (env, p : pat, e : exp) = match (env, p, e) end +fun con env (all as (c, loc)) = + ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) + case c of + TFun (c1, c2) => (TFun (con env c1, con env c2), loc) + | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) + | TKFun (x, c2) => (TKFun (x, con env c2), loc) + | TRecord c => (TRecord (con env c), loc) + + | CRel n => + let + fun find (n', env, nudge, liftC) = + case env of + [] => raise Fail "Reduce.con: CRel" + | Unknown :: rest => find (n', rest, nudge, liftC) + | Known _ :: rest => find (n', rest, nudge, liftC) + | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC', + liftC + liftC') + | UnknownC :: rest => + if n' = 0 then + (CRel (n + nudge), loc) + else + find (n' - 1, rest, nudge, liftC + 1) + | KnownC c :: rest => + if n' = 0 then + con (Lift (liftC, 0) :: rest) c + else + find (n' - 1, rest, nudge - 1, liftC) + in + (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) + find (n, env, 0, 0) + end + | CNamed _ => all + | CFfi _ => all + | CApp (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case #1 c1 of + CAbs (_, _, b) => + con (KnownC c2 :: deKnown env) b + + | CApp ((CMap (dom, ran), _), f) => + (case #1 c2 of + CRecord (_, []) => (CRecord (ran, []), loc) + | CRecord (_, (x, c) :: rest) => + con (deKnown env) + (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) + end + | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) + + | CKApp (c1, k) => + let + val c1 = con env c1 + in + case #1 c1 of + CKAbs (_, b) => + con (deKnown env) b + + | _ => (CKApp (c1, k), loc) + end + | CKAbs (x, b) => (CKAbs (x, con env b), loc) + + | CName _ => all + + | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) + | CConcat (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case (#1 c1, #1 c2) of + (CRecord (k, xcs1), CRecord (_, xcs2)) => + (CRecord (k, xcs1 @ xcs2), loc) + | (CRecord (_, []), _) => c2 + | (_, CRecord (_, [])) => c1 + | _ => (CConcat (c1, c2), loc) + end + | CMap _ => all + + | CUnit => all + + | CTuple cs => (CTuple (map (con env) cs), loc) + | CProj (c, n) => + let + val c = con env c + in + case #1 c of + CTuple cs => List.nth (cs, n - 1) + | _ => (CProj (c, n), loc) + end) + +fun patCon pc = + case pc of + PConVar _ => pc + | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => + PConFfi {mod = m, datatyp = datatyp, params = params, con = c, + arg = Option.map (con (map (fn _ => UnknownC) params)) arg, + kind = kind} + fun exp env (all as (e, loc)) = case e of EPrim _ => all | ERel n => let - fun find (n', env, nudge, lift) = + fun find (n', env, nudge, liftC, liftE) = case env of [] => (ERel (n + nudge), loc) - | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift') + | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE') + | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) + | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) | Unknown :: rest => if n' = 0 then (ERel (n + nudge), loc) else - find (n' - 1, rest, nudge, lift + 1) + find (n' - 1, rest, nudge, liftC, liftE + 1) | Known e :: rest => if n' = 0 then ((*print "SUBSTITUTING\n";*) - exp (Lift lift :: rest) e) + exp (Lift (liftC, liftE) :: rest) e) else - find (n' - 1, rest, nudge - 1, lift) + find (n' - 1, rest, nudge - 1, liftC, liftE) in - find (n, env, 0, 0) + find (n, env, 0, 0, 0) end | ENamed _ => all - | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc) + | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) cs, Option.map (exp env) eo), loc) | EFfi _ => all | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) - | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _, - (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _), - t), _), e) => - (ECon (dk, pc, [t], SOME (exp env e)), loc) - | EApp (e1, e2) => let val e1 = exp env e1 @@ -163,21 +268,28 @@ fun exp env (all as (e, loc)) = | _ => (EApp (e1, e2), loc) end - | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) + | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc) - | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) => - (ECon (dk, pc, [t], NONE), loc) + | ECApp (e, c) => + let + val e = exp env e + val c = con env c + in + case #1 e of + ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b + | _ => (ECApp (e, c), loc) + end - | ECApp (e, c) => (ECApp (exp env e, c), loc) - | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) + | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) | EKApp (e, k) => (EKApp (exp env e, k), loc) | EKAbs (x, e) => (EKAbs (x, exp env e), loc) - | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc) + | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) | EField (e, c, others) => let val e = exp env e + val c = con env c fun default () = (EField (e, c, others), loc) in @@ -189,12 +301,16 @@ fun exp env (all as (e, loc)) = | _ => default () end - | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc) - | ECut (e, c, others) => (ECut (exp env e, c, others), loc) - | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) + | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc) + | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e, + con env c, + {field = con env f, rest = con env r}), loc) + | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc) - | ECase (e, pes, others) => + | ECase (e, pes, {disc = d, result = r}) => let + val others = {disc = con env d, result = con env r} + fun patBinds (p, _) = case p of PWild => 0 @@ -204,9 +320,18 @@ fun exp env (all as (e, loc)) = | PCon (_, _, _, SOME p) => patBinds p | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts + fun pat (all as (p, loc)) = + case p of + PWild => all + | PVar (x, t) => (PVar (x, con env t), loc) + | PPrim _ => all + | PCon (dk, pc, cs, po) => + (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) + | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) + fun push () = (ECase (exp env e, - map (fn (p, e) => (p, + map (fn (p, e) => (pat p, exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e)) pes, others), loc) @@ -226,9 +351,9 @@ fun exp env (all as (e, loc)) = | EWrite e => (EWrite (exp env e), loc) | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) - | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc) - | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc) + | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc) fun reduce file = let diff --git a/src/unnest.sml b/src/unnest.sml index 77589bfb..a2ec32b0 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -204,12 +204,19 @@ fun exp ((ks, ts), e as old, st : state) = | PRecord xpcs => foldl (fn ((_, p, _), ts) => doVars (p, ts)) ts xpcs + + fun bindOne subs = ((0, (ERel 0, #2 ed)) + :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs) + + fun bindMany (n, subs) = + case n of + 0 => subs + | _ => bindMany (n - 1, bindOne subs) in ([(EDVal (p, t, e), #2 ed)], (doVars (p, ts), maxName, ds, - ((0, (ERel 0, #2 ed)) - :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), + bindMany (E.patBindsN p, subs), by)) end | EDValRec vis => @@ -310,6 +317,7 @@ fun exp ((ks, ts), e as old, st : state) = let (*val () = print (Int.toString ex ^ "\n")*) val (name, t') = List.nth (ts, ex) + val t' = squishCon cfv t' in ((EAbs (name, t', @@ -354,6 +362,8 @@ fun exp ((ks, ts), e as old, st : state) = (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) + (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)), + ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*) (ELet (eds, e', t), {maxName = maxName, decls = ds}) -- cgit v1.2.3