Changeset 2717 for extracted/fetch.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 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/fetch.ml

    r2649 r2717  
    3636
    3737open BitVectorTrie
     38
     39open Exp
    3840
    3941open Arithmetic
     
    9698  (Types.pi1
    9799    (FoldStuff.foldl_strong program0 (fun prefix0 x tl _ labels_costs_ppc ->
    98       (let { Types.fst = eta24561; Types.snd = ppc } =
     100      (let { Types.fst = eta28757; Types.snd = ppc } =
    99101         Types.pi1 labels_costs_ppc
    100102       in
    101103      (fun _ ->
    102       (let { Types.fst = labels; Types.snd = costs } = eta24561 in
     104      (let { Types.fst = labels; Types.snd = costs } = eta28757 in
    103105      (fun _ ->
    104106      (let { Types.fst = label; Types.snd = instr } = x in
     
    121123              (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) cost costs
    122124        | ASM.Jmp x0 -> costs
     125        | ASM.Jnz (x0, x1, x2) -> costs
     126        | ASM.MovSuccessor (x0, x1, x2) -> costs
    123127        | ASM.Call x0 -> costs
    124128        | ASM.Mov (x0, x1) -> costs
     
    148152(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
    149153let bitvector_max_nat length0 =
    150   Util.exponential (Nat.S (Nat.S Nat.O)) length0
     154  Exp.exp (Nat.S (Nat.S Nat.O)) length0
    151155
    152156(** val code_memory_size : Nat.nat **)
     
    10121016                       (match b6 with
    10131017                        | Bool.True ->
    1014                           { Types.fst = { Types.fst = (ASM.JMP
    1015                             ASM.INDIRECT_DPTR); Types.snd = pc }; Types.snd =
    1016                             (Nat.S (Nat.S Nat.O)) }
     1018                          { Types.fst = { Types.fst = (ASM.RealInstruction
     1019                            (ASM.JMP ASM.INDIRECT_DPTR)); Types.snd = pc };
     1020                            Types.snd = (Nat.S (Nat.S Nat.O)) }
    10171021                        | Bool.False ->
    10181022                          prod_inv_rect_Type5 (next pmem pc)
Note: See TracChangeset for help on using the changeset viewer.