From f1d236b83003eda71e12840732d159fd23b1b771 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Apr 2014 13:58:18 +0000 Subject: Integration of Jacques-Henri Jourdan's verified parser. (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 344a00f..29e6863 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -23,6 +23,9 @@ Require Tailcall. Require Allocation. Require Ctypes. Require Compiler. +Require Parser. +Require Initializers. +Require Int31. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -102,6 +105,26 @@ Extract Constant Compiler.time => "Clflags.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) +(* Cabs *) +Extract Constant Cabs.cabsloc => +"{ lineno : int; + filename: string; + byteno: int; + ident : int; + }". + +(* Int31 *) +Extract Inductive Int31.digits => "bool" [ "false" "true" ]. +Extract Inductive Int31.int31 => "int" [ "Camlcoq.Int31.constr" ] "Camlcoq.Int31.destr". +Extract Constant Int31.twice => "Camlcoq.Int31.twice". +Extract Constant Int31.twice_plus_one => "Camlcoq.Int31.twice_plus_one". +Extract Constant Int31.compare31 => "Camlcoq.Int31.compare". +Extract Constant Int31.On => "0". +Extract Constant Int31.In => "1". + +(* String in Cabs *) +Extract Constant Cabs.string => "String.t". + (* Processor-specific extraction directives *) Load extractionMachdep. @@ -132,4 +155,5 @@ Separate Extraction Conventions1.dummy_int_reg Conventions1.dummy_float_reg RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin - Machregs.two_address_op Machregs.is_stack_reg. + Machregs.two_address_op Machregs.is_stack_reg + Parser.translation_unit_file. -- cgit v1.2.3