source: extracted/policyFront.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 2.6 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open Fetch
82
83open Status
84
85open Assembly
86
87type ppc_pc_map =
88  (Nat.nat, (Nat.nat, Assembly.jump_length) Types.prod
89  BitVectorTrie.bitVectorTrie) Types.prod
90
91val jmpeqb : Assembly.jump_length -> Assembly.jump_length -> Bool.bool
92
93val expand_relative_jump_internal_unsafe :
94  Assembly.jump_length -> (ASM.subaddressing_mode -> ASM.subaddressing_mode
95  ASM.preinstruction) -> ASM.instruction List.list
96
97val strip_target :
98  ASM.identifier0 ASM.preinstruction -> (ASM.subaddressing_mode ->
99  ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum
100
101val expand_relative_jump_unsafe :
102  Assembly.jump_length -> ASM.identifier0 ASM.preinstruction ->
103  ASM.instruction List.list
104
105val expand_pseudo_instruction_unsafe :
106  Assembly.jump_length -> ASM.pseudo_instruction -> ASM.instruction List.list
107
108val instruction_size_jmplen :
109  Assembly.jump_length -> ASM.pseudo_instruction -> Nat.nat
110
111val max_length :
112  Assembly.jump_length -> Assembly.jump_length -> Assembly.jump_length
113
114val dec_jmple :
115  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
116
117val dec_eq_jump_length :
118  Assembly.jump_length -> Assembly.jump_length -> (__, __) Types.sum
119
120val create_label_map :
121  ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0
122
123val select_reljump_length :
124  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
125  -> Nat.nat -> Assembly.jump_length
126
127val select_call_length :
128  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
129  -> Assembly.jump_length
130
131val select_jump_length :
132  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
133  -> Assembly.jump_length
134
135val destination_of :
136  ASM.identifier0 ASM.preinstruction -> ASM.identifier0 Types.option
137
138val length_of : ASM.identifier0 ASM.preinstruction -> Nat.nat
139
140val jump_expansion_step_instruction :
141  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
142  ASM.preinstruction -> Assembly.jump_length Types.option
143
144val jump_expansion_start :
145  ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
146  ppc_pc_map Types.option Types.sig0
147
Note: See TracBrowser for help on using the repository browser.