{-# OPTIONS -XExistentialQuantification #-}
{-# OPTIONS -XMultiParamTypeClasses #-}

--------------------------------------------------------------------------------
   $ I d : Datatype.hs , v 1.21 2003/12/18 18:27:46 graham Exp $ 
--
   Copyright ( c ) 2003 ,   .   All rights reserved . 
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
   Module       :   Datatype 
   Copyright    :   ( c ) 2003 ,   
   License      :   GPL V2 
--
   Maintainer   :     
--  Stability   :  provisional
   Portability :   H98 + existential types + rank 2 polymorphism 
--
   This module defines the structures used by Swish 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 RDFDatatype , ClassRestrictionRule and RDFDatatypeXsdInteger . 
--  See also module ClassRestrictionRuleTest for test cases.
--
--------------------------------------------------------------------------------

module Swish.HaskellRDF.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 
    , makeVmod_1_1_inv, makeVmod_1_1
    , makeVmod_2_1_inv, makeVmod_2_1
    , makeVmod_2_0
    , makeVmod_2_2
    , makeVmod_N_1
    , DatatypeSub(..)
    )
where

import Swish.HaskellRDF.Ruleset
    ( Ruleset(..)
    , getRulesetAxiom, getRulesetRule
    )

import Swish.HaskellRDF.Rule
    ( Formula(..)
    , Rule(..)
    )

import Swish.HaskellUtils.Namespace
    ( ScopedName(..)
    )

import Swish.HaskellRDF.Vocabulary
    ( swishName )

import Swish.HaskellRDF.VarBinding
    ( VarBinding(..)
    , addVarBinding
    , VarBindingModify(..), OpenVarBindingModify, nullVarBindingModify
    )

import Swish.HaskellUtils.LookupMap
    ( LookupEntryClass(..), LookupMap(..)
    , mapFindMaybe
    )

import Swish.HaskellUtils.ListHelpers
    ( flist
    , deleteIndex
    )

import Data.Maybe( isJust, catMaybes )

import Control.Monad( join, liftM )

------------------------------------------------------------
   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.
--
--  Note, the 'forall' is used in the sense of existentially quantified:
   see the Glasgow Haskell Compiler ( GHC ) user guide , section 7.3.12 
--
data Datatype ex lb vn = forall vt . Datatype (DatatypeVal ex vt lb vn)

instance LookupEntryClass
        (Datatype ex lb vn) ScopedName (Datatype ex lb vn)
    where
    newEntry (_,dt) = dt
    keyVal dt       = (typeName dt, dt)

  |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 named axiom from Datatype value 
getTypeAxiom :: ScopedName -> Datatype ex lb vn -> Maybe (Formula ex)
getTypeAxiom nam dt = getRulesetAxiom nam (typeRules dt)

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

-- |Get cacnonical form of datatype value
typeMkCanonicalForm :: Datatype ex lb vn -> String -> Maybe String
typeMkCanonicalForm (Datatype dtv) valstr = tvalMkCanonicalForm dtv valstr

------------------------------------------------------------
   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 (  in ) a given 
--  type of (syntactic) expression with which it may be used, and
--  a value type (whos existence is hidden as an existential type
   within DatatypeMap 
--
--  (I tried hiding the value type with an internal existential
   declaration , but that would n't wash .   Hence this two - part 
   structure with Datatype ( above ) in which the internal detail 
   of the value type is hidden from users of the Datatype class . ) 
--
   The datatype characteristic functions have two goals : 
--  - to support the general datatype entailment rules defined by
     the RDF semantics specification , and 
--  - 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 : 
--  (a) by variable binding modifiers that can be combined with the
--      query results during forward- for backward-chaining of
--      inference rules, and
--  (b) 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  ) , 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.]]]
    }

--  Other accessor functions

getDTRel ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeRel vt)
getDTRel nam dtv =
    mapFindMaybe nam (LookupMap (tvalRel dtv))

getDTMod ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeMod vt lb vn)
getDTMod nam dtv =
    mapFindMaybe nam (LookupMap (tvalMod dtv))

-- |Get canonical form of datatype value, or None
--
tvalMkCanonicalForm :: DatatypeVal ex vt lb vn -> String -> Maybe String
tvalMkCanonicalForm dtv str = can
    where
        val  = mapL2V (tvalMap dtv) str
        can = join $ liftM (mapV2L (tvalMap dtv)) 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.
--
data DatatypeMap vt = DatatypeMap
    { mapL2V  :: String -> Maybe vt
                            -- ^ Function to map lexical string to
                            --   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 String
                            -- ^ 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:
--  (a) 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.
--  (b) Just an empty list is returned if the supplied values are
--      insufficient to compute any complete sets of values in the
--      relation.
--  (c) 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
    }

instance LookupEntryClass (DatatypeRel vt) ScopedName (DatatypeRel vt)
    where
    newEntry (_,relf) = relf
    keyVal dtrel = (dtRelName dtrel, dtrel)

  |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
    }

instance LookupEntryClass
        (DatatypeMod vt lb vn) ScopedName (DatatypeMod vt lb vn)
    where
    newEntry (_,dmod) = dmod
    keyVal dmod = (dmName dmod, dmod)

-- |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 : : (   , Show lb , Eq vn , Show vn ) 
     = > DatatypeMod vt lb vn - > OpenVarBindingModify lb vn 
 applyDatatypeMod dtmod =   (   ) (   ) 

-- |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 
   : : [ ModifierFn vt ] 
              : : [ [ vt ] - > [ vt ] ] 
   : : ApplyModifier lb vn 
              : : ScopedName - > [ ModifierFn vn ] - > OpenVarBindingModify lb vn 
              : : ScopedName - > [ [ vn ] - > [ vn ] ] - > OpenVarBindingModify lb vn 
   (   ) 
              : : [ [ vn ] - > [ vn ] ] - > OpenVarBindingModify lb vn 

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.
--
         ia 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.
--
   type   vn = [ ModifierFn vn ] - > [ lb ] - > VarBindingModify lb vn 
--
makeVmod_1_1_inv :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_1_1_inv 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 _                     _     = []
makeVmod_1_1_inv _ _ _ =
    error "makeVmod_1_1_inv: 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.
--
         ia 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.
--
makeVmod_1_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_1_1 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 _                     _     = []
makeVmod_1_1 _ _ _ =
    error "makeVmod_1_1: 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.
--
         ia 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.
--
makeVmod_2_1_inv :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_1_inv 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 _                               _     = []
makeVmod_2_1_inv _ _ _ =
    error "makeVmod_2_1_inv: 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.
--
         ia 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.
--
makeVmod_2_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_1 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 _                               _     = []
makeVmod_2_1 _ _ _ =
    error "makeVmod_2_1: 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 . 
--
         ia 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.
--
makeVmod_2_0 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_0 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 _                     _     = []
makeVmod_2_0 _ _ _ =
    error "makeVmod_2_0: 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
--
         ia 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.]]]
--
makeVmod_2_2 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_2 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 _                               _     = []
makeVmod_2_2 _ _ _ =
    error "makeVmod_2_2: 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 . 
--
         ia 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.
--
makeVmod_N_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_N_1 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
makeVmod_N_1 _ _ _ =
    error "makeVmod_N_1: 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 :: (Eq lb, Show lb, Eq vt, Show 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 :: (Eq lb, Show lb, Eq vt, Show 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.
--
--  fnss    is 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 . ) 
   apfn     is 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.
--          The value used must match the type of 'fnss' used.
--
   Returns a ' DatatypeRelFn  ' value that can be used as the 
--  'dtRelFunc' component of a DatatypeRel value.
--  cf. type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]
--
-- type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]
-- type DatatypeRelPr vt = [vt] -> Bool
--
altArgs :: (Eq vt)
    => DatatypeRelPr vt -> [(vt->Bool,[b])]
    -> ((vt->Bool)->b->[Maybe vt]->Maybe [vt])
    -> DatatypeRelFn vt
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 . 
      : : [ 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 = liftM 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 =
    liftM concat $ sequence cvals
    where
        -- cvals :: [Maybe [vt]]
        cvals = flist (map (apfn p) fns) args

--  Merge calculated tuple values with supplied tuple, checking for consistency.
--
     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 p f1 (args!!n)
    where
        apf p f1 (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 p f (args!!n1) (args!!n2)
    where
        apf p f (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 p f (args!!n1) (args!!n2)
    where
        apf p f (Just a1) (Just a2) = if pm r then r else Nothing
            where
                r = f a1 a2
                pm Nothing  = False
                pm (Just r) = all p r
        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 ,  ( 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 p $ foldr (apf f) (Just [z]) args
    | otherwise =
        app p $ apf g a0 (foldr (apf f) (Just [z]) (args `deleteIndex` (n-1)))
    where
        apf :: (a->a->a) -> Maybe a -> Maybe [a] -> Maybe [a]
        apf f (Just a1) (Just [a2]) = Just [f a1 a2]
        apf _ _         _           = Just []
        app :: (a->Bool) -> Maybe [a] -> Maybe [a]
        app p Nothing      = Nothing
        app p r@(Just [a]) = if p a then r else Nothing
        app _ _            = Just []

--------------------------------------------------------
   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:
--  (a) supertypes may be introduced retrospectively,
--  (b) the relationship expressed with respect to a single datatype
--      cannot indicate hiow 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 ,   .   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 
--
--------------------------------------------------------------------------------
  $ Source : /file /  / HaskellRDF / Datatype.hs , v $ 
  $ Author :   
  $ Revision : 1.21 $ 
-- $Log: Datatype.hs,v $
-- Revision 1.21  2003/12/18 18:27:46  graham
  Datatyped literal inferences all working 
-- (except equivalent literals with different datatypes)
--
  Revision 1.20   2003/12/10 03:48:57    
  SwishScript nearly complete :   BwdChain and PrrofCheck to do . 
--
  Revision 1.19   2003/12/08 23:55:36    
-- Various enhancements to variable bindings and proof structure.
-- New module BuiltInMap coded and tested.
-- Script processor is yet to be completed.
--
  Revision 1.18   2003/12/08 17:29:19    
-- Moved OpenVarBinding type definitions from -Datatype to -VarBinding modules.
--
  Revision 1.17   2003/12/04 02:53:27    
  More changes to  functions . 
  SwishScript logic part complete , type - checks OK . 
--
  Revision 1.16   2003/11/28 00:17:55    
  Datatype constraint test cases all passed . 
--
  Revision 1.15   2003/11/27 11:35:49    
-- Variable modifier tests all run.
-- Initial class constraint reasoning tests pass.
-- Fixed bug in class constraint backward-chained reasoning that returned
-- multiple instances of some statements, and did not filter out all occurrences
-- of the original statements.
--
  Revision 1.14   2003/11/25 23:02:17    
-- Reworked datatype variable modifier logic.
  Limited range of test cases so far all pass . 
--
  Revision 1.13   2003/11/24 22:13:09    
-- Working on reworking datatype variable modifiers to work with
-- revised datatype framework.
--
  Revision 1.12   2003/11/17 21:53:31   graham 
  Datatype inference forward chaining updated to allow inconsistent 
-- partial inputs to be detected.  All forward chaining test cases passed.
-- Need to develop backward chaining test cases.
--
  Revision 1.11   2003/11/13 01:13:48    
-- Reworked ruleset to use ScopedName lookup.
-- Various minor fixes.
--
  Revision 1.10   2003/11/11 21:02:55    
-- Working on datatype class-constraint inference rule.  Incomplete.
--
  Revision 1.9   2003/11/07 21:45:47   graham 
-- Started rework of datatype to use new DatatypeRel structure.
--
  Revision 1.8   2003/11/06 17:58:33   graham 
  About to rework Datatype to better support class - based reasoning . 
--
  Revision 1.7   2003/10/24 21:05:08    
-- Working on datatype inference.  Most of the variable binding logic
-- is done, but the rule structure still needs to be worked out to support
-- forward and backward chaining through the same rule.
--
  Revision 1.6   2003/10/22 15:47:46   graham 
-- Working on datatype inference support.
--
  Revision 1.5   2003/10/09 13:58:59   graham 
  Sync with CVS .   Preparing to eliminate QueryBindingFilter in favour 
-- of using just QueryBindingModifier.
--
  Revision 1.4   2003/10/02 13:41:26    
  Supporting changes for RDF axioms and rules defined as Rulesets , 
-- and moved out of module RDFProofCheck.
  Datatype named using ScopedName rather than QName 
  ( Datatype framework is still work in progress ) . 
--
  Revision 1.3   2003/09/24 18:50:52   graham 
  Revised module format to be  compatible . 
--
-- Revision 1.2  2003/09/22 23:25:01  graham
-- Add some tweaks to the datatyping framework
--
  Revision 1.1   2003/07/03 20:31:07    
-- Add initial draft of datatype framework.
--

# OPTIONS -XExistentialQuantification #
# OPTIONS -XMultiParamTypeClasses #
------------------------------------------------------------------------------

  See end of this file for licence information.
------------------------------------------------------------------------------
 |

  Stability   :  provisional

  manipulate datatypes.  It is designed as a basis for handling datatyped

  Testing note:  this module supports a number of specific datatypes.
  It is intended that functionality in this module will be tested via
  See also module ClassRestrictionRuleTest for test cases.

------------------------------------------------------------------------------
----------------------------------------------------------
----------------------------------------------------------
  is used only in implementations of the datatype.
  Users see just the datatype name and associated ruleset.

  Note, the 'forall' is used in the sense of existentially quantified:

 |Make variable binding modifiers based on values supplied
 |Get cacnonical form of datatype value
----------------------------------------------------------
----------------------------------------------------------
 |DatatypeVal is a structure that defines a number of functions
  and values that characterize the behaviour of a datatype.

  type of (syntactic) expression with which it may be used, and
  a value type (whos existence is hidden as an existential type

  (I tried hiding the value type with an internal existential

  - to support the general datatype entailment rules defined by
  - to define additional datatype-specific inference patterns by
    means of which provide additional base functionality to

  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
  separately.  Definitions in this module are generally applicable
  only when using a single datatype.

  An alternative model for datatype value calculations is inspired
  (where the bare integer n here is shorthand for "n"^^xsd:integer)

  (a) by variable binding modifiers that can be combined with the
      query results during forward- for backward-chaining of
      inference rules, and
  (b) by the definition of inference rulesets that involve
      datatype values.
  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.

 ^Identifies the datatype, and also
  its value space class.
 ^A set of named expressions and rules
  that are valid in in any theory that
  recognizes the current datatype.
 ^A function that accepts an expression
  rules from it.  This is provided as a
  hook for creating datatyped class
  restriction rules.
 ^Constructs a list of open variable
  but hiding the actual value type.
 ^Lexical to value mapping, where 'vt' is
  to represent and manipulate values in
  the datatype's value space
 ^A set of named relations on datatype
  values.  Each relation accepts a list
  unspecified values that are in the
  relation with values supplied.
 ^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.]]]
  Other accessor functions
 |Get canonical form of datatype value, or None

 |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.

 ^ Function to map lexical string to
   datatype value.  This effectively
   defines the lexical space of the
   datatype to be all strings for which
   yield a value other than Nothing.
 ^ 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.

  datatype value type.  It returns:
  (a) 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.
  (b) Just an empty list is returned if the supplied values are
      insufficient to compute any complete sets of values in the
      relation.
  (c) Nothing if the supplied values are not consistent with
      the relation.

 |Type for datatype relation predicate:  accepts a list of values
  and determines whether or not they satisfy the relation.

 |Datatype for a named relation on values of a datatype.


  Each function accepts a list of values and returns a list of values.
  The exact significance of the different values supplied and returned
  but in all cases an empty list returned means that the corresponding
  inputs are not consistent with the function and cannot be used.

 |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.

  type:  the modifier functions may be "lifted" or otherwise adapted
  to operate on some other type from which the raw data values are
  extracted.)

 |Wrapper for data type variable binding modifier included in
  a datatype value.

 |Null datatype value modifier
 nullAppf :: ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn
 |Apply datatype variable binding modifier value to list of labels and 
   a variable binding . 
 |Apply datatype variable binding modifier value to list of labels and
  a variable binding.
------------------------------------------------------------
  Functions for creating datatype variable binding modifiers
------------------------------------------------------------
  when the value mapping is a 1->1 function and inverse, such
  as negate.

          the resulting variable binding modifier.
          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.
              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.


  the value mapping is a non-invertable 1->1 injection, such as
  absolute value.

          the resulting variable binding modifier.
          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.

  addition or subtraction.

          the resulting variable binding modifier.
          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.
              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.

  logical AND or OR.

          the resulting variable binding modifier.
          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.
              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.


          the resulting variable binding modifier.
          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.

  quotient/remainder

          the resulting variable binding modifier.
          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.
  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.

  specified, and return null if it doesn't match the calculated value.]]]

  when the value mapping is a N->1 function,

          the resulting variable binding modifier.
          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.

------------------------------------------------------
------------------------------------------------------
  Add value to variable variable binding, if value is singleton list,
  otherwise return empty list.
  a doubleton list, otherwise return empty list.
  If supplied value is non-empty list return supplied variable binding,
  otherwise return empty list.
------------------------------------------------------------
  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

          are support types and function for using altArgs to
          evaluate relations on unary functions (binary relations).

          are support types and function for using altArgs to

  ListFnDescr, ListFnApply and listFnApp:
          are support types and function for using altArgs to
          evaluate relations on list functions (n-way relations),
          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.

  fnss    is 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
          a function descriptor and applies it to a supplied argument
          list to return:
          Just [] indicating insufficient information provided, or
          Nothing indicating inconsistent information provided.
          some other caller-supplied value.
          The value used must match the type of 'fnss' used.

  'dtRelFunc' component of a DatatypeRel value.
  cf. type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]

 type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]
 type DatatypeRelPr vt = [vt] -> Bool

  Calculate new value(s) for each argument from supplied values, and
  Merge calculated values with supplied arguments, and again
  Map list of alternative values for each tuple member to
  a list of alternative tuples.
  Check each tuple against the supplied predicate.
  If any of the alternative tuples does not match the predicate
  then signal an inconsistency.
  Perform alternative calculations for single result value
  that can be calculated from available parameters, or
  Nothing if the available parameters are inconsistent.

          the function descriptor to a tuple of Maybe arguments
          (where Nothing is used to indicate an unknown value)
          for the corresponding tuple member, and a list of
          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.

 cvals :: [Maybe [vt]]
  Merge calculated tuple values with supplied tuple, checking for consistency.

  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.

 |altArgs support for unary functions: function descriptor type
 |altArgs support for unary functions: function descriptor table type
 |altArgs support for unary functions: function applicator type
 |altArgs support for unary functions: function applicator
 |altArgs support for binary functions: function descriptor type
 |altArgs support for binary functions: function descriptor table type
 |altArgs support for binary functions: function applicator type
 |altArgs support for binary functions: function applicator
 |altArgs support for binary function with provision for indicating
  inconsistent supplied values:  function descriptor type
 |altArgs support for binary function with provision for indicating
  inconsistent supplied values:  function descriptor table type
 |altArgs support for binary function with provision for indicating
  inconsistent supplied values:  function applicator type
 |altArgs support for binary function with provision for indicating
  inconsistent supplied values:  function applicator
 |altArgs support for list functions (e.g. sum over list of args),
  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)
  (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.

  lazy evaluation can be used to supply an arbitrarily long list.
  See test cases in spike-altargs.hs for an example.

  Function descriptor type
 |Function table type
 |altArgs support for list functions:  function applicator type
 |altArgs support for list functions:  function applicator
------------------------------------------------------
------------------------------------------------------
 |Describe a subtype/supertype relationship between a pair of datatypes.

  but that suffered from some problems:
  (a) supertypes may be introduced retrospectively,
  (b) the relationship expressed with respect to a single datatype
      cannot indicate hiow 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
  subvt   is the internal value type of the sub-datatype

 ^ Function that maps subtype value to
   corresponding supertype value.
 ^ Function that maps supertype value to
   corresponding subtype value, if there
   is such a value.
------------------------------------------------------------------------------



  (at your option) any later version.

  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.


------------------------------------------------------------------------------
 $Log: Datatype.hs,v $
 Revision 1.21  2003/12/18 18:27:46  graham
 (except equivalent literals with different datatypes)


 Various enhancements to variable bindings and proof structure.
 New module BuiltInMap coded and tested.
 Script processor is yet to be completed.

 Moved OpenVarBinding type definitions from -Datatype to -VarBinding modules.



 Variable modifier tests all run.
 Initial class constraint reasoning tests pass.
 Fixed bug in class constraint backward-chained reasoning that returned
 multiple instances of some statements, and did not filter out all occurrences
 of the original statements.

 Reworked datatype variable modifier logic.

 Working on reworking datatype variable modifiers to work with
 revised datatype framework.

 partial inputs to be detected.  All forward chaining test cases passed.
 Need to develop backward chaining test cases.

 Reworked ruleset to use ScopedName lookup.
 Various minor fixes.

 Working on datatype class-constraint inference rule.  Incomplete.

 Started rework of datatype to use new DatatypeRel structure.


 Working on datatype inference.  Most of the variable binding logic
 is done, but the rule structure still needs to be worked out to support
 forward and backward chaining through the same rule.

 Working on datatype inference support.

 of using just QueryBindingModifier.

 and moved out of module RDFProofCheck.


 Revision 1.2  2003/09/22 23:25:01  graham
 Add some tweaks to the datatyping framework

 Add initial draft of datatype framework.



   $ I d : Datatype.hs , v 1.21 2003/12/18 18:27:46 graham Exp $ 
   Copyright ( c ) 2003 ,   .   All rights reserved . 
   Module       :   Datatype 
   Copyright    :   ( c ) 2003 ,   
   License      :   GPL V2 
   Maintainer   :     
   Portability :   H98 + existential types + rank 2 polymorphism 
   This module defines the structures used by Swish to represent and 
   RDF literals , but the functions in this module are more generic . 
   modules RDFDatatype , ClassRestrictionRule and RDFDatatypeXsdInteger . 

module Swish.HaskellRDF.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 
    , makeVmod_1_1_inv, makeVmod_1_1
    , makeVmod_2_1_inv, makeVmod_2_1
    , makeVmod_2_0
    , makeVmod_2_2
    , makeVmod_N_1
    , DatatypeSub(..)
    )
where

import Swish.HaskellRDF.Ruleset
    ( Ruleset(..)
    , getRulesetAxiom, getRulesetRule
    )

import Swish.HaskellRDF.Rule
    ( Formula(..)
    , Rule(..)
    )

import Swish.HaskellUtils.Namespace
    ( ScopedName(..)
    )

import Swish.HaskellRDF.Vocabulary
    ( swishName )

import Swish.HaskellRDF.VarBinding
    ( VarBinding(..)
    , addVarBinding
    , VarBindingModify(..), OpenVarBindingModify, nullVarBindingModify
    )

import Swish.HaskellUtils.LookupMap
    ( LookupEntryClass(..), LookupMap(..)
    , mapFindMaybe
    )

import Swish.HaskellUtils.ListHelpers
    ( flist
    , deleteIndex
    )

import Data.Maybe( isJust, catMaybes )

import Control.Monad( join, liftM )

   Datatype framework 

  |Datatype wraps a DatatypeVal value , hiding the value type that 
   see the Glasgow Haskell Compiler ( GHC ) user guide , section 7.3.12 
data Datatype ex lb vn = forall vt . Datatype (DatatypeVal ex vt lb vn)

instance LookupEntryClass
        (Datatype ex lb vn) ScopedName (Datatype ex lb vn)
    where
    newEntry (_,dt) = dt
    keyVal dt       = (typeName dt, dt)

  |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

typeMkModifiers :: Datatype ex lb vn -> [OpenVarBindingModify lb vn]
typeMkModifiers (Datatype dtv) = tvalMkMods dtv

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

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

typeMkCanonicalForm :: Datatype ex lb vn -> String -> Maybe String
typeMkCanonicalForm (Datatype dtv) valstr = tvalMkCanonicalForm dtv valstr

   DatatypeVal 

   A datatype is specified with respect to (  in ) a given 
   within DatatypeMap 
   declaration , but that would n't wash .   Hence this two - part 
   structure with Datatype ( above ) in which the internal detail 
   of the value type is hidden from users of the Datatype class . ) 
   The datatype characteristic functions have two goals : 
     the RDF semantics specification , and 
     applications based on RDF inference . 
   Datatype - specific inferences are provided using the DatatypeRel 
   combined values of more than one datatype may be defined 
   by that introduced by CWM for arithmetic operations , e.g. 
        ( 1 2 3 ) math : sum ? x = > ? x rdf : value 6 
   Datatype - specific inference patterns are provided in two ways : 
   I believe the first method to be more flexible than the second , 
data DatatypeVal ex vt lb vn = DatatypeVal
    { tvalName      :: ScopedName
    , tvalRules     :: Ruleset ex
    , tvalMkRules   :: ex -> [Rule ex]
   and devives some datatype - dependent 
    , tvalMkMods    :: [OpenVarBindingModify lb vn]
   binding modifiers based on tvalMod , 
    , tvalMap       :: DatatypeMap vt
   a datatype used within a Haskell program 
    , tvalRel       :: [DatatypeRel vt]
   of ( Maybe  ) , and computes any 
    , tvalMod       :: [DatatypeMod vt lb vn]
    }


getDTRel ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeRel vt)
getDTRel nam dtv =
    mapFindMaybe nam (LookupMap (tvalRel dtv))

getDTMod ::
    ScopedName -> DatatypeVal ex vt lb vn -> Maybe (DatatypeMod vt lb vn)
getDTMod nam dtv =
    mapFindMaybe nam (LookupMap (tvalMod dtv))

tvalMkCanonicalForm :: DatatypeVal ex vt lb vn -> String -> Maybe String
tvalMkCanonicalForm dtv str = can
    where
        val  = mapL2V (tvalMap dtv) str
        can = join $ liftM (mapV2L (tvalMap dtv)) val

data DatatypeMap vt = DatatypeMap
    { mapL2V  :: String -> Maybe vt
    , mapV2L  :: vt -> Maybe String
    }

   The function accepts a list of Maybe vt , where vt is the 
type DatatypeRelFn vt = [Maybe vt] -> Maybe [[vt]]

type DatatypeRelPr vt = [vt] -> Bool

data DatatypeRel vt = DatatypeRel
    { dtRelName :: ScopedName
    , dtRelFunc :: DatatypeRelFn vt
    }

instance LookupEntryClass (DatatypeRel vt) ScopedName (DatatypeRel vt)
    where
    newEntry (_,relf) = relf
    keyVal dtrel = (dtRelName dtrel, dtrel)

  |Datatype value modifier functions type 
   depends on the variable binding pattern used ( cf . ApplyModifier ) , 
type ModifierFn vn = [vn] -> [vn]

   ( Note that vn is not necessarily the same as vt , the datatype value 
type ApplyModifier lb vn =
    ScopedName -> [ModifierFn vn] -> OpenVarBindingModify lb vn

data DatatypeMod vt lb vn = DatatypeMod
    { dmName :: ScopedName
    , dmModf :: [ModifierFn vt]
    , dmAppf :: ApplyModifier lb vn
    }

instance LookupEntryClass
        (DatatypeMod vt lb vn) ScopedName (DatatypeMod vt lb vn)
    where
    newEntry (_,dmod) = dmod
    keyVal dmod = (dmName dmod, dmod)

nullDatatypeMod :: DatatypeMod vt lb vn
nullDatatypeMod = DatatypeMod
    { dmName = swishName "nullDatatypeMod"
    , dmModf = []
    , dmAppf = nullAppf
    }
    where
        nullAppf nam _ lbs = (nullVarBindingModify lbs) { vbmName = nam }


 applyDatatypeMod : : (   , Show lb , Eq vn , Show vn ) 
     = > DatatypeMod vt lb vn - > OpenVarBindingModify lb vn 
 applyDatatypeMod dtmod =   (   ) (   ) 

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 
   : : [ ModifierFn vt ] 
              : : [ [ vt ] - > [ vt ] ] 
   : : ApplyModifier lb vn 
              : : ScopedName - > [ ModifierFn vn ] - > OpenVarBindingModify lb vn 
              : : ScopedName - > [ [ vn ] - > [ vn ] ] - > OpenVarBindingModify lb vn 
   (   ) 
              : : [ [ vn ] - > [ vn ] ] - > OpenVarBindingModify lb vn 

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
-}


  |ApplyModifier function for use with DatatypeMod in cases 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
           ( 2 ) is [ x ] - > [ y ] , used to perform the calculation in a backward 
               direction .   This may be the same as ( 2 ) ( e.g. for negation ) 
   type   vn = [ ModifierFn vn ] - > [ lb ] - > VarBindingModify lb vn 
makeVmod_1_1_inv :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_1_1_inv 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 _                     _     = []
makeVmod_1_1_inv _ _ _ =
    error "makeVmod_1_1_inv: requires 3 functions and 2 labels"

  |ApplyModifier function for use with DatatypeMod in cases when 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
makeVmod_1_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_1_1 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 _                     _     = []
makeVmod_1_1 _ _ _ =
    error "makeVmod_1_1: 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 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
           ( 2 ) is [ y , z ] - > [ x ] , used to perform the calculation in a 
           ( 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 
makeVmod_2_1_inv :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_1_inv 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 _                               _     = []
makeVmod_2_1_inv _ _ _ =
    error "makeVmod_2_1_inv: 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 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
           ( 2 ) is [ y , z ] - > [ x ] , used to perform the calculation in a 
makeVmod_2_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_1 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 _                               _     = []
makeVmod_2_1 _ _ _ =
    error "makeVmod_2_1: 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 . 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
makeVmod_2_0 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_0 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 _                     _     = []
makeVmod_2_0 _ _ _ =
    error "makeVmod_2_0: 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 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
           ( 2 ) is [ y , z ] - > [ w , x ] , used to perform the calculation given 
               two input values . 
   [ [ [ NOTE : this might be generalized to allow one of w or x to be 
makeVmod_2_2 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_2_2 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 _                               _     = []
makeVmod_2_2 _ _ _ =
    error "makeVmod_2_2: requires 2 functions and 4 labels"

  |ApplyModifier function for use with DatatypeMod in cases 
   such as Sigma ( sum ) of a vector . 
         ia the name from the DatatypeMod value that is carried into 
   fns      are functions used to implement details of the variable 
           ( 2 ) is [ y ... ] - > [ x ] , used to perform the calculation . 
makeVmod_N_1 :: (Eq lb, Show lb, Eq vn, Show vn) => ApplyModifier lb vn
makeVmod_N_1 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
makeVmod_N_1 _ _ _ =
    error "makeVmod_N_1: requires 2 functions and at 1 or more labels"

   Local helper functions for makeVmodXXX variants 

addv :: (Eq lb, Show lb, Eq vt, Show 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 
addv2 :: (Eq lb, Show lb, Eq vt, Show vt)
    => lb -> lb -> [vt] -> VarBinding lb vt
    -> [VarBinding lb vt]
addv2 lb1 lb2 [val1,val2] vbind = [addVarBinding lb1 val1 $
                                   addVarBinding lb2 val2 vbind]
addv2 _   _   _           _     = []

selv :: [vt] -> varBinding lb vt -> [varBinding lb vt]
selv [] _     = []
selv _  vbind = [vbind]

   UnaryFnDescr , UnaryFnApply and unaryFnApp : 
   BinaryFnDescr , BinaryFnApply and binaryFnApp : 
           evaluate relations on binary functions ( 3 - way relations ) . 
           where the first member of the list is the value of a 

           relation would offer two alternative values for the root . ) 
   apfn     is a function that takes an argument value predicate , 
           Just a calculated list of one or more possible argument values , 
           May be one of unaryFnApp , binaryFnApp , listFnApp or 
   Returns a ' DatatypeRelFn  ' value that can be used as the 
altArgs :: (Eq vt)
    => DatatypeRelPr vt -> [(vt->Bool,[b])]
    -> ((vt->Bool)->b->[Maybe vt]->Maybe [vt])
    -> DatatypeRelFn vt
altArgs pr fnss apfn args = cvals4 cvals3
    where
   lift inconsistency indicator ( Just / Nothing ) to outermost Monad . 
      : : [ Maybe [ vt ] ] 
        cvals1 = flist (map (applyFdescToTuple apfn) fnss) args
   lift inconsistency indicator ( Just / Nothing ) to outermost Monad . 
     cvals2 : : Maybe [ [ vt ] ] 
        cvals2 = sequence $ mergeTupleVals (map fst fnss) args cvals1
        cvals3 = liftM sequence cvals2
        cvals4 Nothing       = Nothing
        cvals4 cvs@(Just ts) = if all pr ts then cvs else Nothing

   Each result value is a list of zero or more alternatives 
   apfn     is the function that actually applies an element of 
   ( p , fns ) is a pair consisting of a value - checking predicate 
           function descriptors that each return one or more 
applyFdescToTuple ::
    ((vt->Bool)->b->[Maybe vt]->Maybe [vt]) -> (vt->Bool,[b]) -> [Maybe vt]
    -> Maybe [vt]
applyFdescToTuple apfn (p,fns) args =
    liftM concat $ sequence cvals
    where
        cvals = flist (map (apfn p) fns) args

     predicates used for isolated validation of each tuple member 
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]

type UnaryFnDescr a = (a->a,Int)

type UnaryFnTable a = [(a->Bool,[UnaryFnDescr a])]

type UnaryFnApply a = (a->Bool) -> UnaryFnDescr a -> [Maybe a] -> Maybe [a]

unaryFnApp :: UnaryFnApply a
unaryFnApp p (f1,n) args = apf p f1 (args!!n)
    where
        apf p f1 (Just a) = if p r then Just [r] else Nothing where r = f1 a
        apf _ _ Nothing   = Just []

type BinaryFnDescr a = (a->a->a,Int,Int)

type BinaryFnTable a = [(a->Bool,[BinaryFnDescr a])]

type BinaryFnApply a =
    (a->Bool) -> BinaryFnDescr a -> [Maybe a] -> Maybe [a]

binaryFnApp :: BinaryFnApply a
binaryFnApp p (f,n1,n2) args = apf p f (args!!n1) (args!!n2)
    where
        apf p f (Just a1) (Just a2) = if p r then Just [r] else Nothing
            where r = f a1 a2
        apf _ _ _ _  = Just []

type BinMaybeFnDescr a = (a->a->Maybe [a],Int,Int)

type BinMaybeFnTable a = [(a->Bool,[BinMaybeFnDescr a])]

type BinMaybeFnApply a =
    (a->Bool) -> BinMaybeFnDescr a -> [Maybe a] -> Maybe [a]

binMaybeFnApp :: BinMaybeFnApply a
binMaybeFnApp p (f,n1,n2) args = apf p f (args!!n1) (args!!n2)
    where
        apf p f (Just a1) (Just a2) = if pm r then r else Nothing
            where
                r = f a1 a2
                pm Nothing  = False
                pm (Just r) = all p r
        apf _ _ _ _  = Just []

   where first element of list is a fold over the rest of the list , 
   ( c ) list - fold - function inverse ,  ( e.g. ( - ) ) 
   NOTE :   the list of ' ListFnDescr ' values supplied to altArgs must 
   be at least as long as the argument list .   In many cases , Haskell 
type ListFnDescr a = (a->a->a,a,a->a->a,Int)

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

type ListFnApply a = (a->Bool) -> ListFnDescr a -> [Maybe a] -> Maybe [a]

listFnApp :: ListFnApply a
listFnApp p (f,z,g,n) (a0:args)
    | n == 0    =
        app p $ foldr (apf f) (Just [z]) args
    | otherwise =
        app p $ apf g a0 (foldr (apf f) (Just [z]) (args `deleteIndex` (n-1)))
    where
        apf :: (a->a->a) -> Maybe a -> Maybe [a] -> Maybe [a]
        apf f (Just a1) (Just [a2]) = Just [f a1 a2]
        apf _ _         _           = Just []
        app :: (a->Bool) -> Maybe [a] -> Maybe [a]
        app p Nothing      = Nothing
        app p r@(Just [a]) = if p a then r else Nothing
        app _ _            = Just []

   Datatype sub / supertype description 

   Originally , I had this as a supertype field of the DatatypeVal structure , 
   supvt    is the internal value type of the super - 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
    , trelToSub :: supvt -> Maybe subvt
    }


   Copyright ( c ) 2003 ,   .   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 
   Swish is distributed in the hope that it will be useful , 
   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 
  $ Source : /file /  / HaskellRDF / Datatype.hs , v $ 
  $ Author :   
  $ Revision : 1.21 $ 
  Datatyped literal inferences all working 
  Revision 1.20   2003/12/10 03:48:57    
  SwishScript nearly complete :   BwdChain and PrrofCheck to do . 
  Revision 1.19   2003/12/08 23:55:36    
  Revision 1.18   2003/12/08 17:29:19    
  Revision 1.17   2003/12/04 02:53:27    
  More changes to  functions . 
  SwishScript logic part complete , type - checks OK . 
  Revision 1.16   2003/11/28 00:17:55    
  Datatype constraint test cases all passed . 
  Revision 1.15   2003/11/27 11:35:49    
  Revision 1.14   2003/11/25 23:02:17    
  Limited range of test cases so far all pass . 
  Revision 1.13   2003/11/24 22:13:09    
  Revision 1.12   2003/11/17 21:53:31   graham 
  Datatype inference forward chaining updated to allow inconsistent 
  Revision 1.11   2003/11/13 01:13:48    
  Revision 1.10   2003/11/11 21:02:55    
  Revision 1.9   2003/11/07 21:45:47   graham 
  Revision 1.8   2003/11/06 17:58:33   graham 
  About to rework Datatype to better support class - based reasoning . 
  Revision 1.7   2003/10/24 21:05:08    
  Revision 1.6   2003/10/22 15:47:46   graham 
  Revision 1.5   2003/10/09 13:58:59   graham 
  Sync with CVS .   Preparing to eliminate QueryBindingFilter in favour 
  Revision 1.4   2003/10/02 13:41:26    
  Supporting changes for RDF axioms and rules defined as Rulesets , 
  Datatype named using ScopedName rather than QName 
  ( Datatype framework is still work in progress ) . 
  Revision 1.3   2003/09/24 18:50:52   graham 
  Revised module format to be  compatible . 
  Revision 1.1   2003/07/03 20:31:07    
