diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2015-02-15 13:54:59 -0500 |
|---|---|---|
| committer |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-04-09 12:08:26 +0200 |
| commit | b23edffbb4c0f57a5988c3ae218987f15e215097 (patch) | |
| tree | 9a7a3eb7f6c2bbf24b032970fb5fe4242238600d /ide/coq.lang | |
| parent | edab9829134612b191d0f6cd24ac3637d8d4b414 (diff) | |
Add extraction to JSON.
This patch allows Coq terms to be extracted into the widely used JSON
format. This is useful in at least two cases:
- One might want to manipulate Coq values outside of Coq, but without
being forced to use one of the three existing extraction languages
(OCaml, Haskell, or Scheme), and without having to compile Coq's
extracted result. This is especially useful when a Coq evaluation
produces some data structure that needs to be moved out of Coq.
Having to invoke an OCaml/Haskell/Scheme compiler just to get a
data structure out of Coq is somewhat awkward.
- One might want to experiment with extracting Coq code into other
languages (Go, Javascript, etc), without having to write the whole
extraction logic in OCaml and recompile Coq's extraction plugin
each time. This makes it easy to quickly prototype extraction
in any language, without having to build Coq from source.
Extraction to JSON is implemented by adding the JSON "pseudo-language"
to the extraction facility. Thus, one can extract the JSON encoding
of a single term using:
Extraction Language JSON.
Extraction qualid.
and extract an entire Coq library "ident" into "ident.json" using:
Extraction Language JSON.
Extraction Library ident.
Nota (Pierre Letouzey) : this is an updated version of the original
PullRequest, updated to match recent changes in trunk
Diffstat (limited to 'ide/coq.lang')
| -rw-r--r-- | ide/coq.lang | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coq.lang b/ide/coq.lang index 38dabda50..65150d6a9 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -164,7 +164,7 @@ <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> <keyword>\%{locality}Infix</keyword> <keyword>Declare\%{space}ML\%{space}Module</keyword> - <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme)</keyword> + <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> </context> <context id="hint-command" style-ref="vernac-keyword"> <prefix>\%{locality}Hint\%{space}</prefix> |