Implementation of Extractable monad #113
Conversation
template-coq/gen-src/coq_constr.ml
Outdated
| open Plugin_core | ||
| open Constr | ||
|
|
||
| type nat |
There was a problem hiding this comment.
What should this get extracted to?
template-coq/gen-src/Extraction.v
Outdated
| "Coq_constr.tProj" | ||
| "Coq_constr.tFix" | ||
| "Coq_constr.tCoFix" ] "Coq_constr.constr_match". | ||
|
|
There was a problem hiding this comment.
Will need to handle kername and universes.
- the previous implementation was completely wrong.
| | Some typ -> Some (to_constr typ) | ||
| in | ||
| tmMap (fun x -> Obj.magic (of_kername x)) | ||
| (tmDefinition (to_ident nm) typ (to_constr trm)) |
There was a problem hiding this comment.
Are we assuming in the line above that to_constr does unquoting as well?
There was a problem hiding this comment.
What does "unquoting" mean? I think to_constr is just one direction of the isomorphism, it shouldn't need to do anything intelligent.
There was a problem hiding this comment.
Ok. It's body would be very similar to the following?
metacoq/template-coq/src/denote.ml
Line 347 in d5088ac
There was a problem hiding this comment.
It should be similar, except the type will be a little bit different.
There was a problem hiding this comment.
ok. I am working on it (to_constr).
There was a problem hiding this comment.
In #11, denote_term was sufficiently functorized so that we could have used its instantiation as to_constr. Somehow, those changes to denote_term were undone since then. My last commit introduces a lot of code duplication and I think going back to the functorized version of denote_term may be the right approach.
| let to_constr (t : Ast0.term) : Constr.t = | ||
| failwith "to_constr" | ||
|
|
||
| let of_constr (t : Constr.t) : Ast0.term = |
There was a problem hiding this comment.
As @mattam82 pointed out, part of this is in checker/src/term_quoter.ml. checker already depends on template-coq. If we import checker in this file (template-coq/gen-src/run_extractable), we would run into cyclic dependencies between the directories template-coq and checker. Would this work? If not, should we move term_quoter to the template-coq directory?
There was a problem hiding this comment.
Let's move it if we can make it work.
Error: The implementation src/denote.ml
does not match the interface src/denote.cmi:
The value `denote_term' is required but not provided
The value `map_evm' is required but not provided
The value `unquote_universe_instance' is required but not provided
The value `unquote_level' is required but not provided
The value `unquote_string' is required but not provided
The value `unquote_ident' is required but not provided
The value `unquote_bool' is required but not provided
The value `unquote_list' is required but not provided
The value `unquote_pair' is required but not provided
Makefile.coq:604: recipe for target 'src/denote.cmx' failed
…coq into plugin-tm-interp-functor-denote git checkout --ours template-coq/src/denote.ml
File "src/denote.ml", line 1:
Error: The implementation src/denote.ml
does not match the interface src/denote.cmi:
The value `denote_term' is required but not provided
for running live in Coq
…coq into plugin-tm-interp-functor-denote
let getFields mi =
Printf.printf "in get fields\n";
match mi.ind_bodies with
| [] -> Printf.printf "no ind bodies\n"; None
| oib :: l ->
(match l with
| [] ->
(match oib.ind_ctors with
| [] -> Printf.printf "no constructors\n"; None
| ctor0 :: l0 ->
(match l0 with
| [] ->
Some { coq_type = oib.ind_name; ctor =
(let (p, _) = ctor0 in let (x0, _) = p in x0); fields =
oib.ind_projs }
| _ :: _ -> None))
| _ :: _ -> Printf.printf "multiple constructors\n"; None)
it turns out there are multiple constructors for the Point record.
let cl2s cl = String.concat "" (List.map (String.make 1) cl)
let getFields mi =
match mi.ind_bodies with
| [] -> Printf.printf "no ind bodies\n"; None
| oib :: l ->
print_string (String.concat "in get fields: " [cl2s (oib.ind_name)]);
(match l with
| [] ->
(match oib.ind_ctors with
| [] -> Printf.printf "no constructors\n"; None
| ctor0 :: l0 ->
(match l0 with
| [] ->
Some { coq_type = oib.ind_name; ctor =
(let (p, _) = ctor0 in let (x0, _) = p in x0); fields =
oib.ind_projs }
| _ :: _ -> None))
| _ :: _ -> Printf.printf "multiple constructors\n"; None)
Most likely, the inductive structure is corrupt. Some use of
Obj.magic is likely suspect.
it, instead of needing to manually edit the extract
|
I am still getting segfault, as illustrated in the comment in the last commit. Most likely, |
|
@gmalecha I wasn't able to understand |
|
The extraction of genLensN now works. The implementation needs a serious cleanup. |
|
@mattam82. Any objections to merging this? |
|
This is a very large PR, so just a quick summary of what happened in it.
Any feedback is welcome. |
gmalecha
changed the title
|
Ok, it seems very good. However, I can't go in the details because it is complicated. So if I understand well, there are two ways to run an extractable plugin: either as an old plugin with A few remarks:
Say me when you want that I merge. Can you rebase it on top of coq-8.8? |
|
Thanks, @SimonBoulier! I will work on these. For the recursive quoting, I was wondering if it makes more sense to write a dependencies function that would construct a list of all of the (recursive) dependencies of a term. Then you could quote individual pieces as much as you want. Does that seem reasonable? |
I think this would be great, but I'm also not certain. I think I would need a flag that would tell the extraction plugin to not generate code for particular library.
I really don't like generating ml files into the source directory. It makes it hard for me to browse code.
Just to be a little bit more clear I opened PR #133 with my current thinking on this.
|
|
If you do some rebasing, maybe you can do it on top of #128 so that we can merge one after the other ... |
|
I'm really bad at rebasing, so I pushed a new PR #134 . We can merge that and close this one. |
|
Merged in #134 |
This is just a start of #112.
@aa755