Changeset 2717 for extracted/aSMCosts.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2649 r2717  
    55open LabelledObjects
    66
     7open BitVectorTrie
     8
     9open Exp
     10
    711open Arithmetic
    812
     
    7478
    7579open ASM
    76 
    77 open BitVectorTrie
    7880
    7981open Fetch
     
    141143| StructuredTraces.Tal_base_call (pre_fun_call, start_fun_call, final, x2) ->
    142144  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
    143 | StructuredTraces.Tal_base_tailcall (x, x0, x1, x4) ->
    144   assert false (* absurd case *)
     145| StructuredTraces.Tal_base_tailcall
     146    (pre_fun_call, start_fun_call, final, x1) ->
     147  Interpret.current_instruction_cost code_memory (Obj.magic pre_fun_call)
    145148| StructuredTraces.Tal_step_call
    146149    (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
     
    184187   | Nat.S program_size' ->
    185188     (fun _ ->
    186        (let { Types.fst = eta24805; Types.snd = ticks } =
     189       (let { Types.fst = eta31521; Types.snd = ticks } =
    187190          Fetch.fetch code_memory' program_counter'
    188191        in
    189192       let { Types.fst = instruction0; Types.snd = program_counter'' } =
    190          eta24805
     193         eta31521
    191194       in
    192195       (fun _ ->
     
    247250                          (block_cost' code_memory' jump_target program_size'
    248251                            cost_labels Bool.False)))
    249                   | ASM.JMP addr ->
    250                     (fun _ ->
    251                       Nat.plus ticks
    252                         (Types.pi1
    253                           (block_cost' code_memory' program_counter''
    254                             program_size' cost_labels Bool.False)))
    255252                  | ASM.MOVC (src, trgt) ->
    256253                    (fun _ ->
     
    428425                             (Types.pi1
    429426                               (block_cost' code_memory' program_counter''
     427                                 program_size' cost_labels Bool.False)))
     428                       | ASM.JMP addr ->
     429                         (fun _ ->
     430                           Nat.plus ticks
     431                             (Types.pi1
     432                               (block_cost' code_memory' program_counter''
    430433                                 program_size' cost_labels Bool.False)))) __))
    431434                  __))
     
    440443  let cost_of_block =
    441444    block_cost' code_memory program_counter0
    442       (Util.exponential (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S
     445      (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    443446        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    444         (Nat.S (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
     447        (Nat.S Nat.O))))))))))))))))) cost_labels Bool.True
    445448  in
    446449  cost_of_block
Note: See TracChangeset for help on using the changeset viewer.