9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews{- |

8e13601a1bfa6d6c71e055eb557c77e78419271aTinderbox UserModule : $Header$

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsDescription : instance of the class Logic for ConstraintCASL

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark AndrewsCopyright : (c) Uni Bremen 2002-2007

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark AndrewsLicense : GPLv2 or higher, see LICENSE.txt

0c27b3fe77ac1d5094ba3521e8142d9e7973133fMark Andrews

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark AndrewsMaintainer : till@informatik.uni-bremen.de

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark AndrewsStability : provisional

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark AndrewsPortability : portable

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark AndrewsHere is the place where the class Logic is instantiated for CASL.

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews Also the instances for Syntax an Category.

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews-}

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrewsmodule ConstraintCASL.Logic_ConstraintCASL where

b1c6de5456a5287b442de5620282902da39a4968Mark Andrews

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrewsimport Common.AS_Annotation

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrewsimport Common.Parsec((<<))

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrewsimport Text.ParserCombinators.Parsec

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrewsimport Logic.Logic

9198ab377b1cbf07d6d0c6eec25296c135bd66bdMark Andrews

b1c6de5456a5287b442de5620282902da39a4968Mark Andrewsimport ConstraintCASL.AS_ConstraintCASL

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport ConstraintCASL.Formula

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport ConstraintCASL.StaticAna

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport ConstraintCASL.ATC_ConstraintCASL()

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport ConstraintCASL.Print_AS()

24ef32426d91c5140d75031b6443397c6d24006cMark Andrews

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.AS_Basic_CASL

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.Parse_AS_Basic

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.ToDoc()

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.SymbolParser

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.MapSentence

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.ATC_CASL()

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.Sublogic

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.Sign

24ef32426d91c5140d75031b6443397c6d24006cMark Andrewsimport CASL.Morphism

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Huntimport CASL.SymbolMapAnalysis

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Huntimport CASL.Logic_CASL

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Hunt

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Huntdata ConstraintCASL = ConstraintCASL deriving Show

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Hunt

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Huntinstance Language ConstraintCASL where

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Hunt description _ =

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Hunt "ConstraintCASL - a restriction of CASL to constraint\

f30785f506a522ed6a5e394af2bb13b6f883927eEvan Hunt \formulas over predicates"

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Huntinstance Syntax ConstraintCASL ConstraintCASLBasicSpec

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt SYMB_ITEMS SYMB_MAP_ITEMS

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt where

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt parse_basic_spec ConstraintCASL = Just $ basicSpec constraintKeywords

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt parse_symb_items ConstraintCASL = Just $ symbItems []

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt parse_symb_map_items ConstraintCASL = Just $ symbMapItems []

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt

9a020198893d8389f1f3172d88ba6b16d7da3c04Evan Hunt-- lattices (for sublogics) is missing

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrewsinstance Sentences ConstraintCASL ConstraintCASLFORMULA

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews ConstraintCASLSign ConstraintCASLMor Symbol where

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews map_sen ConstraintCASL m = return . mapSen (const id) m

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews parse_sentence ConstraintCASL = Just (fmap item (aFormula [] << eof))

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews sym_of ConstraintCASL = symOf

1864400107f7dc21e1797d602ab1f8523f599df9Mark Andrews symmap_of ConstraintCASL = morphismToSymbMap

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt sym_name ConstraintCASL = symName

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrews simplify_sen ConstraintCASL =

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrews error "simplify_sen ConstraintCASL nyi"

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrews

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrewsinstance StaticAnalysis ConstraintCASL

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrews ConstraintCASLBasicSpec ConstraintCASLFORMULA

d1e22676de16e6dee54c58b27cca11c5fb8f1ff5Mark Andrews SYMB_ITEMS SYMB_MAP_ITEMS

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn ConstraintCASLSign

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn ConstraintCASLMor

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn Symbol RawSymbol where

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn basic_analysis ConstraintCASL = Just basicConstraintCASLAnalysis

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn stat_symb_map_items ConstraintCASL = statSymbMapItems

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn stat_symb_items ConstraintCASL = statSymbItems

8009525601d946805fae58b037cf7dad0da516f8Curtis Blackburn

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews symbol_to_raw ConstraintCASL = symbolToRaw

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews id_to_raw ConstraintCASL = idToRaw

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews matches ConstraintCASL = CASL.Morphism.matches

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews is_transportable ConstraintCASL = isSortInjective

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews empty_signature ConstraintCASL = emptySign ()

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews signature_union ConstraintCASL s = return . addSig const s

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews morphism_union ConstraintCASL = morphismUnion (const id) const

0d6328ce5f6b799f8e7c6cbbb3b965cf29bfb7baMark Andrews final_union ConstraintCASL = finalUnion const

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews is_subsig ConstraintCASL = isSubSig trueC

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews subsig_inclusion ConstraintCASL = sigInclusion ()

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews cogenerated_sign ConstraintCASL = cogeneratedSign ()

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews generated_sign ConstraintCASL = generatedSign ()

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews induced_from_morphism ConstraintCASL = inducedFromMorphism ()

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews induced_from_to_morphism ConstraintCASL =

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews inducedFromToMorphism () trueC const

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews theory_to_taxonomy ConstraintCASL =

bf459d24a117ae2c54c37016430b41cd6d73491cMark Andrews error "theory_to_taxonomy ConstraintCASL nyi" -- convTaxo

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Huntinstance MinSL () ConstraintFORMULA where

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt minSL _ = bottom

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Huntinstance ProjForm () ConstraintFORMULA where

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt projForm _ = Just . ExtFORMULA

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Huntinstance Logic ConstraintCASL CASL_Sublogics

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt ConstraintCASLBasicSpec ConstraintCASLFORMULA

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt SYMB_ITEMS SYMB_MAP_ITEMS

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt ConstraintCASLSign

927e4c9fecf448bf3894c68fcaf9dc2f89557f3aEvan Hunt ConstraintCASLMor

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews Symbol RawSymbol () where

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews stability _ = Experimental

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews proj_sublogic_epsilon ConstraintCASL = pr_epsilon ()

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews all_sublogics _ = sublogics_all [()]

12bf5d4796505b4c20680531da96a31e6c2c1144Evan Hunt empty_proof_tree _ = ()

0c91911b4d1e872b87eaf6431ed47fe24d18dd43Mark Andrews