source: extracted/costInj.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 2.2 KB
Line 
1open Preamble
2
3open Listb_extra
4
5open Executions
6
7open CostMisc
8
9open Deqsets_extra
10
11open CostSpec
12
13open Sets
14
15open Listb
16
17open StructuredTraces
18
19open Graphs
20
21open Order
22
23open Registers
24
25open FrontEndOps
26
27open RTLabs_syntax
28
29open SmallstepExec
30
31open BitVectorTrie
32
33open CostLabel
34
35open Events
36
37open IOMonad
38
39open IO
40
41open Extra_bool
42
43open Coqlib
44
45open Values
46
47open FrontEndVal
48
49open Hide
50
51open ByteValues
52
53open Division
54
55open Z
56
57open BitVectorZ
58
59open Pointers
60
61open GenMem
62
63open FrontEndMem
64
65open Proper
66
67open PositiveMap
68
69open Deqsets
70
71open Extralib
72
73open Lists
74
75open Identifiers
76
77open Exp
78
79open Arithmetic
80
81open Vector
82
83open Div_and_mod
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Extranat
92
93open Integers
94
95open AST
96
97open Globalenvs
98
99open ErrorMessages
100
101open Option
102
103open Setoids
104
105open Monad
106
107open Jmeq
108
109open Russell
110
111open Positive
112
113open PreIdentifiers
114
115open Errors
116
117open Bool
118
119open Relations
120
121open Nat
122
123open Hints_declaration
124
125open Core_notation
126
127open Pts
128
129open Logic
130
131open Types
132
133open List
134
135open RTLabs_semantics
136
137open RTLabs_abstract
138
139open RTLabs_traces
140
141(** val reverse_label_map :
142    RTLabs_syntax.statement Graphs.graph -> PreIdentifiers.identifier
143    Identifiers.identifier_map Types.option **)
144let reverse_label_map g0 =
145  Identifiers.foldi0 PreIdentifiers.LabelTag (fun l s m ->
146    match m with
147    | Types.None -> Types.None
148    | Types.Some m0 ->
149      (match CostSpec.cost_label_of s with
150       | Types.None -> Types.Some m0
151       | Types.Some cl ->
152         (match Identifiers.lookup0 PreIdentifiers.CostTag m0 cl with
153          | Types.None ->
154            Types.Some (Identifiers.add PreIdentifiers.CostTag m0 cl l)
155          | Types.Some x -> Types.None))) g0 (Types.Some
156    (Identifiers.empty_map PreIdentifiers.CostTag))
157
158(** val check_fun_inj : RTLabs_syntax.internal_function -> Bool.bool **)
159let check_fun_inj f =
160  match reverse_label_map f.RTLabs_syntax.f_graph with
161  | Types.None -> Bool.False
162  | Types.Some x -> Bool.True
163
164(** val check_program_cost_injectivity :
165    RTLabs_syntax.rTLabs_program -> Bool.bool **)
166let check_program_cost_injectivity p =
167  Lists.all0 (fun x ->
168    match x.Types.snd with
169    | AST.Internal f -> check_fun_inj f
170    | AST.External x0 -> Bool.True) p.AST.prog_funct
171
Note: See TracBrowser for help on using the repository browser.