{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE OverloadedStrings #-}

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  Datatype
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--                 2011, 2012, 2018, 2019, 2022 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  ExistentialQuantification, OverloadedStrings
--
--  This module defines the structures used to represent and
--  manipulate datatypes.  It is designed as a basis for handling datatyped
--  RDF literals, but the functions in this module are more generic.
--
--------------------------------------------------------------------------------

--  Testing note:  this module supports a number of specific datatypes.
--  It is intended that functionality in this module will be tested via
--  modules "Swish.RDF.RDFDatatype", 
--  "Swish.RDF.ClassRestrictionRule" and
--  "Swish.RDF.RDFDatatypeXsdInteger".
--  See also module ClassRestrictionRuleTest for test cases.

module Swish.Datatype
    ( Datatype(..)
    , typeName, typeRules, typeMkRules, typeMkModifiers, typeMkCanonicalForm
    , getTypeAxiom, getTypeRule
    , DatatypeVal(..)
    , getDTMod
    , getDTRel
    , tvalMkCanonicalForm
    , DatatypeMap(..)
    , DatatypeRel(..), DatatypeRelFn, DatatypeRelPr
    , altArgs
    , UnaryFnDescr,    UnaryFnTable,    UnaryFnApply,    unaryFnApp
    , BinaryFnDescr,   BinaryFnTable,   BinaryFnApply,   binaryFnApp
    , BinMaybeFnDescr, BinMaybeFnTable, BinMaybeFnApply, binMaybeFnApp
    , ListFnDescr,     ListFnTable,     ListFnApply,     listFnApp
    , DatatypeMod(..), ModifierFn
    , ApplyModifier
    , nullDatatypeMod
    -- , applyDatatypeMod
    , makeVmod11inv, makeVmod11
    , makeVmod21inv, makeVmod21
    , makeVmod20
    , makeVmod22
    , makeVmodN1
    , DatatypeSub(..)
    )
where

import Swish.Namespace (ScopedName)
import Swish.Rule (Formula(..), Rule(..))
import Swish.Ruleset (Ruleset(..))
import Swish.Ruleset (getRulesetAxiom, getRulesetRule)
import Swish.VarBinding (VarBinding(..), VarBindingModify(..), OpenVarBindingModify)
import Swish.VarBinding (addVarBinding, nullVarBindingModify)

import Swish.RDF.Vocabulary (swishName)

import Swish.Utils.ListHelpers (flist)

-- used to add Show instances for structures during debugging
-- but backed out again.
--
-- import Swish.Utils.ShowM (ShowM(..))

#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 808)
import Control.Applicative ((<$>))
#endif

import Data.Maybe (isJust, catMaybes)

import qualified Data.Map as M
import qualified Data.Text as T

------------------------------------------------------------
--  Datatype framework
------------------------------------------------------------

-- |Datatype wraps a 'DatatypeVal' value, hiding the value type that
--  is used only in implementations of the datatype.
--  Users see just the datatype name and associated ruleset.
--
data Datatype ex lb vn = forall vt . Datatype (DatatypeVal ex vt lb vn)

-- |Get type name from Datatype value
typeName :: Datatype ex lb vn -> ScopedName
typeName :: forall ex lb vn. Datatype ex lb vn -> ScopedName
typeName (Datatype DatatypeVal ex vt lb vn
dtv) = forall ex vt lb vn. DatatypeVal ex vt lb vn -> ScopedName
tvalName  DatatypeVal ex vt lb vn
dtv

-- |Get static rules from Datatype value
typeRules :: Datatype ex lb vn -> Ruleset ex
typeRules :: forall ex lb vn. Datatype ex lb vn -> Ruleset ex
typeRules (Datatype DatatypeVal ex vt lb vn
dtv) = forall ex vt lb vn. DatatypeVal ex vt lb vn -> Ruleset ex
tvalRules DatatypeVal ex vt lb vn
dtv

-- |Make rules for Datatype value based on supplied expression
typeMkRules :: Datatype ex lb vn -> ex -> [Rule ex]
typeMkRules :: forall ex lb vn. Datatype ex lb vn -> ex -> [Rule ex]
typeMkRules (Datatype DatatypeVal ex vt lb vn
dtv) = forall ex vt lb vn. DatatypeVal ex vt lb vn -> ex -> [Rule ex]
tvalMkRules DatatypeVal ex vt lb vn
dtv

-- |Make variable binding modifiers based on values supplied
typeMkModifiers :: Datatype ex lb vn -> [OpenVarBindingModify lb vn]
typeMkModifiers :: forall ex lb vn. Datatype ex lb vn -> [OpenVarBindingModify lb vn]
typeMkModifiers (Datatype DatatypeVal ex vt lb vn
dtv) = forall ex vt lb vn.
DatatypeVal ex vt lb vn -> [OpenVarBindingModify lb vn]
tvalMkMods DatatypeVal ex vt lb vn
dtv

-- |Get the named axiom from a Datatype value.
getTypeAxiom :: ScopedName -> Datatype ex lb vn -> Maybe (Formula ex)
getTypeAxiom :: forall ex lb vn.
ScopedName -> Datatype ex lb vn -> Maybe (Formula ex)
getTypeAxiom ScopedName
nam Datatype ex lb vn
dt = forall ex. ScopedName -> Ruleset ex -> Maybe (Formula ex)
getRulesetAxiom ScopedName
nam (forall ex lb vn. Datatype ex lb vn -> Ruleset ex
typeRules Datatype ex lb vn
dt)

-- |Get the named rule from a Datatype value.
getTypeRule :: ScopedName -> Datatype ex lb vn -> Maybe (Rule ex)
getTypeRule :: forall ex lb vn. ScopedName -> Datatype ex lb vn -> Maybe (Rule ex)
getTypeRule ScopedName
nam Datatype ex lb vn
dt = forall ex. ScopedName -> Ruleset ex -> Maybe (Rule ex)
getRulesetRule ScopedName
nam (forall ex lb vn. Datatype ex lb vn -> Ruleset ex
typeRules Datatype ex lb vn
dt)

-- |Get the canonical form of a datatype value.
typeMkCanonicalForm :: Datatype ex lb vn -> T.Text -> Maybe T.Text
typeMkCanonicalForm :: forall ex lb vn. Datatype ex lb vn -> Text -> Maybe Text
typeMkCanonicalForm (Datatype DatatypeVal ex vt lb vn
dtv) = forall ex vt lb vn. DatatypeVal ex vt lb vn -> Text -> Maybe Text
tvalMkCanonicalForm DatatypeVal ex vt lb vn
dtv

------------------------------------------------------------
--  DatatypeVal
------------------------------------------------------------

-- |DatatypeVal is a structure that defines a number of functions
--  and values that characterize the behaviour of a datatype.
--
--  A datatype is specified with respect to (polymophic in) a given
--  type of (syntactic) expression with which it may be used, and
--  a value type (whose existence is hidden as an existential type
--  within `DatatypeMap`).
--
--  (I tried hiding the value type with an internal existential
--  declaration, but that wouldn't wash.  Hence this two-part
--  structure with `Datatype` in which the internal detail
--  of the value type is hidden from users of the `Datatype` class.)
--
--  The datatype characteristic functions have two goals:
--
--  (1) to support the general datatype entailment rules defined by
--      the RDF semantics specification, and
--
--  (2) to define additional datatype-specific inference patterns by
--      means of which provide additional base functionality to
--      applications based on RDF inference.
--
--  Datatype-specific inferences are provided using the `DatatypeRel`
--  structure for a datatype, which allows a number of named relations
--  to be defined on datatype values, and provides mechanisms to
--  calculate missing values in a partially-specified member of
--  a relation.
--
--  Note that rules and variable binding modifiers that deal with
--  combined values of more than one datatype may be defined
--  separately.  Definitions in this module are generally applicable
--  only when using a single datatype.
--
--  An alternative model for datatype value calculations is inspired
--  by that introduced by CWM for arithmetic operations, e.g.
--
--  >     (1 2 3) math:sum ?x => ?x rdf:value 6
--
--  (where the bare integer @n@ here is shorthand for @\"n\"^^xsd:integer@).
--
--  Datatype-specific inference patterns are provided in two ways:
--
--  * by variable binding modifiers that can be combined with the
--    query results during forward- for backward-chaining of
--    inference rules, and
--
--  * by the definition of inference rulesets that involve
--    datatype values.
--
--  I believe the first method to be more flexible than the second,
--  in that it more readily supports forward and backward chaining,
--  but can be used only through the definition of new rules.
--
--  Type parameters:
--
--  [@ex@] is the type of expression with which the datatype may be used.
--
--  [@vt@] is the internal value type with which the labels are associated.
--
--  [@lb@] is the type of label that may be used as a variable in an
--         expression or rule.
--
--  [@vn@] is the type of node that may be used to carry a value in an
--         expression or rule.
--
data DatatypeVal ex vt lb vn = DatatypeVal
    { forall ex vt lb vn. DatatypeVal ex vt lb vn -> ScopedName
tvalName      :: ScopedName
                                -- ^Identifies the datatype, and also
                                --  its value space class.
    , forall ex vt lb vn. DatatypeVal ex vt lb vn -> Ruleset ex
tvalRules     :: Ruleset ex
                                -- ^A set of named expressions and rules
                                --  that are valid in in any theory that
                                --  recognizes the current datatype.
    , forall ex vt lb vn. DatatypeVal ex vt lb vn -> ex -> [Rule ex]
tvalMkRules   :: ex -> [Rule ex]
                                -- ^A function that accepts an expression
                                --  and devives some datatype-dependent
                                --  rules from it.  This is provided as a
                                --  hook for creating datatyped class
                                --  restriction rules.
    , forall ex vt lb vn.
DatatypeVal ex vt lb vn -> [OpenVarBindingModify lb vn]
tvalMkMods    :: [OpenVarBindingModify lb vn]
                                -- ^Constructs a list of open variable
                                --  binding modifiers based on tvalMod,
                                --  but hiding the actual value type.
    , forall ex vt lb vn. DatatypeVal ex vt lb vn -> DatatypeMap vt
tvalMap       :: DatatypeMap vt
                                -- ^Lexical to value mapping, where @vt@ is
                                --  a datatype used within a Haskell program
                                --  to represent and manipulate values in
                                --  the datatype's value space
    , forall ex vt lb vn. DatatypeVal ex vt lb vn -> [DatatypeRel vt]
tvalRel       :: [DatatypeRel vt]
                                -- ^A set of named relations on datatype
                                --  values.  Each relation accepts a list
                                --  of @Maybe vt@, and computes any
                                --  unspecified values that are in the
                                --  relation with values supplied.
    , forall ex vt lb vn.
DatatypeVal ex vt lb vn -> [DatatypeMod vt lb vn]
tvalMod       :: [DatatypeMod vt lb vn]
                                -- ^A list of named values that are used to
                                --  construct variable binding modifiers, which
                                --  in turn may be used by a rule definition.
                                --
                                --  TODO: In due course, this value may be
                                --  calculated automatically from the supplied
                                --  value for @tvalRel@.
    }

{-
instance ShowM ex => Show (DatatypeVal ex vt lb vn) where
  show dv = "DatatypeVal: " ++ show (tvalName dv) ++ "\n -> rules:\n" ++ show (tvalRules dv)
-}

--  Other accessor functions

-- | Return the named datatype relation, if it exists.
getDTRel ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeRel vt)
getDTRel :: forall ex vt lb vn.
ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeRel vt)
getDTRel ScopedName
nam DatatypeVal ex vt lb vn
dtv =
    let m :: Map ScopedName (DatatypeRel vt)
m = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\DatatypeRel vt
n -> (forall vt. DatatypeRel vt -> ScopedName
dtRelName DatatypeRel vt
n, DatatypeRel vt
n)) (forall ex vt lb vn. DatatypeVal ex vt lb vn -> [DatatypeRel vt]
tvalRel DatatypeVal ex vt lb vn
dtv)
    in forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ScopedName
nam Map ScopedName (DatatypeRel vt)
m

-- | Return the named datatype value modifier, if it exists.
getDTMod ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeMod vt lb vn)
getDTMod :: forall ex vt lb vn.
ScopedName
-> DatatypeVal ex vt lb vn -> Maybe (DatatypeMod vt lb vn)
getDTMod ScopedName
nam DatatypeVal ex vt lb vn
dtv =
    let m :: Map ScopedName (DatatypeMod vt lb vn)
m = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\DatatypeMod vt lb vn
n -> (forall vt lb vn. DatatypeMod vt lb vn -> ScopedName
dmName DatatypeMod vt lb vn
n, DatatypeMod vt lb vn
n)) (forall ex vt lb vn.
DatatypeVal ex vt lb vn -> [DatatypeMod vt lb vn]
tvalMod DatatypeVal ex vt lb vn
dtv)
    in forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ScopedName
nam Map ScopedName (DatatypeMod vt lb vn)
m

-- |Get the canonical form of a datatype value, or @Nothing@.
--
tvalMkCanonicalForm :: DatatypeVal ex vt lb vn -> T.Text -> Maybe T.Text
tvalMkCanonicalForm :: forall ex vt lb vn. DatatypeVal ex vt lb vn -> Text -> Maybe Text
tvalMkCanonicalForm DatatypeVal ex vt lb vn
dtv Text
str = Maybe Text
can
    where
      dtmap :: DatatypeMap vt
dtmap = forall ex vt lb vn. DatatypeVal ex vt lb vn -> DatatypeMap vt
tvalMap DatatypeVal ex vt lb vn
dtv
      val :: Maybe vt
val   = forall vt. DatatypeMap vt -> Text -> Maybe vt
mapL2V DatatypeMap vt
dtmap Text
str
      can :: Maybe Text
can   = forall vt. DatatypeMap vt -> vt -> Maybe Text
mapV2L DatatypeMap vt
dtmap forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Maybe vt
val

-- |DatatypeMap consists of methods that perform lexical-to-value
--  and value-to-canonical-lexical mappings for a datatype.
--
--  The datatype mappings apply to string lexical forms which
--  are stored as `Data.Text`.
--
data DatatypeMap vt = DatatypeMap
    { forall vt. DatatypeMap vt -> Text -> Maybe vt
mapL2V  :: T.Text -> Maybe vt
                            -- ^ Function to map a lexical string to
                            --   the datatype value.  This effectively
                            --   defines the lexical space of the
                            --   datatype to be all strings for which
                            --   yield a value other than @Nothing@.
    , forall vt. DatatypeMap vt -> vt -> Maybe Text
mapV2L  :: vt -> Maybe T.Text
                            -- ^ Function to map a value to its canonical
                            --   lexical form, if it has such.
    }

-- |Type for a datatype relation inference function.
--
--  A datatype relation defines tuples of values that satisfy some
--  relation.  A datatype relation inference function calculates
--  values that complete a relation with values supplied.
--
--  The function accepts a list of @Maybe vt@, where vt is the
--  datatype value type.  It returns one of:
--
--  * Just a list of lists, where each inner list returned is a
--      complete set of values, including the values supplied, that
--      are in the relation.
--
--  * Just an empty list is returned if the supplied values are
--      insufficient to compute any complete sets of values in the
--      relation.
--
--  * Nothing if the supplied values are not consistent with
--      the relation.
--
type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]

-- |Type for datatype relation predicate:  accepts a list of values
--  and determines whether or not they satisfy the relation.
--
type DatatypeRelPr vt = [vt] -> Bool

-- |Datatype for a named relation on values of a datatype.
--
data DatatypeRel vt = DatatypeRel
    { forall vt. DatatypeRel vt -> ScopedName
dtRelName :: ScopedName
    , forall vt. DatatypeRel vt -> DatatypeRelFn vt
dtRelFunc :: DatatypeRelFn vt
    }

-- |Datatype value modifier functions type
--
--  Each function accepts a list of values and returns a list of values.
--  The exact significance of the different values supplied and returned
--  depends on the variable binding pattern used (cf. 'ApplyModifier'),
--  but in all cases an empty list returned means that the corresponding
--  inputs are not consistent with the function and cannot be used.
--
type ModifierFn vn = [vn] -> [vn]

-- |Type of function used to apply a data value modifier to specified
--  variables in a supplied variable binding.  It also accepts the
--  name of the datatype modifier and carries it into the resulting
--  variable binding modifier.
--
--  (Note that @vn@ is not necessarily the same as @vt@, the datatype value
--  type:  the modifier functions may be lifted or otherwise adapted
--  to operate on some other type from which the raw data values are
--  extracted.)
--
type ApplyModifier lb vn =
    ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn

-- |Wrapper for data type variable binding modifier included in
--  a datatype value.
--
data DatatypeMod vt lb vn = DatatypeMod
    { forall vt lb vn. DatatypeMod vt lb vn -> ScopedName
dmName :: ScopedName
    , forall vt lb vn. DatatypeMod vt lb vn -> [ModifierFn vt]
dmModf :: [ModifierFn vt]
    , forall vt lb vn. DatatypeMod vt lb vn -> ApplyModifier lb vn
dmAppf :: ApplyModifier lb vn
    }

-- |Null datatype value modifier
nullDatatypeMod :: DatatypeMod vt lb vn
nullDatatypeMod :: forall vt lb vn. DatatypeMod vt lb vn
nullDatatypeMod = DatatypeMod
    { dmName :: ScopedName
dmName = LName -> ScopedName
swishName LName
"nullDatatypeMod"
    , dmModf :: [ModifierFn vt]
dmModf = []
    , dmAppf :: ApplyModifier lb vn
dmAppf = forall {p} {a} {b}. ScopedName -> p -> [a] -> VarBindingModify a b
nullAppf
    }
    where
        -- nullAppf :: ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn
        nullAppf :: ScopedName -> p -> [a] -> VarBindingModify a b
nullAppf ScopedName
nam p
_ [a]
lbs = (forall a b. OpenVarBindingModify a b
nullVarBindingModify [a]
lbs) { vbmName :: ScopedName
vbmName = ScopedName
nam }

{-
-- |Apply datatype variable binding modifier value to list of labels and
--  a variable binding.
applyDatatypeMod :: (Eq lb, Show lb, Eq vn, Show vn)
    => DatatypeMod vt lb vn -> OpenVarBindingModify lb vn
applyDatatypeMod dtmod = dmAppf dtmod (dmName dtmod) (dmModf dtmod)
-}

{-
dmName dtmod :: ScopedName
dmModf dtmod :: [ModifierFn vt]
             :: [[vt] -> [vt]]
dmAppf dtmod :: ApplyModifier lb vn
             :: ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn
             :: ScopedName -> [[vn] -> [vn]] -> OpenVarBindingModify lb vn
dmAppf dtmod (dmName dtmod)
             :: [[vn] -> [vn]] -> OpenVarBindingModify lb vn
-}

--------------------------------------------------------------
--  Functions for creating datatype variable binding modifiers
--------------------------------------------------------------

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a @1->1@ function and inverse, such
--  as negate.
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--        
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (0) is @[x,y] -> [?]@, used as a filter (i.e. not creating any
--              new variable bindings), returning a non-empty list if @x@ and @y@
--              are in the appropriate relationship.
--
--          (1) is @[y] -> [x]@, used to perform the calculation in a forward
--              direction.
--
--          (2) is @[x] -> [y]@, used to perform the calculation in a backward
--              direction.  This may be the same as (2) (e.g. for negation)
--              or may be different (e.g. increment).
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.  (The intent is that a variable-free
--          value can be generated as a Curried function, and instantiated
--          for particular variables as required.)
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmod11inv :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod11inv :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod11inv ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1,ModifierFn vn
f2] lbs :: [lb]
lbs@(~[lb
lb1,lb
lb2]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1],[lb
lb2]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 [Just vn
v1,Just vn
v2] VarBinding lb vn
vbind = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv     (ModifierFn vn
f0 [vn
v1,vn
v2]) VarBinding lb vn
vbind
        app2 [Maybe vn
Nothing,Just vn
v2] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb1 (ModifierFn vn
f1 [vn
v2])    VarBinding lb vn
vbind
        app2 [Just vn
v1,Maybe vn
Nothing] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb2 (ModifierFn vn
f2 [vn
v1])    VarBinding lb vn
vbind
        app2 [Maybe vn]
_                     VarBinding lb vn
_     = []
makeVmod11inv ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod11inv: requires 3 functions and 2 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases when
--  the value mapping is a non-invertable @1->1@ injection, such as
--  absolute value.
--
--  [@nam@] is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@] are functions used to implement details of the variable
--          binding modifier:
--
--          (0) is @[x,y] -> [?]@, used as a filter (i.e. not creating any
--              new variable bindings), returning a non-empty list if @x@ and @y@
--              are in the appropriate relationship.
--
--          (1) is @[x]@ -> @[y]@, used to perform the calculation.
--
--  [@lbs@] is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmod11 :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod11 :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod11 ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1] lbs :: [lb]
lbs@(~[lb
lb1,lb
_]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 [Just vn
v1,Just vn
v2] VarBinding lb vn
vbind = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn
v1,vn
v2])  VarBinding lb vn
vbind
        app2 [Maybe vn
Nothing,Just vn
v2] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb1 (ModifierFn vn
f1 [vn
v2]) VarBinding lb vn
vbind
        app2 [Maybe vn]
_                     VarBinding lb vn
_     = []
makeVmod11 ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod11: requires 2 functions and 2 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a @2->1@ invertable function, such as
--  addition or subtraction.
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (1) is @[x,y,z] -> [?]@, used as a filter (i.e. not creating any
--              new variable bindings), returning a non-empty list if
--              @x@, @y@ and @z@ are in the appropriate relationship.
--
--          (2) is @[y,z] -> [x]@, used to perform the calculation in a
--              forward direction.
--
--          (3) is @[x,z] -> [y]@, used to run the calculation backwards to
--              determine the first input argument
--
--          (4) is @[x,y] -> [z]@, used to run the calculation backwards to
--              determine the second input argument
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmod21inv :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod21inv :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod21inv ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1,ModifierFn vn
f2,ModifierFn vn
f3] lbs :: [lb]
lbs@(~[lb
lb1,lb
lb2,lb
lb3]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1],[lb
lb2],[lb
lb3]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 [Just vn
v1,Just vn
v2,Just vn
v3] VarBinding lb vn
vbind = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn
v1,vn
v2,vn
v3]) VarBinding lb vn
vbind
        app2 [Maybe vn
Nothing,Just vn
v2,Just vn
v3] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb1 (ModifierFn vn
f1 [vn
v2,vn
v3]) VarBinding lb vn
vbind
        app2 [Just vn
v1,Maybe vn
Nothing,Just vn
v3] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb2 (ModifierFn vn
f2 [vn
v1,vn
v3]) VarBinding lb vn
vbind
        app2 [Just vn
v1,Just vn
v2,Maybe vn
Nothing] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb3 (ModifierFn vn
f3 [vn
v1,vn
v2]) VarBinding lb vn
vbind
        app2 [Maybe vn]
_                               VarBinding lb vn
_     = []
makeVmod21inv ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod21inv: requires 4 functions and 3 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a @2->1@ non-invertable function, such as
--  logical @AND@ or @OR@.
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (1) is @[x,y,z] -> [?]@, used as a filter (i.e. not creating any
--              new variable bindings), returning a non-empty list if
--              @x@, @y@ and @z@ are in the appropriate relationship.
--
--          (2) is @[y,z] -> [x]@, used to perform the calculation in a
--              forward direction.
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmod21 :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod21 :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod21 ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1] lbs :: [lb]
lbs@(~[lb
lb1,lb
_,lb
_]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 [Just vn
v1,Just vn
v2,Just vn
v3] VarBinding lb vn
vbind = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn
v1,vn
v2,vn
v3]) VarBinding lb vn
vbind
        app2 [Maybe vn
Nothing,Just vn
v2,Just vn
v3] VarBinding lb vn
vbind = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb1 (ModifierFn vn
f1 [vn
v2,vn
v3]) VarBinding lb vn
vbind
        app2 [Maybe vn]
_                               VarBinding lb vn
_     = []
makeVmod21 ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod21: requires 2 functions and 3 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a simple comparson of two values.
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (1) is @[x,y] -> [?]@, used as a filter (i.e. not creating any
--              new variable bindings), returning a non-empty list if
--              @x@ and @y@ are in the appropriate relationship.
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmod20 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod20 :: forall lb vn.
(Eq lb, Show lb, Eq vn, Show vn) =>
ApplyModifier lb vn
makeVmod20 ScopedName
nam [ModifierFn vn
f0] lbs :: [lb]
lbs@(~[lb
_,lb
_]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = forall {varBinding :: * -> * -> *} {lb}.
[Maybe vn] -> varBinding lb vn -> [varBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> varBinding lb vn -> [varBinding lb vn]
app2 [Just vn
v1,Just vn
v2] varBinding lb vn
vbind = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn
v1,vn
v2]) varBinding lb vn
vbind
        app2 [Maybe vn]
_                     varBinding lb vn
_     = []
makeVmod20 ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod20: requires 1 function and 2 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a @2->2@ non-invertable function, such as
--  quotient/remainder
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (1) is @[w,x,y,z] -> [?]@, used as a filter (i.e. not creating
--              any new variable bindings), returning a non-empty list if
--              @w@, @x@, @y@ and @z@ are in the appropriate relationship.
--
--          (2) is @[y,z] -> [w,x]@, used to perform the calculation given
--              two input values.
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
--  NOTE: this might be generalized to allow one of @w@ or @x@ to be
--  specified, and return null if it doesn't match the calculated value.
--
makeVmod22 :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod22 :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmod22 ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1] lbs :: [lb]
lbs@(~[lb
lb1,lb
lb2,lb
_,lb
_]) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1,lb
lb2]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 [Just vn
v1,Just vn
v2,Just vn
v3,Just vn
v4] VarBinding lb vn
vbind =
            forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn
v1,vn
v2,vn
v3,vn
v4]) VarBinding lb vn
vbind
        app2 [Maybe vn
Nothing,Maybe vn
Nothing,Just vn
v3,Just vn
v4] VarBinding lb vn
vbind =
            forall lb vt.
(Ord lb, Ord vt) =>
lb -> lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv2 lb
lb1 lb
lb2 (ModifierFn vn
f1 [vn
v3,vn
v4]) VarBinding lb vn
vbind
        app2 [Maybe vn]
_                               VarBinding lb vn
_     = []
makeVmod22 ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmod22: requires 2 functions and 4 labels"

-- |'ApplyModifier' function for use with 'DatatypeMod' in cases
--  when the value mapping is a @N->1@ function,
--  such as Sigma (sum) of a vector.
--
--  [@nam@]     is the name from the 'DatatypeMod' value that is carried into
--          the resulting variable binding modifier.
--
--  [@fns@]     are functions used to implement details of the variable
--          binding modifier:
--
--          (1) is @[x,y...] -> [?]@, used as a filter (i.e. not creating
--              any new variable bindings), returning a non-empty list if
--              @x@ and @y...@ are in the appropriate relationship.
--
--          (2) is @[y...] -> [x]@, used to perform the calculation.
--
--  [@lbs@]     is a list of specific label values for which a variable binding
--          modifier will be generated.
--
--  Note: an irrefutable pattern match for @lbs@ is used so that a name
--  for the 'VarBindingModify' value can be extracted using an undefined
--  label value.
--
makeVmodN1 :: (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmodN1 :: forall lb vn. (Ord lb, Ord vn) => ApplyModifier lb vn
makeVmodN1 ScopedName
nam [ModifierFn vn
f0,ModifierFn vn
f1] lbs :: [lb]
lbs@(~(lb
lb1:[lb]
_)) = VarBindingModify
    { vbmName :: ScopedName
vbmName   = ScopedName
nam
    , vbmApply :: [VarBinding lb vn] -> [VarBinding lb vn]
vbmApply  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarBinding lb vn -> [VarBinding lb vn]
app1
    , vbmVocab :: [lb]
vbmVocab  = [lb]
lbs
    , vbmUsage :: [[lb]]
vbmUsage  = [[],[lb
lb1]]
    }
    where
        app1 :: VarBinding lb vn -> [VarBinding lb vn]
app1 VarBinding lb vn
vbind = [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding lb vn
vbind) [lb]
lbs) VarBinding lb vn
vbind
        app2 :: [Maybe vn] -> VarBinding lb vn -> [VarBinding lb vn]
app2 vs :: [Maybe vn]
vs@(Maybe vn
v1:[Maybe vn]
_) VarBinding lb vn
vbind
            | forall a. Maybe a -> Bool
isJust Maybe vn
v1 Bool -> Bool -> Bool
&& Bool
isJustvs = forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv (ModifierFn vn
f0 [vn]
jvs) VarBinding lb vn
vbind
            | Bool
isJustvs              = forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb1 (ModifierFn vn
f1 [vn]
jvs) VarBinding lb vn
vbind
            | Bool
otherwise             = []
            where
                isJustvs :: Bool
isJustvs = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe vn]
vs
                jvs :: [vn]
jvs      = forall a. [Maybe a] -> [a]
catMaybes [Maybe vn]
vs
        app2 [Maybe vn]
_ VarBinding lb vn
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"app2 sent empty list" -- -Wall

makeVmodN1 ScopedName
_ [ModifierFn vn]
_ [lb]
_ =
    forall a. HasCallStack => [Char] -> a
error [Char]
"makeVmodN1: requires 2 functions and at 1 or more labels"

--------------------------------------------------------
--  Local helper functions for makeVmodXXX variants
--------------------------------------------------------

--  Add value to variable variable binding, if value is singleton list,
--  otherwise return empty list.
addv :: (Ord lb, Ord vt)
    => lb -> [vt] -> VarBinding lb vt
    -> [VarBinding lb vt]
addv :: forall lb vt.
(Ord lb, Ord vt) =>
lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv lb
lb [vt
val] VarBinding lb vt
vbind = [forall a b.
(Ord a, Ord b) =>
a -> b -> VarBinding a b -> VarBinding a b
addVarBinding lb
lb vt
val VarBinding lb vt
vbind]
addv lb
_  [vt]
_     VarBinding lb vt
_     = []

--  Add two entries to variable variable binding, if value supplied is
--  a doubleton list, otherwise return empty list.
addv2 :: (Ord lb, Ord vt)
    => lb -> lb -> [vt] -> VarBinding lb vt
    -> [VarBinding lb vt]
addv2 :: forall lb vt.
(Ord lb, Ord vt) =>
lb -> lb -> [vt] -> VarBinding lb vt -> [VarBinding lb vt]
addv2 lb
lb1 lb
lb2 [vt
val1,vt
val2] VarBinding lb vt
vbind = [forall a b.
(Ord a, Ord b) =>
a -> b -> VarBinding a b -> VarBinding a b
addVarBinding lb
lb1 vt
val1 forall a b. (a -> b) -> a -> b
$
                                   forall a b.
(Ord a, Ord b) =>
a -> b -> VarBinding a b -> VarBinding a b
addVarBinding lb
lb2 vt
val2 VarBinding lb vt
vbind]
addv2 lb
_   lb
_   [vt]
_           VarBinding lb vt
_     = []

--  If supplied value is non-empty list return supplied variable binding,
--  otherwise return empty list.
selv :: [vt] -> varBinding lb vt -> [varBinding lb vt]
selv :: forall vt (varBinding :: * -> * -> *) lb.
[vt] -> varBinding lb vt -> [varBinding lb vt]
selv [] varBinding lb vt
_     = []
selv [vt]
_  varBinding lb vt
vbind = [varBinding lb vt
vbind]

--------------------------------------------------------------
--  Functions for evaluating arguments in a datatype relation
--------------------------------------------------------------
--
--  altArgs is a generic function for evaluating datatype relation
--          values, based on suppied functions and argument values
--
--  UnaryFnDescr, UnaryFnApply and unaryFnApp:
--          are support types and function for using altArgs to
--          evaluate relations on unary functions (binary relations).
--
--  BinaryFnDescr, BinaryFnApply and binaryFnApp:
--          are support types and function for using altArgs to
--          evaluate relations on binary functions (3-way relations).
--
--  ListFnDescr, ListFnApply and listFnApp:
--          are support types and function for using altArgs to
--          evaluate relations on list functions (n-way relations),
--          where the first member of the list is the value of a
--          fold of a function over the rest of the list.
--
--  See experimental module spike-altargs.hs for test cases and
--  development steps for this function.

-- |Given a list of argument values and a list of functions for
--  calculating new values from supplied values, return a list
--  of argument values, or @Nothing@ if the supplied values are
--  inconsistent with the calculations specified.
--
--  Each list of values returned corresponds to a set of values that
--  satisfy the relation, consistent with the values supplied.
--
--  Functions are described as tuple consisting of:
--
--    (a) a predicate that the argument is required to satisfy
--
--    (b) a function to apply,
--
--    (c) a function to apply function (b) to a list of arguments
--
--    (d) argument list index values to which the function is applied.
--
--  Each supplied argument is of the form @Maybe a@, where the argument
--  has value type a.  @Nothing@ indicates arguments of unknown value.
--
--  The basic idea is that, for each argument position in the relation,
--  a function may be supplied to calculate that argument's possible values
--  from some combination of the other arguments.  The results calculated
--  in this way are compared with the original arguments provided:
--  if the values conflict then the relation is presumed to be
--  unsatisfiable with the supplied values, and @Nothing@ is returned;
--  if there are any calculated values for arguments supplied without
--  any values, then tbe calculated values are used.
--  If there are any arguments for which no values are supplied or
--  calculated, then the relation is presumed to be underdetermined,
--  and @Just []@ is returned.
--
altArgs :: 
  (Eq vt)
  => DatatypeRelPr vt 
  -> [(vt->Bool,[b])]
  -- ^ a list of argument value predicates and
  --   function descriptors.  The predicate indicates any
  --   additional constraints on argument values (e.g. the result
  --   of abs must be positive).  Use @(const True)@ for the predicate
  --   associated with unconstrained relation arguments.
  --   For each argument, a list of function descriptors is
  --   supplied corresponding to alternative values (e.g. a square
  --   relation would offer two alternative values for the root.)

  -> ((vt->Bool)->b->[Maybe vt]->Maybe [vt])
  -- ^ a function that takes an argument value predicate,
  --   a function descriptor and applies it to a supplied argument
  --   list to return:
  --   @Just a@ calculated list of one or more possible argument values,
  --   @Just []@ indicating insufficient information provided, or
  --   @Nothing@ indicating inconsistent information provided.
  --   May be one of 'unaryFnApp', 'binaryFnApp', 'listFnApp' or
  --   some other caller-supplied value.

  -> DatatypeRelFn vt
  -- ^ The return value can be used as the
  -- 'dtRelFunc' component of a 'DatatypeRel' value.

altArgs :: forall vt b.
Eq vt =>
DatatypeRelPr vt
-> [(vt -> Bool, [b])]
-> ((vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt])
-> DatatypeRelFn vt
altArgs DatatypeRelPr vt
pr [(vt -> Bool, [b])]
fnss (vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt]
apfn [Maybe vt]
args = forall {t :: * -> *}.
Foldable t =>
Maybe (t [vt]) -> Maybe (t [vt])
cvals4 Maybe [[vt]]
cvals3
    where
        --  Calculate new value(s) for each argument from supplied values, and
        --  lift inconsistency indicator (Just/Nothing) to outermost Monad.
        --    cvals1 :: [Maybe [vt]]
        cvals1 :: [Maybe [vt]]
cvals1 = forall a b. [a -> b] -> a -> [b]
flist (forall a b. (a -> b) -> [a] -> [b]
map (forall vt b.
((vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt])
-> (vt -> Bool, [b]) -> [Maybe vt] -> Maybe [vt]
applyFdescToTuple (vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt]
apfn) [(vt -> Bool, [b])]
fnss) [Maybe vt]
args
        --  Merge calculated values with supplied arguments, and again
        --  lift inconsistency indicator (Just/Nothing) to outermost Monad.
        --    cvals2 :: Maybe [[vt]]
        cvals2 :: Maybe [[vt]]
cvals2 = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall a.
Eq a =>
[a -> Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(vt -> Bool, [b])]
fnss) [Maybe vt]
args [Maybe [vt]]
cvals1
        --  Map list of alternative values for each tuple member to
        --  a list of alternative tuples.
        cvals3 :: Maybe [[vt]]
cvals3 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence Maybe [[vt]]
cvals2
        --  Check each tuple against the supplied predicate.
        --  If any of the alternative tuples does not match the predicate
        --  then signal an inconsistency.
        cvals4 :: Maybe (t [vt]) -> Maybe (t [vt])
cvals4 Maybe (t [vt])
Nothing       = forall a. Maybe a
Nothing
        cvals4 cvs :: Maybe (t [vt])
cvs@(Just t [vt]
ts) = if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DatatypeRelPr vt
pr t [vt]
ts then Maybe (t [vt])
cvs else forall a. Maybe a
Nothing

--  Perform alternative calculations for single result value
--  Each result value is a list of zero or more alternatives
--  that can be calculated from available parameters, or
--  Nothing if the available parameters are inconsistent.
--
--  apfn    is the function that actually applies an element of
--          the function descriptor to a tuple of Maybe arguments
--          (where Nothing is used to indicate an unknown value)
--  (p,fns) is a pair consisting of a value-checking predicate
--          for the corresponding tuple member, and a list of
--          function descriptors that each return one or more
--          values the tuple member, calculated from other values
--          that are present.  Just [] means no values are
--          calculated for this member, and Nothing means the
--          calculation has detected tuple values supplied that
--          are inconsistent with the datatype relation concerned.
--  args    is a tuple of Maybe tuple elements, (where Nothing
--          indicates an unknown value).
--
--  Returns Maybe a list of alternative values for the member,
--  Just [] to indicate insufficient information to calculate
--  any new values, and Nothing to indicate an inconsistency.
--
applyFdescToTuple ::
    ((vt->Bool)->b->[Maybe vt]->Maybe [vt]) -> (vt->Bool,[b]) -> [Maybe vt]
    -> Maybe [vt]
applyFdescToTuple :: forall vt b.
((vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt])
-> (vt -> Bool, [b]) -> [Maybe vt] -> Maybe [vt]
applyFdescToTuple (vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt]
apfn (vt -> Bool
p,[b]
fns) [Maybe vt]
args =
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Maybe [vt]]
cvals
    where
        -- cvals :: [Maybe [vt]]
        cvals :: [Maybe [vt]]
cvals = forall a b. [a -> b] -> a -> [b]
flist (forall a b. (a -> b) -> [a] -> [b]
map ((vt -> Bool) -> b -> [Maybe vt] -> Maybe [vt]
apfn vt -> Bool
p) [b]
fns) [Maybe vt]
args

--  Merge calculated tuple values with supplied tuple, checking for consistency.
--
--  ps      predicates used for isolated validation of each tuple member
--  args    supplied tuple values, with Nothing for unknown values
--  cvals   list of alternative calculated values for each tuple member,
--          or Nothing if an inconsistency has been detected by the
--          tuple-calculation functions.  Note that this list may contain
--          more entries than args; the surplus entries are ignored
--          (see list functions for how this is used).
--
--  Returns a tuple of Maybe lists of values for each tuple member,
--  containing Nothing if an inconsistency has been detected in the
--  supplied values.
--
mergeTupleVals  :: (Eq a) => [a->Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals :: forall a.
Eq a =>
[a -> Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals [a -> Bool]
_ [Maybe a]
_  (Maybe [a]
Nothing:[Maybe [a]]
_) = [forall a. Maybe a
Nothing]
mergeTupleVals (a -> Bool
_:[a -> Bool]
ps) (Maybe a
Nothing:[Maybe a]
a1s) (Just [a]
a2s:[Maybe [a]]
a2ss)
                             = forall a. a -> Maybe a
Just [a]
a2sforall a. a -> [a] -> [a]
:forall a.
Eq a =>
[a -> Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals [a -> Bool]
ps [Maybe a]
a1s [Maybe [a]]
a2ss
mergeTupleVals (a -> Bool
p:[a -> Bool]
ps) (Just a
a1:[Maybe a]
a1s) (Just []:[Maybe [a]]
a2ss)
    | a -> Bool
p a
a1                   = forall a. a -> Maybe a
Just [a
a1]forall a. a -> [a] -> [a]
:forall a.
Eq a =>
[a -> Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals [a -> Bool]
ps [Maybe a]
a1s [Maybe [a]]
a2ss
    | Bool
otherwise              = [forall a. Maybe a
Nothing]
mergeTupleVals (a -> Bool
p:[a -> Bool]
ps) (Just a
a1:[Maybe a]
a1s) (Just [a]
a2s:[Maybe [a]]
a2ss)
    | a -> Bool
p a
a1 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
a1 [a]
a2s    = forall a. a -> Maybe a
Just [a
a1]forall a. a -> [a] -> [a]
:forall a.
Eq a =>
[a -> Bool] -> [Maybe a] -> [Maybe [a]] -> [Maybe [a]]
mergeTupleVals [a -> Bool]
ps [Maybe a]
a1s [Maybe [a]]
a2ss
    | Bool
otherwise              = [forall a. Maybe a
Nothing]
mergeTupleVals [a -> Bool]
_ [] [Maybe [a]]
_        = []
mergeTupleVals [a -> Bool]
_ [Maybe a]
_  [Maybe [a]]
_        = [forall a. Maybe a
Nothing]

-- |'altArgs' support for unary functions: function descriptor type
type UnaryFnDescr a = (a->a,Int)

-- |'altArgs' support for unary functions: function descriptor table type
type UnaryFnTable a = [(a->Bool,[UnaryFnDescr a])]

-- |'altArgs' support for unary functions: function applicator type
type UnaryFnApply a = (a->Bool) -> UnaryFnDescr a -> [Maybe a] -> Maybe [a]

-- |'altArgs' support for unary functions: function applicator
unaryFnApp :: UnaryFnApply a
unaryFnApp :: forall a. UnaryFnApply a
unaryFnApp a -> Bool
p (a -> a
f1,Int
n) [Maybe a]
args = Maybe a -> Maybe [a]
apf ([Maybe a]
args forall a. [a] -> Int -> a
!! Int
n)
    where
        apf :: Maybe a -> Maybe [a]
apf (Just a
a) = if a -> Bool
p a
r then forall a. a -> Maybe a
Just [a
r] else forall a. Maybe a
Nothing where r :: a
r = a -> a
f1 a
a
        apf Maybe a
Nothing  = forall a. a -> Maybe a
Just []

-- |'altArgs' support for binary functions: function descriptor type
type BinaryFnDescr a = (a -> a -> a, Int, Int)

-- |'altArgs' support for binary functions: function descriptor table type
type BinaryFnTable a = [(a -> Bool, [BinaryFnDescr a])]

-- |'altArgs' support for binary functions: function applicator type
type BinaryFnApply a =
    (a -> Bool) -> BinaryFnDescr a -> [Maybe a] -> Maybe [a]

-- |'altArgs' support for binary functions: function applicator
binaryFnApp :: BinaryFnApply a
binaryFnApp :: forall a. BinaryFnApply a
binaryFnApp a -> Bool
p (a -> a -> a
f,Int
n1,Int
n2) [Maybe a]
args = Maybe a -> Maybe a -> Maybe [a]
apf ([Maybe a]
args forall a. [a] -> Int -> a
!! Int
n1) ([Maybe a]
args forall a. [a] -> Int -> a
!! Int
n2)
    where
        apf :: Maybe a -> Maybe a -> Maybe [a]
apf (Just a
a1) (Just a
a2) = if a -> Bool
p a
r then forall a. a -> Maybe a
Just [a
r] else forall a. Maybe a
Nothing
            where r :: a
r = a -> a -> a
f a
a1 a
a2
        apf Maybe a
_ Maybe a
_  = forall a. a -> Maybe a
Just []

-- |'altArgs' support for binary function with provision for indicating
--  inconsistent supplied values:  function descriptor type
type BinMaybeFnDescr a = (a -> a ->Maybe [a], Int, Int)

-- |'altArgs' support for binary function with provision for indicating
--  inconsistent supplied values:  function descriptor table type
type BinMaybeFnTable a = [(a -> Bool, [BinMaybeFnDescr a])]

-- |'altArgs' support for binary function with provision for indicating
--  inconsistent supplied values:  function applicator type
type BinMaybeFnApply a =
    (a -> Bool) -> BinMaybeFnDescr a -> [Maybe a] -> Maybe [a]

-- |'altArgs' support for binary function with provision for indicating
--  inconsistent supplied values:  function applicator
binMaybeFnApp :: BinMaybeFnApply a
binMaybeFnApp :: forall a. BinMaybeFnApply a
binMaybeFnApp a -> Bool
p (a -> a -> Maybe [a]
f,Int
n1,Int
n2) [Maybe a]
args = Maybe a -> Maybe a -> Maybe [a]
apf ([Maybe a]
args forall a. [a] -> Int -> a
!! Int
n1) ([Maybe a]
args forall a. [a] -> Int -> a
!! Int
n2)
    where
        apf :: Maybe a -> Maybe a -> Maybe [a]
apf (Just a
a1) (Just a
a2) = if forall {t :: * -> *}. Foldable t => Maybe (t a) -> Bool
pm Maybe [a]
r then Maybe [a]
r else forall a. Maybe a
Nothing
            where
                r :: Maybe [a]
r = a -> a -> Maybe [a]
f a
a1 a
a2
                pm :: Maybe (t a) -> Bool
pm Maybe (t a)
Nothing  = Bool
False
                pm (Just t a
x) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all a -> Bool
p t a
x
        apf Maybe a
_ Maybe a
_  = forall a. a -> Maybe a
Just []

-- |'altArgs' support for list functions (e.g. sum over list of args),
--  where first element of list is a fold over the rest of the list,
--  and remaining elements of list can be calculated in terms
--  of the result of the fold and the remaining elements
--
--  List function descriptor is
--
--  (a) list-fold function, f  (e.g. (+)
--        
--  (b) list-fold identity, z  (e.g. 0)
--        
--  (c) list-fold-function inverse, g (e.g. (-))
--        
--  (d) index of element to evaluate
--        
--  such that:
--        
--  >    (a `f` z) == (z `f` a) == a
--  >    (a `g` c) == b <=> a == b `f` c
--  >    (a `g` z) == a
--  >    (a `g` a) == z
--
--  and the result of the folded function does not depend on
--  the order that the list elements are processed.
--
--  NOTE:  the list of 'ListFnDescr' values supplied to 'altArgs' must
--  be at least as long as the argument list.  In many cases, Haskell
--  lazy evaluation can be used to supply an arbitrarily long list.
--  See test cases in spike-altargs.hs for an example.
--
--  Function descriptor type
type ListFnDescr a = (a -> a -> a, a, a -> a -> a, Int)

-- |Function table type
type ListFnTable a = [(a -> Bool, [ListFnDescr a])]

-- |'altArgs' support for list functions:  function applicator type
type ListFnApply a = (a -> Bool) -> ListFnDescr a -> [Maybe a] -> Maybe [a]

-- |'altArgs' support for list functions:  function applicator
listFnApp :: ListFnApply a
listFnApp :: forall a. ListFnApply a
listFnApp a -> Bool
p (a -> a -> a
f,a
z,a -> a -> a
g,Int
n) (Maybe a
a0:[Maybe a]
args)
    | Int
n forall a. Eq a => a -> a -> Bool
== Int
0    =
        Maybe [a] -> Maybe [a]
app forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. (a -> a -> a) -> Maybe a -> Maybe [a] -> Maybe [a]
apf a -> a -> a
f) (forall a. a -> Maybe a
Just [a
z]) [Maybe a]
args
    | Bool
otherwise =
        Maybe [a] -> Maybe [a]
app forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> Maybe a -> Maybe [a] -> Maybe [a]
apf a -> a -> a
g Maybe a
a0 (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a. (a -> a -> a) -> Maybe a -> Maybe [a] -> Maybe [a]
apf a -> a -> a
f) (forall a. a -> Maybe a
Just [a
z]) ([Maybe a]
args forall a. [a] -> Int -> [a]
`deleteIndex` (Int
n forall a. Num a => a -> a -> a
- Int
1)))
    where
        apf :: (a->a->a) -> Maybe a -> Maybe [a] -> Maybe [a]
        apf :: forall a. (a -> a -> a) -> Maybe a -> Maybe [a] -> Maybe [a]
apf a -> a -> a
fn (Just a
a1) (Just [a
a2]) = forall a. a -> Maybe a
Just [a -> a -> a
fn a
a1 a
a2]
        apf a -> a -> a
_  Maybe a
_         Maybe [a]
_           = forall a. a -> Maybe a
Just []
        
        -- app :: Maybe [a] -> Maybe [a]
        app :: Maybe [a] -> Maybe [a]
app Maybe [a]
Nothing      = forall a. Maybe a
Nothing
        app r :: Maybe [a]
r@(Just [a
a]) = if a -> Bool
p a
a then Maybe [a]
r else forall a. Maybe a
Nothing
        app Maybe [a]
_            = forall a. a -> Maybe a
Just []

listFnApp a -> Bool
_ (a -> a -> a, a, a -> a -> a, Int)
_ [] = forall a. HasCallStack => [Char] -> a
error [Char]
"listFnApp called with an empty list" -- -Wall

-- |Delete the n'th element of a list, returning the result
--
--  If the list doesn't have an n'th element, return the list unchanged.
--
deleteIndex :: [a] -> Int -> [a]
deleteIndex :: forall a. [a] -> Int -> [a]
deleteIndex [] Int
_ = []
deleteIndex xxs :: [a]
xxs@(a
x:[a]
xs) Int
n
    | Int
n forall a. Ord a => a -> a -> Bool
<  Int
0    = [a]
xxs
    | Int
n forall a. Eq a => a -> a -> Bool
== Int
0    = [a]
xs
    | Bool
otherwise = a
xforall a. a -> [a] -> [a]
:forall a. [a] -> Int -> [a]
deleteIndex [a]
xs (Int
nforall a. Num a => a -> a -> a
-Int
1)

{-
testdi1 = deleteIndex [1,2,3,4] 0    == [2,3,4]
testdi2 = deleteIndex [1,2,3,4] 1    == [1,3,4]
testdi3 = deleteIndex [1,2,3,4] 2    == [1,2,4]
testdi4 = deleteIndex [1,2,3,4] 3    == [1,2,3]
testdi5 = deleteIndex [1,2,3,4] 4    == [1,2,3,4]
testdi6 = deleteIndex [1,2,3,4] (-1) == [1,2,3,4]
testdi = and
    [ testdi1, testdi2, testdi3, testdi4, testdi5, testdi6 ]
-}

--------------------------------------------------------
--  Datatype sub/supertype description
--------------------------------------------------------

-- |Describe a subtype/supertype relationship between a pair of datatypes.
--
--  Originally, I had this as a supertype field of the DatatypeVal structure,
--  but that suffered from some problems:
--
--  * supertypes may be introduced retrospectively,
--
--  * the relationship expressed with respect to a single datatype
--      cannot indicate how to do injections/restrictions between the
--      underlying value types.
--
--  [@ex@]      is the type of expression with which the datatype may be used.
--
--  [@lb@]      is the type of the variable labels used.
--
--  [@vn@]      is the type of value node used to contain a datatyped value
--
--  [@supvt@]   is the internal value type of the super-datatype
--
--  [@subvt@]   is the internal value type of the sub-datatype
--
data DatatypeSub ex lb vn supvt subvt = DatatypeSub
    { forall ex lb vn supvt subvt.
DatatypeSub ex lb vn supvt subvt -> DatatypeVal ex supvt lb vn
trelSup   :: DatatypeVal ex supvt lb vn
                                -- ^ Datatype that is a supertype of @trelSub@,
                                --   having value space @supvt@.
    , forall ex lb vn supvt subvt.
DatatypeSub ex lb vn supvt subvt -> DatatypeVal ex subvt lb vn
trelSub   :: DatatypeVal ex subvt lb vn
                                -- ^ Datatype that is a subtype of @trelSup@,
                                --   having value space @supvt@.
    , forall ex lb vn supvt subvt.
DatatypeSub ex lb vn supvt subvt -> subvt -> supvt
trelToSup :: subvt -> supvt
                                -- ^ Function that maps subtype value to
                                --   corresponding supertype value.
    , forall ex lb vn supvt subvt.
DatatypeSub ex lb vn supvt subvt -> supvt -> Maybe subvt
trelToSub :: supvt -> Maybe subvt
                                -- ^ Function that maps supertype value to
                                --   corresponding subtype value, if there
                                --   is such a value.
    }

--------------------------------------------------------------------------------
--
--  Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--    2011, 2012, 2018, 2019, 2022 Douglas Burke
--  All rights reserved.
--
--  This file is part of Swish.
--
--  Swish is free software; you can redistribute it and/or modify
--  it under the terms of the GNU General Public License as published by
--  the Free Software Foundation; either version 2 of the License, or
--  (at your option) any later version.
--
--  Swish is distributed in the hope that it will be useful,
--  but WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--  GNU General Public License for more details.
--
--  You should have received a copy of the GNU General Public License
--  along with Swish; if not, write to:
--    The Free Software Foundation, Inc.,
--    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
--
--------------------------------------------------------------------------------