From b23edffbb4c0f57a5988c3ae218987f15e215097 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sun, 15 Feb 2015 13:54:59 -0500 Subject: 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 --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide/coq.lang') 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 @@ (\%{locality}|(Reserved|Tactic)\%{space})?Notation \%{locality}Infix Declare\%{space}ML\%{space}Module - Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme) + Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON) \%{locality}Hint\%{space} -- cgit v1.2.3