4865N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

4865N/A{- |

4865N/AModule : $Header$

4865N/ADescription : VSE refinement as comorphism

4865N/ACopyright : (c) M. Codescu, DFKI Bremen 2008

4865N/ALicense : GPLv2 or higher, see LICENSE.txt

4865N/A

4865N/AMaintainer : Mihai.Codescu@dfki.de

4865N/AStability : provisional

4865N/APortability : non-portable (imports Logic.Logic)

4865N/A

4865N/AThe embedding comorphism from CASL to VSE.

4865N/A-}

4865N/A

4865N/Amodule Comorphisms.CASL2VSERefine (CASL2VSERefine (..)) where

4865N/A

4865N/Aimport Logic.Logic

4865N/Aimport Logic.Comorphism

4865N/A

4865N/Aimport CASL.Logic_CASL

4865N/Aimport CASL.Sublogic as SL

4865N/Aimport CASL.Sign

4865N/Aimport CASL.AS_Basic_CASL

4865N/Aimport CASL.Morphism

4865N/A

4865N/Aimport VSE.Logic_VSE

4865N/Aimport VSE.As

4865N/Aimport VSE.Ana

4865N/A

4865N/Aimport Common.AS_Annotation

4865N/Aimport Common.Id

4865N/Aimport Common.ProofTree

4865N/Aimport Common.Result

4865N/Aimport Common.Utils (number)

4865N/Aimport Common.Lib.State

4865N/Aimport qualified Common.Lib.MapSet as MapSet

4865N/A

4865N/Aimport qualified Data.Set as Set

4865N/Aimport qualified Data.Map as Map

4865N/A

4865N/A-- | The identity of the comorphism

4865N/Adata CASL2VSERefine = CASL2VSERefine deriving (Show)

4865N/A

4865N/Ainstance Language CASL2VSERefine -- default definition is okay

4865N/A

4865N/Ainstance Comorphism CASL2VSERefine

4865N/A CASL CASL_Sublogics

4865N/A CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

4865N/A CASLSign

4865N/A CASLMor

4865N/A Symbol RawSymbol ProofTree

4865N/A VSE ()

4865N/A VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS

4865N/A VSESign

4865N/A VSEMor

4865N/A Symbol RawSymbol () where

4865N/A sourceLogic CASL2VSERefine = CASL

4865N/A sourceSublogic CASL2VSERefine = SL.cFol

4865N/A targetLogic CASL2VSERefine = VSE

4865N/A mapSublogic CASL2VSERefine _ = Just ()

4865N/A map_theory CASL2VSERefine = mapCASLTheory

4865N/A map_morphism CASL2VSERefine = return . mapMor

4865N/A map_sentence CASL2VSERefine _ = error "map sen nyi" -- return. mapCASSen

4865N/A map_symbol CASL2VSERefine = error "map symbol nyi"

4865N/A has_model_expansion CASL2VSERefine = True

4865N/A -- check these 3, but should be fine

4865N/A is_weakly_amalgamable CASL2VSERefine = True

4865N/A isInclusionComorphism CASL2VSERefine = False

4865N/A

4865N/AmapCASLTheory :: (CASLSign, [Named CASLFORMULA]) ->

4865N/A Result (VSESign, [Named Sentence])

4865N/AmapCASLTheory (sig, n_sens) =

4865N/A let (tsig, genAx) = mapSig sig

4865N/A tsens = map mapNamedSen n_sens

4865N/A allSens = tsens ++ genAx

4865N/A in if null $ checkCases tsig allSens then return (tsig, allSens) else

4865N/A fail "case error in signature"

4865N/A

4865N/AmapSig :: CASLSign -> (VSESign, [Named Sentence])

4865N/AmapSig sign =

4865N/A let wrapSort (procsym, axs) s = let

4865N/A restrName = gnRestrName s

4865N/A eqName = gnEqName s

4865N/A sProcs = [(restrName, Profile [Procparam In s] Nothing),

4865N/A (eqName,

4865N/A Profile [Procparam In s, Procparam In s]

4865N/A (Just uBoolean))]

4865N/A varx = Qual_var (genToken "x") s nullRange

4865N/A vary = Qual_var (genToken "y") s nullRange

4865N/A varz = Qual_var (genToken "z") s nullRange

4865N/A varb = Qual_var (genToken "b")

4865N/A uBoolean nullRange

4865N/A varb1 = Qual_var (genToken "b1")

4865N/A uBoolean nullRange

4865N/A varb2 = Qual_var (genToken "b2")

4865N/A uBoolean nullRange

4865N/A sSens = [ makeNamed ("ga_termination_eq_" ++ show s) $

4865N/A Quantification Universal [Var_decl [genToken "x",

4865N/A genToken "y"] s nullRange

4865N/A , Var_decl [genToken "b"]

4865N/A uBoolean nullRange]

4865N/A (mkImpl

4865N/A (conjunct [

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange) nullRange)

4865N/A [varx] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange) nullRange)

4865N/A [vary] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange

4865N/A ])

4865N/A (ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [varx, vary] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange)

4865N/A ) nullRange ,

4865N/A makeNamed ("ga_refl_eq_" ++ show s) $

4865N/A Quantification Universal [Var_decl [genToken "x"] s nullRange

4865N/A , Var_decl [genToken "b"]

4865N/A uBoolean nullRange]

4865N/A (mkImpl

4865N/A (ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange ) nullRange)

4865N/A [varx] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange)

4865N/A

4865N/A (ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [varx, varx] nullRange))

4865N/A nullRange)

4865N/A (mkStEq

4865N/A varb

4865N/A (Application (Qual_op_name uTrue

4865N/A (Op_type Total []

4865N/A uBoolean

4865N/A nullRange) nullRange)

4865N/A [] nullRange)

4865N/A )) nullRange)

4865N/A ) nullRange

4865N/A , makeNamed ("ga_sym_eq_" ++ show s) $

4865N/A Quantification Universal [Var_decl [genToken "x",

4865N/A genToken "y"] s nullRange

4865N/A , Var_decl [genToken "b1",

4865N/A genToken "b2"]

4865N/A uBoolean nullRange]

4865N/A (mkImpl

4865N/A (conjunct [

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange) nullRange)

4865N/A [varx] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange) nullRange)

4865N/A [vary] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b1")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [varx, vary] nullRange))

4865N/A nullRange)

4865N/A (mkStEq varb1 aTrue)

4865N/A ) nullRange

4865N/A ])

4865N/A (ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b2")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [vary, varx] nullRange))

4865N/A nullRange)

4865N/A (mkStEq varb2 aTrue)

4865N/A ) nullRange)

4865N/A ) nullRange

4865N/A , makeNamed ("ga_trans_eq_" ++ show s) $

4865N/A Quantification Universal [Var_decl [genToken "x",

4865N/A genToken "y",

4865N/A genToken "z"] s nullRange

4865N/A , Var_decl [genToken "b1",

4865N/A genToken "b2",

4865N/A genToken "b"]

4865N/A uBoolean nullRange]

4865N/A (mkImpl

4865N/A (conjunct [

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange) nullRange)

4865N/A [varx] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange ) nullRange)

4865N/A [vary] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Call

4865N/A (Predication (Qual_pred_name restrName

4865N/A (Pred_type [s] nullRange ) nullRange)

4865N/A [varz] nullRange))

4865N/A nullRange)

4865N/A trueForm ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b1")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [varx, vary] nullRange))

4865N/A nullRange)

4865N/A (mkStEq varb1 aTrue)

4865N/A ) nullRange,

4865N/A ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b2")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [vary, varz] nullRange))

4865N/A nullRange)

4865N/A (mkStEq varb2 aTrue)

4865N/A ) nullRange

4865N/A ])

4865N/A (ExtFORMULA $ Ranged

4865N/A (Dlformula Diamond

4865N/A (Ranged

4865N/A (Assign (genToken "b")

4865N/A (Application

4865N/A (Qual_op_name

4865N/A (gnEqName s)

4865N/A (Op_type Partial [s, s] uBoolean nullRange)

4865N/A nullRange)

4865N/A [varx, varz] nullRange))

4865N/A nullRange)

4865N/A (mkStEq varb aTrue)

4865N/A ) nullRange)

4865N/A ) nullRange ]

4865N/A in

4865N/A (sProcs ++ procsym, sSens ++ axs)

(sortProcs, sortSens) = foldl wrapSort ([], []) $

Set.toList $ sortSet sign

wrapOp (procsym, axs) (i, opTypes) = let

funName = mkGenName i

fProcs = map (\ profile ->

(funName,

Profile

(map (Procparam In) $ opArgs profile)

(Just $ opRes profile))) opTypes

opTypeSens (OpType _ w s) = let

xtokens = map (\ (_, ii) -> genNumVar "x" ii) $

number w

xvars = map (

\ (si, ii) ->

Qual_var (genNumVar "x" ii )

si nullRange ) $

number w

yvars = map (

\ (si, ii) ->

Qual_var (genNumVar "y" ii )

si nullRange ) $

number w

ytokens = map (\ (_, ii) -> genNumVar "y" ii) $

number w

btokens = map (\ (_, ii) -> genNumVar "b" ii) $

number w

xtoken = genToken "x"

ytoken = genToken "y"

btoken = genToken "b"

xvar = Qual_var (genToken "x")

s nullRange

yvar = Qual_var (genToken "y")

s nullRange

bvar = Qual_var (genToken "b")

uBoolean nullRange

congrF = [makeNamed "" $

Quantification Universal ([Var_decl [xtoken, ytoken] s

nullRange

, Var_decl (btoken : btokens)

uBoolean nullRange

] ++ map

(\ ((t1, t2), si) ->

Var_decl [t1, t2] si

nullRange)

(zip (zip xtokens ytokens) w)

)

(mkImpl

(conjunct

(concatMap (\ (si, ii) -> let

xv = Qual_var (genNumVar "x" ii)

si nullRange

yv = Qual_var (genNumVar "y" ii)

si nullRange

varbi = genNumVar "b" ii

bi1 = Qual_var (genNumVar "b" ii)

uBoolean nullRange

in

[ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type [si] nullRange) nullRange )

[xv] nullRange))

nullRange)

trueForm ) nullRange ,

ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type [si] nullRange) nullRange)

[yv] nullRange))

nullRange)

trueForm ) nullRange ,

ExtFORMULA $ mkRanged $ Dlformula Diamond

(Ranged

(Assign varbi

(Application

(Qual_op_name

(gnEqName si)

(Op_type Partial [si, si] uBoolean nullRange)

nullRange)

[xv, yv] nullRange))

nullRange)

(mkStEq bi1 aTrue)

] ) $

number w )

) -- hypothesis

(ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged

(Assign (genToken "x")

(Application

(Qual_op_name

(mkGenName i)

(Op_type Partial w s nullRange)

nullRange)

xvars nullRange))

nullRange)

(ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged

(Assign (genToken "y")

(Application

(Qual_op_name

(mkGenName i)

(Op_type Partial w s nullRange)

nullRange)

yvars nullRange))

nullRange)

(ExtFORMULA $

Ranged (

Dlformula Diamond

( Ranged

(Assign (genToken "b")

(Application

(Qual_op_name

(gnEqName s)

(Op_type Partial [s, s] uBoolean nullRange)

nullRange)

[xvar, yvar] nullRange))

nullRange

)

(mkStEq bvar aTrue)

) nullRange)

) nullRange)

) nullRange) -- conclusion

)

nullRange

]

termF = if not $ null w then

[ makeNamed "" $ Quantification Universal

(Var_decl [xtoken] s nullRange

: map (\ (t1, si) -> Var_decl [t1] si nullRange)

(zip xtokens w))

(mkImpl

(conjunct

(concatMap (\ (si, ii) -> let

xv = Qual_var (genNumVar "x" ii) si nullRange in

[ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type (w ++ [s]) nullRange) nullRange)

[xv] nullRange))

nullRange)

trueForm ) nullRange

] ) $

number w )

)

(ExtFORMULA $ Ranged

(

Dlformula Diamond

(Ranged

(Assign (genToken "x")

(Application

(Qual_op_name

(mkGenName i)

(Op_type Partial w s nullRange)

nullRange)

xvars nullRange))

nullRange)

(ExtFORMULA $

Ranged

(Dlformula Diamond (Ranged

(Call (Predication (Qual_pred_name

(gnRestrName s)

(Pred_type [s] nullRange) nullRange)

[xvar] nullRange))

nullRange)

trueForm

)

nullRange)

) nullRange)

)

nullRange

]

else

[makeNamed "" $ Quantification Universal

[Var_decl [xtoken] s nullRange]

(ExtFORMULA $ Ranged

(

Dlformula Diamond

(Ranged

(Assign (genToken "x")

(Application

(Qual_op_name

(mkGenName i)

(Op_type Partial [] s nullRange)

nullRange)

[] nullRange))

nullRange)

(ExtFORMULA $

Ranged

(Dlformula Diamond (Ranged

(Call (Predication (Qual_pred_name

(gnRestrName s)

(Pred_type [s] nullRange) nullRange)

[xvar] nullRange))

nullRange)

trueForm

)

nullRange)

) nullRange) nullRange]

in

if null w then termF else congrF ++ termF

fSens = concatMap opTypeSens opTypes

in

(procsym ++ fProcs, axs ++ fSens)

(opProcs, opSens) = foldl wrapOp ([], []) $

MapSet.toList $ opMap sign

wrapPred (procsym, axs) (i, predTypes) = let

procName = mkGenName i

pProcs = map (\ profile -> (procName,

Profile

(map (Procparam In) $ predArgs profile)

(Just uBoolean))) predTypes

predTypeSens (PredType w) = let

xtokens = map (\ (_, ii) -> genNumVar "x" ii) $

number w

xvars = map (

\ (si, ii) ->

Qual_var (genNumVar "x" ii )

si nullRange ) $

number w

ytokens = map (\ (_, ii) -> genNumVar "y" ii) $

number w

btokens = map (\ (_, ii) -> genNumVar "b" ii) $

number w

btoken = genToken "b"

r1 = genToken "r1"

r2 = genToken "r2"

rvar1 = Qual_var (genToken "r1")

uBoolean nullRange

rvar2 = Qual_var (genToken "r2")

uBoolean nullRange

congrP = [makeNamed "" $ Quantification Universal

(Var_decl (btoken : r1 : r2 : btokens) uBoolean nullRange

: map (\ ((t1, t2), si) -> Var_decl [t1, t2] si nullRange)

(zip (zip xtokens ytokens) w))

(mkImpl

(conjunct

(concatMap (\ (si, ii) -> let

xv = Qual_var (genNumVar "x" ii)

si nullRange

yv = Qual_var (genNumVar "y" ii)

si nullRange

bi1 = Qual_var (genNumVar "b" ii)

uBoolean nullRange

in

[ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type [si] nullRange) nullRange)

[xv] nullRange))

nullRange)

trueForm ) nullRange ,

ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type [si] nullRange) nullRange)

[yv] nullRange))

nullRange)

trueForm ) nullRange ,

ExtFORMULA $ mkRanged $ Dlformula Diamond

(Ranged

(Assign (genNumVar "b" ii)

(Application

(Qual_op_name

(gnEqName si)

(Op_type Partial [si, si] uBoolean nullRange)

nullRange)

[xv, yv] nullRange))

nullRange)

(mkStEq

bi1 aTrue)

] ) $

number w )

) -- hypothesis

(ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged (Call (Predication

(Qual_pred_name (mkGenName i)

(Pred_type (w ++ [uBoolean]) nullRange)

nullRange)

(map (

\ (si, ii) ->

Qual_var (genNumVar "x" ii )

si nullRange )

(number w) ++ [rvar1]) nullRange)) nullRange)

(ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged (Call (Predication

(Qual_pred_name (mkGenName i)

(Pred_type (w ++ [uBoolean]) nullRange)

nullRange)

(map (

\ (si, ii) ->

Qual_var (genNumVar "y" ii )

si nullRange )

(number w) ++ [rvar2]) nullRange)) nullRange)

(mkStEq

rvar1

rvar2

)

) nullRange)

) nullRange) -- conclusion

)

nullRange

]

termP = [ makeNamed "" $ Quantification Universal

(map

(\ (t1, si) ->

Var_decl [t1] si

nullRange)

(zip xtokens w)

++ [Var_decl [r1]

uBoolean nullRange])

(mkImpl

(conjunct

(concatMap (\ (si, ii) -> let

xv = Qual_var (genNumVar "x" ii)

si nullRange

in

[ExtFORMULA $ Ranged ( Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName si)

(Pred_type [si] nullRange) nullRange)

[xv] nullRange))

nullRange)

trueForm ) nullRange

] ) $

number w )

)

(ExtFORMULA $ Ranged

(

Dlformula Diamond

(Ranged

(Call (Predication (Qual_pred_name (mkGenName i)

(Pred_type (w ++ [uBoolean]) nullRange)

nullRange)

(xvars ++ [rvar1])

nullRange))

nullRange)

trueForm

) nullRange)

)

nullRange

]

in congrP ++ termP

pSens = concatMap predTypeSens predTypes

in

(procsym ++ pProcs, axs ++ pSens)

(predProcs, predSens) = foldl wrapPred ([], []) $

MapSet.toList $ predMap sign

procs = Procs $ Map.fromList (sortProcs ++ opProcs ++ predProcs)

newPreds = procsToPredMap procs

newOps = procsToOpMap procs

in (sign { opMap = newOps,

predMap = newPreds,

extendedInfo = procs,

sentences = [] }, sortSens ++ opSens ++ predSens)

mapNamedSen :: Named CASLFORMULA -> Named Sentence

mapNamedSen n_sen = let

sen = sentence n_sen

trans = mapCASLSen sen

in

n_sen {sentence = trans}

mapMor :: CASLMor -> VSEMor

mapMor m = let

(om, pm) = vseMorExt m

in m

{ msource = fst $ mapSig $ msource m

, mtarget = fst $ mapSig $ mtarget m

, op_map = om

, pred_map = pm

, extended_map = emptyMorExt

}

mapCASLSen :: CASLFORMULA -> Sentence

mapCASLSen f = let

(sen, (_i, vars)) = runState (mapCASLSenAux f) (0, Set.empty)

in

case f of

Sort_gen_ax _ _ -> sen

_ -> addQuantifiers vars sen

addQuantifiers :: VarSet -> Sentence -> Sentence

addQuantifiers vars sen =

Quantification Universal

(map (\ (v, s) -> Var_decl [v] s nullRange) $ Set.toList vars) sen nullRange

mapCASLSenAux :: CASLFORMULA -> State (Int, VarSet) Sentence

mapCASLSenAux f = case f of

Sort_gen_ax constrs isFree -> do

let

(genSorts, _, _ ) = recover_Sort_gen_ax constrs

toProcs (Op_name _, _) = error "must be qual names"

toProcs (Qual_op_name op (Op_type _fkind args res _range) _, l) =

( Qual_op_name (mkGenName op)

(Op_type Partial args res nullRange) nullRange,

l)

opsToProcs (Constraint nSort syms oSort) =

Constraint nSort (map toProcs syms) oSort

return $ ExtFORMULA $ Ranged

(RestrictedConstraint

(map opsToProcs constrs)

(Map.fromList $ map (\ s -> (s, gnRestrName s)) genSorts)

isFree)

nullRange

Atom b _ps -> return $ boolForm b

Equation t1 Strong t2 _ps -> do

let sort1 = sortOfTerm t1

n1 <- freshIndex sort1 -- (typeof t1)

prg1 <- mapCASLTerm n1 t1

n2 <- freshIndex sort1 -- (typeof t2)

prg2 <- mapCASLTerm n2 t2

n <- freshIndex uBoolean

return $ ExtFORMULA $ Ranged

(Dlformula Diamond

(Ranged

(Seq (Ranged (Seq prg1 prg2) nullRange)

(Ranged

(Assign

(genNumVar "x" n)

(Application

(Qual_op_name

(gnEqName sort1)

(Op_type Partial [sort1, sort1] uBoolean nullRange)

nullRange)

[Qual_var (genNumVar "x" n1) sort1 nullRange,

Qual_var (genNumVar "x" n2) sort1 nullRange]

nullRange

)

) nullRange)

)

nullRange)

(mkStEq (Qual_var (genNumVar "x" n) uBoolean nullRange)

aTrue)

)

nullRange

{- here i have to return smth like

-- <: xn1 := prg1;

-- xn2 := prg2;

-- xn := gn_eq_s(xn1,xn2) :> xn = True " -}

Predication pn as _qs -> do

indexes <- mapM (freshIndex . sortOfTerm) as

prgs <- mapM (\ (ti, i) -> mapCASLTerm i ti) $ zip as indexes

let xvars = map (\ (ti, i) ->

Qual_var (genNumVar "x" i)

(sortOfTerm ti) nullRange ) $ zip as indexes

n <- freshIndex uBoolean

let asgn = if not $ null prgs then

foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) prgs

else Ranged Skip nullRange

case pn of

Pred_name _ -> fail "must be qualified"

Qual_pred_name pname (Pred_type ptype _) _ -> return $ ExtFORMULA $ Ranged

(Dlformula Diamond

(Ranged

(Seq

asgn

(Ranged (Assign (genNumVar "x" n)

(Application

(Qual_op_name

(mkGenName pname)

(Op_type Partial ptype uBoolean nullRange) nullRange)

xvars nullRange))

nullRange))

nullRange)

(mkStEq

(Qual_var (genNumVar "x" n) uBoolean nullRange)

aTrue))

nullRange

{- <: xi := prgi;

x:= gn_p(x1,..,xn):> x = True -}

Junction j fs _r -> do

mapFs <- mapM mapCASLSenAux fs

return $ Junction j mapFs nullRange

Relation f1 c f2 _r -> do

trf1 <- mapCASLSenAux f1

trf2 <- mapCASLSenAux f2

return $ Relation trf1 c trf2 nullRange

Negation f1 _r -> do

trf <- mapCASLSenAux f1

return $ mkNeg trf

Quantification q vars sen _ ->

case q of

Universal -> do

trSen <- mapCASLSenAux sen

let h = map (\ (Var_decl varS s _) -> let

restrs = map (\ v -> ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName s)

(Pred_type [s] nullRange)

nullRange

)

[Qual_var v s nullRange]

nullRange

)

)

nullRange)

trueForm) nullRange)

varS

in

conjunct restrs)

vars

let sen' = mkImpl

(foldr1 (\ sen1 sen2 -> conjunct [sen1, sen2]) h)

trSen

return $ Quantification q vars sen' nullRange

Existential -> do

trSen <- mapCASLSenAux sen

let h = map (\ (Var_decl varS s _) -> let

restrs = map (\ v -> ExtFORMULA $ Ranged (

Dlformula Diamond

(Ranged

(Call

(Predication

(Qual_pred_name

(gnRestrName s)

(Pred_type [s] nullRange)

nullRange

)

[Qual_var v s nullRange]

nullRange

)

)

nullRange)

trueForm) nullRange)

varS

in

conjunct restrs)

vars

let sen' = conjunct

[foldr1 (\ sen1 sen2 -> conjunct [sen1, sen2]) h,

trSen]

return $ Quantification q vars sen' nullRange

Unique_existential -> fail "nyi Unique_existential"

_ -> fail "Comorphisms.CASL2VSERefine.mapCASLSenAux"

mapCASLTerm :: Int -> TERM () -> State (Int, VarSet) Program

mapCASLTerm n t = case t of

Qual_var v s _ps -> return $

Ranged (Assign (genNumVar "x" n)

(Qual_var v s nullRange)) nullRange

Application opsym as _qs -> do

indexes <- mapM (freshIndex . sortOfTerm) as

let xvars = map (\ (ti, i) ->

Qual_var (genNumVar "x" i)

(sortOfTerm ti) nullRange ) $ zip as indexes

prgs <- mapM (\ (ti, i) -> mapCASLTerm i ti) $ zip as indexes

let asgn = if not $ null prgs then

foldr1 (\ p1 p2 -> Ranged (Seq p1 p2) nullRange) prgs

else Ranged Skip nullRange

case opsym of

Op_name _ -> fail "must be qualified"

Qual_op_name oName (Op_type _ args res _) _ ->

case args of

[] -> return $ Ranged (Assign (genNumVar "x" n)

(Application

(Qual_op_name

(mkGenName oName)

(Op_type Partial args res nullRange)

nullRange

)

xvars nullRange))

nullRange

_ -> return $ Ranged

(Seq

asgn

(Ranged (Assign (genNumVar "x" n)

(Application

(Qual_op_name

(mkGenName oName)

(Op_type Partial args res nullRange)

nullRange

)

xvars nullRange))

nullRange))

nullRange

_ -> fail "nyi term"

freshIndex :: SORT -> State (Int, VarSet) Int

freshIndex ss = do

(i, s) <- get

let v = genNumVar "x" i

put (i + 1, Set.insert (v, ss) s)

return i