/
Syntax.hs
89 lines (65 loc) · 2.79 KB
/
Syntax.hs
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
{-#LANGUAGE FlexibleInstances, MultiParamTypeClasses, GADTs, TypeOperators, PatternSynonyms, RankNTypes, FlexibleContexts, StandaloneDeriving, DeriveGeneric #-}
module Carnap.Languages.PurePropositional.Syntax where
import Carnap.Core.Data.Optics
import Carnap.Core.Data.Classes
import Carnap.Core.Data.Types
import Carnap.Core.Data.Util (checkChildren)
import Carnap.Core.Unification.Unification
import Carnap.Core.Unification.Combination
import Carnap.Core.Unification.FirstOrder
import Carnap.Core.Util
import Carnap.Languages.Util.LanguageClasses
import Control.Lens.Plated (transform, children)
import Control.Applicative
import Control.Lens.Prism
import Data.Typeable (Typeable)
import Carnap.Languages.Util.GenericConstructors
type PureProp = IntProp Bool
instance Evaluable PureProp where
eval (Prop n) = Form $ even n
instance Modelable (Int -> Bool) PureProp where
satisfies f (Prop n) = Form $ f n
type PureConn = BooleanConn Bool
instance Evaluable PureConn where
eval Iff = liftA2 (==)
eval If = \(Form x) y -> if x then y else Form True
eval Or = \(Form x) y -> if x then Form True else y
eval And = \(Form x) y -> if x then y else Form False
--XXX: we avoid liftA2 here, to preserve laziness
eval Not = fmap not
instance Modelable (Int -> Bool) PureConn where
satisfies = const eval
type PureConst = BooleanConst Bool
instance Evaluable PureConst where
eval Verum = Form True
eval Falsum = Form False
instance Modelable (Int -> Bool) PureConst where
satisfies = const eval
type PureSchematicProp = SchematicIntProp Bool
type PurePropositionalContext = PropositionalContext Bool
instance Evaluable PurePropositionalContext where
eval _ = error "don't evaluate schemata!"
instance Modelable (Int -> Bool) PurePropositionalContext where
satisfies = const eval
type PurePropLexicon = Predicate PureProp
:|: Predicate PureSchematicProp
:|: Connective PureConn
:|: SubstitutionalVariable
:|: Connective PurePropositionalContext
:|: Connective PureConst
:|: EndLang
instance BoundVars PurePropLexicon
type PurePropLanguage = FixLang PurePropLexicon
instance CopulaSchema PurePropLanguage
type PureForm = PurePropLanguage (Form Bool)
instance PrismPropLex PurePropLexicon Bool
instance PrismBooleanConnLex PurePropLexicon Bool
instance PrismGenericContext PurePropLexicon Bool Bool
instance PrismBooleanConst PurePropLexicon Bool
instance PrismSchematicProp PurePropLexicon Bool
instance PrismSubstitutionalVariable PurePropLexicon
instance CanonicalForm PureForm
instance Eq (PurePropLanguage a) where
(==) = (=*)
instance UniformlyOrd PurePropLanguage where
phi <=* psi = show phi <= show psi