-
Notifications
You must be signed in to change notification settings - Fork 2
/
README
80 lines (62 loc) · 3.02 KB
/
README
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
Haskell port of John Harrison's text
Handbook of Practical Logic and Automated Reasoning
http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521899574
--------------------------------------------------------------------------------
Differences
--------------------------------------------------------------------------------
There is one major difference, and a number of minor differences between
this Haskell port and Harrison's original Ocaml code. Harrison makes
heavy use of camlp4 to parse formulas. This includes the syntax p /\ q and
p \/ q for conjunction and disjunction respectively. This is a problem
for Haskell, since neither /\ nor \/ is allowed in a string literal. This
makes parsing Harrison's formulas impossible using Haskell "String"s.
To overcome this difficulty, I use Template Haskell's quotation facilities.
This resembles camlp4 in that formulas can now be parsed at the ghci
command line as
[$fol| p /\ q |] and [$fol| p \/ q |]
similar to the Ocaml
<<p /\ q>> <<p \/ q>>.
'fol' is the name of the quotation parser. Since there is no state
in Haskell, it is not possible to omit the parser name, as it is in ocaml.
(The default parser in camlp4 is a ref cell. and
<<p /\ q>> is shorthand for <:parse_formula<p /\ q>>)
To make quotations easier to parse, I decided to change the
Formula datatype. Harrison uses
> data Formula a = Atom a
> | Top
> | Bot
> | Not Formula
> | And Formula Formula
> | Or Formula Formula
> | Imp Formula Formula
> | Iff Formula Formula
> | All Var Formula
> | Ex Var Formula
He instantiates this with only two types:
> data Prop = P String
> data Fol = R String [Term]
Since the propositional encoding is not adequate, given the
presence of All and Ex, I decided it would do little harm to replace
P "p" with R "p" []. The type we use is
> data Formula = Atom Fol
> | Top
> | Bot
> | Not Formula
> | And Formula Formula
> | Or Formula Formula
> | Imp Formula Formula
> | Iff Formula Formula
> | All Var Formula
> | Ex Var Formula
> deriving(Eq, Ord, Data, Typeable)
This choice has turned out to be a good one. I wanted to be explicit
about types, and thus the type annotations are considerably simpler.
It also obviates the need for many type class annotations, since
Harrison relies upon Ocaml's ordering cheat: (<) : a -> a -> bool.
This is well known to be a bad idea, as it breaks type abstraction.
While in ML it is an understandable compromise between abstraction and
obviating the need to write comparison functions, it is not necessary
in Haskell. We can simply derive Ord and Eq for new types.
Other differences are mostly cosmetic. I prefer a point free style,
and have changed some of the code accordingly, but it is easy to
see the two versions are identical.