- Timestamp:
- Feb 27, 2013, 10:46:33 PM (7 years ago)
- Location:
- extracted
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
extracted/compiler.ml
r2743 r2746 337 337 open ASMCostsSplit 338 338 339 type strong_decidable = (__, __) Types.sum 340 341 (** val strong_decidable_in_codomain : 342 Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ -> 343 strong_decidable **) 344 let strong_decidable_in_codomain a0 n m = 345 BitVectorTrie.bitVectorTrie_rect_Type0 (fun a' a1 -> 346 Bool.bool_inv_rect_Type0 (Deqsets.eqb a0 a' a1) (fun _ -> Types.Inl __) 347 (fun _ -> Types.Inr __)) (fun n0 l r hl hr a1 -> 348 match hl a1 with 349 | Types.Inl _ -> Types.Inl __ 350 | Types.Inr _ -> 351 (match hr a1 with 352 | Types.Inl _ -> Types.Inl __ 353 | Types.Inr _ -> Types.Inr __)) (fun n0 a1 -> Types.Inr __) n m 354 339 355 (** val compile : 340 356 Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod, … … 351 367 let k' = 352 368 lift_cost_map_back_to_front p' 353 (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false 354 (* absurd case *)) k 369 (Fetch.load_code_memory p4.Types.fst) p4.Types.snd 370 (Obj.magic 371 (strong_decidable_in_codomain 372 (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S 373 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 374 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 375 Nat.O)))))))))))))))) (Obj.magic p4).Types.snd)) k 355 376 in 356 377 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4; -
extracted/compiler.mli
r2743 r2746 295 295 open ASMCostsSplit 296 296 297 type strong_decidable = (__, __) Types.sum 298 299 val strong_decidable_in_codomain : 300 Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ -> 301 strong_decidable 302 297 303 val compile : 298 304 Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod, -
extracted/policy.ml
r2717 r2746 101 101 | Nat.S m -> 102 102 (fun _ -> 103 (let { Types.fst = no_ch; Types.snd = z } = 104 Types.pi1 (jump_expansion_internal program0 m) 105 in 103 let res1 = Types.pi1 (jump_expansion_internal program0 m) in 104 (let { Types.fst = no_ch; Types.snd = z } = res1 in 106 105 (fun _ -> 107 106 (match z with … … 111 110 (fun _ -> 112 111 match no_ch with 113 | Bool.True -> Types.pi1 (jump_expansion_internal program0 m)112 | Bool.True -> res1 114 113 | Bool.False -> 115 114 Types.pi1 -
extracted/untrusted/glue.ml
r2742 r2746 26 26 else if n < 0 then assert false 27 27 else Nat.S (matitanat_of_int (n-1)) 28 29 let rec int_of_matitanat = 30 function 31 Nat.O -> 0 32 | Nat.S n -> int_of_matitanat n + 1 -
extracted/untrusted/glue.mli
r2742 r2746 6 6 7 7 val matitanat_of_int : int -> Nat.nat 8 9 val int_of_matitanat : Nat.nat -> int
Note: See TracChangeset
for help on using the changeset viewer.