Skip to content

Commit

Permalink
fully apply constructor by manual eta-expansion
Browse files Browse the repository at this point in the history
  • Loading branch information
flupe committed Jan 17, 2024
1 parent dcecf7e commit 07b2479
Showing 3 changed files with 104 additions and 43 deletions.
70 changes: 54 additions & 16 deletions app/Agda/Core/ToCore.hs
Original file line number Diff line number Diff line change
@@ -5,9 +5,11 @@ module Agda.Core.ToCore
( ToCore(..)
, ToCoreM
, Defs
, Cons
, convert
) where

import Control.Monad (when)
import Control.Monad.Reader (ReaderT, runReaderT, MonadReader, asks)
import Control.Monad.Except (MonadError(throwError))
import Data.Functor ((<&>))
@@ -18,44 +20,62 @@ import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Internal (lensSort, unDom, unEl)
import Agda.Syntax.Internal.Elim (allApplyElims)
import Agda.TypeChecking.Substitute ()
import Agda.TypeChecking.Substitute.Class (Subst, absBody)
import Agda.Utils.Maybe (fromMaybeM)
import Agda.TypeChecking.Substitute.Class (Subst, absBody, raise)
import Agda.Utils.Maybe (fromMaybeM, whenNothingM)
import Agda.Utils.Lens ((^.))

import Data.Map.Strict qualified as Map
import Agda.Syntax.Internal qualified as I

import Agda.Core.Syntax (Term(..), Elim(..), Elims, Sort(..))
import Agda.Core.Syntax qualified as Core

import Scope.In (In)
import Scope.In qualified as Scope

-- | Global definitions are represented as a mapping from @QName@s
-- to proofs of global scope membership.
-- to proofs of global def scope membership.
type Defs = Map QName In

-- | Same for constructors, for the global scope of all constructors.
type Cons = Map QName In


-- TODO(flupe): move this to Agda.Core.Syntax
-- | Apply a core term to elims
tApp :: Term -> Elims -> Term
tApp t [] = t
tApp t (e:es) = TApp t e `tApp` es

-- | Global information available during translation.
type ToCoreGlobal = (Defs, Cons)

-- | Custom monad used for translating to core syntax.
-- Gives access to global defs.
-- Gives access to global defs and constructors.
-- Translation may fail.
newtype ToCoreM a = ToCoreM { runToCore :: ReaderT Defs (Either String) a }
newtype ToCoreM a = ToCoreM { runToCore :: ReaderT ToCoreGlobal (Either String) a }
deriving newtype (Functor, Applicative, Monad, MonadError String)
deriving newtype (MonadReader Defs)
deriving newtype (MonadReader ToCoreGlobal)

asksDef :: (Defs -> a) -> ToCoreM a
asksDef = asks . (. fst)

asksCons :: (Cons -> a) -> ToCoreM a
asksCons = asks . (. snd)

-- | Lookup a global definition in the current module.
-- Fails if the definition cannot be found there.
-- | Lookup a definition name in the current module.
-- Fails if the definition cannot be found.
lookupDef :: QName -> ToCoreM In
lookupDef qn = fromMaybeM complain $ asks (Map.!? qn)
lookupDef qn = fromMaybeM complain $ asksDef (Map.!? qn)
where complain = throwError $ "Trying to access a definition from another module: " ++ prettyShow qn
--
-- | Lookup a constructor name in the current module.
-- Fails if the constructor cannot be found.
lookupCons :: QName -> ToCoreM In
lookupCons qn = fromMaybeM complain $ asksCons (Map.!? qn)
where complain = throwError $ "Trying to access a constructor from another module: " ++ prettyShow qn


-- | Class for things that can be converted to core syntax
@@ -65,9 +85,11 @@ class ToCore a where


-- | Convert some term to Agda's core representation.
convert :: ToCore a => Defs -> a -> Either String (CoreOf a)
convert defs t = runReaderT (runToCore $ toCore t) defs
convert :: ToCore a => Defs -> Cons -> a -> Either String (CoreOf a)
convert defs cons t = runReaderT (runToCore $ toCore t) (defs, cons)

toSubst :: [Term] -> Core.Subst
toSubst = foldr Core.SCons Core.SNil

instance ToCore I.Term where
type CoreOf I.Term = Term
@@ -84,9 +106,21 @@ instance ToCore I.Term where

toCore (I.Def qn es) = tApp <$> (TDef <$> lookupDef qn) <*> toCore es

-- TODO(flupe)
toCore (I.Con ch ci es) = throwError "constructors not supported"
toCore (I.Con ch ci es)
| Just args <- allApplyElims es
= do
-- @l@ is the amount of arguments missing from the application.
-- we need to eta-expand manually @l@ times to fully-apply the constructor.
let l = length (I.conFields ch) - length es
let vs = reverse $ take l $ TVar <$> iterate Scope.inThere Scope.inHere
con <- lookupCons (I.conName ch)

t <- TCon con . toSubst . (++ vs) <$> toCore (raise l args)

-- in the end, we bind @l@ fresh variables
pure (iterate TLam t !! l)

toCore I.Con{} = throwError "cubical endpoint application to constructors not supported"

toCore (I.Pi dom codom) = TPi <$> toCore dom <*> toCore codom
-- NOTE(flupe): we will need the sorts in the core syntax soon
@@ -129,7 +163,11 @@ instance ToCore I.Type where

instance (Subst a, ToCore a) => ToCore (I.Abs a) where
type CoreOf (I.Abs a) = CoreOf a
toCore t = toCore (absBody t)
toCore = toCore . absBody

instance ToCore a => ToCore (Arg a) where
type CoreOf (Arg a) = CoreOf a
toCore = toCore . unArg


-- TODO(flupe): enforce that there are no weird modalities in the arg (e.g: disallow irrelevance)
@@ -140,8 +178,8 @@ instance ToCore a => ToCore (I.Dom a) where

instance ToCore I.Elim where
type CoreOf I.Elim = Elim
toCore (I.Apply x) = EArg <$> toCore (unArg x)
toCore I.Proj{} = throwError "record projections not supported"
toCore (I.Apply x) = EArg <$> toCore (unArg x)
toCore (I.Proj _ qn) = EProj <$> lookupDef qn
toCore I.IApply{} = throwError "cubical endpoint application not supported"


58 changes: 34 additions & 24 deletions app/Main.hs
Original file line number Diff line number Diff line change
@@ -2,10 +2,11 @@ module Main where

import Control.Monad (when)
import Control.Monad.IO.Class (liftIO)
import Data.Foldable (for_)
import Data.Version (showVersion)
import Data.Either (partitionEithers)
import Data.Foldable (for_, foldl')
import Data.Map.Strict (Map)
import Data.Foldable (foldl')
import Data.Maybe (catMaybes, mapMaybe, isJust)
import Data.Version (showVersion)

import Data.Map.Strict qualified as Map

@@ -15,15 +16,18 @@ import Agda.Compiler.Backend
import Agda.Syntax.Internal
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
import Agda.Core.ToCore
import Agda.Utils.Either (maybeRight)

import Scope.Core as Scope
import Scope.In as Scope

import Paths_agda_core


main :: IO ()
main = runAgda [Backend backend]


backend :: Backend' () () () () Definition
backend = Backend'
{ backendName = "agda-core"
@@ -41,27 +45,33 @@ backend = Backend'
}



-- TODO(flupe): for datatype definitions,
-- also populate a mapping for constructors
-- TODO(flupe): for record definitions,
-- also add record fields as defs

-- | Given a list of definitions,
-- compute a mapping from def QNames to module scope membership proofs.
getModuleScope :: [Definition] -> Defs
getModuleScope (fmap defName -> defs) =
let !n = length defs in
Map.fromList $ zip (reverse defs)
$ iterate Scope.inThere Scope.inHere

-- construct definition and constructor membership proofs, along with constructor arity.
getModuleScope :: [Definition] -> (Defs, Cons)
getModuleScope defs =
let ps = iterate Scope.inThere Scope.inHere
(ds, cs) :: ([QName], [QName])
= partitionEithers $ flip mapMaybe defs \def ->
let name = defName def
in case theDef def of
Datatype{} -> Just $ Left name
Function{} -> Just $ Left name
Record{} -> Just $ Left name
Constructor{} -> Just $ Right name
_ -> Nothing
in ( Map.fromList $ zip (reverse ds) ps
, Map.fromList $ zip (reverse cs) ps
)

checkModule :: IsMain -> TopLevelModuleName -> [Definition] -> TCM ()
checkModule IsMain tlm defs = do

reportSDoc "agda-core.check" 5 $ text "Checking module" <+> prettyTCM tlm

let !gdefs = getModuleScope defs
let (!gdefs, !gcons) = getModuleScope defs

reportSDoc "agda-core.check" 5 $ text "Module definitions:" <+> prettyTCM (Map.keys gdefs)
reportSDoc "agda-core.check" 5 $ text "Module constructors:" <+> prettyTCM (Map.keys gcons)

for_ defs \def -> do

@@ -70,8 +80,7 @@ checkModule IsMain tlm defs = do

reportSDoc "agda-core.check" 5 $ text "Checking" <+> dn

-- TODO(flupe): convert type of def.
case convert gdefs (unEl defType) of
case convert gdefs gcons (unEl defType) of
Left e -> reportSDoc "agda-core.check" 5 $
text "Couldn't convert type of" <+> dn
<+> text "to core syntax:" <+> text e
@@ -81,10 +90,11 @@ checkModule IsMain tlm defs = do
-- NOTE(flupe): currently we only support definitions with no arguments (implying no pattern-matching)
-- i.e functions have to be written with explicit lambdas
Function{..}
| [cl] <- funClauses
| not (isJust (maybeRight funProjection >>= projProper)) -- discard record projections
, [cl] <- funClauses
, [] <- clausePats cl
, Just body <- clauseBody cl
-> case convert gdefs body of
-> case convert gdefs gcons body of
Left e -> reportSDoc "agda-core.check" 5 $ text "Failed to convert to core syntax:" <+> text e
Right ct -> reportSDoc "agda-core.check" 5 $ text "Definition:" <+> text (show ct) -- liftIO $ print ct -- TODO(flupe): launch type-checker

@@ -93,10 +103,10 @@ checkModule IsMain tlm defs = do
Axiom{} -> reportSDoc "agda-core.check" 5 $ text "Postulates not supported"
Primitive{} -> reportSDoc "agda-core.check" 5 $ text "Primitives not supported"
PrimitiveSort{} -> reportSDoc "agda-core.check" 5 $ text "Primitive sorts not supported"
Constructor{} -> reportSDoc "agda-core.check" 5 $ text "Constructors not supported"

_ -> reportSDoc "agda-core.check" 5 $ text "Unsupported, skipping" <+> prettyTCM defName
Constructor{} -> pure () -- NOTE(flupe): will be handled when datatypes are handled

_ -> reportSDoc "agda-core.check" 5 $ text "Unsupported, skipping" <+> prettyTCM defName

-- for now, we only check the main module
checkModule NotMain _ _ = pure ()

19 changes: 16 additions & 3 deletions test/one.agda
Original file line number Diff line number Diff line change
@@ -3,14 +3,27 @@ module one where
data : Set where
tt :

record Σ (A : Set) (B : A Set) : Set where
constructor _,_
field
fst : A
snd : B fst

data _+_ (A B : Set) : Set where
inl : A A + B
inr : B A + B

t :
t = tt

left : (A B : Set) A A + B
left = λ A B x inl x

id : (A : Set) A A
id = λ _ x x
id = λ A x x

ap : (A B : Set) (A B) A B
ap = λ A _ f x f (id A x)
ap = λ A B f x f (id A x)

dap : (A : Set) (B : A Set) ( x B x) x B x
dap = λ A _ f x f (id A x)
dap = λ A B f x f (id A x)

0 comments on commit 07b2479

Please sign in to comment.