{-# OPTIONS_GHC -Wno-orphans -Wno-redundant-constraints #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE ScopedTypeVariables         #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TemplateHaskell   #-}
-- | Functions over Second-Order Abstract Syntax (SOAS)
-- represented using scope-safe Haskell types (via Free Foil).
module Language.SOAS.Impl where


import Data.List (find)
import Data.Bifunctor
import qualified Control.Monad.Foil as Foil
import           Control.Monad.Free.Foil
import Language.SOAS.Impl.Generated
import qualified Language.SOAS.Syntax.Abs    as Raw
import qualified Language.SOAS.Syntax.Lex    as Raw
import qualified Language.SOAS.Syntax.Par    as Raw
import qualified Language.SOAS.Syntax.Print  as Raw
import           System.Exit                     (exitFailure)

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :set -XDataKinds
-- >>> import qualified Control.Monad.Foil as Foil
-- >>> import Control.Monad.Free.Foil
-- >>> import Data.String (fromString)

-- * Standard Types

-- | Standard terms with source code location annotations.
type Term = Term' Raw.BNFC'Position
-- | Standard types with source code location annotations.
type Type = Type' Raw.BNFC'Position

-- | Standard metavariable substitutions with source code location annotations.
type Subst = Subst' Raw.BNFC'Position Foil.VoidS
-- | Standard unification constraints with source code location annotations.
type Constraint = Constraint' Raw.BNFC'Position Foil.VoidS
-- | Standard operator typings with source code location annotations.
type OpTyping = OpTyping' Raw.BNFC'Position Foil.VoidS

-- * Metavariable substitutions

-- | Lookup a substitution by its 'Raw.MetaVarIdent'.
--
-- >>> lookupSubst "?m" ["?n[] ↦ Zero()", "?m[x y] ↦ App(y, x)"]
-- Just ?m [x0 x1] ↦ App (x1, x0)
lookupSubst :: Raw.MetaVarIdent -> [Subst] -> Maybe Subst
lookupSubst :: MetaVarIdent -> [Subst] -> Maybe Subst
lookupSubst MetaVarIdent
m = (Subst -> Bool) -> [Subst] -> Maybe Subst
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Subst -> Bool) -> [Subst] -> Maybe Subst)
-> (Subst -> Bool) -> [Subst] -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ \(Subst BNFC'Position
_loc MetaVarIdent
m' Binders' BNFC'Position 'VoidS i
_ Term' BNFC'Position i
_) -> MetaVarIdent
m MetaVarIdent -> MetaVarIdent -> Bool
forall a. Eq a => a -> a -> Bool
== MetaVarIdent
m'

-- | Apply meta variable substitutions to a term.
--
-- >>> applySubsts Foil.emptyScope ["?m[x y] ↦ Lam(z. App(z, App(x, y)))"] "Lam(x. ?m[App(x, ?m[x, x]), x])"
-- Lam (x0 . Lam (x2 . App (x2, App (App (x0, Lam (x2 . App (x2, App (x0, x0)))), x0))))
--
-- >>> applySubsts Foil.emptyScope ["?m[x y] ↦ App(y, x)"] "Lam(f. Lam(x. ?m[?m[x, f], f]))"
-- Lam (x0 . Lam (x1 . App (x0, App (x0, x1))))
applySubsts :: Foil.Distinct n => Foil.Scope n -> [Subst] -> Term n -> Term n
applySubsts :: forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope n
scope [Subst]
substs Term n
term =
  case Term n
term of
    MetaVar BNFC'Position
_loc MetaVarIdent
m [Term n]
args | Just (Subst BNFC'Position
_ MetaVarIdent
_ Binders' BNFC'Position 'VoidS i
binders Term' BNFC'Position i
body) <- MetaVarIdent -> [Subst] -> Maybe Subst
lookupSubst MetaVarIdent
m [Subst]
substs ->
      let args' :: [Term n]
args' = (Term n -> Term n) -> [Term n] -> [Term n]
forall a b. (a -> b) -> [a] -> [b]
map (Scope n -> [Subst] -> Term n -> Term n
forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope n
scope [Subst]
substs) [Term n]
args
       in Scope n
-> Substitution
     (AST (Binders' BNFC'Position) (Term'Sig BNFC'Position)) 'VoidS n
-> Binders' BNFC'Position 'VoidS i
-> [Term n]
-> Term' BNFC'Position i
-> Term n
forall (sig :: * -> * -> *) (o :: S) (binder' :: S -> S -> *)
       (binder :: S -> S -> *) (n :: S) (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder', CoSinkable binder,
 SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) n o
-> binder' n i
-> [AST binder sig o]
-> AST binder sig i
-> AST binder sig o
substitutePattern Scope n
scope Substitution
  (AST (Binders' BNFC'Position) (Term'Sig BNFC'Position)) 'VoidS n
forall (e :: S -> *) (n :: S). Substitution e 'VoidS n
Foil.voidSubst Binders' BNFC'Position 'VoidS i
binders [Term n]
args' Term' BNFC'Position i
body
    Var{} -> Term n
term
    -- NOTE: generic recursive processing!
    Node Term'Sig
  BNFC'Position
  (ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
  (Term n)
node -> Term'Sig
  BNFC'Position
  (ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
  (Term n)
-> Term n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
 -> ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
-> (Term n -> Term n)
-> Term'Sig
     BNFC'Position
     (ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
     (Term n)
-> Term'Sig
     BNFC'Position
     (ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
     (Term n)
forall a b c d.
(a -> b)
-> (c -> d)
-> Term'Sig BNFC'Position a c
-> Term'Sig BNFC'Position b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
-> ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
goScoped (Scope n -> [Subst] -> Term n -> Term n
forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope n
scope [Subst]
substs) Term'Sig
  BNFC'Position
  (ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n)
  (Term n)
node)
  where
    goScoped :: ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
-> ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
goScoped (ScopedAST Binders' BNFC'Position n l
binders AST (Binders' BNFC'Position) (Term'Sig BNFC'Position) l
body) =
      case Binders' BNFC'Position n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct Binders' BNFC'Position n l
binders of
        DistinctEvidence l
Foil.Distinct ->
          let scope' :: Scope l
scope' = Binders' BNFC'Position n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern Binders' BNFC'Position n l
binders Scope n
scope
           in Binders' BNFC'Position n l
-> AST (Binders' BNFC'Position) (Term'Sig BNFC'Position) l
-> ScopedAST (Binders' BNFC'Position) (Term'Sig BNFC'Position) n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST Binders' BNFC'Position n l
binders (Scope l
-> [Subst]
-> AST (Binders' BNFC'Position) (Term'Sig BNFC'Position) l
-> AST (Binders' BNFC'Position) (Term'Sig BNFC'Position) l
forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope l
scope' [Subst]
substs AST (Binders' BNFC'Position) (Term'Sig BNFC'Position) l
body)

-- | Check if a (simultaneous) substitution is a solution to a set of constraints:
--
-- >>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x. ?m[?m[x, f], f] = App(f, App(f, x))"]
-- True
-- >>> isSolutionFor ["?m[x y] ↦ App(y, x)"] ["∀ f x y. ?m[?m[x, f], f] = App(f, App(f, y))"]
-- False
--
-- >>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, x))))"]
-- True
-- >>> isSolutionFor ["?m[x] ↦ Lam(f. App(f, x))"] ["∀ y x. ?m[?m[x]] = Lam(f. App(f, Lam(f. App(f, y))))"]
-- False
isSolutionFor :: [Subst] -> [Constraint] -> Bool
isSolutionFor :: [Subst] -> [Constraint] -> Bool
isSolutionFor [Subst]
substs = (Constraint -> Bool) -> [Constraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Constraint -> Bool
isSatisfied
  where
    isSatisfied :: Constraint -> Bool
isSatisfied (ConstraintEq BNFC'Position
_loc Binders' BNFC'Position 'VoidS i
binders Term' BNFC'Position i
l Term' BNFC'Position i
r) =
      case Binders' BNFC'Position 'VoidS i -> DistinctEvidence i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct Binders' BNFC'Position 'VoidS i
binders of
        DistinctEvidence i
Foil.Distinct ->
          let scope :: Scope i
scope = Binders' BNFC'Position 'VoidS i -> Scope 'VoidS -> Scope i
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern Binders' BNFC'Position 'VoidS i
binders Scope 'VoidS
Foil.emptyScope
          in Scope i -> Term' BNFC'Position i -> Term' BNFC'Position i -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope i
scope (Scope i
-> [Subst] -> Term' BNFC'Position i -> Term' BNFC'Position i
forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope i
scope [Subst]
substs Term' BNFC'Position i
l) (Scope i
-> [Subst] -> Term' BNFC'Position i -> Term' BNFC'Position i
forall (n :: S).
Distinct n =>
Scope n -> [Subst] -> Term n -> Term n
applySubsts Scope i
scope [Subst]
substs Term' BNFC'Position i
r)

-- * Entrypoint

-- | A SOAS interpreter implemented via the free foil.
defaultMain :: IO ()
defaultMain :: IO ()
defaultMain = do
  String
input <- IO String
getContents
  case [Token] -> Err TermTyping
Raw.pTermTyping (String -> [Token]
Raw.tokens String
input) of
    Left String
err -> do
      String -> IO ()
putStrLn String
err
      IO ()
forall a. IO a
exitFailure
    Right TermTyping
typing -> String -> IO ()
putStrLn (TermTyping -> String
forall a. Print a => a -> String
Raw.printTree TermTyping
typing)