Changeset 2746 for extracted/compiler.ml


Ignore:
Timestamp:
Feb 27, 2013, 10:46:33 PM (7 years ago)
Author:
sacerdot
Message:
  1. debugging code in glue
  2. updated version
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2743 r2746  
    337337open ASMCostsSplit
    338338
     339type strong_decidable = (__, __) Types.sum
     340
     341(** val strong_decidable_in_codomain :
     342    Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
     343    strong_decidable **)
     344let 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
    339355(** val compile :
    340356    Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
     
    351367        let k' =
    352368          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
    355376        in
    356377        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
Note: See TracChangeset for help on using the changeset viewer.