source: extracted/frontEndMem.mli @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 8 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
RevLine 
[2601]1open Preamble
2
3open Hide
4
5open ByteValues
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]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
[2717]35open Exp
36
[2601]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
[2649]85open Coqlib
86
[2601]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.