{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

{- |

Module : $Header$

Description : logic instance for FPL

Copyright : (c) Christian Maeder, DFKI GmbH 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable

Instance of class Logic for FPL.

-}

module Fpl.Logic_Fpl where

import Logic.Logic

import Fpl.As

import Fpl.Sign

import Fpl.StatAna

import Fpl.Morphism

import Fpl.ATC_Fpl ()

import CASL.Sign

import CASL.Morphism

import CASL.SymbolMapAnalysis

import CASL.AS_Basic_CASL

import CASL.Parse_AS_Basic

import CASL.SimplifySen

import CASL.SymbolParser

import CASL.Taxonomy

import CASL.Logic_CASL ()

import Common.DocUtils

data Fpl = Fpl deriving Show

instance Language Fpl where

description _ = unlines

[ "logic of functional programs (FPL) as CASL extension" ]

instance SignExtension SignExt where

isSubSignExtension = isSubFplSign

instance Syntax Fpl FplBasicSpec SYMB_ITEMS SYMB_MAP_ITEMS where

parse_basic_spec Fpl = Just $ basicSpec fplReservedWords

parse_symb_items Fpl = Just $ symbItems fplReservedWords

parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords

instance Sentences Fpl FplForm FplSign FplMor Symbol where

map_sen Fpl m = return . mapFplSen m

sym_of Fpl = symOf

symmap_of Fpl = morphismToSymbMap

sym_name Fpl = symName

simplify_sen Fpl = simplifySen minFplTerm simplifyTermExt . addBuiltins

print_sign Fpl = printSign pretty

instance StaticAnalysis Fpl FplBasicSpec FplForm

SYMB_ITEMS SYMB_MAP_ITEMS

FplSign

FplMor

Symbol RawSymbol where

basic_analysis Fpl = Just basicFplAnalysis

stat_symb_map_items Fpl _ _ = statSymbMapItems

stat_symb_items Fpl _ = statSymbItems

symbol_to_raw Fpl = symbolToRaw

id_to_raw Fpl = idToRaw

matches Fpl = CASL.Morphism.matches

empty_signature Fpl = emptySign emptyFplSign

signature_union Fpl s = return . addSig addFplSign s

intersection Fpl s = return . interSig interFplSign s

morphism_union Fpl = plainMorphismUnion addFplSign

final_union Fpl = finalUnion addFplSign

is_subsig Fpl = isSubSig isSubFplSign

subsig_inclusion Fpl = sigInclusion emptyMorExt

cogenerated_sign Fpl = cogeneratedSign emptyMorExt

generated_sign Fpl = generatedSign emptyMorExt

induced_from_morphism Fpl = inducedFromMorphism emptyMorExt

induced_from_to_morphism Fpl =

inducedFromToMorphism emptyMorExt isSubFplSign diffFplSign

theory_to_taxonomy Fpl = convTaxo

instance Logic Fpl ()

FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS

FplSign

FplMor

Symbol RawSymbol () where

stability _ = Unstable

empty_proof_tree _ = ()