29 case class Free(name: String, typ: Typ = dummyT) extends Term |
29 case class Free(name: String, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
31 case class Bound(index: Int) extends Term |
31 case class Bound(index: Int) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
|
34 |
|
35 |
|
36 /* Pure logic */ |
|
37 |
|
38 def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty)) |
|
39 val propT: Typ = Type(Pure_Thy.PROP, Nil) |
|
40 def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2)) |
|
41 |
|
42 def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, itselfT(ty)) |
|
43 |
|
44 def const_of_class(c: String): String = c + "_class" |
|
45 |
|
46 def mk_of_sort(ty: Typ, s: Sort): List[Term] = |
|
47 { |
|
48 val class_type = funT(itselfT(ty), propT) |
|
49 val t = mk_type(ty) |
|
50 s.map(c => App(Const(const_of_class(c), class_type), t)) |
|
51 } |
34 |
52 |
35 |
53 |
36 /* type arguments of consts */ |
54 /* type arguments of consts */ |
37 |
55 |
38 def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] = |
56 def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] = |