{- |
Module      :  ./CASL/CompositionTable/ModelFormula.hs
Description :  intermediate calculus formula
Copyright   :  (c) DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

-}

module CASL.CompositionTable.ModelFormula where

import CASL.AS_Basic_CASL
import CASL.Fold

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.List

data Form
  = Quant QUANTIFIER [Int] Form
  | Junct Bool [Form]  -- True for and, False for or
  | Impl Bool Form Form  -- True for => False for <=>
  | Neg Form
  | Const Bool
  | Eq Term Term

data Term
  = Cond Term Form Term
  | Appl Op [Term]
  | Var Int

data Op =
    Comp | Inter | Union
  | Compl | Conv | Shortcut | Inv | Home
  | One | Iden | Zero

getVars :: [VAR_DECL] -> [VAR]
getVars :: [VAR_DECL] -> [VAR]
getVars = (VAR_DECL -> [VAR]) -> [VAR_DECL] -> [VAR]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl vs :: [VAR]
vs _ _) -> [VAR]
vs)

vars :: FORMULA f -> Set.Set VAR
vars :: FORMULA f -> Set VAR
vars = Record f (Set VAR) (Set VAR) -> FORMULA f -> Set VAR
forall f a b. Record f a b -> FORMULA f -> a
foldFormula ((f -> Set VAR)
-> ([Set VAR] -> Set VAR)
-> Set VAR
-> Record f (Set VAR) (Set VAR)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord (Set VAR -> f -> Set VAR
forall a b. a -> b -> a
const Set VAR
forall a. Set a
Set.empty) [Set VAR] -> Set VAR
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set VAR
forall a. Set a
Set.empty)
    { foldQual_var :: TERM f -> VAR -> SORT -> Range -> Set VAR
foldQual_var = \ _ v :: VAR
v _ _ -> VAR -> Set VAR
forall a. a -> Set a
Set.singleton VAR
v
    , foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> Set VAR -> Range -> Set VAR
foldQuantification = \ _ _ vdecl :: [VAR_DECL]
vdecl phiVars :: Set VAR
phiVars _ ->
           Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set VAR
phiVars (Set VAR -> Set VAR) -> Set VAR -> Set VAR
forall a b. (a -> b) -> a -> b
$ [VAR] -> Set VAR
forall a. Ord a => [a] -> Set a
Set.fromList ([VAR] -> Set VAR) -> [VAR] -> Set VAR
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [VAR]
getVars [VAR_DECL]
vdecl
    }

lkup :: Map.Map VAR Int -> VAR -> Int
lkup :: Map VAR Int -> VAR -> Int
lkup = (VAR -> Map VAR Int -> Int) -> Map VAR Int -> VAR -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((VAR -> Map VAR Int -> Int) -> Map VAR Int -> VAR -> Int)
-> (VAR -> Map VAR Int -> Int) -> Map VAR Int -> VAR -> Int
forall a b. (a -> b) -> a -> b
$ Int -> VAR -> Map VAR Int -> Int
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Int
forall a. HasCallStack => [Char] -> a
error "CompositionTable.lkup")

getOp :: String -> Op
getOp :: [Char] -> Op
getOp s :: [Char]
s = let err :: a
err = [Char] -> a
forall a. HasCallStack => [Char] -> a
error "CompositionTable.getOp" in
  case [Char] -> [Char] -> Maybe [Char]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "RA_" [Char]
s of
  Just r :: [Char]
r -> case [Char]
r of
    "composition" -> Op
Comp
    "intersection" -> Op
Inter
    "union" -> Op
Union
    "complement" -> Op
Compl
    "converse" -> Op
Conv
    "shortcut" -> Op
Shortcut
    "inverse" -> Op
Inv
    "homing" -> Op
Home
    "one" -> Op
One
    "identity" -> Op
Iden
    "zero" -> Op
Zero
    _ -> Op
forall a. a
err
  Nothing -> Op
forall a. a
err

fromCASL :: Map.Map OP_SYMB String -> Map.Map VAR Int -> Record f Form Term
fromCASL :: Map OP_SYMB [Char] -> Map VAR Int -> Record f Form Term
fromCASL oM :: Map OP_SYMB [Char]
oM m :: Map VAR Int
m = let err :: a
err = [Char] -> a
forall a. HasCallStack => [Char] -> a
error "CompositionTable.CASLFormula" in Record :: forall f a b.
(FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a)
-> (FORMULA f -> Junctor -> [a] -> Range -> a)
-> (FORMULA f -> a -> Relation -> a -> Range -> a)
-> (FORMULA f -> a -> Range -> a)
-> (FORMULA f -> Bool -> Range -> a)
-> (FORMULA f -> PRED_SYMB -> [b] -> Range -> a)
-> (FORMULA f -> b -> Range -> a)
-> (FORMULA f -> b -> Equality -> b -> Range -> a)
-> (FORMULA f -> b -> SORT -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> SORT -> OP_TYPE -> a -> a)
-> (FORMULA f -> SORT -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> VAR -> SORT -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> VAR -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> f -> b)
-> Record f a b
Record
    { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> Form -> Range -> Form
foldQuantification = \ _ q :: QUANTIFIER
q vs :: [VAR_DECL]
vs f :: Form
f _ ->
        QUANTIFIER -> [Int] -> Form -> Form
Quant QUANTIFIER
q ((VAR -> Int) -> [VAR] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Map VAR Int -> VAR -> Int
lkup Map VAR Int
m) ([VAR] -> [Int]) -> [VAR] -> [Int]
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [VAR]
getVars [VAR_DECL]
vs) Form
f
    , foldJunction :: FORMULA f -> Junctor -> [Form] -> Range -> Form
foldJunction = \ _ k :: Junctor
k as :: [Form]
as _ -> Bool -> [Form] -> Form
Junct (Junctor
k Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
== Junctor
Con) [Form]
as
    , foldRelation :: FORMULA f -> Form -> Relation -> Form -> Range -> Form
foldRelation = \ _ f :: Form
f r :: Relation
r g :: Form
g _ -> Bool -> Form -> Form -> Form
Impl (Relation
r Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence) Form
f Form
g
    , foldNegation :: FORMULA f -> Form -> Range -> Form
foldNegation = \ _ f :: Form
f _ -> Form -> Form
Neg Form
f
    , foldAtom :: FORMULA f -> Bool -> Range -> Form
foldAtom = \ _ b :: Bool
b _ -> Bool -> Form
Const Bool
b
    , foldPredication :: FORMULA f -> PRED_SYMB -> [Term] -> Range -> Form
foldPredication = FORMULA f -> PRED_SYMB -> [Term] -> Range -> Form
forall a. a
err
    , foldDefinedness :: FORMULA f -> Term -> Range -> Form
foldDefinedness = FORMULA f -> Term -> Range -> Form
forall a. a
err
    , foldEquation :: FORMULA f -> Term -> Equality -> Term -> Range -> Form
foldEquation = \ _ t :: Term
t _ s :: Term
s _ -> Term -> Term -> Form
Eq Term
t Term
s
    , foldMembership :: FORMULA f -> Term -> SORT -> Range -> Form
foldMembership = FORMULA f -> Term -> SORT -> Range -> Form
forall a. a
err
    , foldMixfix_formula :: FORMULA f -> Term -> Form
foldMixfix_formula = FORMULA f -> Term -> Form
forall a. a
err
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> Form
foldSort_gen_ax = FORMULA f -> [Constraint] -> Bool -> Form
forall a. a
err
    , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> Form -> Form
foldQuantOp = FORMULA f -> SORT -> OP_TYPE -> Form -> Form
forall a. a
err
    , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> Form -> Form
foldQuantPred = FORMULA f -> SORT -> PRED_TYPE -> Form -> Form
forall a. a
err
    , foldExtFORMULA :: FORMULA f -> f -> Form
foldExtFORMULA = FORMULA f -> f -> Form
forall a. a
err
    , foldQual_var :: TERM f -> VAR -> SORT -> Range -> Term
foldQual_var = \ _ v :: VAR
v _ _ -> Int -> Term
Var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Map VAR Int -> VAR -> Int
lkup Map VAR Int
m VAR
v
    , foldApplication :: TERM f -> OP_SYMB -> [Term] -> Range -> Term
foldApplication = \ _ op :: OP_SYMB
op ts :: [Term]
ts _ ->
        Op -> [Term] -> Term
Appl ([Char] -> Op
getOp ([Char] -> Op) -> [Char] -> Op
forall a b. (a -> b) -> a -> b
$ [Char] -> OP_SYMB -> Map OP_SYMB [Char] -> [Char]
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault "" OP_SYMB
op Map OP_SYMB [Char]
oM) [Term]
ts
    , foldSorted_term :: TERM f -> Term -> SORT -> Range -> Term
foldSorted_term = \ _ t :: Term
t _ _ -> Term
t
    , foldCast :: TERM f -> Term -> SORT -> Range -> Term
foldCast = \ _ t :: Term
t _ _ -> Term
t
    , foldConditional :: TERM f -> Term -> Form -> Term -> Range -> Term
foldConditional = \ _ t :: Term
t f :: Form
f s :: Term
s _ -> Term -> Form -> Term -> Term
Cond Term
t Form
f Term
s
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> Term
foldMixfix_qual_pred = TERM f -> PRED_SYMB -> Term
forall a. a
err
    , foldMixfix_term :: TERM f -> [Term] -> Term
foldMixfix_term = TERM f -> [Term] -> Term
forall a. a
err
    , foldMixfix_token :: TERM f -> VAR -> Term
foldMixfix_token = TERM f -> VAR -> Term
forall a. a
err
    , foldMixfix_sorted_term :: TERM f -> SORT -> Range -> Term
foldMixfix_sorted_term = TERM f -> SORT -> Range -> Term
forall a. a
err
    , foldMixfix_cast :: TERM f -> SORT -> Range -> Term
foldMixfix_cast = TERM f -> SORT -> Range -> Term
forall a. a
err
    , foldMixfix_parenthesized :: TERM f -> [Term] -> Range -> Term
foldMixfix_parenthesized = TERM f -> [Term] -> Range -> Term
forall a. a
err
    , foldMixfix_bracketed :: TERM f -> [Term] -> Range -> Term
foldMixfix_bracketed = TERM f -> [Term] -> Range -> Term
forall a. a
err
    , foldMixfix_braced :: TERM f -> [Term] -> Range -> Term
foldMixfix_braced = TERM f -> [Term] -> Range -> Term
forall a. a
err
    , foldExtTERM :: TERM f -> f -> Term
foldExtTERM = TERM f -> f -> Term
forall a. a
err
    }