source: extracted/frontEndMem.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: 1.3 KB
Line 
1open Preamble
2
3open Hide
4
5open ByteValues
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Identifiers
28
29open Integers
30
31open AST
32
33open Division
34
35open Exp
36
37open Arithmetic
38
39open Extranat
40
41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Positive
48
49open Z
50
51open BitVectorZ
52
53open Pointers
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Extralib
82
83open GenMem
84
85open Coqlib
86
87open Values
88
89open FrontEndVal
90
91val loadn :
92  GenMem.mem1 -> Pointers.pointer -> Nat.nat -> ByteValues.beval List.list
93  Types.option
94
95val load :
96  AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 Types.option
97
98val loadv : AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 Types.option
99
100val storen :
101  GenMem.mem1 -> Pointers.pointer -> ByteValues.beval List.list ->
102  GenMem.mem1 Types.option
103
104val store :
105  AST.typ -> GenMem.mem1 -> Pointers.pointer -> Values.val0 -> GenMem.mem1
106  Types.option
107
108val storev :
109  AST.typ -> GenMem.mem1 -> Values.val0 -> Values.val0 -> GenMem.mem1
110  Types.option
111
112val valid_pointer : GenMem.mem1 -> Pointers.pointer -> Bool.bool
113
Note: See TracBrowser for help on using the repository browser.