Equations `tProj` issue

[wrsturgeon]

Hi,

Thanks for making this library! I'm new to it, but I haven't been able to use it successfully yet:

TL;DR: Equations.Init.sigma seems to cause an unhandled tProj error (raised here). Is this easily fixable, or is there somewhere I can understand a bit better what this means and how to prevent it?

Longer explanation: I've been trying to extract MetaRocq's typechecker (that is, MetaRocq.SafeChecker.PCUICSafeChecker.typecheck_program) to Rust, and the simplest way to do so seems to be with a file like this:

From MetaCoq.SafeChecker Require Import
  PCUICSafeChecker
  .
From RustExtraction Require Import
  Loader
  ExtrRustBasic
  ExtrRustUncheckedArith
  .
Redirect "pcuic.rs"
  Rust Extract @PCUICSafeChecker.typecheck_program.

With the above file named Extract.v and -output-dir=src, this creates exactly one file, src/pcuic.rs.out, with the following contents:

File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive eq into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive feq into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive fdiv into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive flt into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive fabs into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive frshiftexp into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive l_and into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive l_sr into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive normfr_mantissa into an axiom.
[primitive-turned-into-axiom,metacoq,default]
File "./Extract.v", line 9, characters 0-71:
Warning: Quoting primitive string_compare into an axiom.
[primitive-turned-into-axiom,metacoq,default]
Debug: Quoting executed in: 17.750382s
Debug: Extraction executed in: 11.438570s
unhandled tProj on Equations.Init.sigma
failed after printing
[and then it prints a few thousand lines of Rust code, then stops abruptly in the middle of a function]

I haven't been able to find an example that uses Equations (here or in ConCert). Is there one, or is there something I can do to prevent this?

Thanks again for anything that might help. It's exciting to be able to extract to Rust!

[4ever2]

It looks like primitive projections might be used somewhere in the code that you are trying to extract (see https://github.com/mattam82/Coq-Equations/blob/96195721772cecb2f39f6bd922a85c8070b49d0a/theories/Init.v#L69).
Primitive projections are currently not supported (#8)