0 | module Core.SchemeEval.Quote
  1 |
  2 | import Core.Context
  3 | import Core.Env
  4 | import Core.SchemeEval.Compile
  5 | import Core.SchemeEval.Evaluate
  6 |
  7 | mutual
  8 |   quoteArgs : {auto c : Ref Ctxt Defs} ->
  9 |               {bound, free : _} ->
 10 |               Ref Sym Integer -> Bounds bound ->
 11 |               Env Term free -> List (Core (SNF free)) ->
 12 |               Core (List (Term (bound ++ free)))
 13 |   quoteArgs q bound env args
 14 |       = traverse (\arg => do arg' <- arg
 15 |                              quoteGen q bound env arg') args
 16 |
 17 |   quotePi : {auto c : Ref Ctxt Defs} ->
 18 |             {bound, free : _} ->
 19 |             Ref Sym Integer -> Bounds bound ->
 20 |             Env Term free -> PiInfo (SNF free) ->
 21 |             Core (PiInfo (Term (bound ++ free)))
 22 |   quotePi q bound env Explicit = pure Explicit
 23 |   quotePi q bound env Implicit = pure Implicit
 24 |   quotePi q bound env AutoImplicit = pure AutoImplicit
 25 |   quotePi q bound env (DefImplicit t)
 26 |       = do t' <- quoteGen q bound env t
 27 |            pure (DefImplicit t')
 28 |
 29 |   quoteBinder : {auto c : Ref Ctxt Defs} ->
 30 |                 {bound, free : _} ->
 31 |                 Ref Sym Integer -> Bounds bound ->
 32 |                 Env Term free -> Binder (SNF free) ->
 33 |                 Core (Binder (Term (bound ++ free)))
 34 |   quoteBinder q bound env (Lam fc r p ty)
 35 |      = do ty' <- quoteGen q bound env ty
 36 |           p' <- quotePi q bound env p
 37 |           pure (Lam fc r p' ty')
 38 |   quoteBinder q bound env (Let fc r val ty)
 39 |      = do ty' <- quoteGen q bound env ty
 40 |           val' <- quoteGen q bound env val
 41 |           pure (Let fc r val' ty')
 42 |   quoteBinder q bound env (Pi fc r p ty)
 43 |      = do ty' <- quoteGen q bound env ty
 44 |           p' <- quotePi q bound env p
 45 |           pure (Pi fc r p' ty')
 46 |   quoteBinder q bound env (PVar fc r p ty)
 47 |      = do ty' <- quoteGen q bound env ty
 48 |           p' <- quotePi q bound env p
 49 |           pure (PVar fc r p' ty')
 50 |   quoteBinder q bound env (PLet fc r val ty)
 51 |      = do ty' <- quoteGen q bound env ty
 52 |           val' <- quoteGen q bound env val
 53 |           pure (PLet fc r val' ty')
 54 |   quoteBinder q bound env (PVTy fc r ty)
 55 |      = do ty' <- quoteGen q bound env ty
 56 |           pure (PVTy fc r ty')
 57 |
 58 |   quoteHead : {auto c : Ref Ctxt Defs} ->
 59 |               {bound, free : _} ->
 60 |               Ref Sym Integer ->
 61 |               FC -> Bounds bound -> Env Term free -> SHead free ->
 62 |               Core (Term (bound ++ free))
 63 |   quoteHead {bound} q fc bounds env (SLocal idx prf)
 64 |       = let MkVar prf' = addLater bound prf in
 65 |             pure (Local fc Nothing _ prf')
 66 |     where
 67 |       addLater : {idx : _} ->
 68 |                  (ys : Scope) -> (0 p : IsVar n idx xs) ->
 69 |                  Var (ys ++ xs)
 70 |       addLater [] isv = MkVar isv
 71 |       addLater (x :: xs) isv
 72 |           = let MkVar isv' = addLater xs isv in
 73 |                 MkVar (Later isv')
 74 |   quoteHead q fc bounds env (SRef nt n)
 75 |       = pure $ case findName bounds of
 76 |              Just (MkVar p) => Local fc Nothing _ (embedIsVar p)
 77 |              Nothing => Ref fc nt n
 78 |     where
 79 |       findName : Bounds bound' -> Maybe (Var bound')
 80 |       findName None = Nothing
 81 |       findName (Add x n' ns)
 82 |           = if n == n'
 83 |                then Just first
 84 |                else do MkVar p <-findName ns
 85 |                        Just (MkVar (Later p))
 86 |   quoteHead q fc bounds env (SMeta n i args)
 87 |       = do args' <- quoteArgs q bounds env args
 88 |            pure $ Meta fc n i args'
 89 |
 90 |   quoteGen : {auto c : Ref Ctxt Defs} ->
 91 |              {bound, vars : _} ->
 92 |              Ref Sym Integer -> Bounds bound ->
 93 |              Env Term vars -> SNF vars -> Core (Term (bound ++ vars))
 94 |   quoteGen q bound env (SBind fc n b sc)
 95 |       = do i <- nextName
 96 |            let var = UN (Basic ("b-" ++ show (fromInteger i)))
 97 |            -- Ref Bound gets turned directly into a symbol by seval, which
 98 |            -- we can then read back when quoting the scope
 99 |            arg <- seval EvalAll env (Ref fc Bound var)
100 |            sc' <- quoteGen q (Add n var bound) env !(sc arg)
101 |            b' <- quoteBinder q bound env b
102 |            pure (Bind fc n b' sc')
103 |   quoteGen q bound env (SApp fc f args)
104 |       = do f' <- quoteHead q fc bound env f
105 |            args' <- quoteArgs q bound env args
106 |            pure $ apply fc f' args'
107 |   quoteGen q bound env (SDCon fc n t ar args)
108 |       = do args' <- quoteArgs q bound env args
109 |            pure $ apply fc (Ref fc (DataCon t ar) n) args'
110 |   quoteGen q bound env (STCon fc n ar args)
111 |       = do args' <- quoteArgs q bound env args
112 |            pure $ apply fc (Ref fc (TyCon ar) n) args'
113 |   quoteGen q bound env (SDelayed fc r arg)
114 |       = do argQ <- quoteGen q bound env arg
115 |            pure (TDelayed fc r argQ)
116 |   quoteGen q bound env (SDelay fc r ty arg)
117 |       = do argQ <- quoteGen q bound env !arg
118 |            tyQ <- quoteGen q bound env !ty
119 |            pure (TDelay fc r tyQ argQ)
120 |   quoteGen q bound env (SForce fc r arg)
121 |       = case arg of
122 |              SDelay fc _ _ arg => quoteGen q bound env !arg
123 |              _ => do arg' <- quoteGen q bound env arg
124 |                      pure $ (TForce fc r arg')
125 |   quoteGen q bound env (SPrimVal fc c) = pure $ PrimVal fc c
126 |   quoteGen q bound env (SErased fc Impossible) = pure $ Erased fc Impossible
127 |   quoteGen q bound env (SErased fc Placeholder) = pure $ Erased fc Placeholder
128 |   quoteGen q bound env (SErased fc (Dotted t))
129 |     = pure $ Erased fc $ Dotted !(quoteGen q bound env t)
130 |   quoteGen q bound env (SType fc u) = pure $ TType fc u
131 |
132 | export
133 | quote : {auto c : Ref Ctxt Defs} ->
134 |         {vars : _} ->
135 |         Env Term vars -> SNF vars -> Core (Term vars)
136 | quote env tm
137 |     = do q <- newRef Sym 0
138 |          quoteGen q None env tm
139 |