source: extracted/interpret.mli @ 2890

Last change on this file since 2890 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.5 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open String
6
7open Exp
8
9open Arithmetic
10
11open Vector
12
13open FoldStuff
14
15open BitVector
16
17open Extranat
18
19open Integers
20
21open AST
22
23open LabelledObjects
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 Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Util
52
53open List
54
55open Lists
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Positive
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open Identifiers
76
77open CostLabel
78
79open ASM
80
81open Status
82
83open StatusProofs
84
85open Fetch
86
87open Hide
88
89open Division
90
91open Z
92
93open BitVectorZ
94
95open Pointers
96
97open Coqlib
98
99open Values
100
101open Events
102
103open IOMonad
104
105open IO
106
107open Sets
108
109open Listb
110
111open StructuredTraces
112
113open AbstractStatus
114
115val execute_1_preinstruction :
116  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
117  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
118  Status.preStatus
119
120val execute_1_preinstruction_ok' :
121  (Nat.nat, Nat.nat) Types.prod -> 'a2 -> ('a1 -> 'a2 Status.preStatus ->
122  BitVector.word) -> 'a1 ASM.preinstruction -> 'a2 Status.preStatus -> 'a2
123  Status.preStatus Types.sig0
124
125val compute_target_of_unconditional_jump :
126  BitVector.word -> ASM.instruction -> BitVector.word
127
128val is_unconditional_jump : ASM.instruction -> Bool.bool
129
130val program_counter_after_other :
131  BitVector.word -> ASM.instruction -> BitVector.word
132
133val addr_of_relative :
134  'a1 -> ASM.subaddressing_mode -> 'a1 Status.preStatus -> BitVector.word
135
136val execute_1_0 :
137  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
138  ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod ->
139  Status.status Types.sig0
140
141val current_instruction_cost :
142  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status -> Nat.nat
143
144val execute_1' :
145  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
146  Status.status Types.sig0
147
148val execute_1 :
149  BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
150  Status.status
151
152val execute_1_pseudo_instruction0 :
153  (Nat.nat, Nat.nat) Types.prod -> ASM.pseudo_assembly_program ->
154  Status.pseudoStatus -> ASM.pseudo_instruction -> BitVector.word ->
155  Status.pseudoStatus
156
157val execute_1_pseudo_instruction :
158  ASM.pseudo_assembly_program -> (BitVector.word -> __ -> (Nat.nat, Nat.nat)
159  Types.prod) -> Status.pseudoStatus -> Status.pseudoStatus
160
161val execute :
162  Nat.nat -> BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
163  Status.status
164
Note: See TracBrowser for help on using the repository browser.