62 extends Proof |
62 extends Proof |
63 |
63 |
64 |
64 |
65 /* Pure logic */ |
65 /* Pure logic */ |
66 |
66 |
67 def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty)) |
|
68 val propT: Typ = Type(Pure_Thy.PROP, Nil) |
|
69 def funT(ty1: Typ, ty2: Typ): Typ = Type(Pure_Thy.FUN, List(ty1, ty2)) |
|
70 |
|
71 def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, List(ty)) |
67 def mk_type(ty: Typ): Term = Const(Pure_Thy.TYPE, List(ty)) |
72 |
68 |
73 def const_of_class(c: String): String = c + "_class" |
69 def const_of_class(c: String): String = c + "_class" |
74 |
70 |
75 def mk_of_sort(ty: Typ, s: Sort): List[Term] = |
71 def mk_of_sort(ty: Typ, s: Sort): List[Term] = |
76 { |
72 { |
77 val t = mk_type(ty) |
73 val t = mk_type(ty) |
78 s.map(c => App(Const(const_of_class(c), List(ty)), t)) |
74 s.map(c => App(Const(const_of_class(c), List(ty)), t)) |
79 } |
|
80 |
|
81 |
|
82 /* type arguments of consts */ |
|
83 |
|
84 def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] = |
|
85 { |
|
86 var subst = Map.empty[String, Typ] |
|
87 |
|
88 def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ) |
|
89 def raw_match(arg: (Typ, Typ)) |
|
90 { |
|
91 arg match { |
|
92 case (TFree(a, _), ty) => |
|
93 subst.get(a) match { |
|
94 case None => subst += (a -> ty) |
|
95 case Some(ty1) => if (ty != ty1) bad_match() |
|
96 } |
|
97 case (Type(c1, args1), Type(c2, args2)) if c1 == c2 => |
|
98 (args1 zip args2).foreach(raw_match) |
|
99 case _ => bad_match() |
|
100 } |
|
101 } |
|
102 raw_match(decl, typ) |
|
103 |
|
104 typargs.map(subst) |
|
105 } |
75 } |
106 |
76 |
107 |
77 |
108 |
78 |
109 /** cache **/ |
79 /** cache **/ |