From 6a2f9c59ea44d754050b4a2ccb624adcc846924d Mon Sep 17 00:00:00 2001 From: aspiwack Date: Fri, 24 Aug 2012 17:36:32 +0000 Subject: Add option Set/Unset Extraction Conservative Types. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/table.mli | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 060abf804..b17f83715 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -132,6 +132,10 @@ type opt_flag = val optims : unit -> opt_flag +(*s Controls whether dummy lambda are removed *) + +val conservative_types : unit -> bool + (*s Target language. *) type lang = Ocaml | Haskell | Scheme -- cgit v1.2.3