97 open Hints_declaration
109 (** val reverse_label_map :
110 RTLabs_syntax.statement Graphs.graph -> PreIdentifiers.identifier
111 Identifiers.identifier_map Types.option **)
112 let reverse_label_map g =
113 Identifiers.foldi PreIdentifiers.LabelTag (fun l s m ->
115 | Types.None -> Types.None
117 (match CostSpec.cost_label_of s with
118 | Types.None -> Types.Some m0
120 (match Identifiers.lookup PreIdentifiers.CostTag m0 cl with
122 Types.Some (Identifiers.add PreIdentifiers.CostTag m0 cl l)
123 | Types.Some x -> Types.None))) g (Types.Some
124 (Identifiers.empty_map PreIdentifiers.CostTag))
126 (** val check_fun_inj : RTLabs_syntax.internal_function -> Bool.bool **)
127 let check_fun_inj f =
128 match reverse_label_map f.RTLabs_syntax.f_graph with
129 | Types.None -> Bool.False
130 | Types.Some x -> Bool.True
132 (** val check_program_cost_injectivity :
133 RTLabs_syntax.rTLabs_program -> Bool.bool **)
134 let check_program_cost_injectivity p =
136 match x.Types.snd with
137 | AST.Internal f -> check_fun_inj f
138 | AST.External x0 -> Bool.True) p.AST.prog_funct
140 (** val check_program_cost_injectivity_prf :
141 RTLabs_syntax.rTLabs_program -> __ Errors.res **)
142 let check_program_cost_injectivity_prf p =
143 (match check_program_cost_injectivity p with
144 | Bool.True -> (fun _ -> Errors.OK __)
146 (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadCostLabelling))) __