Skip to content

Commit 5c738c6

Browse files
gilithgilith
committed
Basic syntax and printing in TPTP format
1 parent 4c49aa4 commit 5c738c6

File tree

6 files changed

+530
-0
lines changed

6 files changed

+530
-0
lines changed

‎hol.cabal

+7
Original file line numberDiff line numberDiff line change
@@ -41,11 +41,13 @@ Library
4141
HOL.Rule
4242
HOL.Sequent
4343
HOL.Subst
44+
HOL.Syntax
4445
HOL.Term
4546
HOL.TermAlpha
4647
HOL.TermData
4748
HOL.Theory
4849
HOL.Thm
50+
HOL.Tptp
4951
HOL.Type
5052
HOL.TypeData
5153
HOL.TypeOp
@@ -83,11 +85,13 @@ executable hol-pkg
8385
HOL.Rule
8486
HOL.Sequent
8587
HOL.Subst
88+
HOL.Syntax
8689
HOL.Term
8790
HOL.TermAlpha
8891
HOL.TermData
8992
HOL.Theory
9093
HOL.Thm
94+
HOL.Tptp
9195
HOL.Type
9296
HOL.TypeData
9397
HOL.TypeOp
@@ -127,11 +131,13 @@ test-suite hol-test
127131
HOL.Rule
128132
HOL.Sequent
129133
HOL.Subst
134+
HOL.Syntax
130135
HOL.Term
131136
HOL.TermAlpha
132137
HOL.TermData
133138
HOL.Theory
134139
HOL.Thm
140+
HOL.Tptp
135141
HOL.Type
136142
HOL.TypeData
137143
HOL.TypeOp
@@ -178,6 +184,7 @@ benchmark hol-profile
178184
HOL.TermData
179185
HOL.Theory
180186
HOL.Thm
187+
HOL.Tptp
181188
HOL.Type
182189
HOL.TypeData
183190
HOL.TypeOp

‎src/HOL/Const.hs

+6
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,9 @@ existsName = Name boolNamespace "?"
104104
existsUniqueName :: Name
105105
existsUniqueName = Name boolNamespace "?!"
106106

107+
falseName :: Name
108+
falseName = Name boolNamespace "F"
109+
107110
forallName :: Name
108111
forallName = Name boolNamespace "!"
109112

@@ -113,6 +116,9 @@ impName = Name boolNamespace "==>"
113116
negName :: Name
114117
negName = Name boolNamespace "~"
115118

119+
trueName :: Name
120+
trueName = Name boolNamespace "T"
121+
116122
-- Lists
117123

118124
appendName :: Name

‎src/HOL/Sequent.hs

+1
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import qualified Data.Foldable as Foldable
1515
import Data.Maybe (isNothing,fromMaybe)
1616
import Data.Set (Set)
1717
import qualified Data.Set as Set
18+
1819
import qualified HOL.Const as Const
1920
import qualified HOL.Subst as Subst
2021
import HOL.TermAlpha (TermAlpha)

‎src/HOL/Syntax.hs

+165
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
{- |
2+
module: $Header$
3+
description: Higher order logic syntax
4+
license: MIT
5+
6+
maintainer: Joe Leslie-Hurd <[email protected]>
7+
stability: provisional
8+
portability: portable
9+
-}
10+
11+
module HOL.Syntax
12+
where
13+
14+
import qualified HOL.Const as Const
15+
import HOL.Data (Const,Term,Type,Var)
16+
--import HOL.Name (Name)
17+
--import qualified HOL.Name as Name
18+
--import HOL.Print (toString)
19+
--import HOL.Term (renameFresh)
20+
import qualified HOL.Term as Term
21+
import HOL.Theory (Theory)
22+
import qualified HOL.Theory as Theory
23+
import qualified HOL.Type as Type
24+
--import qualified HOL.TypeOp as TypeOp
25+
import HOL.Util (mkUnsafe1,mkUnsafe2,mkUnsafe3)
26+
import qualified HOL.Var as Var
27+
28+
-------------------------------------------------------------------------------
29+
-- Types
30+
-------------------------------------------------------------------------------
31+
32+
mkUnaryType :: Type -> Type
33+
mkUnaryType a = Type.mkFun a a
34+
35+
mkBinaryType :: Type -> Type
36+
mkBinaryType a = Type.mkFun a (mkUnaryType a)
37+
38+
-------------------------------------------------------------------------------
39+
-- Constants
40+
-------------------------------------------------------------------------------
41+
42+
existsConst :: Theory -> Maybe Const
43+
existsConst thy = Theory.lookupConst thy Const.existsName
44+
45+
forallConst :: Theory -> Maybe Const
46+
forallConst thy = Theory.lookupConst thy Const.forallName
47+
48+
-------------------------------------------------------------------------------
49+
-- Booleans
50+
-------------------------------------------------------------------------------
51+
52+
-- Types
53+
54+
mkQuantType :: Type -> Type
55+
mkQuantType a = Type.mkFun (Type.mkFun a Type.bool) Type.bool
56+
57+
-- Truth
58+
59+
trueConst :: Theory -> Maybe Const
60+
trueConst thy = Theory.lookupConst thy Const.trueName
61+
62+
trueTerm :: Theory -> Maybe Term
63+
trueTerm thy = do
64+
c <- trueConst thy
65+
return $ Term.mkConst c Type.bool
66+
67+
trueTermUnsafe :: Theory -> Term
68+
trueTermUnsafe = mkUnsafe1 "HOL.Syntax.trueTerm" trueTerm
69+
70+
-- Falsity
71+
72+
falseConst :: Theory -> Maybe Const
73+
falseConst thy = Theory.lookupConst thy Const.falseName
74+
75+
falseTerm :: Theory -> Maybe Term
76+
falseTerm thy = do
77+
c <- falseConst thy
78+
return $ Term.mkConst c Type.bool
79+
80+
falseTermUnsafe :: Theory -> Term
81+
falseTermUnsafe = mkUnsafe1 "HOL.Syntax.falseTerm" falseTerm
82+
83+
-- Negation
84+
85+
negConst :: Theory -> Maybe Const
86+
negConst thy = Theory.lookupConst thy Const.negName
87+
88+
negTerm :: Theory -> Maybe Term
89+
negTerm thy = do
90+
c <- negConst thy
91+
return $ Term.mkConst c (mkUnaryType Type.bool)
92+
93+
mkNegTerm :: Theory -> Term -> Maybe Term
94+
mkNegTerm thy t = do
95+
c <- negTerm thy
96+
Term.mkApp c t
97+
98+
mkNegTermUnsafe :: Theory -> Term -> Term
99+
mkNegTermUnsafe = mkUnsafe2 "HOL.Syntax.mkNegTerm" mkNegTerm
100+
101+
-- Implication
102+
103+
impConst :: Theory -> Maybe Const
104+
impConst thy = Theory.lookupConst thy Const.impName
105+
106+
impTerm :: Theory -> Maybe Term
107+
impTerm thy = do
108+
c <- impConst thy
109+
return $ Term.mkConst c (mkBinaryType Type.bool)
110+
111+
mkImpTerm :: Theory -> Term -> Term -> Maybe Term
112+
mkImpTerm thy t u = do
113+
c <- impTerm thy
114+
Term.listMkApp c [t,u]
115+
116+
mkImpTermUnsafe :: Theory -> Term -> Term -> Term
117+
mkImpTermUnsafe = mkUnsafe3 "HOL.Syntax.mkImpTerm" mkImpTerm
118+
119+
-- Existential quantification
120+
121+
existsTerm :: Theory -> Type -> Maybe Term
122+
existsTerm thy a = do
123+
c <- existsConst thy
124+
return $ Term.mkConst c (mkQuantType a)
125+
126+
mkExistsTerm :: Theory -> Var -> Term -> Maybe Term
127+
mkExistsTerm thy v t = do
128+
q <- existsTerm thy (Var.typeOf v)
129+
Term.mkApp q (Term.mkAbs v t)
130+
131+
mkExistsTermUnsafe :: Theory -> Var -> Term -> Term
132+
mkExistsTermUnsafe = mkUnsafe3 "HOL.Syntax.mkExistsTerm" mkExistsTerm
133+
134+
listMkExistsTerm :: Theory -> [Var] -> Term -> Maybe Term
135+
listMkExistsTerm _ [] t = return t
136+
listMkExistsTerm thy (v : vs) t = do
137+
u <- listMkExistsTerm thy vs t
138+
mkExistsTerm thy v u
139+
140+
listMkExistsTermUnsafe :: Theory -> [Var] -> Term -> Term
141+
listMkExistsTermUnsafe = mkUnsafe3 "HOL.Syntax.listMkExistsTerm" listMkExistsTerm
142+
143+
-- Universal quantification
144+
145+
forallTerm :: Theory -> Type -> Maybe Term
146+
forallTerm thy a = do
147+
c <- forallConst thy
148+
return $ Term.mkConst c (mkQuantType a)
149+
150+
mkForallTerm :: Theory -> Var -> Term -> Maybe Term
151+
mkForallTerm thy v t = do
152+
q <- forallTerm thy (Var.typeOf v)
153+
Term.mkApp q (Term.mkAbs v t)
154+
155+
mkForallTermUnsafe :: Theory -> Var -> Term -> Term
156+
mkForallTermUnsafe = mkUnsafe3 "HOL.Syntax.mkForallTerm" mkForallTerm
157+
158+
listMkForallTerm :: Theory -> [Var] -> Term -> Maybe Term
159+
listMkForallTerm _ [] t = return t
160+
listMkForallTerm thy (v : vs) t = do
161+
u <- listMkForallTerm thy vs t
162+
mkForallTerm thy v u
163+
164+
listMkForallTermUnsafe :: Theory -> [Var] -> Term -> Term
165+
listMkForallTermUnsafe = mkUnsafe3 "HOL.Syntax.listMkForallTerm" listMkForallTerm

0 commit comments

Comments
 (0)