modules, functor, trouble · Coq users

Stream: Coq users

Topic: modules, functor, trouble

Quinn (Jan 14 2022 at 17:50):

I have File.v

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 File2.v:

From vnTinyRAM Require Import File.
Import vnTinyRAMTypes (* fail: cannot import functor vnTinyRAMTypes *)

My hypothesis: I'd be able to instantiate wordSize and 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.

Paolo Giarrusso (Jan 14 2022 at 20:25):

Yes with Module params <: Params. Definition wordSize := 64. ... End params. Module Import foo := vnTinyRAMTypes params.

Paolo Giarrusso (Jan 14 2022 at 20:26):

(sorry for layout, I'm on a tablet)

Quinn (Jan 14 2022 at 21:18):

worked, thanks!

I'll notice it worked with both params : Params and params <: Params... hm

Paolo Giarrusso (Jan 14 2022 at 22:38):

Yes but those are pretty different; Eval cbv in params.wordSize. is the simplest example.

Paolo Giarrusso (Jan 14 2022 at 22:39):

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

Paolo Giarrusso (Jan 14 2022 at 22:42):

BTW, you can even drop <: Params altogether, yet still apply vnTinyRAMTypes params as above as long as params still satisfies the interface.

Paolo Giarrusso (Jan 14 2022 at 22:46):

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

Quinn (Jan 14 2022 at 23:05):

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.

Paolo Giarrusso (Jan 15 2022 at 00:40):

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