structure MTPGlobal = MTPGlobal (structure MetaGlobal = MetaGlobal) structure FunSyn = FunSyn (structure IntSyn' = IntSyn structure Whnf = Whnf structure Conv = Conv); structure StateSyn = StateSyn (structure FunSyn' = FunSyn structure IntSyn' = IntSyn structure Whnf = Whnf structure Conv = Conv) structure FunNames = FunNames (structure Global = Global structure FunSyn' = FunSyn structure HashTable = StringHashTable); structure FunPrint = FunPrint (structure FunSyn' = FunSyn structure Formatter = Formatter structure Print = Print structure Names = Names); (* moves eventually into the Twelf core *) structure Weaken = Weaken (structure IntSyn' = IntSyn structure Whnf = Whnf) structure FunWeaken = FunWeaken (structure FunSyn' = FunSyn structure Weaken = Weaken) structure FunTypeCheck = FunTypeCheck (structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure Abstract = Abstract structure TypeCheck = TypeCheck structure Conv = Conv structure Weaken = Weaken structure Subordinate = Subordinate structure Whnf = Whnf structure Print = Print structure FunPrint = FunPrint); structure RelFun = RelFun (structure Global = Global structure FunSyn' = FunSyn structure ModeSyn = ModeSyn structure Names = Names structure TypeCheck = TypeCheck structure Trail = Trail structure Unify = UnifyTrail structure Whnf = Whnf structure Print = Print structure Weaken = Weaken structure FunWeaken = FunWeaken structure FunNames = FunNames); (* Functor instantiation for the Prover *) structure MTPData = MTPData (structure MTPGlobal = MTPGlobal) structure MTPAbstract = MTPAbstract (structure IntSyn' = IntSyn structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure Whnf = Whnf structure Constraints = Constraints structure Unify = UnifyTrail structure Subordinate = Subordinate structure TypeCheck = TypeCheck structure FunTypeCheck = FunTypeCheck structure Abstract = Abstract); structure MTPInit = MTPInit (structure MTPGlobal = MTPGlobal structure IntSyn = IntSyn structure Names = Names structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure MTPData = MTPData structure Formatter = Formatter structure Whnf = Whnf structure Print = Print structure FunPrint = FunPrint) structure MTPrint = MTPrint (structure Global = Global structure IntSyn = IntSyn structure FunSyn = FunSyn structure Names = Names structure StateSyn' = StateSyn structure Formatter' = Formatter structure Print = Print structure FunPrint = FunPrint) structure MTPSearch = MTPSearch (structure Global = Global structure MTPGlobal = MTPGlobal structure IntSyn' = IntSyn structure Abstract = Abstract structure Conv = Conv structure StateSyn' = StateSyn structure CompSyn' = CompSyn structure Compile = Compile structure Whnf = Whnf structure Unify = UnifyTrail structure Index = IndexSkolem (* structure Assign = Assign *) structure CPrint = CPrint structure Print = Print structure Names = Names structure CSManager = CSManager); structure MTPFilling = MTPFilling (structure MTPGlobal = MTPGlobal structure IntSyn = IntSyn structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure MTPData = MTPData structure Whnf = Whnf structure Abstract = Abstract structure TypeCheck = TypeCheck structure Search = MTPSearch structure Whnf = Whnf) structure MTPSplitting = MTPSplitting (structure MTPGlobal = MTPGlobal structure Global = Global structure IntSyn = IntSyn structure FunSyn = FunSyn structure StateSyn' = StateSyn structure Heuristic = Heuristic structure MTPrint = MTPrint structure MTPAbstract = MTPAbstract structure Names = Names (* to be removed -cs *) structure Conv = Conv structure Whnf = Whnf structure TypeCheck = TypeCheck structure Subordinate = Subordinate structure FunTypeCheck = FunTypeCheck structure Index = Index structure Print = Print structure Unify = UnifyTrail structure CSManager = CSManager); structure UniqueSearch = UniqueSearch (structure Global = Global structure IntSyn' = IntSyn structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure Abstract = Abstract structure MTPGlobal = MTPGlobal structure CompSyn' = CompSyn structure Whnf = Whnf structure Unify = UnifyTrail structure Index = Index structure Compile = Compile structure CPrint = CPrint structure Print = Print structure Names = Names structure CSManager = CSManager); structure Inference = Inference (structure MTPGlobal = MTPGlobal structure IntSyn = IntSyn structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure Abstract = Abstract structure TypeCheck = TypeCheck structure FunTypeCheck = FunTypeCheck structure UniqueSearch = UniqueSearch structure Whnf = Whnf structure Print = Print) structure MTPRecursion = MTPRecursion (structure MTPGlobal = MTPGlobal structure Global = Global structure IntSyn = IntSyn structure FunSyn = FunSyn structure StateSyn' = StateSyn structure FunTypeCheck = FunTypeCheck structure MTPSearch = MTPSearch structure Abstract = Abstract structure MTPAbstract = MTPAbstract structure Whnf = Whnf structure Unify = UnifyTrail structure Conv = Conv structure Names = Names structure Subordinate = Subordinate structure MTPrint = MTPrint structure Print = Print structure TypeCheck = TypeCheck structure FunPrint = FunPrint structure Formatter = Formatter structure CSManager = CSManager); structure MTPStrategy = MTPStrategy (structure MTPGlobal = MTPGlobal structure StateSyn' = StateSyn structure MTPrint = MTPrint structure MTPData = MTPData structure MTPFilling = MTPFilling structure MTPSplitting = MTPSplitting structure MTPRecursion = MTPRecursion structure Inference = Inference structure Timers = Timers) structure MTProver = MTProver (structure MTPGlobal = MTPGlobal structure IntSyn' = IntSyn structure FunSyn = FunSyn structure StateSyn = StateSyn structure Order = Order structure MTPrint = MTPrint structure MTPInit = MTPInit structure MTPStrategy = MTPStrategy structure RelFun = RelFun) structure CombiProver = CombiProver (structure MTPGlobal = MTPGlobal structure IntSyn' = IntSyn structure ProverNew = MTProver structure ProverOld = Prover) structure MTPi = MTPi (structure MTPGlobal = MTPGlobal structure IntSyn = IntSyn structure FunSyn' = FunSyn structure StateSyn' = StateSyn structure FunTypeCheck = FunTypeCheck structure RelFun = RelFun structure Formatter = Formatter structure Print = Print structure MTPrint = MTPrint structure MTPInit = MTPInit structure MTPFilling = MTPFilling structure MTPData = MTPData structure MTPSplitting = MTPSplitting structure MTPRecursion = MTPRecursion structure Inference = Inference structure MTPStrategy = MTPStrategy structure Names = Names structure Order = Order structure Timers = Timers structure Ring = Ring)