Go backward to Sharing of Modules Go up to Top Go forward to External Modules

Redeclaration of Modules

module S = { var A: K; fun F=@A+1 };
module M = { import S; proc INIT=A:=0 };
module N = { import S; proc SUCC=A:=F };
import M; import N; in call INIT; call SUCC

• Prohibited by typing rules.
• S would be imported twice!
• However, makes sense if S is evaluated eagerly!

Alternative typing rules required for eagerly evaluated modules and multiple import of same module.