69240
|
1 |
{- generated by Isabelle -}
|
|
2 |
|
|
3 |
{- Title: Tools/Haskell/Term.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
Lambda terms, types, sorts.
|
|
8 |
-}
|
|
9 |
|
|
10 |
module Isabelle.Term (
|
|
11 |
Indexname,
|
|
12 |
|
|
13 |
Sort, dummyS,
|
|
14 |
|
|
15 |
Typ(..), dummyT, Term(..))
|
|
16 |
where
|
|
17 |
|
|
18 |
type Indexname = (String, Int)
|
|
19 |
|
|
20 |
|
|
21 |
type Sort = [String]
|
|
22 |
|
|
23 |
dummyS :: Sort
|
|
24 |
dummyS = [""]
|
|
25 |
|
|
26 |
|
|
27 |
data Typ =
|
|
28 |
Type (String, [Typ])
|
|
29 |
| TFree (String, Sort)
|
|
30 |
| TVar (Indexname, Sort)
|
|
31 |
deriving Show
|
|
32 |
|
|
33 |
dummyT :: Typ
|
|
34 |
dummyT = Type ("dummy", [])
|
|
35 |
|
|
36 |
|
|
37 |
data Term =
|
|
38 |
Const (String, Typ)
|
|
39 |
| Free (String, Typ)
|
|
40 |
| Var (Indexname, Typ)
|
|
41 |
| Bound Int
|
|
42 |
| Abs (String, Typ, Term)
|
|
43 |
| App (Term, Term)
|
|
44 |
deriving Show
|