2 files changed, 63 insertions(+), 63 deletions(-)

M src/Compiler/CPS.idr
M src/Compiler/CPSI.idr

@@ 9,8 9,6 @@ import Core.Name
 import public Core.TT
 import Libraries.Data.SortedMap
 
-import Compiler.CPSI
-
 public export
 data Atom : Type where
   KLocal : FC -> Name -> Atom


@@ 318,64 316,3 @@ defToCPS (MkNmFun args body) = MkCNFun ((MN "__cps_k" 0)::args) <$> simplifyTwic
 defToCPS (MkNmForeign ccs fargs ty) = pure $ MkCNForeign ccs fargs ty
 defToCPS (MkNmCon tag arity nt) = pure $ MkCNCon tag arity nt
 defToCPS (MkNmError _) = pure $ MkCNError "ERROR"
-
-forgetAtom : Names vars -> CPSI.Atom vars -> Atom
-forgetAtom locs (KLocal fc p) = KLocal fc (getLocName _ locs p)
-forgetAtom _ (KRef fc n) = KRef fc n
-forgetAtom _ (KPrimVal fc c) = KPrimVal fc c
-forgetAtom _ (KErased fc) = KErased fc
-
-mutual
-  forgetExp : Names vars -> CPSExp vars -> CPSNmExp
-  forgetExp locs (KJump fc f args) =
-    KNJump fc (forgetAtom locs f) (map (forgetAtom locs) args)
-  forgetExp locs (KCon fc name ci tag args n cont) =
-    let locs' = addLocs [n] locs in
-    KNCon fc name ci tag (map (forgetAtom locs) args) (getLocName _ locs' First) $
-      forgetExp locs' cont
-  forgetExp locs (KExtPrim fc fn args n cont) =
-    let locs' = addLocs [n] locs in
-    KNExtPrim fc fn (map (forgetAtom locs) args) (getLocName _ locs' First) $
-      forgetExp locs' cont
-  forgetExp locs (KFix fc args body n cont) =
-    let locs' = addLocs [n] locs
-        args' = addLocs args locs
-    in
-    KNFix fc (conArgs args args') (forgetExp args' body) (getLocName _ locs'
-                  First) (forgetExp locs' cont)
-  forgetExp locs (KOp fc fn args n cont) =
-    let locs' = addLocs [n] locs in
-    KNOp fc fn (map (forgetAtom locs) args) (getLocName _ locs' First) $
-      forgetExp locs' cont
-  forgetExp locs (KConCase fc sc alts def) =
-    KNConCase fc (forgetAtom locs sc) (map (forgetConAlt locs) alts)
-              (map (forgetExp locs) def)
-  forgetExp locs (KConstCase fc sc alts def) =
-    KNConstCase fc (forgetAtom locs sc) (map (forgetConstAlt locs) alts)
-              (map (forgetExp locs) def)
-  forgetExp locs (KCrash fc s) = KNCrash fc s
-
-  forgetConAlt : Names vars -> CPSConAlt vars -> CPSNmConAlt
-  forgetConAlt locs (MkKConAlt name ci tag args body) =
-    let locs' = addLocs args locs in
-    MkKNConAlt name ci tag (conArgs args locs') (forgetExp locs' body)
-
-  forgetConstAlt : Names vars -> CPSConstAlt vars -> CPSNmConstAlt
-  forgetConstAlt locs (MkKConstAlt c body) =
-    MkKNConstAlt c (forgetExp locs body)
-
-export
-forget : {vars : _} -> CPSExp vars -> CPSNmExp
-forget {vars} exp =
-  forgetExp (addLocs vars [])
-            (rewrite appendNilRightNeutral vars in exp)
-
-export
-forgetDef : CPSDef -> CPSNamedDef
-forgetDef (MkCFun args e) =
-  let ns = addLocs args []
-      args' = conArgs {vars = []} args ns in
-      MkCNFun args' (forget e)
-forgetDef (MkCCon tag arity nt) = MkCNCon tag arity nt
-forgetDef (MkCForeign ccs args ty) = MkCNForeign ccs args ty
-forgetDef (MkCError err) = MkCNError err

@@ 11,6 11,8 @@ import Core.Core
 import Core.Name
 import public Core.TT
 
+import Compiler.CPS
+
 %default covering
 
 dummy : Int -> Name


@@ 348,3 350,64 @@ defToCPS (MkFun args body) =
 defToCPS (MkForeign ccs fargs ty) = MkCForeign ccs fargs ty
 defToCPS (MkCon tag arity nt) = MkCCon tag arity nt
 defToCPS (MkError _) = MkCError "ERROR"
+
+forgetAtom : Names vars -> CPSI.Atom vars -> Atom
+forgetAtom locs (KLocal fc p) = KLocal fc (getLocName _ locs p)
+forgetAtom _ (KRef fc n) = KRef fc n
+forgetAtom _ (KPrimVal fc c) = KPrimVal fc c
+forgetAtom _ (KErased fc) = KErased fc
+
+mutual
+  forgetExp : Names vars -> CPSExp vars -> CPSNmExp
+  forgetExp locs (KJump fc f args) =
+    KNJump fc (forgetAtom locs f) (map (forgetAtom locs) args)
+  forgetExp locs (KCon fc name ci tag args n cont) =
+    let locs' = addLocs [n] locs in
+    KNCon fc name ci tag (map (forgetAtom locs) args) (getLocName _ locs' First) $
+      forgetExp locs' cont
+  forgetExp locs (KExtPrim fc fn args n cont) =
+    let locs' = addLocs [n] locs in
+    KNExtPrim fc fn (map (forgetAtom locs) args) (getLocName _ locs' First) $
+      forgetExp locs' cont
+  forgetExp locs (KFix fc args body n cont) =
+    let locs' = addLocs [n] locs
+        args' = addLocs args locs
+    in
+    KNFix fc (conArgs args args') (forgetExp args' body) (getLocName _ locs'
+                  First) (forgetExp locs' cont)
+  forgetExp locs (KOp fc fn args n cont) =
+    let locs' = addLocs [n] locs in
+    KNOp fc fn (map (forgetAtom locs) args) (getLocName _ locs' First) $
+      forgetExp locs' cont
+  forgetExp locs (KConCase fc sc alts def) =
+    KNConCase fc (forgetAtom locs sc) (map (forgetConAlt locs) alts)
+              (map (forgetExp locs) def)
+  forgetExp locs (KConstCase fc sc alts def) =
+    KNConstCase fc (forgetAtom locs sc) (map (forgetConstAlt locs) alts)
+              (map (forgetExp locs) def)
+  forgetExp locs (KCrash fc s) = KNCrash fc s
+
+  forgetConAlt : Names vars -> CPSConAlt vars -> CPSNmConAlt
+  forgetConAlt locs (MkKConAlt name ci tag args body) =
+    let locs' = addLocs args locs in
+    MkKNConAlt name ci tag (conArgs args locs') (forgetExp locs' body)
+
+  forgetConstAlt : Names vars -> CPSConstAlt vars -> CPSNmConstAlt
+  forgetConstAlt locs (MkKConstAlt c body) =
+    MkKNConstAlt c (forgetExp locs body)
+
+export
+forget : {vars : _} -> CPSExp vars -> CPSNmExp
+forget {vars} exp =
+  forgetExp (addLocs vars [])
+            (rewrite appendNilRightNeutral vars in exp)
+
+export
+forgetDef : CPSDef -> CPSNamedDef
+forgetDef (MkCFun args e) =
+  let ns = addLocs args []
+      args' = conArgs {vars = []} args ns in
+      MkCNFun args' (forget e)
+forgetDef (MkCCon tag arity nt) = MkCNCon tag arity nt
+forgetDef (MkCForeign ccs args ty) = MkCNForeign ccs args ty
+forgetDef (MkCError err) = MkCNError err