walker (Jan 18 2023 at 23:19): 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 ?
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 ?
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
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
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 ?
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 ?
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: Oct 04 2023 at 23:01 UTC