equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature TYPE = |
8 signature TYPE = |
9 sig |
9 sig |
10 (*constraints*) |
10 (*constraints*) |
|
11 val mark_polymorphic: typ -> typ |
11 val constraint: typ -> term -> term |
12 val constraint: typ -> term -> term |
12 val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string |
13 val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string |
13 (*type signatures and certified types*) |
14 (*type signatures and certified types*) |
14 datatype decl = |
15 datatype decl = |
15 LogicalType of int | |
16 LogicalType of int | |
99 structure Type: TYPE = |
100 structure Type: TYPE = |
100 struct |
101 struct |
101 |
102 |
102 (** constraints **) |
103 (** constraints **) |
103 |
104 |
|
105 (*indicate polymorphic Vars*) |
|
106 fun mark_polymorphic T = Type ("_polymorphic_", [T]); |
|
107 |
104 fun constraint T t = |
108 fun constraint T t = |
105 if T = dummyT then t |
109 if T = dummyT then t |
106 else Const ("_type_constraint_", T --> T) $ t; |
110 else Const ("_type_constraint_", T --> T) $ t; |
107 |
111 |
108 fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U = |
112 fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U = |