%freeze
From The Twelf Project
| This article describes an undocumented feature of Twelf. The information may be incomplete and subject to change. |
The %freeze declaration freezes a set of type families. A frozen family cannot be extended: new constants at that type cannot be added, nor can the subordination relation be extended such that the family could depend on other types. The %thaw declaration can be used to reenable the extension of a type family.
[edit] Syntax
The syntax is as follows:
%freeze t1 t2 ... tn.
The type families t1–tn are frozen.
[edit] Example
Suppose we define addition in the natural way:
nat : type. z : nat. s : nat -> nat. %prefix 9999 s. plus : nat -> nat -> nat -> type. %mode plus +N +M -O. plus/z : plus z N N. plus/s : plus (s N) M (s P) <- plus N M P.
At this point, we may still extend the definition of addition:
plus/zz : plus M z M.
Twelf 1.5R3, Aug 30, 2005 (%trustme)plus/zz : {M:nat} plus M z M.
%% OK %%
However, if we freeze plus then this will not be allowed:
%freeze plus. plus/zzz : plus z z z.
Twelf 1.5R3, Aug 30, 2005 (%trustme)%freeze plus. plus/zzz : plus z z z. Error: Freezing violation: constant plus/zzz extends type family plus
%% ABORT %%
More subtly, we will not be able to extend the subordination relation for plus:
%freeze plus. thing : type. oops : (thing -> plus _ _ _) -> type.
Twelf 1.5R3, Aug 30, 2005 (%trustme)%freeze plus. thing : type. oops : {X1:nat} {X2:nat} {X3:nat} (thing -> plus X1 X2 X3) -> type. Error: Freezing violation: plus would depend on thing
%% ABORT %%
The subordination relation can be extended such that other non-frozen types depend on a frozen type, of course:
%freeze plus. thing : type. okay : (plus _ _ _ -> thing) -> type.
Twelf 1.5R3, Aug 30, 2005 (%trustme)%freeze plus. thing : type. okay : {X1:nat} {X2:nat} {X3:nat} (plus X1 X2 X3 -> thing) -> type.
%% OK %%
Because types are automatically frozen in common cases (see below), one may occasionally need to induce subordination relations in anticipation of code that follows freezing. This can be done as in the type oops above, before using %freeze or metatheory like %worlds.
[edit] Autofreeze
Twelf CVS[?] automatically freezes any family for which there has been a %worlds declaration. This prevents mistakes where a metatheorem is proved for a type family but then that type family is extended, invalidating the theorem.[?]
