hets/Fpl/Logic_Fpl.hs

	Logic_Fpl.hs revision 19defe35cc864caeb98dd4ea1d429b1f989ecdff


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
{-# 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
      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 = morphismUnion (const id) 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 _ = ()