source: driver/extracted/initialisation.mli @ 3106

Last change on this file since 3106 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: 1.8 KB
Line 
1open Preamble
2
3open CostLabel
4
5open FrontEndVal
6
7open Hide
8
9open ByteValues
10
11open GenMem
12
13open FrontEndMem
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open Extralib
22
23open Lists
24
25open Identifiers
26
27open Integers
28
29open AST
30
31open Division
32
33open Exp
34
35open Arithmetic
36
37open Extranat
38
39open Vector
40
41open FoldStuff
42
43open BitVector
44
45open Z
46
47open BitVectorZ
48
49open Pointers
50
51open ErrorMessages
52
53open Option
54
55open Setoids
56
57open Monad
58
59open Positive
60
61open PreIdentifiers
62
63open Errors
64
65open Div_and_mod
66
67open Jmeq
68
69open Russell
70
71open Util
72
73open Bool
74
75open Relations
76
77open Nat
78
79open List
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Types
90
91open Coqlib
92
93open Values
94
95open FrontEndOps
96
97open Cminor_syntax
98
99open Extra_bool
100
101open Globalenvs
102
103val init_expr :
104  AST.init_data -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option
105
106val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
107
108val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
109
110val init_datum :
111  AST.ident -> AST.region -> AST.init_data -> Nat.nat -> Cminor_syntax.stmt
112  Types.sig0
113
114val init_var :
115  AST.ident -> AST.region -> AST.init_data List.list -> Cminor_syntax.stmt
116  Types.sig0
117
118val init_vars :
119  ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
120  List.list -> Cminor_syntax.stmt Types.sig0
121
122val add_statement :
123  CostLabel.costlabel -> AST.ident -> Cminor_syntax.stmt Types.sig0 ->
124  (AST.ident, Cminor_syntax.internal_function AST.fundef) Types.prod
125  List.list -> (AST.ident, Cminor_syntax.internal_function AST.fundef)
126  Types.prod List.list
127
128val empty_vars :
129  ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
130  List.list -> ((AST.ident, AST.region) Types.prod, Nat.nat) Types.prod
131  List.list
132
133val replace_init :
134  CostLabel.costlabel -> Cminor_syntax.cminor_program ->
135  Cminor_syntax.cminor_noinit_program
136
Note: See TracBrowser for help on using the repository browser.