From c595d5cc3105b0bec4faa0a5ed7e1c37de0c5e2c Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sat, 4 Apr 2015 10:42:18 -0400 Subject: Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181) The extraction machinery has specialized support for extracting [ascii] characters into native characters in the target language, as opposed to using an explicit constructor from 8 boolean bits. This works by hard-coding the name of the character type in the target language. Unfortunately, the hard-coded type for Haskell was "Char", not the fully-qualified "Prelude.Char". As a result, it was impossible to extract characters into Haskell without getting type errors about "Char". This patch changes this hard-coded name to "Prelude.Char". --- plugins/extraction/common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 21819aa8f1..0748af1ead 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -628,7 +628,7 @@ let check_extract_ascii () = try let char_type = match lang () with | Ocaml -> "char" - | Haskell -> "Char" + | Haskell -> "Prelude.Char" | _ -> raise Not_found in String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) -- cgit v1.2.3 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 --- plugins/extraction/common.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0748af1ead..094d91d20b 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -600,6 +600,7 @@ let pp_global k r = let rls = List.rev ls in (* for what come next it's easier this way *) match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) + | JSON -> unquote s (* no modular JSON extraction... *) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) -- cgit v1.2.3 From fb8c4b8903e82b36ebcf28dfe18282fb05a93d4f Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sun, 5 Apr 2015 10:52:45 -0400 Subject: JSON extraction: construct full names (dot-separated) in pp_global This is important to disambiguate identical names from different modules. --- plugins/extraction/common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 094d91d20b..97f856944c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -600,7 +600,7 @@ let pp_global k r = let rls = List.rev ls in (* for what come next it's easier this way *) match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) - | JSON -> unquote s (* no modular JSON extraction... *) + | JSON -> dottify (List.map unquote rls) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) -- cgit v1.2.3