%freeze

From The Twelf Project
Jump to: navigation, search
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.

Syntax

The syntax is as follows:

%freeze t1 t2 ... tn.

The type families t1tn are frozen.

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.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

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.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%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.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%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.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%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.

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.[?]