{- FOURMOLU_DISABLE -}
-- The MIT License (MIT)

-- Copyright (c) 2016-2024 Objectionary.com

-- Permission is hereby granted, free of charge, to any person obtaining a copy
-- of this software and associated documentation files (the "Software"), to deal
-- in the Software without restriction, including without limitation the rights
-- to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the Software is
-- furnished to do so, subject to the following conditions:

-- The above copyright notice and this permission notice shall be included
-- in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-- FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-- OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-- SOFTWARE.
{- FOURMOLU_ENABLE -}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-forall-identifier #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-partial-fields #-}
{-# OPTIONS_GHC -Wno-type-defaults #-}

module Language.EO.Phi.Rules.Yaml where

import Control.Monad (guard, unless)
import Control.Monad.State (State, evalState)
import Data.Aeson (FromJSON (..), Options (sumEncoding), SumEncoding (UntaggedValue), genericParseJSON)
import Data.Aeson.Types (defaultOptions)
import Data.Coerce (coerce)
import Data.List (intercalate)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.String (IsString (..))
import Data.Yaml qualified as Yaml
import GHC.Generics (Generic)

import Language.EO.Phi (printTree)
import Language.EO.Phi.Rules.Common (Context (..), NamedRule)
import Language.EO.Phi.Rules.Common qualified as Common
import Language.EO.Phi.Syntax.Abs
import PyF (fmt)

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :set -XOverloadedLists

instance FromJSON Object where parseJSON :: Value -> Parser Object
parseJSON = ([Char] -> Object) -> Parser [Char] -> Parser Object
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> Object
forall a. IsString a => [Char] -> a
fromString (Parser [Char] -> Parser Object)
-> (Value -> Parser [Char]) -> Value -> Parser Object
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON Binding where parseJSON :: Value -> Parser Binding
parseJSON = ([Char] -> Binding) -> Parser [Char] -> Parser Binding
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> Binding
forall a. IsString a => [Char] -> a
fromString (Parser [Char] -> Parser Binding)
-> (Value -> Parser [Char]) -> Value -> Parser Binding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON

instance FromJSON ObjectMetaId where parseJSON :: Value -> Parser ObjectMetaId
parseJSON = ([Char] -> ObjectMetaId) -> Parser [Char] -> Parser ObjectMetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> ObjectMetaId
ObjectMetaId (Parser [Char] -> Parser ObjectMetaId)
-> (Value -> Parser [Char]) -> Value -> Parser ObjectMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON LabelMetaId where parseJSON :: Value -> Parser LabelMetaId
parseJSON = ([Char] -> LabelMetaId) -> Parser [Char] -> Parser LabelMetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> LabelMetaId
LabelMetaId (Parser [Char] -> Parser LabelMetaId)
-> (Value -> Parser [Char]) -> Value -> Parser LabelMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON TailMetaId where parseJSON :: Value -> Parser TailMetaId
parseJSON = ([Char] -> TailMetaId) -> Parser [Char] -> Parser TailMetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> TailMetaId
TailMetaId (Parser [Char] -> Parser TailMetaId)
-> (Value -> Parser [Char]) -> Value -> Parser TailMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON BindingsMetaId where parseJSON :: Value -> Parser BindingsMetaId
parseJSON = ([Char] -> BindingsMetaId)
-> Parser [Char] -> Parser BindingsMetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> BindingsMetaId
BindingsMetaId (Parser [Char] -> Parser BindingsMetaId)
-> (Value -> Parser [Char]) -> Value -> Parser BindingsMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON BytesMetaId where parseJSON :: Value -> Parser BytesMetaId
parseJSON = ([Char] -> BytesMetaId) -> Parser [Char] -> Parser BytesMetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> BytesMetaId
BytesMetaId (Parser [Char] -> Parser BytesMetaId)
-> (Value -> Parser [Char]) -> Value -> Parser BytesMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON

instance FromJSON MetaId where
  parseJSON :: Value -> Parser MetaId
parseJSON = ([Char] -> MetaId) -> Parser [Char] -> Parser MetaId
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> MetaId
forall a. IsString a => [Char] -> a
fromString (Parser [Char] -> Parser MetaId)
-> (Value -> Parser [Char]) -> Value -> Parser MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON

instance FromJSON Attribute where parseJSON :: Value -> Parser Attribute
parseJSON = ([Char] -> Attribute) -> Parser [Char] -> Parser Attribute
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> Attribute
forall a. IsString a => [Char] -> a
fromString (Parser [Char] -> Parser Attribute)
-> (Value -> Parser [Char]) -> Value -> Parser Attribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON
instance FromJSON RuleAttribute where parseJSON :: Value -> Parser RuleAttribute
parseJSON = ([Char] -> RuleAttribute) -> Parser [Char] -> Parser RuleAttribute
forall a b. (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Char] -> RuleAttribute
forall a. IsString a => [Char] -> a
fromString (Parser [Char] -> Parser RuleAttribute)
-> (Value -> Parser [Char]) -> Value -> Parser RuleAttribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser [Char]
forall a. FromJSON a => Value -> Parser a
parseJSON

instance FromJSON LabelId
instance FromJSON AlphaIndex

data RuleSet = RuleSet
  { RuleSet -> [Char]
title :: String
  , RuleSet -> [Rule]
rules :: [Rule]
  }
  deriving ((forall x. RuleSet -> Rep RuleSet x)
-> (forall x. Rep RuleSet x -> RuleSet) -> Generic RuleSet
forall x. Rep RuleSet x -> RuleSet
forall x. RuleSet -> Rep RuleSet x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RuleSet -> Rep RuleSet x
from :: forall x. RuleSet -> Rep RuleSet x
$cto :: forall x. Rep RuleSet x -> RuleSet
to :: forall x. Rep RuleSet x -> RuleSet
Generic, Value -> Parser [RuleSet]
Value -> Parser RuleSet
(Value -> Parser RuleSet)
-> (Value -> Parser [RuleSet]) -> FromJSON RuleSet
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser RuleSet
parseJSON :: Value -> Parser RuleSet
$cparseJSONList :: Value -> Parser [RuleSet]
parseJSONList :: Value -> Parser [RuleSet]
FromJSON, Int -> RuleSet -> ShowS
[RuleSet] -> ShowS
RuleSet -> [Char]
(Int -> RuleSet -> ShowS)
-> (RuleSet -> [Char]) -> ([RuleSet] -> ShowS) -> Show RuleSet
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleSet -> ShowS
showsPrec :: Int -> RuleSet -> ShowS
$cshow :: RuleSet -> [Char]
show :: RuleSet -> [Char]
$cshowList :: [RuleSet] -> ShowS
showList :: [RuleSet] -> ShowS
Show)

data RuleContext = RuleContext
  { RuleContext -> Maybe Object
global_object :: Maybe Object
  , RuleContext -> Maybe Object
current_object :: Maybe Object
  , RuleContext -> Maybe Attribute
current_attribute :: Maybe Attribute
  }
  deriving ((forall x. RuleContext -> Rep RuleContext x)
-> (forall x. Rep RuleContext x -> RuleContext)
-> Generic RuleContext
forall x. Rep RuleContext x -> RuleContext
forall x. RuleContext -> Rep RuleContext x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RuleContext -> Rep RuleContext x
from :: forall x. RuleContext -> Rep RuleContext x
$cto :: forall x. Rep RuleContext x -> RuleContext
to :: forall x. Rep RuleContext x -> RuleContext
Generic, Value -> Parser [RuleContext]
Value -> Parser RuleContext
(Value -> Parser RuleContext)
-> (Value -> Parser [RuleContext]) -> FromJSON RuleContext
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser RuleContext
parseJSON :: Value -> Parser RuleContext
$cparseJSONList :: Value -> Parser [RuleContext]
parseJSONList :: Value -> Parser [RuleContext]
FromJSON, Int -> RuleContext -> ShowS
[RuleContext] -> ShowS
RuleContext -> [Char]
(Int -> RuleContext -> ShowS)
-> (RuleContext -> [Char])
-> ([RuleContext] -> ShowS)
-> Show RuleContext
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleContext -> ShowS
showsPrec :: Int -> RuleContext -> ShowS
$cshow :: RuleContext -> [Char]
show :: RuleContext -> [Char]
$cshowList :: [RuleContext] -> ShowS
showList :: [RuleContext] -> ShowS
Show)

data Rule = Rule
  { Rule -> [Char]
name :: String
  , Rule -> [Char]
description :: String
  , Rule -> Maybe RuleContext
context :: Maybe RuleContext
  , Rule -> Maybe [MetaId]
forall :: Maybe [MetaId]
  , Rule -> Object
pattern :: Object
  , Rule -> Object
result :: Object
  , Rule -> Maybe [FreshMetaId]
fresh :: Maybe [FreshMetaId]
  , Rule -> Maybe [Condition]
when :: Maybe [Condition]
  , Rule -> Maybe [RuleTest]
tests :: Maybe [RuleTest]
  }
  deriving ((forall x. Rule -> Rep Rule x)
-> (forall x. Rep Rule x -> Rule) -> Generic Rule
forall x. Rep Rule x -> Rule
forall x. Rule -> Rep Rule x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Rule -> Rep Rule x
from :: forall x. Rule -> Rep Rule x
$cto :: forall x. Rep Rule x -> Rule
to :: forall x. Rep Rule x -> Rule
Generic, Value -> Parser [Rule]
Value -> Parser Rule
(Value -> Parser Rule) -> (Value -> Parser [Rule]) -> FromJSON Rule
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser Rule
parseJSON :: Value -> Parser Rule
$cparseJSONList :: Value -> Parser [Rule]
parseJSONList :: Value -> Parser [Rule]
FromJSON, Int -> Rule -> ShowS
[Rule] -> ShowS
Rule -> [Char]
(Int -> Rule -> ShowS)
-> (Rule -> [Char]) -> ([Rule] -> ShowS) -> Show Rule
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Rule -> ShowS
showsPrec :: Int -> Rule -> ShowS
$cshow :: Rule -> [Char]
show :: Rule -> [Char]
$cshowList :: [Rule] -> ShowS
showList :: [Rule] -> ShowS
Show)

data FreshMetaId = FreshMetaId
  { FreshMetaId -> LabelMetaId
name :: LabelMetaId
  , FreshMetaId -> Maybe [Char]
prefix :: Maybe String
  }
  deriving ((forall x. FreshMetaId -> Rep FreshMetaId x)
-> (forall x. Rep FreshMetaId x -> FreshMetaId)
-> Generic FreshMetaId
forall x. Rep FreshMetaId x -> FreshMetaId
forall x. FreshMetaId -> Rep FreshMetaId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FreshMetaId -> Rep FreshMetaId x
from :: forall x. FreshMetaId -> Rep FreshMetaId x
$cto :: forall x. Rep FreshMetaId x -> FreshMetaId
to :: forall x. Rep FreshMetaId x -> FreshMetaId
Generic, Value -> Parser [FreshMetaId]
Value -> Parser FreshMetaId
(Value -> Parser FreshMetaId)
-> (Value -> Parser [FreshMetaId]) -> FromJSON FreshMetaId
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser FreshMetaId
parseJSON :: Value -> Parser FreshMetaId
$cparseJSONList :: Value -> Parser [FreshMetaId]
parseJSONList :: Value -> Parser [FreshMetaId]
FromJSON, Int -> FreshMetaId -> ShowS
[FreshMetaId] -> ShowS
FreshMetaId -> [Char]
(Int -> FreshMetaId -> ShowS)
-> (FreshMetaId -> [Char])
-> ([FreshMetaId] -> ShowS)
-> Show FreshMetaId
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FreshMetaId -> ShowS
showsPrec :: Int -> FreshMetaId -> ShowS
$cshow :: FreshMetaId -> [Char]
show :: FreshMetaId -> [Char]
$cshowList :: [FreshMetaId] -> ShowS
showList :: [FreshMetaId] -> ShowS
Show)

data RuleTest = RuleTest
  { RuleTest -> [Char]
name :: String
  , RuleTest -> Object
input :: Object
  , RuleTest -> [Object]
output :: [Object]
  , RuleTest -> Maybe [RuleTestOption]
options :: Maybe [RuleTestOption]
  }
  deriving ((forall x. RuleTest -> Rep RuleTest x)
-> (forall x. Rep RuleTest x -> RuleTest) -> Generic RuleTest
forall x. Rep RuleTest x -> RuleTest
forall x. RuleTest -> Rep RuleTest x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RuleTest -> Rep RuleTest x
from :: forall x. RuleTest -> Rep RuleTest x
$cto :: forall x. Rep RuleTest x -> RuleTest
to :: forall x. Rep RuleTest x -> RuleTest
Generic, Value -> Parser [RuleTest]
Value -> Parser RuleTest
(Value -> Parser RuleTest)
-> (Value -> Parser [RuleTest]) -> FromJSON RuleTest
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser RuleTest
parseJSON :: Value -> Parser RuleTest
$cparseJSONList :: Value -> Parser [RuleTest]
parseJSONList :: Value -> Parser [RuleTest]
FromJSON, Int -> RuleTest -> ShowS
[RuleTest] -> ShowS
RuleTest -> [Char]
(Int -> RuleTest -> ShowS)
-> (RuleTest -> [Char]) -> ([RuleTest] -> ShowS) -> Show RuleTest
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleTest -> ShowS
showsPrec :: Int -> RuleTest -> ShowS
$cshow :: RuleTest -> [Char]
show :: RuleTest -> [Char]
$cshowList :: [RuleTest] -> ShowS
showList :: [RuleTest] -> ShowS
Show)

newtype RuleTestOption = TakeOne {RuleTestOption -> Bool
take_one :: Bool}
  -- deriving (Generic, Show, FromJSON)
  deriving (RuleTestOption -> RuleTestOption -> Bool
(RuleTestOption -> RuleTestOption -> Bool)
-> (RuleTestOption -> RuleTestOption -> Bool) -> Eq RuleTestOption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RuleTestOption -> RuleTestOption -> Bool
== :: RuleTestOption -> RuleTestOption -> Bool
$c/= :: RuleTestOption -> RuleTestOption -> Bool
/= :: RuleTestOption -> RuleTestOption -> Bool
Eq, (forall x. RuleTestOption -> Rep RuleTestOption x)
-> (forall x. Rep RuleTestOption x -> RuleTestOption)
-> Generic RuleTestOption
forall x. Rep RuleTestOption x -> RuleTestOption
forall x. RuleTestOption -> Rep RuleTestOption x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RuleTestOption -> Rep RuleTestOption x
from :: forall x. RuleTestOption -> Rep RuleTestOption x
$cto :: forall x. Rep RuleTestOption x -> RuleTestOption
to :: forall x. Rep RuleTestOption x -> RuleTestOption
Generic, Int -> RuleTestOption -> ShowS
[RuleTestOption] -> ShowS
RuleTestOption -> [Char]
(Int -> RuleTestOption -> ShowS)
-> (RuleTestOption -> [Char])
-> ([RuleTestOption] -> ShowS)
-> Show RuleTestOption
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleTestOption -> ShowS
showsPrec :: Int -> RuleTestOption -> ShowS
$cshow :: RuleTestOption -> [Char]
show :: RuleTestOption -> [Char]
$cshowList :: [RuleTestOption] -> ShowS
showList :: [RuleTestOption] -> ShowS
Show)
instance FromJSON RuleTestOption where
  parseJSON :: Value -> Parser RuleTestOption
parseJSON = Options -> Value -> Parser RuleTestOption
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
defaultOptions{sumEncoding = UntaggedValue}

data AttrsInBindings = AttrsInBindings
  { AttrsInBindings -> [RuleAttribute]
attrs :: [RuleAttribute]
  , AttrsInBindings -> [Binding]
bindings :: [Binding]
  }
  deriving ((forall x. AttrsInBindings -> Rep AttrsInBindings x)
-> (forall x. Rep AttrsInBindings x -> AttrsInBindings)
-> Generic AttrsInBindings
forall x. Rep AttrsInBindings x -> AttrsInBindings
forall x. AttrsInBindings -> Rep AttrsInBindings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AttrsInBindings -> Rep AttrsInBindings x
from :: forall x. AttrsInBindings -> Rep AttrsInBindings x
$cto :: forall x. Rep AttrsInBindings x -> AttrsInBindings
to :: forall x. Rep AttrsInBindings x -> AttrsInBindings
Generic, Int -> AttrsInBindings -> ShowS
[AttrsInBindings] -> ShowS
AttrsInBindings -> [Char]
(Int -> AttrsInBindings -> ShowS)
-> (AttrsInBindings -> [Char])
-> ([AttrsInBindings] -> ShowS)
-> Show AttrsInBindings
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AttrsInBindings -> ShowS
showsPrec :: Int -> AttrsInBindings -> ShowS
$cshow :: AttrsInBindings -> [Char]
show :: AttrsInBindings -> [Char]
$cshowList :: [AttrsInBindings] -> ShowS
showList :: [AttrsInBindings] -> ShowS
Show, Value -> Parser [AttrsInBindings]
Value -> Parser AttrsInBindings
(Value -> Parser AttrsInBindings)
-> (Value -> Parser [AttrsInBindings]) -> FromJSON AttrsInBindings
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
$cparseJSON :: Value -> Parser AttrsInBindings
parseJSON :: Value -> Parser AttrsInBindings
$cparseJSONList :: Value -> Parser [AttrsInBindings]
parseJSONList :: Value -> Parser [AttrsInBindings]
FromJSON)
data Condition
  = IsNF {Condition -> Object
nf :: Object}
  | IsNFInsideFormation {Condition -> Object
nf_inside_formation :: Object}
  | PresentAttrs {Condition -> AttrsInBindings
present_attrs :: AttrsInBindings}
  | AbsentAttrs {Condition -> AttrsInBindings
absent_attrs :: AttrsInBindings}
  | AttrNotEqual {Condition -> (Attribute, Attribute)
not_equal :: (Attribute, Attribute)}
  | ApplyInSubformations {Condition -> Bool
apply_in_subformations :: Bool}
  | ApplyInAbstractSubformations {Condition -> Bool
apply_in_abstract_subformations :: Bool}
  deriving ((forall x. Condition -> Rep Condition x)
-> (forall x. Rep Condition x -> Condition) -> Generic Condition
forall x. Rep Condition x -> Condition
forall x. Condition -> Rep Condition x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Condition -> Rep Condition x
from :: forall x. Condition -> Rep Condition x
$cto :: forall x. Rep Condition x -> Condition
to :: forall x. Rep Condition x -> Condition
Generic, Int -> Condition -> ShowS
[Condition] -> ShowS
Condition -> [Char]
(Int -> Condition -> ShowS)
-> (Condition -> [Char])
-> ([Condition] -> ShowS)
-> Show Condition
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Condition -> ShowS
showsPrec :: Int -> Condition -> ShowS
$cshow :: Condition -> [Char]
show :: Condition -> [Char]
$cshowList :: [Condition] -> ShowS
showList :: [Condition] -> ShowS
Show)
instance FromJSON Condition where
  parseJSON :: Value -> Parser Condition
parseJSON = Options -> Value -> Parser Condition
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
defaultOptions{sumEncoding = UntaggedValue}

parseRuleSetFromFile :: FilePath -> IO RuleSet
parseRuleSetFromFile :: [Char] -> IO RuleSet
parseRuleSetFromFile = [Char] -> IO RuleSet
forall (m :: * -> *) a. (MonadIO m, FromJSON a) => [Char] -> m a
Yaml.decodeFileThrow

convertRule :: Rule -> Common.Rule
convertRule :: Rule -> Rule
convertRule Rule{[Char]
Maybe [MetaId]
Maybe [Condition]
Maybe [RuleTest]
Maybe [FreshMetaId]
Maybe RuleContext
Object
$sel:name:Rule :: Rule -> [Char]
$sel:description:Rule :: Rule -> [Char]
$sel:context:Rule :: Rule -> Maybe RuleContext
$sel:forall:Rule :: Rule -> Maybe [MetaId]
$sel:pattern:Rule :: Rule -> Object
$sel:result:Rule :: Rule -> Object
$sel:fresh:Rule :: Rule -> Maybe [FreshMetaId]
$sel:when:Rule :: Rule -> Maybe [Condition]
$sel:tests:Rule :: Rule -> Maybe [RuleTest]
name :: [Char]
description :: [Char]
context :: Maybe RuleContext
forall :: Maybe [MetaId]
pattern :: Object
result :: Object
fresh :: Maybe [FreshMetaId]
when :: Maybe [Condition]
tests :: Maybe [RuleTest]
..} Context
ctx Object
obj = do
  -- first validate pattern and result in the rule
  -- TODO: we should perform this check once, not every time we run the rule
  let freshMetaIds :: Set MetaId
freshMetaIds =
        (LabelMetaId -> MetaId) -> Set LabelMetaId -> Set MetaId
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic LabelMetaId -> MetaId
MetaIdLabel (Set LabelMetaId -> Set MetaId) -> Set LabelMetaId -> Set MetaId
forall a b. (a -> b) -> a -> b
$
          ([FreshMetaId] -> Set LabelMetaId)
-> Maybe [FreshMetaId] -> Set LabelMetaId
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ([LabelMetaId] -> Set LabelMetaId
forall a. Ord a => [a] -> Set a
Set.fromList ([LabelMetaId] -> Set LabelMetaId)
-> ([FreshMetaId] -> [LabelMetaId])
-> [FreshMetaId]
-> Set LabelMetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FreshMetaId -> LabelMetaId) -> [FreshMetaId] -> [LabelMetaId]
forall a b. (a -> b) -> [a] -> [b]
map (\FreshMetaId{$sel:name:FreshMetaId :: FreshMetaId -> LabelMetaId
name = LabelMetaId
x} -> LabelMetaId
x)) Maybe [FreshMetaId]
fresh

      patternMetaIds :: Set MetaId
patternMetaIds = Object -> Set MetaId
objectMetaIds Object
pattern
      resultMetaIds :: Set MetaId
resultMetaIds = Object -> Set MetaId
objectMetaIds Object
result

      unusedFreshMetaIds :: Set MetaId
unusedFreshMetaIds = Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set MetaId
freshMetaIds Set MetaId
resultMetaIds

      ppMetaIds :: Set MetaId -> [Char]
ppMetaIds = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ([[Char]] -> [Char])
-> (Set MetaId -> [[Char]]) -> Set MetaId -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> [Char]) -> [MetaId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> [Char]
forall a. Print a => a -> [Char]
printTree ([MetaId] -> [[Char]])
-> (Set MetaId -> [MetaId]) -> Set MetaId -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList

  Bool -> [()] -> [()]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set MetaId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set MetaId
unusedFreshMetaIds) ([()] -> [()]) -> [()] -> [()]
forall a b. (a -> b) -> a -> b
$
    [Char] -> [()]
forall a. HasCallStack => [Char] -> a
error ([Char]
"invalid rule: result does not use some fresh variables quantified by the fresh: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set MetaId -> [Char]
ppMetaIds Set MetaId
unusedFreshMetaIds)

  case Maybe [MetaId]
forall of
    Maybe [MetaId]
Nothing -> () -> [()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just [MetaId]
forall' -> do
      let forallMetaIds :: Set MetaId
forallMetaIds = [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
forall'
          resultAllowedMetaIds :: Set MetaId
resultAllowedMetaIds = Set MetaId
forallMetaIds Set MetaId -> Set MetaId -> Set MetaId
forall a. Semigroup a => a -> a -> a
<> Set MetaId
freshMetaIds
          unquantifiedMetaIds :: Set MetaId
unquantifiedMetaIds = Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set MetaId
patternMetaIds Set MetaId
forallMetaIds
          unusedMetaIds :: Set MetaId
unusedMetaIds = Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set MetaId
forallMetaIds Set MetaId
patternMetaIds
          unquantifiedResultMetaIds :: Set MetaId
unquantifiedResultMetaIds = Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set MetaId
resultMetaIds Set MetaId
resultAllowedMetaIds
      Bool -> [()] -> [()]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set MetaId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set MetaId
unquantifiedMetaIds) ([()] -> [()]) -> [()] -> [()]
forall a b. (a -> b) -> a -> b
$
        [Char] -> [()]
forall a. HasCallStack => [Char] -> a
error ([Char]
"invalid rule: pattern uses meta variables not quantified by the forall: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set MetaId -> [Char]
ppMetaIds Set MetaId
unquantifiedMetaIds)
      Bool -> [()] -> [()]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set MetaId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set MetaId
unusedMetaIds) ([()] -> [()]) -> [()] -> [()]
forall a b. (a -> b) -> a -> b
$
        [Char] -> [()]
forall a. HasCallStack => [Char] -> a
error ([Char]
"invalid rule: pattern does not use some variables quantified by the forall: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set MetaId -> [Char]
ppMetaIds Set MetaId
unusedMetaIds)
      Bool -> [()] -> [()]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set MetaId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set MetaId
unquantifiedResultMetaIds) ([()] -> [()]) -> [()] -> [()]
forall a b. (a -> b) -> a -> b
$
        [Char] -> [()]
forall a. HasCallStack => [Char] -> a
error ([Char]
"invalid rule: result uses meta variables not quantified by the forall or the fresh: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set MetaId -> [Char]
ppMetaIds Set MetaId
unquantifiedResultMetaIds)

  Subst
contextSubsts <- Context -> Maybe RuleContext -> [Subst]
matchContext Context
ctx Maybe RuleContext
context
  let pattern' :: Object
pattern' = Subst -> Object -> Object
applySubst Subst
contextSubsts Object
pattern
      result' :: Object
result' = Subst -> Object -> Object
applySubst Subst
contextSubsts Object
result
  Subst
subst <- Object -> Object -> [Subst]
matchObject Object
pattern' Object
obj
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ (Condition -> Bool) -> [Condition] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Condition
cond -> Context -> Condition -> Subst -> Bool
checkCond Context
ctx Condition
cond (Subst
contextSubsts Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst)) ([Condition] -> Maybe [Condition] -> [Condition]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Condition]
when)
  let substFresh :: Subst
substFresh = Context -> Object -> Maybe [FreshMetaId] -> Subst
mkFreshSubst Context
ctx Object
result' Maybe [FreshMetaId]
fresh
      result'' :: Object
result'' = Subst -> Object -> Object
applySubst (Subst
contextSubsts Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
substFresh) Object
result'
      -- TODO #152:30m what context should we pass to evaluate meta funcs?
      obj' :: Object
obj' = Object -> Object -> Object
evaluateMetaFuncs Object
obj Object
result''
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Object -> Bool
objectHasMetavars Object
obj')
  Object -> [Object]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Object
obj'

convertRuleNamed :: Rule -> NamedRule
convertRuleNamed :: Rule -> NamedRule
convertRuleNamed Rule
rule = (Rule
rule.name, Rule -> Rule
convertRule Rule
rule)

mkFreshSubst :: Context -> Object -> Maybe [FreshMetaId] -> Subst
mkFreshSubst :: Context -> Object -> Maybe [FreshMetaId] -> Subst
mkFreshSubst Context
ctx Object
obj Maybe [FreshMetaId]
metas =
  Subst
    { $sel:objectMetas:Subst :: [(ObjectMetaId, Object)]
objectMetas = []
    , $sel:bindingsMetas:Subst :: [(BindingsMetaId, [Binding])]
bindingsMetas = []
    , $sel:attributeMetas:Subst :: [(LabelMetaId, Attribute)]
attributeMetas = Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)]
mkFreshAttributes (Context -> Set LabelId
usedLabelIds Context
ctx Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> Object -> Set LabelId
objectLabelIds Object
obj) ([FreshMetaId] -> Maybe [FreshMetaId] -> [FreshMetaId]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [FreshMetaId]
metas)
    , $sel:bytesMetas:Subst :: [(BytesMetaId, Bytes)]
bytesMetas = []
    , $sel:contextMetas:Subst :: [(TailMetaId, OneHoleContext)]
contextMetas = []
    }

mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)]
mkFreshAttributes :: Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)]
mkFreshAttributes Set LabelId
_ids [] = []
mkFreshAttributes Set LabelId
ids (FreshMetaId
x : [FreshMetaId]
xs) =
  case Set LabelId
-> FreshMetaId -> ((LabelMetaId, Attribute), Set LabelId)
mkFreshAttribute Set LabelId
ids FreshMetaId
x of
    ((LabelMetaId, Attribute)
ma, Set LabelId
ids') -> (LabelMetaId, Attribute)
ma (LabelMetaId, Attribute)
-> [(LabelMetaId, Attribute)] -> [(LabelMetaId, Attribute)]
forall a. a -> [a] -> [a]
: Set LabelId -> [FreshMetaId] -> [(LabelMetaId, Attribute)]
mkFreshAttributes Set LabelId
ids' [FreshMetaId]
xs

mkFreshAttribute :: Set LabelId -> FreshMetaId -> ((LabelMetaId, Attribute), Set LabelId)
mkFreshAttribute :: Set LabelId
-> FreshMetaId -> ((LabelMetaId, Attribute), Set LabelId)
mkFreshAttribute Set LabelId
ids FreshMetaId{Maybe [Char]
LabelMetaId
$sel:name:FreshMetaId :: FreshMetaId -> LabelMetaId
$sel:prefix:FreshMetaId :: FreshMetaId -> Maybe [Char]
name :: LabelMetaId
prefix :: Maybe [Char]
..} = ((LabelMetaId
name, LabelId -> Attribute
Label LabelId
label), LabelId -> Set LabelId -> Set LabelId
forall a. Ord a => a -> Set a -> Set a
Set.insert LabelId
label Set LabelId
ids)
 where
  label :: LabelId
label =
    [LabelId] -> LabelId
forall a. HasCallStack => [a] -> a
head
      [ LabelId
l
      | Integer
i <- [Integer
1 ..]
      , let l :: LabelId
l = [Char] -> LabelId
LabelId ([Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"tmp" Maybe [Char]
prefix [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"$" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i)
      , LabelId
l LabelId -> Set LabelId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set LabelId
ids
      ]

usedLabelIds :: Context -> Set LabelId
usedLabelIds :: Context -> Set LabelId
usedLabelIds Context{Bool
[NamedRule]
NonEmpty Object
Atoms
Attribute
builtinRules :: Bool
allRules :: [NamedRule]
enabledAtoms :: Atoms
knownAtoms :: Atoms
outerFormations :: NonEmpty Object
currentAttr :: Attribute
insideFormation :: Bool
insideAbstractFormation :: Bool
dataizePackage :: Bool
minimizeTerms :: Bool
insideSubObject :: Bool
builtinRules :: Context -> Bool
allRules :: Context -> [NamedRule]
enabledAtoms :: Context -> Atoms
knownAtoms :: Context -> Atoms
outerFormations :: Context -> NonEmpty Object
currentAttr :: Context -> Attribute
insideFormation :: Context -> Bool
insideAbstractFormation :: Context -> Bool
dataizePackage :: Context -> Bool
minimizeTerms :: Context -> Bool
insideSubObject :: Context -> Bool
..} = Object -> Set LabelId
objectLabelIds Object
globalObject
 where
  globalObject :: Object
globalObject = NonEmpty Object -> Object
forall a. NonEmpty a -> a
NonEmpty.last NonEmpty Object
outerFormations

objectLabelIds :: Object -> Set LabelId
objectLabelIds :: Object -> Set LabelId
objectLabelIds = \case
  Object
GlobalObject -> Set LabelId
forall a. Monoid a => a
mempty
  Object
ThisObject -> Set LabelId
forall a. Monoid a => a
mempty
  Formation [Binding]
bindings -> (Binding -> Set LabelId) -> [Binding] -> Set LabelId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding -> Set LabelId
bindingLabelIds [Binding]
bindings
  ObjectDispatch Object
obj Attribute
a -> Object -> Set LabelId
objectLabelIds Object
obj Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> Attribute -> Set LabelId
attrLabelIds Attribute
a
  Application Object
obj [Binding]
bindings -> Object -> Set LabelId
objectLabelIds Object
obj Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> (Binding -> Set LabelId) -> [Binding] -> Set LabelId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding -> Set LabelId
bindingLabelIds [Binding]
bindings
  Object
Termination -> Set LabelId
forall a. Monoid a => a
mempty
  MetaObject{} -> Set LabelId
forall a. Monoid a => a
mempty
  MetaFunction MetaFunctionName
_ Object
obj -> Object -> Set LabelId
objectLabelIds Object
obj
  MetaTailContext Object
obj TailMetaId
_ -> Object -> Set LabelId
objectLabelIds Object
obj
  MetaSubstThis Object
obj Object
obj' -> Object -> Set LabelId
objectLabelIds Object
obj Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> Object -> Set LabelId
objectLabelIds Object
obj'
  MetaContextualize Object
obj Object
obj' -> Object -> Set LabelId
objectLabelIds Object
obj Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> Object -> Set LabelId
objectLabelIds Object
obj'

bindingLabelIds :: Binding -> Set LabelId
bindingLabelIds :: Binding -> Set LabelId
bindingLabelIds = \case
  AlphaBinding Attribute
a Object
obj -> Object -> Set LabelId
objectLabelIds Object
obj Set LabelId -> Set LabelId -> Set LabelId
forall a. Semigroup a => a -> a -> a
<> Attribute -> Set LabelId
attrLabelIds Attribute
a
  DeltaBinding Bytes
_bytes -> Set LabelId
forall a. Monoid a => a
mempty
  EmptyBinding Attribute
a -> Attribute -> Set LabelId
attrLabelIds Attribute
a
  Binding
DeltaEmptyBinding -> Set LabelId
forall a. Monoid a => a
mempty
  LambdaBinding Function
_ -> Set LabelId
forall a. Monoid a => a
mempty
  MetaBindings BindingsMetaId
_ -> Set LabelId
forall a. Monoid a => a
mempty
  MetaDeltaBinding BytesMetaId
_ -> Set LabelId
forall a. Monoid a => a
mempty

attrLabelIds :: Attribute -> Set LabelId
attrLabelIds :: Attribute -> Set LabelId
attrLabelIds (Label LabelId
l) = LabelId -> Set LabelId
forall a. a -> Set a
Set.singleton LabelId
l
attrLabelIds Attribute
_ = Set LabelId
forall a. Monoid a => a
mempty

-- >>> matchContext (Context [] ["⟦ a ↦ ⟦ ⟧, x ↦ ξ.a ⟧"] (Label (LabelId "x"))) (Just (RuleContext Nothing (Just "⟦ !a ↦ !obj, !B ⟧") (Just "!a")))
-- [Subst {
--   objectMetas = [!obj -> 'ξ.a']
--   bindingsMetas = [!B -> 'a ↦ ⟦ ⟧']
--   attributeMetas = [!a -> 'x']
-- }]
matchContext :: Common.Context -> Maybe RuleContext -> [Subst]
matchContext :: Context -> Maybe RuleContext -> [Subst]
matchContext Common.Context{} Maybe RuleContext
Nothing = [Subst
emptySubst]
matchContext Common.Context{Bool
[NamedRule]
NonEmpty Object
Atoms
Attribute
builtinRules :: Context -> Bool
allRules :: Context -> [NamedRule]
enabledAtoms :: Context -> Atoms
knownAtoms :: Context -> Atoms
outerFormations :: Context -> NonEmpty Object
currentAttr :: Context -> Attribute
insideFormation :: Context -> Bool
insideAbstractFormation :: Context -> Bool
dataizePackage :: Context -> Bool
minimizeTerms :: Context -> Bool
insideSubObject :: Context -> Bool
builtinRules :: Bool
allRules :: [NamedRule]
enabledAtoms :: Atoms
knownAtoms :: Atoms
outerFormations :: NonEmpty Object
currentAttr :: Attribute
insideFormation :: Bool
insideAbstractFormation :: Bool
dataizePackage :: Bool
minimizeTerms :: Bool
insideSubObject :: Bool
..} (Just (RuleContext{Maybe Attribute
Maybe Object
$sel:global_object:RuleContext :: RuleContext -> Maybe Object
$sel:current_object:RuleContext :: RuleContext -> Maybe Object
$sel:current_attribute:RuleContext :: RuleContext -> Maybe Attribute
global_object :: Maybe Object
current_object :: Maybe Object
current_attribute :: Maybe Attribute
..})) = do
  Subst
subst1 <- [Subst] -> (Object -> [Subst]) -> Maybe Object -> [Subst]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Subst
emptySubst] (Object -> Object -> [Subst]
`matchObject` Object
globalObject) Maybe Object
global_object
  Subst
subst2 <- [Subst] -> (Object -> [Subst]) -> Maybe Object -> [Subst]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Subst
emptySubst] ((Object -> Object -> [Subst]
`matchObject` Object
thisObject) (Object -> [Subst]) -> (Object -> Object) -> Object -> [Subst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Object -> Object
applySubst Subst
subst1) Maybe Object
current_object
  Subst
subst3 <- [Subst] -> (Attribute -> [Subst]) -> Maybe Attribute -> [Subst]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Subst
emptySubst] ((Attribute -> Attribute -> [Subst]
`matchAttr` Attribute
currentAttr) (Attribute -> [Subst])
-> (Attribute -> Attribute) -> Attribute -> [Subst]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Attribute -> Attribute
applySubstAttr (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2)) Maybe Attribute
current_attribute
  Subst -> [Subst]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst3)
 where
  globalObject :: Object
globalObject = NonEmpty Object -> Object
forall a. NonEmpty a -> a
NonEmpty.last NonEmpty Object
outerFormations
  thisObject :: Object
thisObject = NonEmpty Object -> Object
forall a. NonEmpty a -> a
NonEmpty.head NonEmpty Object
outerFormations

objectMetaIds :: Object -> Set MetaId
objectMetaIds :: Object -> Set MetaId
objectMetaIds (Formation [Binding]
bindings) = (Binding -> Set MetaId) -> [Binding] -> Set MetaId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding -> Set MetaId
bindingMetaIds [Binding]
bindings
objectMetaIds (Application Object
object [Binding]
bindings) = Object -> Set MetaId
objectMetaIds Object
object Set MetaId -> Set MetaId -> Set MetaId
forall a. Semigroup a => a -> a -> a
<> (Binding -> Set MetaId) -> [Binding] -> Set MetaId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding -> Set MetaId
bindingMetaIds [Binding]
bindings
objectMetaIds (ObjectDispatch Object
object Attribute
attr) = Object -> Set MetaId
objectMetaIds Object
object Set MetaId -> Set MetaId -> Set MetaId
forall a. Semigroup a => a -> a -> a
<> Attribute -> Set MetaId
attrMetaIds Attribute
attr
objectMetaIds Object
GlobalObject = Set MetaId
forall a. Monoid a => a
mempty
objectMetaIds Object
ThisObject = Set MetaId
forall a. Monoid a => a
mempty
objectMetaIds Object
Termination = Set MetaId
forall a. Monoid a => a
mempty
objectMetaIds (MetaObject ObjectMetaId
x) = MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (ObjectMetaId -> MetaId
MetaIdObject ObjectMetaId
x)
objectMetaIds (MetaFunction MetaFunctionName
_ Object
obj) = Object -> Set MetaId
objectMetaIds Object
obj
objectMetaIds (MetaTailContext Object
obj TailMetaId
x) = Object -> Set MetaId
objectMetaIds Object
obj Set MetaId -> Set MetaId -> Set MetaId
forall a. Semigroup a => a -> a -> a
<> MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (TailMetaId -> MetaId
MetaIdTail TailMetaId
x)
objectMetaIds (MetaSubstThis Object
obj Object
obj') = (Object -> Set MetaId) -> [Object] -> Set MetaId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Object -> Set MetaId
objectMetaIds [Object
obj, Object
obj']
objectMetaIds (MetaContextualize Object
obj Object
obj') = (Object -> Set MetaId) -> [Object] -> Set MetaId
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Object -> Set MetaId
objectMetaIds [Object
obj, Object
obj']

bindingMetaIds :: Binding -> Set MetaId
bindingMetaIds :: Binding -> Set MetaId
bindingMetaIds (AlphaBinding Attribute
attr Object
obj) = Attribute -> Set MetaId
attrMetaIds Attribute
attr Set MetaId -> Set MetaId -> Set MetaId
forall a. Semigroup a => a -> a -> a
<> Object -> Set MetaId
objectMetaIds Object
obj
bindingMetaIds (EmptyBinding Attribute
attr) = Attribute -> Set MetaId
attrMetaIds Attribute
attr
bindingMetaIds (DeltaBinding Bytes
_) = Set MetaId
forall a. Monoid a => a
mempty
bindingMetaIds Binding
DeltaEmptyBinding = Set MetaId
forall a. Monoid a => a
mempty
bindingMetaIds (LambdaBinding Function
_) = Set MetaId
forall a. Monoid a => a
mempty
bindingMetaIds (MetaBindings BindingsMetaId
x) = MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (BindingsMetaId -> MetaId
MetaIdBindings BindingsMetaId
x)
bindingMetaIds (MetaDeltaBinding BytesMetaId
x) = MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (BytesMetaId -> MetaId
MetaIdBytes BytesMetaId
x)

attrMetaIds :: Attribute -> Set MetaId
attrMetaIds :: Attribute -> Set MetaId
attrMetaIds Attribute
Phi = Set MetaId
forall a. Monoid a => a
mempty
attrMetaIds Attribute
Rho = Set MetaId
forall a. Monoid a => a
mempty
attrMetaIds (Label LabelId
_) = Set MetaId
forall a. Monoid a => a
mempty
attrMetaIds (Alpha AlphaIndex
_) = Set MetaId
forall a. Monoid a => a
mempty
attrMetaIds (MetaAttr LabelMetaId
x) = MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (LabelMetaId -> MetaId
MetaIdLabel LabelMetaId
x)

objectHasMetavars :: Object -> Bool
objectHasMetavars :: Object -> Bool
objectHasMetavars (Formation [Binding]
bindings) = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
bindingHasMetavars [Binding]
bindings
objectHasMetavars (Application Object
object [Binding]
bindings) = Object -> Bool
objectHasMetavars Object
object Bool -> Bool -> Bool
|| (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
bindingHasMetavars [Binding]
bindings
objectHasMetavars (ObjectDispatch Object
object Attribute
attr) = Object -> Bool
objectHasMetavars Object
object Bool -> Bool -> Bool
|| Attribute -> Bool
attrHasMetavars Attribute
attr
objectHasMetavars Object
GlobalObject = Bool
False
objectHasMetavars Object
ThisObject = Bool
False
objectHasMetavars Object
Termination = Bool
False
objectHasMetavars (MetaObject ObjectMetaId
_) = Bool
True
objectHasMetavars (MetaFunction MetaFunctionName
_ Object
_) = Bool
True
objectHasMetavars MetaTailContext{} = Bool
True
objectHasMetavars (MetaSubstThis Object
_ Object
_) = Bool
True -- technically not a metavar, but a substitution
objectHasMetavars (MetaContextualize Object
_ Object
_) = Bool
True

bindingHasMetavars :: Binding -> Bool
bindingHasMetavars :: Binding -> Bool
bindingHasMetavars (AlphaBinding Attribute
attr Object
obj) = Attribute -> Bool
attrHasMetavars Attribute
attr Bool -> Bool -> Bool
|| Object -> Bool
objectHasMetavars Object
obj
bindingHasMetavars (EmptyBinding Attribute
attr) = Attribute -> Bool
attrHasMetavars Attribute
attr
bindingHasMetavars (DeltaBinding Bytes
_) = Bool
False
bindingHasMetavars Binding
DeltaEmptyBinding = Bool
False
bindingHasMetavars (LambdaBinding Function
_) = Bool
False
bindingHasMetavars (MetaBindings BindingsMetaId
_) = Bool
True
bindingHasMetavars (MetaDeltaBinding BytesMetaId
_) = Bool
True

attrHasMetavars :: Attribute -> Bool
attrHasMetavars :: Attribute -> Bool
attrHasMetavars Attribute
Phi = Bool
False
attrHasMetavars Attribute
Rho = Bool
False
attrHasMetavars (Label LabelId
_) = Bool
False
attrHasMetavars (Alpha AlphaIndex
_) = Bool
False
attrHasMetavars (MetaAttr LabelMetaId
_) = Bool
True

-- | Given a condition, and a substition from object matching
--   tells whether the condition matches the object
checkCond :: Common.Context -> Condition -> Subst -> Bool
checkCond :: Context -> Condition -> Subst -> Bool
checkCond Context
ctx (IsNF Object
obj) Subst
subst = Context -> Object -> Bool
Common.isNF Context
ctx (Object -> Bool) -> Object -> Bool
forall a b. (a -> b) -> a -> b
$ Subst -> Object -> Object
applySubst Subst
subst Object
obj
checkCond Context
ctx (IsNFInsideFormation Object
obj) Subst
subst = Context -> Object -> Bool
Common.isNF Context
ctx{insideFormation = True} (Object -> Bool) -> Object -> Bool
forall a b. (a -> b) -> a -> b
$ Subst -> Object -> Object
applySubst Subst
subst Object
obj
checkCond Context
_ctx (PresentAttrs (AttrsInBindings [RuleAttribute]
attrs [Binding]
bindings)) Subst
subst = (RuleAttribute -> Bool) -> [RuleAttribute] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RuleAttribute -> [Binding] -> Bool
`hasAttr` [Binding]
substitutedBindings) [RuleAttribute]
substitutedAttrs
 where
  substitutedBindings :: [Binding]
substitutedBindings = (Binding -> [Binding]) -> [Binding] -> [Binding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Subst -> Binding -> [Binding]
applySubstBinding Subst
subst) [Binding]
bindings
  ruleToNormalAttr :: RuleAttribute -> Attribute
  ruleToNormalAttr :: RuleAttribute -> Attribute
ruleToNormalAttr (ObjectAttr Attribute
a) = Attribute
a
  -- Hack to be able to use applySubstAttr with RuleAttribute.
  -- Should not actually substitute anything anyway since they are not metavariables
  ruleToNormalAttr RuleAttribute
DeltaAttr = LabelId -> Attribute
Label ([Char] -> LabelId
LabelId [Char]
"Δ")
  ruleToNormalAttr RuleAttribute
LambdaAttr = LabelId -> Attribute
Label ([Char] -> LabelId
LabelId [Char]
"λ")
  normalToRuleAttr :: Attribute -> RuleAttribute
  normalToRuleAttr :: Attribute -> RuleAttribute
normalToRuleAttr (Label (LabelId [Char]
"Δ")) = RuleAttribute
DeltaAttr
  normalToRuleAttr (Label (LabelId [Char]
"λ")) = RuleAttribute
LambdaAttr
  normalToRuleAttr Attribute
a = Attribute -> RuleAttribute
ObjectAttr Attribute
a
  substitutedAttrs :: [RuleAttribute]
substitutedAttrs = (RuleAttribute -> RuleAttribute)
-> [RuleAttribute] -> [RuleAttribute]
forall a b. (a -> b) -> [a] -> [b]
map (Attribute -> RuleAttribute
normalToRuleAttr (Attribute -> RuleAttribute)
-> (RuleAttribute -> Attribute) -> RuleAttribute -> RuleAttribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Attribute -> Attribute
applySubstAttr Subst
subst (Attribute -> Attribute)
-> (RuleAttribute -> Attribute) -> RuleAttribute -> Attribute
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RuleAttribute -> Attribute
ruleToNormalAttr) [RuleAttribute]
attrs
checkCond Context
ctx (AbsentAttrs AttrsInBindings
s) Subst
subst = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Condition -> Subst -> Bool
checkCond Context
ctx (AttrsInBindings -> Condition
PresentAttrs AttrsInBindings
s) Subst
subst
checkCond Context
_ctx (AttrNotEqual (Attribute
a1, Attribute
a2)) Subst
subst = Subst -> Attribute -> Attribute
applySubstAttr Subst
subst Attribute
a1 Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
/= Subst -> Attribute -> Attribute
applySubstAttr Subst
subst Attribute
a2
checkCond Context
ctx (ApplyInSubformations Bool
shouldApply) Subst
_subst
  | Bool
shouldApply = Bool
True
  | Bool
otherwise = Bool -> Bool
not (Context -> Bool
insideFormation Context
ctx)
checkCond Context
ctx (ApplyInAbstractSubformations Bool
shouldApply) Subst
_subst
  | Bool
shouldApply = Bool
True
  | Bool
otherwise = Bool -> Bool
not (Context -> Bool
insideAbstractFormation Context
ctx)

hasAttr :: RuleAttribute -> [Binding] -> Bool
hasAttr :: RuleAttribute -> [Binding] -> Bool
hasAttr RuleAttribute
attr = (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RuleAttribute -> Binding -> Bool
isAttr RuleAttribute
attr)
 where
  isAttr :: RuleAttribute -> Binding -> Bool
isAttr (ObjectAttr Attribute
a) (AlphaBinding Attribute
a' Object
_) = Attribute
a Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
a'
  isAttr (ObjectAttr Attribute
a) (EmptyBinding Attribute
a') = Attribute
a Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
a'
  isAttr RuleAttribute
DeltaAttr (DeltaBinding Bytes
_) = Bool
True
  isAttr RuleAttribute
DeltaAttr Binding
DeltaEmptyBinding = Bool
True
  isAttr RuleAttribute
LambdaAttr (LambdaBinding Function
_) = Bool
True
  isAttr RuleAttribute
_ Binding
_ = Bool
False

-- input: ⟦ a ↦ ⟦ c ↦ ⟦ ⟧ ⟧, b ↦ ⟦ ⟧ ⟧.a

-- pattern:   ⟦ !a ↦ !n, !B ⟧.!a
-- result:    !n(ρ ↦ ⟦ !B ⟧)

-- match pattern input (get substitution):
--  !a = a
--  !n = ⟦ c ↦ ⟦ ⟧ ⟧
--  !B = b ↦ ⟦ ⟧

-- actual result (after applying substitution):
--  ⟦ c ↦ ⟦ ⟧ ⟧(ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)

data OneHoleContext = OneHoleContext
  { OneHoleContext -> ObjectMetaId
holeMetaId :: !ObjectMetaId
  , OneHoleContext -> Object
contextObject :: !Object
  }
  deriving (Int -> OneHoleContext -> ShowS
[OneHoleContext] -> ShowS
OneHoleContext -> [Char]
(Int -> OneHoleContext -> ShowS)
-> (OneHoleContext -> [Char])
-> ([OneHoleContext] -> ShowS)
-> Show OneHoleContext
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OneHoleContext -> ShowS
showsPrec :: Int -> OneHoleContext -> ShowS
$cshow :: OneHoleContext -> [Char]
show :: OneHoleContext -> [Char]
$cshowList :: [OneHoleContext] -> ShowS
showList :: [OneHoleContext] -> ShowS
Show)

data Subst = Subst
  { Subst -> [(ObjectMetaId, Object)]
objectMetas :: [(ObjectMetaId, Object)]
  , Subst -> [(BindingsMetaId, [Binding])]
bindingsMetas :: [(BindingsMetaId, [Binding])]
  , Subst -> [(LabelMetaId, Attribute)]
attributeMetas :: [(LabelMetaId, Attribute)]
  , Subst -> [(BytesMetaId, Bytes)]
bytesMetas :: [(BytesMetaId, Bytes)]
  , Subst -> [(TailMetaId, OneHoleContext)]
contextMetas :: [(TailMetaId, OneHoleContext)]
  }
instance Show Subst where
  show :: Subst -> [Char]
show Subst{[(BytesMetaId, Bytes)]
[(ObjectMetaId, Object)]
[(BindingsMetaId, [Binding])]
[(TailMetaId, OneHoleContext)]
[(LabelMetaId, Attribute)]
$sel:objectMetas:Subst :: Subst -> [(ObjectMetaId, Object)]
$sel:bindingsMetas:Subst :: Subst -> [(BindingsMetaId, [Binding])]
$sel:attributeMetas:Subst :: Subst -> [(LabelMetaId, Attribute)]
$sel:bytesMetas:Subst :: Subst -> [(BytesMetaId, Bytes)]
$sel:contextMetas:Subst :: Subst -> [(TailMetaId, OneHoleContext)]
objectMetas :: [(ObjectMetaId, Object)]
bindingsMetas :: [(BindingsMetaId, [Binding])]
attributeMetas :: [(LabelMetaId, Attribute)]
bytesMetas :: [(BytesMetaId, Bytes)]
contextMetas :: [(TailMetaId, OneHoleContext)]
..} =
    [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate
      [Char]
"\n"
      [ [Char]
"Subst {"
      , [Char]
"  objectMetas = [" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(ObjectMetaId, Object)] -> [Char]
forall {a} {a}. (Print a, Print a) => [(a, a)] -> [Char]
showMappings [(ObjectMetaId, Object)]
objectMetas [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]"
      , [Char]
"  bindingsMetas = [" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(BindingsMetaId, [Binding])] -> [Char]
forall {a} {a}. (Print a, Print a) => [(a, a)] -> [Char]
showMappings [(BindingsMetaId, [Binding])]
bindingsMetas [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]"
      , [Char]
"  attributeMetas = [" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(LabelMetaId, Attribute)] -> [Char]
forall {a} {a}. (Print a, Print a) => [(a, a)] -> [Char]
showMappings [(LabelMetaId, Attribute)]
attributeMetas [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]"
      , [Char]
"  bytesMetas = [" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(BytesMetaId, Bytes)] -> [Char]
forall {a} {a}. (Print a, Print a) => [(a, a)] -> [Char]
showMappings [(BytesMetaId, Bytes)]
bytesMetas [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]"
      , [Char]
"  contextMetas = [" [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(TailMetaId, OneHoleContext)] -> [Char]
forall a. Show a => a -> [Char]
show [(TailMetaId, OneHoleContext)]
contextMetas [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Char]
"]"
      , [Char]
"}"
      ]
   where
    showMappings :: [(a, a)] -> [Char]
showMappings [(a, a)]
metas = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"; " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ((a, a) -> [Char]) -> [(a, a)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
metaId, a
obj) -> [fmt|{printTree metaId} -> '{printTree obj}'|]) [(a, a)]
metas

instance Semigroup Subst where
  <> :: Subst -> Subst -> Subst
(<>) = Subst -> Subst -> Subst
mergeSubst

instance Monoid Subst where
  mempty :: Subst
mempty = Subst
emptySubst

emptySubst :: Subst
emptySubst :: Subst
emptySubst = [(ObjectMetaId, Object)]
-> [(BindingsMetaId, [Binding])]
-> [(LabelMetaId, Attribute)]
-> [(BytesMetaId, Bytes)]
-> [(TailMetaId, OneHoleContext)]
-> Subst
Subst [] [] [] [] []

-- >>> putStrLn $ Language.EO.Phi.printTree (applySubst (Subst [("!n", "⟦ c ↦ ⟦ ⟧ ⟧")] [("!B", ["b ↦ ⟦ ⟧"])] [("!a", "a")]) "!n(ρ ↦ ⟦ !B ⟧)" :: Object)
-- ⟦ c ↦ ⟦ ⟧ ⟧ (ρ ↦ ⟦ b ↦ ⟦ ⟧ ⟧)
applySubst :: Subst -> Object -> Object
applySubst :: Subst -> Object -> Object
applySubst subst :: Subst
subst@Subst{[(BytesMetaId, Bytes)]
[(ObjectMetaId, Object)]
[(BindingsMetaId, [Binding])]
[(TailMetaId, OneHoleContext)]
[(LabelMetaId, Attribute)]
$sel:objectMetas:Subst :: Subst -> [(ObjectMetaId, Object)]
$sel:bindingsMetas:Subst :: Subst -> [(BindingsMetaId, [Binding])]
$sel:attributeMetas:Subst :: Subst -> [(LabelMetaId, Attribute)]
$sel:bytesMetas:Subst :: Subst -> [(BytesMetaId, Bytes)]
$sel:contextMetas:Subst :: Subst -> [(TailMetaId, OneHoleContext)]
objectMetas :: [(ObjectMetaId, Object)]
bindingsMetas :: [(BindingsMetaId, [Binding])]
attributeMetas :: [(LabelMetaId, Attribute)]
bytesMetas :: [(BytesMetaId, Bytes)]
contextMetas :: [(TailMetaId, OneHoleContext)]
..} = \case
  Formation [Binding]
bindings ->
    [Binding] -> Object
Formation (Subst -> [Binding] -> [Binding]
applySubstBindings Subst
subst [Binding]
bindings)
  Application Object
obj [Binding]
bindings ->
    Object -> [Binding] -> Object
Application (Subst -> Object -> Object
applySubst Subst
subst Object
obj) (Subst -> [Binding] -> [Binding]
applySubstBindings Subst
subst [Binding]
bindings)
  ObjectDispatch Object
obj Attribute
a ->
    Object -> Attribute -> Object
ObjectDispatch (Subst -> Object -> Object
applySubst Subst
subst Object
obj) (Subst -> Attribute -> Attribute
applySubstAttr Subst
subst Attribute
a)
  Object
GlobalObject -> Object
GlobalObject
  Object
ThisObject -> Object
ThisObject
  obj :: Object
obj@(MetaObject ObjectMetaId
x) -> Object -> Maybe Object -> Object
forall a. a -> Maybe a -> a
fromMaybe Object
obj (Maybe Object -> Object) -> Maybe Object -> Object
forall a b. (a -> b) -> a -> b
$ ObjectMetaId -> [(ObjectMetaId, Object)] -> Maybe Object
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ObjectMetaId
x [(ObjectMetaId, Object)]
objectMetas
  Object
Termination -> Object
Termination
  MetaSubstThis Object
obj Object
thisObj -> Object -> Object -> Object
MetaSubstThis (Subst -> Object -> Object
applySubst Subst
subst Object
obj) (Subst -> Object -> Object
applySubst Subst
subst Object
thisObj)
  MetaContextualize Object
obj Object
thisObj -> Object -> Object -> Object
MetaContextualize (Subst -> Object -> Object
applySubst Subst
subst Object
obj) (Subst -> Object -> Object
applySubst Subst
subst Object
thisObj)
  obj :: Object
obj@MetaFunction{} -> Object
obj
  MetaTailContext Object
obj TailMetaId
c ->
    case TailMetaId
-> [(TailMetaId, OneHoleContext)] -> Maybe OneHoleContext
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TailMetaId
c [(TailMetaId, OneHoleContext)]
contextMetas of
      Maybe OneHoleContext
Nothing -> Object -> TailMetaId -> Object
MetaTailContext (Subst -> Object -> Object
applySubst Subst
subst Object
obj) TailMetaId
c
      Just OneHoleContext{ObjectMetaId
Object
$sel:holeMetaId:OneHoleContext :: OneHoleContext -> ObjectMetaId
$sel:contextObject:OneHoleContext :: OneHoleContext -> Object
holeMetaId :: ObjectMetaId
contextObject :: Object
..} ->
        let holeSubst :: Subst
holeSubst = Subst
forall a. Monoid a => a
mempty{objectMetas = [(holeMetaId, applySubst subst obj)]}
         in Subst -> Object -> Object
applySubst Subst
holeSubst Object
contextObject

applySubstAttr :: Subst -> Attribute -> Attribute
applySubstAttr :: Subst -> Attribute -> Attribute
applySubstAttr Subst{[(BytesMetaId, Bytes)]
[(ObjectMetaId, Object)]
[(BindingsMetaId, [Binding])]
[(TailMetaId, OneHoleContext)]
[(LabelMetaId, Attribute)]
$sel:objectMetas:Subst :: Subst -> [(ObjectMetaId, Object)]
$sel:bindingsMetas:Subst :: Subst -> [(BindingsMetaId, [Binding])]
$sel:attributeMetas:Subst :: Subst -> [(LabelMetaId, Attribute)]
$sel:bytesMetas:Subst :: Subst -> [(BytesMetaId, Bytes)]
$sel:contextMetas:Subst :: Subst -> [(TailMetaId, OneHoleContext)]
objectMetas :: [(ObjectMetaId, Object)]
bindingsMetas :: [(BindingsMetaId, [Binding])]
attributeMetas :: [(LabelMetaId, Attribute)]
bytesMetas :: [(BytesMetaId, Bytes)]
contextMetas :: [(TailMetaId, OneHoleContext)]
..} = \case
  attr :: Attribute
attr@(MetaAttr LabelMetaId
x) -> Attribute -> Maybe Attribute -> Attribute
forall a. a -> Maybe a -> a
fromMaybe Attribute
attr (Maybe Attribute -> Attribute) -> Maybe Attribute -> Attribute
forall a b. (a -> b) -> a -> b
$ LabelMetaId -> [(LabelMetaId, Attribute)] -> Maybe Attribute
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup LabelMetaId
x [(LabelMetaId, Attribute)]
attributeMetas
  Attribute
attr -> Attribute
attr

applySubstBindings :: Subst -> [Binding] -> [Binding]
applySubstBindings :: Subst -> [Binding] -> [Binding]
applySubstBindings Subst
subst = (Binding -> [Binding]) -> [Binding] -> [Binding]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Subst -> Binding -> [Binding]
applySubstBinding Subst
subst)

applySubstBinding :: Subst -> Binding -> [Binding]
applySubstBinding :: Subst -> Binding -> [Binding]
applySubstBinding subst :: Subst
subst@Subst{[(BytesMetaId, Bytes)]
[(ObjectMetaId, Object)]
[(BindingsMetaId, [Binding])]
[(TailMetaId, OneHoleContext)]
[(LabelMetaId, Attribute)]
$sel:objectMetas:Subst :: Subst -> [(ObjectMetaId, Object)]
$sel:bindingsMetas:Subst :: Subst -> [(BindingsMetaId, [Binding])]
$sel:attributeMetas:Subst :: Subst -> [(LabelMetaId, Attribute)]
$sel:bytesMetas:Subst :: Subst -> [(BytesMetaId, Bytes)]
$sel:contextMetas:Subst :: Subst -> [(TailMetaId, OneHoleContext)]
objectMetas :: [(ObjectMetaId, Object)]
bindingsMetas :: [(BindingsMetaId, [Binding])]
attributeMetas :: [(LabelMetaId, Attribute)]
bytesMetas :: [(BytesMetaId, Bytes)]
contextMetas :: [(TailMetaId, OneHoleContext)]
..} = \case
  AlphaBinding Attribute
a Object
obj ->
    [Attribute -> Object -> Binding
AlphaBinding (Subst -> Attribute -> Attribute
applySubstAttr Subst
subst Attribute
a) (Subst -> Object -> Object
applySubst Subst
subst Object
obj)]
  EmptyBinding Attribute
a ->
    [Attribute -> Binding
EmptyBinding (Subst -> Attribute -> Attribute
applySubstAttr Subst
subst Attribute
a)]
  DeltaBinding Bytes
bytes -> [Bytes -> Binding
DeltaBinding (Bytes -> Bytes
forall a b. Coercible a b => a -> b
coerce Bytes
bytes)]
  Binding
DeltaEmptyBinding -> [Binding
DeltaEmptyBinding]
  LambdaBinding Function
bytes -> [Function -> Binding
LambdaBinding (Function -> Function
forall a b. Coercible a b => a -> b
coerce Function
bytes)]
  b :: Binding
b@(MetaBindings BindingsMetaId
m) -> [Binding] -> Maybe [Binding] -> [Binding]
forall a. a -> Maybe a -> a
fromMaybe [Binding
b] (BindingsMetaId -> [(BindingsMetaId, [Binding])] -> Maybe [Binding]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup BindingsMetaId
m [(BindingsMetaId, [Binding])]
bindingsMetas)
  b :: Binding
b@(MetaDeltaBinding BytesMetaId
m) -> [Binding] -> (Bytes -> [Binding]) -> Maybe Bytes -> [Binding]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Binding
b] (Binding -> [Binding]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Binding -> [Binding]) -> (Bytes -> Binding) -> Bytes -> [Binding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bytes -> Binding
DeltaBinding) (BytesMetaId -> [(BytesMetaId, Bytes)] -> Maybe Bytes
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup BytesMetaId
m [(BytesMetaId, Bytes)]
bytesMetas)

mergeSubst :: Subst -> Subst -> Subst
mergeSubst :: Subst -> Subst -> Subst
mergeSubst (Subst [(ObjectMetaId, Object)]
xs [(BindingsMetaId, [Binding])]
ys [(LabelMetaId, Attribute)]
zs [(BytesMetaId, Bytes)]
ws [(TailMetaId, OneHoleContext)]
us) (Subst [(ObjectMetaId, Object)]
xs' [(BindingsMetaId, [Binding])]
ys' [(LabelMetaId, Attribute)]
zs' [(BytesMetaId, Bytes)]
ws' [(TailMetaId, OneHoleContext)]
us') =
  [(ObjectMetaId, Object)]
-> [(BindingsMetaId, [Binding])]
-> [(LabelMetaId, Attribute)]
-> [(BytesMetaId, Bytes)]
-> [(TailMetaId, OneHoleContext)]
-> Subst
Subst ([(ObjectMetaId, Object)]
xs [(ObjectMetaId, Object)]
-> [(ObjectMetaId, Object)] -> [(ObjectMetaId, Object)]
forall a. [a] -> [a] -> [a]
++ [(ObjectMetaId, Object)]
xs') ([(BindingsMetaId, [Binding])]
ys [(BindingsMetaId, [Binding])]
-> [(BindingsMetaId, [Binding])] -> [(BindingsMetaId, [Binding])]
forall a. [a] -> [a] -> [a]
++ [(BindingsMetaId, [Binding])]
ys') ([(LabelMetaId, Attribute)]
zs [(LabelMetaId, Attribute)]
-> [(LabelMetaId, Attribute)] -> [(LabelMetaId, Attribute)]
forall a. [a] -> [a] -> [a]
++ [(LabelMetaId, Attribute)]
zs') ([(BytesMetaId, Bytes)]
ws [(BytesMetaId, Bytes)]
-> [(BytesMetaId, Bytes)] -> [(BytesMetaId, Bytes)]
forall a. [a] -> [a] -> [a]
++ [(BytesMetaId, Bytes)]
ws') ([(TailMetaId, OneHoleContext)]
us [(TailMetaId, OneHoleContext)]
-> [(TailMetaId, OneHoleContext)] -> [(TailMetaId, OneHoleContext)]
forall a. [a] -> [a] -> [a]
++ [(TailMetaId, OneHoleContext)]
us')

-- 1. need to implement applySubst' :: Subst -> Object -> Object
-- 2. complete the code
matchObject :: Object -> Object -> [Subst]
matchObject :: Object -> Object -> [Subst]
matchObject (Formation [Binding]
ps) (Formation [Binding]
bs) = [Binding] -> [Binding] -> [Subst]
matchBindings [Binding]
ps [Binding]
bs
matchObject (Application Object
obj [Binding]
bindings) (Application Object
obj' [Binding]
bindings') = do
  Subst
subst1 <- Object -> Object -> [Subst]
matchObject Object
obj Object
obj'
  Subst
subst2 <- [Binding] -> [Binding] -> [Subst]
matchBindings (Subst -> [Binding] -> [Binding]
applySubstBindings Subst
subst1 [Binding]
bindings) [Binding]
bindings'
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2)
matchObject (ObjectDispatch Object
pat Attribute
a) (ObjectDispatch Object
obj Attribute
a') = do
  Subst
subst1 <- Object -> Object -> [Subst]
matchObject Object
pat Object
obj
  Subst
subst2 <- Attribute -> Attribute -> [Subst]
matchAttr (Subst -> Attribute -> Attribute
applySubstAttr Subst
subst1 Attribute
a) Attribute
a'
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2)
matchObject (MetaObject ObjectMetaId
m) Object
obj =
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst
emptySubst{objectMetas = [(m, obj)]}
matchObject (MetaTailContext Object
pat TailMetaId
x) Object
obj = do
  (subst :: Subst
subst@Subst{[(BytesMetaId, Bytes)]
[(ObjectMetaId, Object)]
[(BindingsMetaId, [Binding])]
[(TailMetaId, OneHoleContext)]
[(LabelMetaId, Attribute)]
$sel:objectMetas:Subst :: Subst -> [(ObjectMetaId, Object)]
$sel:bindingsMetas:Subst :: Subst -> [(BindingsMetaId, [Binding])]
$sel:attributeMetas:Subst :: Subst -> [(LabelMetaId, Attribute)]
$sel:bytesMetas:Subst :: Subst -> [(BytesMetaId, Bytes)]
$sel:contextMetas:Subst :: Subst -> [(TailMetaId, OneHoleContext)]
objectMetas :: [(ObjectMetaId, Object)]
bindingsMetas :: [(BindingsMetaId, [Binding])]
attributeMetas :: [(LabelMetaId, Attribute)]
bytesMetas :: [(BytesMetaId, Bytes)]
contextMetas :: [(TailMetaId, OneHoleContext)]
..}, OneHoleContext
matchedCtx) <- TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)]
matchOneHoleContext TailMetaId
x Object
pat Object
obj
  Subst -> [Subst]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
subst{contextMetas = contextMetas <> [(x, matchedCtx)]}
matchObject Object
Termination Object
Termination = [Subst
emptySubst]
matchObject Object
ThisObject Object
ThisObject = [Subst
emptySubst]
matchObject Object
GlobalObject Object
GlobalObject = [Subst
emptySubst]
matchObject Object
_ Object
_ = [] -- ? emptySubst ?

matchOneHoleContext :: TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)]
matchOneHoleContext :: TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)]
matchOneHoleContext TailMetaId
ctxId Object
pat Object
obj = [(Subst, OneHoleContext)]
matchWhole [(Subst, OneHoleContext)]
-> [(Subst, OneHoleContext)] -> [(Subst, OneHoleContext)]
forall a. Semigroup a => a -> a -> a
<> [(Subst, OneHoleContext)]
matchPart
 where
  TailMetaId [Char]
name = TailMetaId
ctxId
  holeId :: ObjectMetaId
holeId = [Char] -> ObjectMetaId
ObjectMetaId ([Char]
name [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":hole") -- FIXME: ensure fresh names
  matchWhole :: [(Subst, OneHoleContext)]
matchWhole = do
    Subst
subst' <- Object -> Object -> [Subst]
matchObject Object
pat Object
obj
    (Subst, OneHoleContext) -> [(Subst, OneHoleContext)]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
subst', ObjectMetaId -> Object -> OneHoleContext
OneHoleContext ObjectMetaId
holeId (ObjectMetaId -> Object
MetaObject ObjectMetaId
holeId))
  matchPart :: [(Subst, OneHoleContext)]
matchPart = case Object
obj of
    ObjectDispatch Object
obj' Attribute
a -> do
      (Subst
subst, OneHoleContext{ObjectMetaId
Object
$sel:holeMetaId:OneHoleContext :: OneHoleContext -> ObjectMetaId
$sel:contextObject:OneHoleContext :: OneHoleContext -> Object
holeMetaId :: ObjectMetaId
contextObject :: Object
..}) <- TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)]
matchOneHoleContext TailMetaId
ctxId Object
pat Object
obj'
      (Subst, OneHoleContext) -> [(Subst, OneHoleContext)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, OneHoleContext{$sel:contextObject:OneHoleContext :: Object
contextObject = Object -> Attribute -> Object
ObjectDispatch Object
contextObject Attribute
a, ObjectMetaId
$sel:holeMetaId:OneHoleContext :: ObjectMetaId
holeMetaId :: ObjectMetaId
..})
    -- FIXME: consider matching inside bindings of application as well
    Application Object
obj' [Binding]
bindings -> do
      (Subst
subst, OneHoleContext{ObjectMetaId
Object
$sel:holeMetaId:OneHoleContext :: OneHoleContext -> ObjectMetaId
$sel:contextObject:OneHoleContext :: OneHoleContext -> Object
holeMetaId :: ObjectMetaId
contextObject :: Object
..}) <- TailMetaId -> Object -> Object -> [(Subst, OneHoleContext)]
matchOneHoleContext TailMetaId
ctxId Object
pat Object
obj'
      (Subst, OneHoleContext) -> [(Subst, OneHoleContext)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
subst, OneHoleContext{$sel:contextObject:OneHoleContext :: Object
contextObject = Object -> [Binding] -> Object
Application Object
contextObject [Binding]
bindings, ObjectMetaId
$sel:holeMetaId:OneHoleContext :: ObjectMetaId
holeMetaId :: ObjectMetaId
..})
    -- cases below cannot be matched
    Formation{} -> []
    Object
GlobalObject -> []
    Object
ThisObject -> []
    Object
Termination -> []
    -- should cases below be errors?
    MetaSubstThis{} -> []
    MetaContextualize{} -> []
    MetaObject{} -> []
    MetaTailContext{} -> []
    MetaFunction{} -> []

-- | Evaluate meta functions
-- given top-level context as an object
-- and an object
evaluateMetaFuncs :: Object -> Object -> Object
evaluateMetaFuncs :: Object -> Object -> Object
evaluateMetaFuncs Object
_obj' Object
obj =
  State MetaState Object -> MetaState -> Object
forall s a. State s a -> s -> a
evalState
    (Object -> State MetaState Object
evaluateMetaFuncs' Object
obj)
    MetaState{}

data MetaState = MetaState
  {
  }
  deriving ((forall x. MetaState -> Rep MetaState x)
-> (forall x. Rep MetaState x -> MetaState) -> Generic MetaState
forall x. Rep MetaState x -> MetaState
forall x. MetaState -> Rep MetaState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaState -> Rep MetaState x
from :: forall x. MetaState -> Rep MetaState x
$cto :: forall x. Rep MetaState x -> MetaState
to :: forall x. Rep MetaState x -> MetaState
Generic)

evaluateMetaFuncs' :: Object -> State MetaState Object
evaluateMetaFuncs' :: Object -> State MetaState Object
evaluateMetaFuncs' (Formation [Binding]
bindings) = [Binding] -> Object
Formation ([Binding] -> Object)
-> StateT MetaState Identity [Binding] -> State MetaState Object
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding -> StateT MetaState Identity Binding)
-> [Binding] -> StateT MetaState Identity [Binding]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Binding -> StateT MetaState Identity Binding
evaluateMetaFuncsBinding [Binding]
bindings
evaluateMetaFuncs' (Application Object
obj [Binding]
bindings) = Object -> [Binding] -> Object
Application (Object -> [Binding] -> Object)
-> State MetaState Object
-> StateT MetaState Identity ([Binding] -> Object)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object -> State MetaState Object
evaluateMetaFuncs' Object
obj StateT MetaState Identity ([Binding] -> Object)
-> StateT MetaState Identity [Binding] -> State MetaState Object
forall a b.
StateT MetaState Identity (a -> b)
-> StateT MetaState Identity a -> StateT MetaState Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Binding -> StateT MetaState Identity Binding)
-> [Binding] -> StateT MetaState Identity [Binding]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Binding -> StateT MetaState Identity Binding
evaluateMetaFuncsBinding [Binding]
bindings
evaluateMetaFuncs' (ObjectDispatch Object
obj Attribute
a) = Object -> Attribute -> Object
ObjectDispatch (Object -> Attribute -> Object)
-> State MetaState Object
-> StateT MetaState Identity (Attribute -> Object)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object -> State MetaState Object
evaluateMetaFuncs' Object
obj StateT MetaState Identity (Attribute -> Object)
-> StateT MetaState Identity Attribute -> State MetaState Object
forall a b.
StateT MetaState Identity (a -> b)
-> StateT MetaState Identity a -> StateT MetaState Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Attribute -> StateT MetaState Identity Attribute
forall a. a -> StateT MetaState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Attribute
a
evaluateMetaFuncs' (MetaSubstThis Object
obj Object
thisObj) = Object -> State MetaState Object
evaluateMetaFuncs' (Object -> Object -> Object
substThis Object
thisObj Object
obj)
evaluateMetaFuncs' (MetaContextualize Object
obj Object
thisObj) = Object -> State MetaState Object
evaluateMetaFuncs' (Object -> Object -> Object
contextualize Object
thisObj Object
obj)
evaluateMetaFuncs' Object
obj = Object -> State MetaState Object
forall a. a -> StateT MetaState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Object
obj

evaluateMetaFuncsBinding :: Binding -> State MetaState Binding
evaluateMetaFuncsBinding :: Binding -> StateT MetaState Identity Binding
evaluateMetaFuncsBinding (AlphaBinding Attribute
attr Object
obj) = Attribute -> Object -> Binding
AlphaBinding Attribute
attr (Object -> Binding)
-> State MetaState Object -> StateT MetaState Identity Binding
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object -> State MetaState Object
evaluateMetaFuncs' Object
obj
evaluateMetaFuncsBinding Binding
binding = Binding -> StateT MetaState Identity Binding
forall a. a -> StateT MetaState Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Binding
binding

matchBindings :: [Binding] -> [Binding] -> [Subst]
matchBindings :: [Binding] -> [Binding] -> [Subst]
matchBindings [] [] = [Subst
emptySubst]
matchBindings [MetaBindings BindingsMetaId
b] [Binding]
bindings =
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    Subst
emptySubst
      { bindingsMetas = [(b, bindings)]
      }
matchBindings (Binding
p : [Binding]
ps) [Binding]
bs = do
  ([Binding]
bs', Subst
subst1) <- Binding -> [Binding] -> [([Binding], Subst)]
matchFindBinding Binding
p [Binding]
bs
  Subst
subst2 <- [Binding] -> [Binding] -> [Subst]
matchBindings (Subst -> [Binding] -> [Binding]
applySubstBindings Subst
subst1 [Binding]
ps) [Binding]
bs'
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2)
matchBindings [] [Binding]
_ = []

-- >>> select [1,2,3,4]
-- [(1,[2,3,4]),(2,[1,3,4]),(3,[1,2,4]),(4,[1,2,3])]
select :: [a] -> [(a, [a])]
select :: forall a. [a] -> [(a, [a])]
select [] = []
select [a
x] = [(a
x, [])]
select (a
x : [a]
xs) =
  (a
x, [a]
xs)
    (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [ (a
y, a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ys)
      | (a
y, [a]
ys) <- [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
select [a]
xs
      ]

matchFindBinding :: Binding -> [Binding] -> [([Binding], Subst)]
matchFindBinding :: Binding -> [Binding] -> [([Binding], Subst)]
matchFindBinding Binding
p [Binding]
bindings =
  [ ([Binding]
leftover, Subst
subst)
  | (Binding
binding, [Binding]
leftover) <- [Binding] -> [(Binding, [Binding])]
forall a. [a] -> [(a, [a])]
select [Binding]
bindings
  , Subst
subst <- Binding -> Binding -> [Subst]
matchBinding Binding
p Binding
binding
  ]

matchBinding :: Binding -> Binding -> [Subst]
matchBinding :: Binding -> Binding -> [Subst]
matchBinding MetaBindings{} Binding
_ = []
matchBinding (AlphaBinding Attribute
a Object
obj) (AlphaBinding Attribute
a' Object
obj') = do
  Subst
subst1 <- Attribute -> Attribute -> [Subst]
matchAttr Attribute
a Attribute
a'
  Subst
subst2 <- Object -> Object -> [Subst]
matchObject Object
obj Object
obj'
  Subst -> [Subst]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst
subst1 Subst -> Subst -> Subst
forall a. Semigroup a => a -> a -> a
<> Subst
subst2)
matchBinding (MetaDeltaBinding BytesMetaId
m) (DeltaBinding Bytes
bytes) = [Subst
emptySubst{bytesMetas = [(m, bytes)]}]
matchBinding (DeltaBinding Bytes
bytes) (DeltaBinding Bytes
bytes')
  | Bytes
bytes Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
bytes' = [Subst
emptySubst]
matchBinding Binding
DeltaEmptyBinding Binding
DeltaEmptyBinding = [Subst
emptySubst]
matchBinding (EmptyBinding Attribute
a1) (EmptyBinding Attribute
a2) = Attribute -> Attribute -> [Subst]
matchAttr Attribute
a1 Attribute
a2
matchBinding (LambdaBinding Function
f1) (LambdaBinding Function
f2)
  | Function
f1 Function -> Function -> Bool
forall a. Eq a => a -> a -> Bool
== Function
f2 = [Subst
emptySubst]
matchBinding Binding
_ Binding
_ = []

matchAttr :: Attribute -> Attribute -> [Subst]
matchAttr :: Attribute -> Attribute -> [Subst]
matchAttr Attribute
l Attribute
r | Attribute
l Attribute -> Attribute -> Bool
forall a. Eq a => a -> a -> Bool
== Attribute
r = [Subst
emptySubst]
matchAttr (MetaAttr LabelMetaId
metaId) Attribute
attr =
  [ Subst
emptySubst
      { attributeMetas = [(metaId, attr)]
      }
  ]
matchAttr Attribute
_ Attribute
_ = []

substThis :: Object -> Object -> Object
substThis :: Object -> Object -> Object
substThis Object
thisObj = Object -> Object
go
 where
  isAttachedRho :: Binding -> Bool
isAttachedRho (AlphaBinding Attribute
Rho Object
_) = Bool
True
  isAttachedRho Binding
_ = Bool
False

  isEmptyRho :: Binding -> Bool
isEmptyRho (EmptyBinding Attribute
Rho) = Bool
True
  isEmptyRho Binding
_ = Bool
False

  go :: Object -> Object
go = \case
    Object
ThisObject -> Object
thisObj -- ξ is substituted
    -- IMPORTANT: we are injecting a ρ-attribute in formations!
    obj :: Object
obj@(Formation [Binding]
bindings)
      | (Binding -> Bool) -> [Binding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Binding -> Bool
isAttachedRho [Binding]
bindings -> Object
obj
      | Bool
otherwise -> [Binding] -> Object
Formation ((Binding -> Bool) -> [Binding] -> [Binding]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Binding -> Bool) -> Binding -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binding -> Bool
isEmptyRho) [Binding]
bindings [Binding] -> [Binding] -> [Binding]
forall a. [a] -> [a] -> [a]
++ [Attribute -> Object -> Binding
AlphaBinding Attribute
Rho Object
thisObj])
    -- everywhere else we simply recursively traverse the φ-term
    Application Object
obj [Binding]
bindings -> Object -> [Binding] -> Object
Application (Object -> Object
go Object
obj) ((Binding -> Binding) -> [Binding] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map (Object -> Binding -> Binding
substThisBinding Object
thisObj) [Binding]
bindings)
    ObjectDispatch Object
obj Attribute
a -> Object -> Attribute -> Object
ObjectDispatch (Object -> Object
go Object
obj) Attribute
a
    Object
GlobalObject -> Object
GlobalObject
    Object
Termination -> Object
Termination
    obj :: Object
obj@MetaTailContext{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaContextualize{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaSubstThis{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaObject{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaFunction{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)

-- {⟦ x ↦ ⟦ b ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ b ↦ ⟦ Δ ⤍ 02- ⟧, c ↦ ⟦ a ↦ ξ.ρ.ρ.b ⟧.a ⟧.c ⟧.φ, λ ⤍ Package ⟧}

-- {⟦ λ ⤍ Package, x ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧}

substThisBinding :: Object -> Binding -> Binding
substThisBinding :: Object -> Binding -> Binding
substThisBinding Object
obj = \case
  AlphaBinding Attribute
a Object
obj' -> Attribute -> Object -> Binding
AlphaBinding Attribute
a (Object -> Object -> Object
substThis Object
obj Object
obj')
  EmptyBinding Attribute
a -> Attribute -> Binding
EmptyBinding Attribute
a
  DeltaBinding Bytes
bytes -> Bytes -> Binding
DeltaBinding Bytes
bytes
  Binding
DeltaEmptyBinding -> Binding
DeltaEmptyBinding
  LambdaBinding Function
bytes -> Function -> Binding
LambdaBinding Function
bytes
  b :: Binding
b@MetaBindings{} -> [Char] -> Binding
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> [Char]
forall a. Print a => a -> [Char]
printTree Binding
b)
  b :: Binding
b@MetaDeltaBinding{} -> [Char] -> Binding
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to substitute ξ in " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> [Char]
forall a. Print a => a -> [Char]
printTree Binding
b)

contextualize :: Object -> Object -> Object
contextualize :: Object -> Object -> Object
contextualize Object
thisObj = Object -> Object
go
 where
  go :: Object -> Object
go = \case
    Object
ThisObject -> Object
thisObj -- ξ is substituted
    obj :: Object
obj@(Formation [Binding]
_bindings) -> Object
obj
    ObjectDispatch Object
obj Attribute
a -> Object -> Attribute -> Object
ObjectDispatch (Object -> Object
go Object
obj) Attribute
a
    Application Object
obj [Binding]
bindings -> Object -> [Binding] -> Object
Application (Object -> Object
go Object
obj) ((Binding -> Binding) -> [Binding] -> [Binding]
forall a b. (a -> b) -> [a] -> [b]
map (Object -> Binding -> Binding
contextualizeBinding Object
thisObj) [Binding]
bindings)
    Object
GlobalObject -> Object
GlobalObject -- TODO: Change to what GlobalObject is attached to
    Object
Termination -> Object
Termination
    obj :: Object
obj@MetaTailContext{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaContextualize{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaSubstThis{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaObject{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)
    obj :: Object
obj@MetaFunction{} -> [Char] -> Object
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Object -> [Char]
forall a. Print a => a -> [Char]
printTree Object
obj)

contextualizeBinding :: Object -> Binding -> Binding
contextualizeBinding :: Object -> Binding -> Binding
contextualizeBinding Object
obj = \case
  AlphaBinding Attribute
a Object
obj' -> Attribute -> Object -> Binding
AlphaBinding Attribute
a (Object -> Object -> Object
contextualize Object
obj Object
obj')
  EmptyBinding Attribute
a -> Attribute -> Binding
EmptyBinding Attribute
a
  DeltaBinding Bytes
bytes -> Bytes -> Binding
DeltaBinding Bytes
bytes
  Binding
DeltaEmptyBinding -> Binding
DeltaEmptyBinding
  LambdaBinding Function
bytes -> Function -> Binding
LambdaBinding Function
bytes
  b :: Binding
b@MetaBindings{} -> [Char] -> Binding
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> [Char]
forall a. Print a => a -> [Char]
printTree Binding
b)
  b :: Binding
b@MetaDeltaBinding{} -> [Char] -> Binding
forall a. HasCallStack => [Char] -> a
error ([Char]
"impossible: trying to contextualize " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> Binding -> [Char]
forall a. Print a => a -> [Char]
printTree Binding
b)