Stream: Coq users

Topic: Extraction wierd behavriour


view this post on Zulip walker (Jan 18 2023 at 23:19):

I have a file term.v that looks like this:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(* Grammer of a term *)
Inductive Term : Type :=
 (* bounded variable with binder removed,identified using debruijn-levels *)
| var (idx: nat): Term
 (* Universes.. TODO this must be replaced with subtyping based universes *)
| univ (l: nat): Term
 (* Function type from A to B*)
| pi (A: Term) (B: Term)
 (* Lambda Abstraction (Function implementation) *)
| lam (T: Term) (y: Term)
 (* Function Application *)
| appl (m: Term) (n: Term)
 (* sigma type*)
| sigma (A: Term) (B: Term)
  (* dependent pairs*)
| pair (M N: Term) (m: Term) (n: Term)
  (* projection for dependent pair *)
| proj1 (m: Term)
| proj2 (m: Term).

Tactic Notation "TermElim" :=
elim => /=
    [ idx
    | lvl
    | A IHA B IHB
    | T IHT y IHy
    | m IHm n IHn
    | A IHA B IHB
    | M IHM N IHN m IHm n IHn
    | m IHm
    | m IHm
    ].

In a different file, Ido the following to extract

From Coq Require Extraction.
From Coq Require Import ExtrOcamlBasic ExtrOcamlNatBigInt.

Set Warnings "-extraction-opaque-accessed".


Cd "src".
Separate Extraction term.

I get the expected term.ml term.mli but there also two strange empty files called Datatypes.ml Datatypes.mli. How to get rid of them ?

view this post on Zulip walker (Jan 18 2023 at 23:20):

one more thing in term.ml, I see inductive principles being extracted, and I don't think I will ever need them, how to prevent those from being extracted ?

view this post on Zulip Gaëtan Gilbert (Jan 18 2023 at 23:29):

datatypes is used for nat, but ExtrOcamlNatBigInt replaces the inductive nat so it ends up empty

view this post on Zulip Gaëtan Gilbert (Jan 18 2023 at 23:30):

walker said:

one more thing in term.ml, I see inductive principles being extracted, and I don't think I will ever need them, how to prevent those from being extracted ?

you can unset https://coq.github.io/doc/master/refman/proofs/writing-proofs/reasoning-inductives.html#coq:flag.Elimination-Schemes when declaring the inductive if you really don't need them

view this post on Zulip walker (Jan 18 2023 at 23:33):

Gaëtan Gilbert said:

datatypes is used for nat, but ExtrOcamlNatBigInt replaces the inductive nat so it ends up empty

but is there a way to not have the file ?

view this post on Zulip walker (Jan 18 2023 at 23:45):

now that we are at it, extracting some other file gives a strange warning

The identifier Datatypes_nat__canonical__eqtype_Equality contains __ which is
reserved for the extraction [extraction-reserved-identifier,extraction]coqtop

Is that something I need to be concerned about ?

view this post on Zulip walker (Jan 19 2023 at 09:23):

I am getting a strange error typing to compile the extracted code:

1046 | ......let h0 = h fix_0 in
1047 |       (fun _UU0393_ t3 fuel ->
1048 |       let (a, b) = h0 in
1049 |       let (a0, b0) = b in
1050 |       let (a1, b1) = b0 in
...
1083 |            (a1 _UU0393_ m fuel))
1084 |        | Coq_proj2 m ->
1085 |          Coq_type_infer_graph_equation_9 (_UU0393_, m, fuel,
1086 |            (a1 _UU0393_ m fuel))))
Error: This kind of expression is not allowed as right-hand side of `let rec`

Last updated: Jun 16 2024 at 03:41 UTC