Changeset 2746 for extracted


Ignore:
Timestamp:
Feb 27, 2013, 10:46:33 PM (7 years ago)
Author:
sacerdot
Message:
  1. debugging code in glue
  2. updated version
Location:
extracted
Files:
5 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;
  • extracted/compiler.mli

    r2743 r2746  
    295295open ASMCostsSplit
    296296
     297type strong_decidable = (__, __) Types.sum
     298
     299val strong_decidable_in_codomain :
     300  Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
     301  strong_decidable
     302
    297303val compile :
    298304  Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
  • extracted/policy.ml

    r2717 r2746  
    101101   | Nat.S m ->
    102102     (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
    106105       (fun _ ->
    107106       (match z with
     
    111110          (fun _ ->
    112111            match no_ch with
    113             | Bool.True -> Types.pi1 (jump_expansion_internal program0 m)
     112            | Bool.True -> res1
    114113            | Bool.False ->
    115114              Types.pi1
  • extracted/untrusted/glue.ml

    r2742 r2746  
    2626 else if n < 0 then assert false
    2727 else Nat.S (matitanat_of_int (n-1))
     28
     29let 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  
    66
    77val matitanat_of_int : int -> Nat.nat
     8
     9val int_of_matitanat : Nat.nat -> int
Note: See TracChangeset for help on using the changeset viewer.