Skip to content

Commit

Permalink
Cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
fizruk committed Oct 26, 2024
1 parent 02ebc95 commit cbf7149
Show file tree
Hide file tree
Showing 3 changed files with 23 additions and 20 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -475,8 +475,8 @@ toFreeFoilClauseFromBinding config termConfig@FreeFoilTermConfig{..} rawRetType
ForallC _params _ctx con -> go con
RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)

toFreeFoilClauseFromQualified :: Name -> FreeFoilConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromQualified rawTypeName config rawRetType = go
toFreeFoilClauseFromQualified ::FreeFoilConfig -> Type -> Con -> Q [Clause]
toFreeFoilClauseFromQualified config rawRetType = go
where
go = \case
GadtC conNames rawArgTypes rawRetType' -> concat <$> do
Expand Down Expand Up @@ -676,7 +676,7 @@ mkFreeFoilConversions config@FreeFoilConfig{..} = concat <$> sequence
safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType
addModFinalizer $ putDoc (DeclDoc funName)
("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")
clauses <- concat <$> mapM (toFreeFoilClauseFromQualified rawName config rawType) cons
clauses <- concat <$> mapM (toFreeFoilClauseFromQualified config rawType) cons
return
[ SigD funName (AppT (AppT ArrowT safeType) rawType)
, FunD funName clauses
Expand Down
36 changes: 19 additions & 17 deletions haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
-- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
--
-- Free foil provides __general__ definitions or implementations for the following:
Expand Down Expand Up @@ -38,20 +38,20 @@ module Language.LambdaPi.Impl.FreeFoilTH where
import qualified Control.Monad.Foil as Foil
import Control.Monad.Foil.TH
import Control.Monad.Free.Foil
import Control.Monad.Free.Foil.Generic
import Control.Monad.Free.Foil.TH
import Data.Bifunctor.TH
import Data.Map (Map)
import qualified Data.Map as Map
import Data.String (IsString (..))
import Generics.Kind.TH (deriveGenericK)
import qualified GHC.Generics as GHC
import qualified Language.LambdaPi.Syntax.Abs as Raw
import qualified Language.LambdaPi.Syntax.Layout as Raw
import qualified Language.LambdaPi.Syntax.Lex as Raw
import qualified Language.LambdaPi.Syntax.Par as Raw
import qualified Language.LambdaPi.Syntax.Print as Raw
import System.Exit (exitFailure)
import Control.Monad.Free.Foil.Generic
import Generics.Kind.TH (deriveGenericK)
import qualified GHC.Generics as GHC


-- $setup
Expand Down Expand Up @@ -138,9 +138,11 @@ fromTerm' :: Term' a n -> Raw.Term' a
fromTerm' = convertFromAST
convertFromTerm'Sig
(Raw.Var (error "location missing"))
fromFoilPattern'
(fromFoilPattern' mkVarIdent)
(Raw.AScopedTerm (error "location missing"))
(\n -> Raw.VarIdent ("x" ++ show n))
mkVarIdent
where
mkVarIdent n = Raw.VarIdent ("x" ++ show n)

-- | Parse scope-safe terms via raw representation.
--
Expand Down
1 change: 1 addition & 0 deletions haskell/soas/soas.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ custom-setup

library
exposed-modules:
Language.SOAS.FreeFoilConfig
Language.SOAS.Impl
Language.SOAS.Syntax.Abs
Language.SOAS.Syntax.Lex
Expand Down

0 comments on commit cbf7149

Please sign in to comment.