{-# 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 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 (Datatype dtv) = tvalName  dtv

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

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

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

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

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

-- |Get the canonical form of a datatype value.
typeMkCanonicalForm :: Datatype ex lb vn -> T.Text -> Maybe T.Text
typeMkCanonicalForm (Datatype dtv) = tvalMkCanonicalForm 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
    { tvalName      :: ScopedName
                                -- ^Identifies the datatype, and also
                                --  its value space class.
    , tvalRules     :: Ruleset ex
                                -- ^A set of named expressions and rules
                                --  that are valid in in any theory that
                                --  recognizes the current datatype.
    , 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.
    , tvalMkMods    :: [OpenVarBindingModify lb vn]
                                -- ^Constructs a list of open variable
                                --  binding modifiers based on tvalMod,
                                --  but hiding the actual value type.
    , 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
    , 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.
    , 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 nam dtv =
    let m = M.fromList $ map (\n -> (dtRelName n, n)) (tvalRel dtv)
    in M.lookup nam m

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

-- |Get the canonical form of a datatype value, or @Nothing@.
--
tvalMkCanonicalForm :: DatatypeVal ex vt lb vn -> T.Text -> Maybe T.Text
tvalMkCanonicalForm dtv str = can
    where
      dtmap = tvalMap dtv
      val   = mapL2V dtmap str
      can   = mapV2L dtmap =<< 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
    { 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@.
    , 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
    { dtRelName :: ScopedName
    , 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
    { dmName :: ScopedName
    , dmModf :: [ModifierFn vt]
    , dmAppf :: ApplyModifier lb vn
    }

-- |Null datatype value modifier
nullDatatypeMod :: DatatypeMod vt lb vn
nullDatatypeMod = DatatypeMod
    { dmName = swishName "nullDatatypeMod"
    , dmModf = []
    , dmAppf = nullAppf
    }
    where
        -- nullAppf :: ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn
        nullAppf nam _ lbs = (nullVarBindingModify lbs) { vbmName = 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 nam [f0,f1,f2] lbs@(~[lb1,lb2]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1],[lb2]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2] vbind = selv     (f0 [v1,v2]) vbind
        app2 [Nothing,Just v2] vbind = addv lb1 (f1 [v2])    vbind
        app2 [Just v1,Nothing] vbind = addv lb2 (f2 [v1])    vbind
        app2 _                     _     = []
makeVmod11inv _ _ _ =
    error "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 nam [f0,f1] lbs@(~[lb1,_]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2] vbind = selv (f0 [v1,v2])  vbind
        app2 [Nothing,Just v2] vbind = addv lb1 (f1 [v2]) vbind
        app2 _                     _     = []
makeVmod11 _ _ _ =
    error "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 nam [f0,f1,f2,f3] lbs@(~[lb1,lb2,lb3]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1],[lb2],[lb3]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2,Just v3] vbind = selv (f0 [v1,v2,v3]) vbind
        app2 [Nothing,Just v2,Just v3] vbind = addv lb1 (f1 [v2,v3]) vbind
        app2 [Just v1,Nothing,Just v3] vbind = addv lb2 (f2 [v1,v3]) vbind
        app2 [Just v1,Just v2,Nothing] vbind = addv lb3 (f3 [v1,v2]) vbind
        app2 _                               _     = []
makeVmod21inv _ _ _ =
    error "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 nam [f0,f1] lbs@(~[lb1,_,_]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2,Just v3] vbind = selv (f0 [v1,v2,v3]) vbind
        app2 [Nothing,Just v2,Just v3] vbind = addv lb1 (f1 [v2,v3]) vbind
        app2 _                               _     = []
makeVmod21 _ _ _ =
    error "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 nam [f0] lbs@(~[_,_]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2] vbind = selv (f0 [v1,v2]) vbind
        app2 _                     _     = []
makeVmod20 _ _ _ =
    error "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 nam [f0,f1] lbs@(~[lb1,lb2,_,_]) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1,lb2]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 [Just v1,Just v2,Just v3,Just v4] vbind =
            selv (f0 [v1,v2,v3,v4]) vbind
        app2 [Nothing,Nothing,Just v3,Just v4] vbind =
            addv2 lb1 lb2 (f1 [v3,v4]) vbind
        app2 _                               _     = []
makeVmod22 _ _ _ =
    error "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 nam [f0,f1] lbs@(~(lb1:_)) = VarBindingModify
    { vbmName   = nam
    , vbmApply  = concatMap app1
    , vbmVocab  = lbs
    , vbmUsage  = [[],[lb1]]
    }
    where
        app1 vbind = app2 (map (vbMap vbind) lbs) vbind
        app2 vs@(v1:_) vbind
            | isJust v1 && isJustvs = selv (f0 jvs) vbind
            | isJustvs              = addv lb1 (f1 jvs) vbind
            | otherwise             = []
            where
                isJustvs = all isJust vs
                jvs      = catMaybes vs
        app2 _ _ = error "app2 sent empty list" -- -Wall

makeVmodN1 _ _ _ =
    error "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 lb [val] vbind = [addVarBinding lb val vbind]
addv _  _     _     = []

--  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 lb1 lb2 [val1,val2] vbind = [addVarBinding lb1 val1 $
                                   addVarBinding lb2 val2 vbind]
addv2 _   _   _           _     = []

--  If supplied value is non-empty list return supplied variable binding,
--  otherwise return empty list.
selv :: [vt] -> varBinding lb vt -> [varBinding lb vt]
selv [] _     = []
selv _  vbind = [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 pr fnss apfn args = cvals4 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 = flist (map (applyFdescToTuple apfn) fnss) args
        --  Merge calculated values with supplied arguments, and again
        --  lift inconsistency indicator (Just/Nothing) to outermost Monad.
        --    cvals2 :: Maybe [[vt]]
        cvals2 = sequence $ mergeTupleVals (map fst fnss) args cvals1
        --  Map list of alternative values for each tuple member to
        --  a list of alternative tuples.
        cvals3 = fmap sequence cvals2
        --  Check each tuple against the supplied predicate.
        --  If any of the alternative tuples does not match the predicate
        --  then signal an inconsistency.
        cvals4 Nothing       = Nothing
        cvals4 cvs@(Just ts) = if all pr ts then cvs else 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 apfn (p,fns) args =
    concat <$> sequence cvals
    where
        -- cvals :: [Maybe [vt]]
        cvals = flist (map (apfn p) fns) 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 _ _  (Nothing:_) = [Nothing]
mergeTupleVals (_:ps) (Nothing:a1s) (Just a2s:a2ss)
                             = Just a2s:mergeTupleVals ps a1s a2ss
mergeTupleVals (p:ps) (Just a1:a1s) (Just []:a2ss)
    | p a1                   = Just [a1]:mergeTupleVals ps a1s a2ss
    | otherwise              = [Nothing]
mergeTupleVals (p:ps) (Just a1:a1s) (Just a2s:a2ss)
    | p a1 && elem a1 a2s    = Just [a1]:mergeTupleVals ps a1s a2ss
    | otherwise              = [Nothing]
mergeTupleVals _ [] _        = []
mergeTupleVals _ _  _        = [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 p (f1,n) args = apf (args!!n)
    where
        apf (Just a) = if p r then Just [r] else Nothing where r = f1 a
        apf Nothing  = 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 p (f,n1,n2) args = apf (args!!n1) (args!!n2)
    where
        apf (Just a1) (Just a2) = if p r then Just [r] else Nothing
            where r = f a1 a2
        apf _ _  = 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 p (f,n1,n2) args = apf (args!!n1) (args!!n2)
    where
        apf (Just a1) (Just a2) = if pm r then r else Nothing
            where
                r = f a1 a2
                pm Nothing  = False
                pm (Just x) = all p x
        apf _ _  = 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 p (f,z,g,n) (a0:args)
    | n == 0    =
        app $ foldr (apf f) (Just [z]) args
    | otherwise =
        app $ apf g a0 (foldr (apf f) (Just [z]) (args `deleteIndex` (n-1)))
    where
        apf :: (a->a->a) -> Maybe a -> Maybe [a] -> Maybe [a]
        apf fn (Just a1) (Just [a2]) = Just [fn a1 a2]
        apf _  _         _           = Just []

        -- app :: Maybe [a] -> Maybe [a]
        app Nothing      = Nothing
        app r@(Just [a]) = if p a then r else Nothing
        app _            = Just []

listFnApp _ _ [] = error "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 [] _ = []
deleteIndex xxs@(x:xs) n
    | n <  0    = xxs
    | n == 0    = xs
    | otherwise = x:deleteIndex xs (n-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
    { trelSup   :: DatatypeVal ex supvt lb vn
                                -- ^ Datatype that is a supertype of @trelSub@,
                                --   having value space @supvt@.
    , trelSub   :: DatatypeVal ex subvt lb vn
                                -- ^ Datatype that is a subtype of @trelSup@,
                                --   having value space @supvt@.
    , trelToSup :: subvt -> supvt
                                -- ^ Function that maps subtype value to
                                --   corresponding supertype value.
    , 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 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
--
--------------------------------------------------------------------------------