equal
deleted
inserted
replaced
8 signature TYPE = |
8 signature TYPE = |
9 sig |
9 sig |
10 (*constraints*) |
10 (*constraints*) |
11 val mark_polymorphic: typ -> typ |
11 val mark_polymorphic: typ -> typ |
12 val constraint: typ -> term -> term |
12 val constraint: typ -> term -> term |
|
13 val constraint_type: Proof.context -> typ -> typ |
13 val strip_constraints: term -> term |
14 val strip_constraints: term -> term |
14 val appl_error: Proof.context -> term -> typ -> term -> typ -> string |
15 val appl_error: Proof.context -> term -> typ -> term -> typ -> string |
15 (*type signatures and certified types*) |
16 (*type signatures and certified types*) |
16 datatype decl = |
17 datatype decl = |
17 LogicalType of int | |
18 LogicalType of int | |
108 |
109 |
109 fun constraint T t = |
110 fun constraint T t = |
110 if T = dummyT then t |
111 if T = dummyT then t |
111 else Const ("_type_constraint_", T --> T) $ t; |
112 else Const ("_type_constraint_", T --> T) $ t; |
112 |
113 |
|
114 fun constraint_type ctxt T = |
|
115 let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T); |
|
116 in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end; |
|
117 |
113 fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t |
118 fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t |
114 | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u |
119 | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u |
115 | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t) |
120 | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t) |
116 | strip_constraints a = a; |
121 | strip_constraints a = a; |
117 |
122 |