source: extracted/costCheck.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: 5.2 KB
Line 
1open Preamble
2
3open Graphs
4
5open Order
6
7open Registers
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open GenMem
16
17open FrontEndMem
18
19open Division
20
21open Z
22
23open BitVectorZ
24
25open Pointers
26
27open Coqlib
28
29open Values
30
31open FrontEndOps
32
33open BitVectorTrie
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open Exp
64
65open Arithmetic
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107open CostSpec
108
109open Extra_bool
110
111open Sets
112
113open Listb
114
115open Listb_extra
116
117open CostMisc
118
119(** val check_well_cost_fn : RTLabs_syntax.internal_function -> Bool.bool **)
120let check_well_cost_fn f =
121  Bool.andb
122    (Identifiers.idmap_all PreIdentifiers.LabelTag f.RTLabs_syntax.f_graph
123      (fun l s _ ->
124      CostSpec.well_cost_labelled_statement f.RTLabs_syntax.f_graph s))
125    (CostSpec.is_cost_label
126      (Identifiers.lookup_present PreIdentifiers.LabelTag
127        f.RTLabs_syntax.f_graph (Types.pi1 f.RTLabs_syntax.f_entry)))
128
129open Deqsets_extra
130
131(** val check_label_bounded :
132    RTLabs_syntax.statement Graphs.graph -> Graphs.label -> Graphs.label
133    List.list -> Identifiers.identifier_set -> Nat.nat ->
134    Identifiers.identifier_set Types.option **)
135let rec check_label_bounded g0 checking checking_tail to_check term_check =
136  let stop_now = Types.Some to_check in
137  (match term_check with
138   | Nat.O -> (fun _ -> assert false (* absurd case *))
139   | Nat.S term_check' ->
140     (fun _ ->
141       let st =
142         Identifiers.lookup_present PreIdentifiers.LabelTag g0 checking
143       in
144       let succs = CostSpec.successors st in
145       (match succs with
146        | List.Nil -> (fun _ -> stop_now)
147        | List.Cons (h, t) ->
148          (match t with
149           | List.Nil ->
150             (fun _ ->
151               let st' =
152                 Identifiers.lookup_present PreIdentifiers.LabelTag g0 h
153               in
154               (match CostSpec.is_cost_label st' with
155                | Bool.True -> stop_now
156                | Bool.False ->
157                  (match Identifiers.try_remove PreIdentifiers.LabelTag
158                           to_check h with
159                   | Types.None ->
160                     (fun _ ->
161                       match Bool.orb
162                               (Deqsets.eqb
163                                 (Identifiers.deq_identifier
164                                   PreIdentifiers.LabelTag) (Obj.magic h)
165                                 (Obj.magic checking))
166                               (Listb.memb
167                                 (Identifiers.deq_identifier
168                                   PreIdentifiers.LabelTag) (Obj.magic h)
169                                 (Obj.magic checking_tail)) with
170                       | Bool.True -> Types.None
171                       | Bool.False -> stop_now)
172                   | Types.Some to_check' ->
173                     (fun _ ->
174                       check_label_bounded g0 h (List.Cons (checking,
175                         checking_tail)) to_check'.Types.snd term_check')) __))
176           | List.Cons (x, x0) -> (fun _ -> stop_now))) __)) __
177
178(** val check_graph_bounded :
179    RTLabs_syntax.statement Graphs.graph -> Identifiers.identifier_set ->
180    Graphs.label -> Nat.nat -> Bool.bool **)
181let rec check_graph_bounded g0 to_check start term_check =
182  (match term_check with
183   | Nat.O -> (fun _ -> assert false (* absurd case *))
184   | Nat.S term_check' ->
185     (fun _ ->
186       (match check_label_bounded g0 start List.Nil to_check
187                (Identifiers.id_map_size PreIdentifiers.LabelTag g0) with
188        | Types.None -> (fun _ -> Bool.False)
189        | Types.Some to_check' ->
190          (fun _ ->
191            (match Identifiers.choose PreIdentifiers.LabelTag to_check' with
192             | Types.None -> (fun _ _ _ -> Bool.True)
193             | Types.Some l_to_check'' ->
194               (fun _ _ _ ->
195                 check_graph_bounded g0 l_to_check''.Types.snd
196                   l_to_check''.Types.fst.Types.fst term_check')) __ __ __))
197         __)) __
198
199(** val check_sound_cost_fn :
200    RTLabs_syntax.internal_function -> Bool.bool **)
201let check_sound_cost_fn fn =
202  (match Identifiers.try_remove PreIdentifiers.LabelTag
203           (Identifiers.id_set_of_map PreIdentifiers.LabelTag
204             fn.RTLabs_syntax.f_graph) (Types.pi1 fn.RTLabs_syntax.f_entry) with
205   | Types.None -> (fun _ -> assert false (* absurd case *))
206   | Types.Some to_check ->
207     (fun _ _ _ ->
208       check_graph_bounded fn.RTLabs_syntax.f_graph to_check.Types.snd
209         (Types.pi1 fn.RTLabs_syntax.f_entry)
210         (Identifiers.id_map_size PreIdentifiers.LabelTag
211           fn.RTLabs_syntax.f_graph))) __ __ __
212
213(** val check_cost_program : RTLabs_syntax.rTLabs_program -> Bool.bool **)
214let check_cost_program p =
215  Lists.all0 (fun fn ->
216    match fn.Types.snd with
217    | AST.Internal fn0 ->
218      Bool.andb (check_well_cost_fn fn0) (check_sound_cost_fn fn0)
219    | AST.External x -> Bool.True) p.AST.prog_funct
220
Note: See TracBrowser for help on using the repository browser.