Module Type Params. Parameter wordSize : nat. Parameter registerCount : nat. (* TODO: proof obligation for the relation, that log equation from the paper*) End Params. Module vnTinyRAMTypes (params : Params). Import params. Inductive bit : Type := | off | on. ... End vnTinyRAMTypes
It compiles nicely and in
From vnTinyRAM Require Import File. Import vnTinyRAMTypes (* fail: cannot import functor vnTinyRAMTypes *)
My hypothesis: I'd be able to instantiate
registerCount at particular
nats at the time of importing the functor, though I'm not sure by what notation I thought I'd be able to do this.
Module params <: Params. Definition wordSize := 64. ... End params. Module Import foo := vnTinyRAMTypes params.
(sorry for layout, I'm on a tablet)
I'll notice it worked with both
params : Params and
params <: Params... hm
Yes but those are pretty different;
Eval cbv in params.wordSize. is the simplest example.
<: just checks that
params can be given type
Params but keeps the original type (with its extra definitions), while
: hides away everything that isn't in the interface.
BTW, you can even drop
<: Params altogether, yet still apply
vnTinyRAMTypes params as above as long as
params still satisfies the interface.
this section of the reference manual has some examples: https://coq.inria.fr/refman/language/core/modules.html#examples
earlier, there's even a reference: https://coq.inria.fr/refman/language/core/modules.html#using-modules
I think the syntax I wished I had was
Import vnTinyRAMTypes with (Params 16 16). where the name of the
Module Type just automatically becomes a combinator with signature drawn from the
Parameter declarations in it's body, if that makes sense.
All Coq modules must be named. That wouldn't stop
Module p := Params 16 16, but that syntax doesn't work either. Have you considered functions taking records?
Last updated: Sep 23 2023 at 15:01 UTC