source: extracted/policyStep.mli @ 2717

Last change on this file since 2717 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: 864 bytes
Line 
1open Preamble
2
3open Assembly
4
5open Status
6
7open Fetch
8
9open String
10
11open LabelledObjects
12
13open BitVectorTrie
14
15open Exp
16
17open Arithmetic
18
19open Integers
20
21open AST
22
23open CostLabel
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Positive
48
49open Identifiers
50
51open Extranat
52
53open Vector
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Types
62
63open List
64
65open Util
66
67open FoldStuff
68
69open Bool
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Relations
80
81open Nat
82
83open BitVector
84
85open ASM
86
87open PolicyFront
88
89val jump_expansion_step :
90  ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map Types.sig0
91  -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool, PolicyFront.ppc_pc_map
92  Types.option) Types.prod Types.sig0
93
Note: See TracBrowser for help on using the repository browser.