summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 15:58:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-01 15:58:55 -0400
commit6578fad1ed0871839d4b99a40cd626d4f39bf162 (patch)
treef4112230acc95c284530da52a823ff9b88516349 /src
parent3c78af90b54d01c97ab75fd7290281dfb96921ee (diff)
First Unnest tests working
Diffstat (limited to 'src')
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml9
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml29
-rw-r--r--src/elab_print.sml4
-rw-r--r--src/elab_util.sig25
-rw-r--r--src/elab_util.sml107
-rw-r--r--src/sources3
-rw-r--r--src/termination.sml2
-rw-r--r--src/unnest.sig34
-rw-r--r--src/unnest.sml369
11 files changed, 583 insertions, 5 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index e26ec13c..bc1974a1 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -58,6 +58,7 @@ signature COMPILER = sig
val parse : (job, Source.file) phase
val elaborate : (Source.file, Elab.file) phase
+ val unnest : (Elab.file, Elab.file) phase
val termination : (Elab.file, Elab.file) phase
val explify : (Elab.file, Expl.file) phase
val corify : (Expl.file, Core.file) phase
@@ -80,6 +81,7 @@ signature COMPILER = sig
val toParseJob : (string, job) transform
val toParse : (string, Source.file) transform
val toElaborate : (string, Elab.file) transform
+ val toUnnest : (string, Elab.file) transform
val toTermination : (string, Elab.file) transform
val toExplify : (string, Expl.file) transform
val toCorify : (string, Core.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index 4f1bce11..e92f86c3 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -383,12 +383,19 @@ val elaborate = {
val toElaborate = transform elaborate "elaborate" o toParse
+val unnest = {
+ func = Unnest.unnest,
+ print = ElabPrint.p_file ElabEnv.empty
+}
+
+val toUnnest = transform unnest "unnest" o toElaborate
+
val termination = {
func = (fn file => (Termination.check file; file)),
print = ElabPrint.p_file ElabEnv.empty
}
-val toTermination = transform termination "termination" o toElaborate
+val toTermination = transform termination "termination" o toUnnest
val explify = {
func = Explify.explify,
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 727ee259..90cf8153 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -30,6 +30,10 @@ signature ELAB_ENV = sig
exception SynUnif
val liftConInCon : int -> Elab.con -> Elab.con
+ val liftExpInExp : int -> Elab.exp -> Elab.exp
+
+ val subExpInExp : (int * Elab.exp) -> Elab.exp -> Elab.exp
+
type env
val empty : env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f4f5d2cb..2732de13 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -61,6 +61,20 @@ val liftConInCon =
val lift = liftConInCon 0
+val liftConInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ CRel xn =>
+ if xn < bound then
+ c
+ else
+ CRel (xn + 1)
+ | _ => c,
+ exp = fn _ => fn e => e,
+ bind = fn (bound, U.Exp.RelC _) => bound + 1
+ | (bound, _) => bound}
+
val liftExpInExp =
U.Exp.mapB {kind = fn k => k,
con = fn _ => fn c => c,
@@ -78,6 +92,21 @@ val liftExpInExp =
val liftExp = liftExpInExp 0
+val subExpInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn _ => fn c => c,
+ exp = fn (xn, rep) => fn e =>
+ case e of
+ ERel xn' =>
+ (case Int.compare (xn', xn) of
+ EQUAL => #1 rep
+ | GREATER=> ERel (xn' - 1)
+ | LESS => e)
+ | _ => e,
+ bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+ | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
+ | (ctx, _) => ctx}
+
(* Back to environments *)
datatype 'a var' =
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 3d7ce625..b236954e 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -198,7 +198,7 @@ fun p_patCon env pc =
string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
else
string (#1 (E.lookupENamed env n)))
- handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+ handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
| PConProj (m1, ms, x) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
@@ -247,7 +247,7 @@ fun p_exp' par env (e, _) =
string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
else
string (#1 (E.lookupENamed env n)))
- handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+ handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
| EModProj (m1, ms, x) =>
let
val m1x = #1 (E.lookupStrNamed env m1)
diff --git a/src/elab_util.sig b/src/elab_util.sig
index f4edd972..f9988981 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -57,6 +57,11 @@ structure Con : sig
-> Elab.con -> Elab.con
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool} -> Elab.con -> bool
+
+ val foldB : {kind : Elab.kind' * 'state -> 'state,
+ con : 'context * Elab.con' * 'state -> 'state,
+ bind : 'context * binder -> 'context}
+ -> 'context -> 'state -> Elab.con -> 'state
end
structure Exp : sig
@@ -83,6 +88,12 @@ structure Exp : sig
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool,
exp : Elab.exp' -> bool} -> Elab.exp -> bool
+
+ val foldB : {kind : Elab.kind' * 'state -> 'state,
+ con : 'context * Elab.con' * 'state -> 'state,
+ exp : 'context * Elab.exp' * 'state -> 'state,
+ bind : 'context * binder -> 'context}
+ -> 'context -> 'state -> Elab.exp -> 'state
end
structure Sgn : sig
@@ -156,6 +167,20 @@ structure Decl : sig
str : Elab.str' -> 'a option,
decl : Elab.decl' -> 'a option}
-> Elab.decl -> 'a option
+
+ val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state,
+ con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
+ exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
+ sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
+ sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
+ str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
+ decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
+ bind : 'context * binder -> 'context}
+ -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
+end
+
+structure File : sig
+ val maxName : Elab.file -> int
end
end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 28fe8f22..2e190d1e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -226,6 +226,13 @@ fun exists {kind, con} k =
S.Return _ => true
| S.Continue _ => false
+fun foldB {kind, con, bind} ctx st c =
+ case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+ con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
+ bind = bind} ctx c st of
+ S.Continue (_, st) => st
+ | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
+
end
structure Exp = struct
@@ -340,8 +347,20 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
S.bind2 (mfe ctx e,
fn e' =>
S.bind2 (ListUtil.mapfold (fn (p, e) =>
- S.map2 (mfe ctx e,
- fn e' => (p, e'))) pes,
+ let
+ fun pb ((p, _), ctx) =
+ case p of
+ PWild => ctx
+ | PVar (x, t) => bind (ctx, RelE (x, t))
+ | PPrim _ => ctx
+ | PCon (_, _, _, NONE) => ctx
+ | PCon (_, _, _, SOME p) => pb (p, ctx)
+ | PRecord xps => foldl (fn ((_, p, _), ctx) =>
+ pb (p, ctx)) ctx xps
+ in
+ S.map2 (mfe (pb (p, ctx)) e,
+ fn e' => (p, e'))
+ end) pes,
fn pes' =>
S.bind2 (mfc ctx disc,
fn disc' =>
@@ -431,6 +450,14 @@ fun mapB {kind, con, exp, bind} ctx e =
S.Continue (e, ()) => e
| S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
+fun foldB {kind, con, exp, bind} ctx st e =
+ case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)),
+ con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
+ exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
+ bind = bind} ctx e st of
+ S.Continue (_, st) => st
+ | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
+
end
structure Sgn = struct
@@ -888,6 +915,82 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
S.Return x => SOME x
| S.Continue _ => NONE
+fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
+ case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)),
+ con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
+ exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
+ sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
+ sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
+ str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
+ decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
+ bind = bind} ctx d st of
+ S.Continue x => x
+ | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
+
+end
+
+structure File = struct
+
+fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
+
+and maxNameDecl (d, _) =
+ case d of
+ DCon (_, n, _, _) => n
+ | DDatatype (_, n, _, ns) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ n ns
+ | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ (Int.max (n1, n2)) ns
+ | DVal (_, n, _, _) => n
+ | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
+ | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
+ | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+ | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+ | DConstraint _ => 0
+ | DClass (_, n, _) => n
+ | DExport _ => 0
+ | DTable (n, _, _, _) => n
+ | DSequence (n, _, _) => n
+ | DDatabase _ => 0
+
+and maxNameStr (str, _) =
+ case str of
+ StrConst ds => maxName ds
+ | StrVar n => n
+ | StrProj (str, _) => maxNameStr str
+ | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
+ | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
+ | StrError => 0
+
+and maxNameSgn (sgn, _) =
+ case sgn of
+ SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
+ | SgnVar n => n
+ | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
+ | SgnWhere (sgn, _, _) => maxNameSgn sgn
+ | SgnProj (n, _, _) => n
+ | SgnError => 0
+
+and maxNameSgi (sgi, _) =
+ case sgi of
+ SgiConAbs (_, n, _) => n
+ | SgiCon (_, n, _, _) => n
+ | SgiDatatype (_, n, _, ns) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ n ns
+ | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
+ foldl (fn ((_, n', _), m) => Int.max (n', m))
+ (Int.max (n1, n2)) ns
+ | SgiVal (_, n, _) => n
+ | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+ | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
+ | SgiConstraint _ => 0
+ | SgiTable (n, _, _, _) => n
+ | SgiSequence (n, _, _) => n
+ | SgiClassAbs (_, n) => n
+ | SgiClass (_, n, _) => n
+
end
end
diff --git a/src/sources b/src/sources
index ebf71d9e..984b5e23 100644
--- a/src/sources
+++ b/src/sources
@@ -50,6 +50,9 @@ elab_err.sml
elaborate.sig
elaborate.sml
+unnest.sig
+unnest.sml
+
termination.sig
termination.sml
diff --git a/src/termination.sml b/src/termination.sml
index b0716eca..6ed4d92f 100644
--- a/src/termination.sml
+++ b/src/termination.sml
@@ -292,6 +292,8 @@ fun declOk' env (d, loc) =
| EError => (Rabble, calls)
| EUnif (ref (SOME e)) => exp parent (penv, calls) e
| EUnif (ref NONE) => (Rabble, calls)
+
+ | ELet (_, e) => exp parent (penv, calls) e
end
fun doVali (i, (_, f, _, e), calls) =
diff --git a/src/unnest.sig b/src/unnest.sig
new file mode 100644
index 00000000..6508a781
--- /dev/null
+++ b/src/unnest.sig
@@ -0,0 +1,34 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Remove nested function definitions *)
+
+signature UNNEST = sig
+
+ val unnest : Elab.file -> Elab.file
+
+end
diff --git a/src/unnest.sml b/src/unnest.sml
new file mode 100644
index 00000000..e5eddc42
--- /dev/null
+++ b/src/unnest.sml
@@ -0,0 +1,369 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ *
+ * - Redistributions of source code must retain the above copyright notice,
+ * this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright notice,
+ * this list of conditions and the following disclaimer in the documentation
+ * and/or other materials provided with the distribution.
+ * - The names of contributors may not be used to endorse or promote products
+ * derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(* Remove nested function definitions *)
+
+structure Unnest :> UNNEST = struct
+
+open Elab
+
+structure E = ElabEnv
+structure U = ElabUtil
+
+structure IS = IntBinarySet
+
+val fvsCon = U.Con.foldB {kind = fn (_, st) => st,
+ con = fn (cb, c, cvs) =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ IS.add (cvs, n - cb)
+ else
+ cvs
+ | _ => cvs,
+ bind = fn (cb, b) =>
+ case b of
+ U.Con.Rel _ => cb + 1
+ | _ => cb}
+ 0 IS.empty
+
+fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st,
+ con = fn ((cb, eb), c, st as (cvs, evs)) =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ (IS.add (cvs, n - cb), evs)
+ else
+ st
+ | _ => st,
+ exp = fn ((cb, eb), e, st as (cvs, evs)) =>
+ case e of
+ ERel n =>
+ if n >= eb then
+ (cvs, IS.add (evs, n - eb))
+ else
+ st
+ | _ => st,
+ bind = fn (ctx as (cb, eb), b) =>
+ case b of
+ U.Exp.RelC _ => (cb + 1, eb)
+ | U.Exp.RelE _ => (cb, eb + 1)
+ | _ => ctx}
+ (0, nr) (IS.empty, IS.empty)
+
+fun positionOf (x : int) ls =
+ let
+ fun po n ls =
+ case ls of
+ [] => raise Fail "Unnest.positionOf"
+ | x' :: ls' =>
+ if x' = x then
+ n
+ else
+ po (n + 1) ls'
+ in
+ po 0 ls
+ handle Fail _ => raise Fail ("Unnset.positionOf("
+ ^ Int.toString x
+ ^ ", "
+ ^ String.concatWith ";" (map Int.toString ls)
+ ^ ")")
+ end
+
+fun squishCon cfv =
+ U.Con.mapB {kind = fn k => k,
+ con = fn cb => fn c =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ CRel (positionOf (n - cb) cfv + cb)
+ else
+ c
+ | _ => c,
+ bind = fn (cb, b) =>
+ case b of
+ U.Con.Rel _ => cb + 1
+ | _ => cb}
+ 0
+
+fun squishExp (nr, cfv, efv) =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn (cb, eb) => fn c =>
+ case c of
+ CRel n =>
+ if n >= cb then
+ CRel (positionOf (n - cb) cfv + cb)
+ else
+ c
+ | _ => c,
+ exp = fn (cb, eb) => fn e =>
+ case e of
+ ERel n =>
+ if n >= eb then
+ ERel (positionOf (n - eb) efv + eb)
+ else
+ e
+ | _ => e,
+ bind = fn (ctx as (cb, eb), b) =>
+ case b of
+ U.Exp.RelC _ => (cb + 1, eb)
+ | U.Exp.RelE _ => (cb, eb + 1)
+ | _ => ctx}
+ (0, nr)
+
+type state = {
+ maxName : int,
+ decls : decl list
+}
+
+fun kind (k, st) = (k, st)
+
+fun exp ((ks, ts), e, st : state) =
+ case e of
+ ELet (eds, e) =>
+ let
+ val doSubst = foldl (fn (p, e) => E.subExpInExp p e)
+
+ val (eds, (maxName, ds, subs)) =
+ ListUtil.foldlMapConcat
+ (fn (ed, (maxName, ds, subs)) =>
+ case #1 ed of
+ EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs))
+ | EDValRec vis =>
+ let
+ val loc = #2 ed
+
+ val nr = length vis
+ val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) =>
+ let
+ val (cfv', efv') = fvsExp nr e
+ (*val () = Print.prefaces "fvsExp"
+ [("e", ElabPrint.p_exp E.empty e),
+ ("cfv", Print.PD.string
+ (Int.toString (IS.numItems cfv'))),
+ ("efv", Print.PD.string
+ (Int.toString (IS.numItems efv')))]*)
+ val cfv'' = fvsCon t
+ in
+ (IS.union (cfv, IS.union (cfv', cfv'')),
+ IS.union (efv, efv'))
+ end)
+ (IS.empty, IS.empty) vis
+
+ (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*)
+ val cfv = IS.foldl (fn (x, cfv) =>
+ let
+ (*val () = print (Int.toString x ^ "\n")*)
+ val (_, t) = List.nth (ts, x)
+ in
+ IS.union (cfv, fvsCon t)
+ end)
+ cfv efv
+ (*val () = print "B\n"*)
+
+ val (vis, maxName) =
+ ListUtil.foldlMap (fn ((x, t, e), maxName) =>
+ ((x, maxName, t, e),
+ maxName + 1))
+ maxName vis
+
+ fun apply e =
+ let
+ val e = IS.foldl (fn (x, e) =>
+ (ECApp (e, (CRel x, loc)), loc))
+ e cfv
+ in
+ IS.foldl (fn (x, e) =>
+ (EApp (e, (ERel x, loc)), loc))
+ e efv
+ end
+
+ val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs
+
+ val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) =>
+ let
+ val e = apply (ENamed n, loc)
+ in
+ (0, E.liftExpInExp (nr - i - 1) e)
+ end)
+ vis
+ val subs' = rev subs'
+
+ val cfv = IS.listItems cfv
+ val efv = IS.listItems efv
+ val efn = length efv
+
+ (*val subsInner = subs
+ @ map (fn (i, e) =>
+ (i + efn,
+ E.liftExpInExp efn e)) subs'*)
+
+ val subs = subs @ subs'
+
+ val vis = map (fn (x, n, t, e) =>
+ let
+ (*val () = Print.prefaces "preSubst"
+ [("e", ElabPrint.p_exp E.empty e)]*)
+ val e = doSubst e subs(*Inner*)
+
+ (*val () = Print.prefaces "squishCon"
+ [("t", ElabPrint.p_con E.empty t)]*)
+ val t = squishCon cfv t
+ (*val () = Print.prefaces "squishExp"
+ [("e", ElabPrint.p_exp E.empty e)]*)
+ val e = squishExp (nr, cfv, efv) e
+
+ val (e, t) = foldr (fn (ex, (e, t)) =>
+ let
+ val (name, t') = List.nth (ts, ex)
+ in
+ ((EAbs (name,
+ t',
+ t,
+ e), loc),
+ (TFun (t',
+ t), loc))
+ end)
+ (e, t) efv
+
+ val (e, t) = foldr (fn (cx, (e, t)) =>
+ let
+ val (name, k) = List.nth (ks, cx)
+ in
+ ((ECAbs (Explicit,
+ name,
+ k,
+ e), loc),
+ (TCFun (Explicit,
+ name,
+ k,
+ t), loc))
+ end)
+ (e, t) cfv
+ in
+ (x, n, t, e)
+ end)
+ vis
+
+ val d = (DValRec vis, #2 ed)
+ in
+ ([], (maxName, d :: ds, subs))
+ end)
+ (#maxName st, #decls st, []) eds
+ in
+ (ELet (eds, doSubst e subs),
+ {maxName = maxName,
+ decls = ds})
+ end
+
+ | _ => (e, st)
+
+fun default (ctx, d, st) = (d, st)
+
+fun bind ((ks, ts), b) =
+ case b of
+ U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts)
+ | U.Decl.RelE p => (ks, p :: ts)
+ | _ => (ks, ts)
+
+val unnestDecl = U.Decl.foldMapB {kind = kind,
+ con = default,
+ exp = exp,
+ sgn_item = default,
+ sgn = default,
+ str = default,
+ decl = default,
+ bind = bind}
+ ([], [])
+
+fun unnest file =
+ let
+ fun doDecl (all as (d, loc), st : state) =
+ let
+ fun default () = ([all], st)
+ fun explore () =
+ let
+ val (d, st) = unnestDecl st all
+ in
+ (rev (d :: #decls st),
+ {maxName = #maxName st,
+ decls = []})
+ end
+ in
+ case d of
+ DCon _ => default ()
+ | DDatatype _ => default ()
+ | DDatatypeImp _ => default ()
+ | DVal _ => explore ()
+ | DValRec _ => explore ()
+ | DSgn _ => default ()
+ | DStr (x, n, sgn, str) =>
+ let
+ val (str, st) = doStr (str, st)
+ in
+ ([(DStr (x, n, sgn, str), loc)], st)
+ end
+ | DFfiStr _ => default ()
+ | DConstraint _ => default ()
+ | DExport _ => default ()
+ | DTable _ => default ()
+ | DSequence _ => default ()
+ | DClass _ => default ()
+ | DDatabase _ => default ()
+ end
+
+ and doStr (all as (str, loc), st) =
+ let
+ fun default () = (all, st)
+ in
+ case str of
+ StrConst ds =>
+ let
+ val (ds, st) = ListUtil.foldlMapConcat doDecl st ds
+ in
+ ((StrConst ds, loc), st)
+ end
+ | StrVar _ => default ()
+ | StrProj _ => default ()
+ | StrFun (x, n, dom, ran, str) =>
+ let
+ val (str, st) = doStr (str, st)
+ in
+ ((StrFun (x, n, dom, ran, str), loc), st)
+ end
+ | StrApp _ => default ()
+ | StrError => raise Fail "Unnest: StrError"
+ end
+
+ val (ds, _) = ListUtil.foldlMapConcat doDecl
+ {maxName = U.File.maxName file + 1,
+ decls = []} file
+ in
+ ds
+ end
+
+end