From 4f523e7d25ed22b6e41cabf1c2bd091afc0fde7f Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 28 Nov 2011 16:10:46 +0000 Subject: Extraction: Richer patterns in matchs as proposed by P.N. Tollitte The MLcase has notably changed: - No more case_info in it, but only a type annotation - No more "one branch for one constructor", but rather a sequence of patterns. Earlier "full" pattern correspond to pattern Pusual. Patterns Pwild and Prel allow to encode optimized matchs without hacks as earlier. Other pattern situations aren't used (yet) by extraction, but only by P.N Tollitte's code. A MLtuple constructor has been introduced. It isn't used by the extraction for the moment, but only but P.N. Tollitte's code. Many pretty-print functions in ocaml.ml and other have been reorganized git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/table.mli | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index cdd792222..a3b7124e1 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -74,6 +74,14 @@ val lookup_type : constant -> ml_schema val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind +val add_inductive_kind : mutual_inductive -> inductive_kind -> unit +val is_coinductive : global_reference -> bool +val is_coinductive_type : ml_type -> bool +(* What are the fields of a record (empty for a non-record) *) +val get_record_fields : + global_reference -> global_reference option list +val record_fields_of_type : ml_type -> global_reference option list + val add_recursors : Environ.env -> mutual_inductive -> unit val is_recursor : global_reference -> bool -- cgit v1.2.3