WIP delete me later (it compiles with holes, need filling)

(cherry picked from commit 3578f70)

Author: GulinSS

src/Compiler/ANF.idr

@@ -194,12 +194,12 @@ mlet fc val sc
 
 bindAsFresh :
   {auto v : Ref Next Int} ->
-  (args : List Name) -> AVars vars' ->
-  Core (List Int, AVars (Scope.ext vars' args))
-bindAsFresh [] vs = pure ([], vs)
-bindAsFresh (n :: ns) vs
+  (args : Scope) -> AVars vars' ->
+  Core (List Int, AVars (vars' ++ args))
+bindAsFresh [<] vs = pure ([], vs)
+bindAsFresh (ns :< n) vs
     = do i <- nextVar
-         mapFst (i ::) <$> bindAsFresh ns (vs :< i)
+         bimap (i ::) (:< i) <$> bindAsFresh ns vs
 
 mutual
   anfArgs : {auto v : Ref Next Int} ->
@@ -211,7 +211,7 @@ mutual
 
   anf : {auto v : Ref Next Int} ->
         AVars vars -> Lifted vars -> Core ANF
-  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs))
+  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup vs p))
   anf vs (LAppName fc lazy n args)
       = anfArgs fc vs args (AAppName fc lazy n)
   anf vs (LUnderApp fc n m args)
@@ -264,12 +264,12 @@ export
 toANF : LiftedDef -> Core ANFDef
 toANF (MkLFun args scope sc)
     = do v <- newRef Next (the Int 0)
-         (iargs, vsNil) <- bindAsFresh (cast args) AVars.empty
+         (iargs, vsNil) <- bindAsFresh args AVars.empty
          let vs : AVars args
            := rewrite sym $ appendLinLeftNeutral args in
-              rewrite snocAppendAsFish Scope.empty args in vsNil
-         (iargs', vs) <- bindAsFresh (cast scope) vs
-         sc' <- anf (rewrite snocAppendAsFish args scope in vs) sc
+              vsNil
+         (iargs', vs) <- bindAsFresh scope vs
+         sc' <- anf vs sc
          pure $ MkAFun (iargs ++ iargs') sc'
 toANF (MkLCon t a ns) = pure $ MkACon t a ns
 toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t

src/Compiler/CaseOpts.idr

@@ -47,9 +47,9 @@ shiftVar : {outer : Scope} -> {args : List Name} ->
            NVar n ((vars :< x <>< args) ++ outer)
 shiftVar nvar
   = let out = mkSizeOf outer in
-    case locateNVar out nvar of
+    case locateNVar out (?sdfd nvar) of
       Left nvar => embed nvar
-      Right (MkNVar p) => weakenNs out (shiftUndersN (mkSizeOf _) p)
+      Right (MkNVar p) => weakenNs out (shiftUndersN (mkSizeOf _) (?sdf p))
 
 mutual
   shiftBinder : {outer, args : _} ->
@@ -95,11 +95,13 @@ mutual
                 CConAlt (((vars <>< args) :< old) ++ outer) ->
                 CConAlt ((vars :< new <>< args) ++ outer)
   shiftBinderConAlt new (MkConAlt n ci t args' sc)
-      = let sc' : CExp (((vars <>< args) :< old) ++ (outer <>< args'))
-                = rewrite sym $ snocAppendFishAssociative (vars <>< args :< old) outer args' in sc in
+      = let sc' : CExp (((vars <>< args) :< old) ++ (Scope.addInner outer args'))
+                -- = rewrite sym $ snocAppendFishAssociative (vars <>< args :< old) outer (?sdfdf args') in sc in
+                = (?sdfd2 sc) in
         MkConAlt n ci t args' $
-           rewrite snocAppendFishAssociative (vars :< new <>< args) outer args'
-             in shiftBinder new {outer = outer <>< args'} sc'
+        --    rewrite snocAppendFishAssociative (vars :< new <>< args) outer (?fdgdfg args')
+        --      in shiftBinder new {outer = outer <>< args'} sc'
+           ?sdfdsf $ shiftBinder new (?vbnvvbn sc')
 
   shiftBinderConstAlt : {outer, args : _} ->
                 (new : Name) ->
@@ -123,8 +125,8 @@ tryLiftOut : (new : Name) ->
 tryLiftOut new [] = Just []
 tryLiftOut new (MkConAlt n ci t args (CLam fc x sc) :: as)
     = do as' <- tryLiftOut new as
-         let sc' = liftOutLambda new sc
-         pure (MkConAlt n ci t args sc' :: as')
+         let sc' = liftOutLambda new (?sdfdf sc)
+         pure (MkConAlt n ci t args (?sfdfgdfg sc') :: as')
 tryLiftOut _ _ = Nothing
 
 tryLiftOutConst : (new : Name) ->
@@ -318,8 +320,8 @@ doCaseOfCase fc x xalts xdef alts def
     updateAlt (MkConAlt n ci t args sc)
         = MkConAlt n ci t args $
               CConCase fc sc
-                       (map (weakensN (mkSizeOf args)) alts)
-                       (map (weakensN (mkSizeOf args)) def)
+                       (?bvnvbnvbnbn (map (weakensN (mkSizeOf (?cvbcbcvb args))) alts))
+                       (?sdfsdf (map (weakensN (mkSizeOf (?sdffsdf args))) def))
 
     updateDef : CExp vars -> CExp vars
     updateDef sc = CConCase fc sc alts def

src/Compiler/CompileExpr.idr

@@ -10,6 +10,7 @@ import Core.Name
 import Core.Normalise
 import Core.Options
 import Core.TT
+import Core.TT.Subst
 import Core.Value
 
 import Data.List
@@ -66,7 +67,7 @@ etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args))
 etaExpand i (S k) exp args
     = CLam (getFC exp) (MN "eta" i)
              (etaExpand (i + 1) k (weaken exp)
-                  (first :: map weakenVar args))
+                  (first :: map later args))
 
 export
 expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars
@@ -229,7 +230,7 @@ mutual
            Just gdef <- lookupCtxtExact x (gamma defs)
                 | Nothing => -- primitive type match
                      do xn <- getFullName x
-                        pure $ MkConAlt xn TYCON Nothing args !(toCExpTree n sc)
+                        pure $ MkConAlt xn TYCON Nothing (cast args) !(?sdfds $ toCExpTree n sc)
                                   :: !(conCases n ns)
            case (definition gdef) of
                 DCon _ arity (Just pos) => conCases n ns -- skip it
@@ -239,8 +240,13 @@ mutual
                         sc' <- toCExpTree n sc
                         ns' <- conCases n ns
                         if dcon (definition gdef)
-                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) (toList args') (?dfsdf $ shrinkCExp sub (?bfdgdfg sc')) :: ns'
-                           else pure $ MkConAlt xn !(dconFlag xn) Nothing (toList args') (?cbcbcv $ shrinkCExp sub (?gffgh sc')) :: ns'
+                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) args' (?dfsdf $ shrinkCExp sub (?bfdgdfg (?sdfdf sc'))) :: ns'
+                           else pure $ MkConAlt xn !(dconFlag xn) Nothing args' (?cbcbcv $ shrinkCExp sub (?gffgh (?sdfsdfd sc'))) :: ns'
+--   $ rewrite sym $ snocAppendAsFish vars args in
+--     rewrite fishAsSnocAppend vars args in
+--     embed th
+
+
     where
       dcon : Def -> Bool
       dcon (DCon {}) = True
@@ -307,11 +313,13 @@ mutual
                                     := rewrite sym $ fishAsSnocAppend vars args in sc'
 
                                 let scope : CExp ((vars ++ [<MN "eff" 0]) ++ cast args)
+                                    -- scope = rewrite sym $ appendAssociative vars [<MN "eff" 0] (cast args) in
+                                    --         insertNames {outer=cast args}
+                                    --                     {inner=vars}
+                                    --                     {ns = [<MN "eff" 0]}
+                                    --                     (mkSizeOf _) (mkSizeOf _) sc''
                                     scope = rewrite sym $ appendAssociative vars [<MN "eff" 0] (cast args) in
-                                            insertNames {outer=cast args}
-                                                        {inner=vars}
-                                                        {ns = [<MN "eff" 0]}
-                                                        (mkSizeOf _) (mkSizeOf _) sc''
+                                            ?sdfdsf $ insertNames (mkSizeOf _) (mkSizeOf _) sc''
                                 let tm = CLet fc (MN "eff" 0) NotInline scr (substs (cast s) env scope)
                                 log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}, scope: \{show scope}"
                                 pure (Just tm)
@@ -546,7 +554,7 @@ lamRHS ns tm
           tmExp = substs s env (rewrite appendLinLeftNeutral ns in tm)
           newArgs = getNewArgs env
           bounds = mkBounds newArgs
-          expLocs = mkLocals zero {vars = Scope.empty} bounds tmExp in
+          expLocs = mkLocals bounds zero tmExp in
           lamBind (getFC tm) _ expLocs
   where
     lamBind : FC -> (ns : Scope) -> CExp ns -> ClosedCExp
@@ -578,7 +586,7 @@ toCDef n ty _ (ExternDef arity)
         -- TODO has quadratic runtime
         getVars : ArgList k ns -> List (Var ns)
         getVars Z = []
-        getVars (S rest) = first :: map weakenVar (getVars rest)
+        getVars (S rest) = first :: map later (getVars rest)
 
 toCDef n ty _ (ForeignDef arity cs)
     = do defs <- get Ctxt
@@ -591,7 +599,7 @@ toCDef n ty _ (Builtin {arity} op)
         -- TODO has quadratic runtime
         getVars : ArgList k ns -> Vect k (Var ns)
         getVars Z = []
-        getVars (S rest) = first :: map weakenVar (getVars rest)
+        getVars (S rest) = first :: map later (getVars rest)
 
 toCDef n _ _ (DCon tag arity pos)
     = do let nt = snd <$> pos

src/Compiler/ES/TailRec.idr

@@ -249,7 +249,7 @@ tcDoneName gi = MN "TcDone" gi
 conAlt : TcGroup -> TcFunction -> NamedConAlt
 conAlt (MkTcGroup tcIx funs) (MkTcFunction n ix args exp) =
   let name = tcContinueName tcIx ix
-   in MkNConAlt name DATACON (Just ix) args (toTc exp)
+   in MkNConAlt name DATACON (Just ix) (?dfgdfg args) (toTc exp)
 
    where
      mutual

src/Compiler/ES/ToAst.idr

@@ -223,7 +223,7 @@ mutual
     -- We map the list of args to the corresponding
     -- data projections (field accessors). They'll
     -- be then properly inlined when converting `x`.
-    projections sc args
+    projections sc (?sdfsdf args)
     MkEConAlt (tag n tg) ci <$> stmt e x
 
   -- a single branch in a pattern match on a constant

src/Compiler/Inline.idr

@@ -130,8 +130,8 @@ mutual
   usedCon : {free : _} ->
             {idx : Nat} -> (0 p : IsVar n idx free) -> CConAlt free -> Int
   usedCon n (MkConAlt _ _ _ args sc)
-      = let MkVar n' = weakensN (mkSizeOf args) (MkVar n) in
-            used n' sc
+      = let MkVar n' = weakensN (mkSizeOf (?sdfsdf args)) (MkVar n) in
+            used n' (?sdfsddgff sc)
 
   usedConst : {free : _} ->
               {idx : Nat} -> (0 p : IsVar n idx free) -> CConstAlt free -> Int
@@ -313,10 +313,12 @@ mutual
             FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (Scope.addInner free vars) ->
             Core (CConAlt free)
   evalAlt {free} {vars} fc rec env stk (MkConAlt n ci t args sc)
-      = do (bs, env') <- extendLoc fc env args
+      = do (bs, env') <- extendLoc fc env (?gdffdg args)
            scEval <- eval rec env' stk
-                          (rewrite sym $ snocAppendFishAssociative free vars args in sc)
-           pure $ MkConAlt n ci t args (rewrite snocAppendFishAssociative free Scope.empty args in refsToLocals bs scEval)
+                        --   (rewrite sym $ snocAppendFishAssociative free vars (?vcbb args) in sc)
+                       (?vbcvb sc)
+           -- pure $ MkConAlt n ci t args (rewrite snocAppendFishAssociative free Scope.empty (?adsasd args) in refsToLocals bs scEval)
+           pure $ MkConAlt n ci t args (?sdfsdf2 $ refsToLocals bs scEval)
 
   evalConstAlt : {vars, free : _} ->
                  {auto c : Ref Ctxt Defs} ->
@@ -338,12 +340,13 @@ mutual
   pickAlt {vars} {free} rec env stk con@(CCon fc n ci t args) (MkConAlt n' _ t' args' sc :: alts) def
       =
         if matches n t n' t'
-           then case checkLengthMatch args' args of
+           then case checkLengthMatch (?fsdf args') args of
                      Nothing => pure Nothing
                      Just m =>
-                         do let env' = extend env args' args m
+                         do let env' = extend env (?vcb args') args (?vdfdfg m)
                             pure $ Just !(eval rec env' stk
-                                    (rewrite sym $ snocAppendFishAssociative free vars args' in sc))
+                                    -- (rewrite sym $ snocAppendFishAssociative free vars (?sdfsdf5 args') in sc))
+                                    (?fdfgdfg sc))
            else pickAlt rec env stk con alts def
     where
       matches : Name -> Maybe Int -> Name -> Maybe Int -> Bool