Changeset 2773 for extracted/uses.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/uses.ml

    r2742 r2773  
    99open LabelledObjects
    1010
     11open BitVectorTrie
     12
    1113open Graphs
    1214
     
    1618
    1719open Registers
    18 
    19 open BitVectorTrie
    2020
    2121open CostLabel
     
    3737open Extralib
    3838
    39 open Setoids
    40 
    41 open Monad
    42 
    43 open Option
    44 
    4539open Lists
    4640
     
    5650
    5751open Arithmetic
     52
     53open Setoids
     54
     55open Monad
     56
     57open Option
    5858
    5959open Extranat
     
    113113    Identifiers.identifier_map **)
    114114let examine_internal globals fun0 =
    115   let incr = fun r map1 ->
    116     match Identifiers.lookup0 PreIdentifiers.RegisterTag map1 r with
     115  let incr = fun r map ->
     116    match Identifiers.lookup PreIdentifiers.RegisterTag map r with
    117117    | Types.None ->
    118       Identifiers.add PreIdentifiers.RegisterTag map1 r Positive.One
     118      Identifiers.add PreIdentifiers.RegisterTag map r Positive.One
    119119    | Types.Some v ->
    120       Identifiers.add PreIdentifiers.RegisterTag map1 r (Positive.succ v)
     120      Identifiers.add PreIdentifiers.RegisterTag map r (Positive.succ v)
    121121  in
    122   let incr_arg = fun arg map1 ->
     122  let incr_arg = fun arg map ->
    123123    match arg with
    124     | Joint.Reg r -> incr r map1
    125     | Joint.Imm x -> map1
     124    | Joint.Reg r -> incr r map
     125    | Joint.Imm x -> map
    126126  in
    127   let f = fun x instr map1 ->
     127  let f = fun x instr map ->
    128128    match instr with
    129129    | Joint.Sequential (s, x0) ->
    130130      (match s with
    131        | Joint.COST_LABEL x1 -> map1
    132        | Joint.CALL (x1, x2, x3) -> map1
    133        | Joint.COND (r, x1) -> Obj.magic incr r map1
     131       | Joint.COST_LABEL x1 -> map
     132       | Joint.CALL (x1, x2, x3) -> map
     133       | Joint.COND (r, x1) -> Obj.magic incr r map
    134134       | Joint.Step_seq s0 ->
    135135         (match s0 with
    136           | Joint.COMMENT x1 -> map1
     136          | Joint.COMMENT x1 -> map
    137137          | Joint.MOVE pair ->
    138             let { Types.fst = r5; Types.snd = r6 } = Obj.magic pair in
    139             let incr_dst = fun arg map4 ->
     138            let { Types.fst = r1; Types.snd = r2 } = Obj.magic pair in
     139            let incr_dst = fun arg map0 ->
    140140              match arg with
    141               | ERTL.PSD r -> incr r map4
    142               | ERTL.HDW x1 -> map4
     141              | ERTL.PSD r -> incr r map0
     142              | ERTL.HDW x1 -> map0
    143143            in
    144             incr_dst r5
    145               (match r6 with
    146                | Joint.Reg a -> incr_dst a map1
    147                | Joint.Imm x1 -> map1)
    148           | Joint.POP r -> Obj.magic incr r map1
    149           | Joint.PUSH r -> Obj.magic incr_arg r map1
    150           | Joint.ADDRESS (x1, x3, x4) -> map1
    151           | Joint.OPACCS (x1, r5, r6, r7, r8) ->
    152             Obj.magic incr r5
    153               (Obj.magic incr r6
    154                 (Obj.magic incr_arg r7 (Obj.magic incr_arg r8 map1)))
    155           | Joint.OP1 (x1, r5, r6) ->
    156             Obj.magic incr r5 (Obj.magic incr r6 map1)
    157           | Joint.OP2 (x1, r5, r6, r7) ->
    158             Obj.magic incr r5
    159               (Obj.magic incr_arg r6 (Obj.magic incr_arg r7 map1))
    160           | Joint.CLEAR_CARRY -> map1
    161           | Joint.SET_CARRY -> map1
    162           | Joint.LOAD (r5, x1, x2) -> Obj.magic incr r5 map1
    163           | Joint.STORE (x1, x2, r) -> Obj.magic incr_arg r map1
     144            incr_dst r1
     145              (match r2 with
     146               | Joint.Reg a -> incr_dst a map
     147               | Joint.Imm x1 -> map)
     148          | Joint.POP r -> Obj.magic incr r map
     149          | Joint.PUSH r -> Obj.magic incr_arg r map
     150          | Joint.ADDRESS (x1, x3, x4) -> map
     151          | Joint.OPACCS (x1, r1, r2, r3, r4) ->
     152            Obj.magic incr r1
     153              (Obj.magic incr r2
     154                (Obj.magic incr_arg r3 (Obj.magic incr_arg r4 map)))
     155          | Joint.OP1 (x1, r1, r2) ->
     156            Obj.magic incr r1 (Obj.magic incr r2 map)
     157          | Joint.OP2 (x1, r1, r2, r3) ->
     158            Obj.magic incr r1
     159              (Obj.magic incr_arg r2 (Obj.magic incr_arg r3 map))
     160          | Joint.CLEAR_CARRY -> map
     161          | Joint.SET_CARRY -> map
     162          | Joint.LOAD (r1, x1, x2) -> Obj.magic incr r1 map
     163          | Joint.STORE (x1, x2, r) -> Obj.magic incr_arg r map
    164164          | Joint.Extension_seq s1 ->
    165165            (match Obj.magic s1 with
    166166             | ERTLptr.Ertlptr_ertl s2 ->
    167167               (match s2 with
    168                 | ERTL.Ertl_new_frame -> map1
    169                 | ERTL.Ertl_del_frame -> map1
    170                 | ERTL.Ertl_frame_size r -> incr r map1)
    171              | ERTLptr.LOW_ADDRESS (r, x1) -> incr r map1
    172              | ERTLptr.HIGH_ADDRESS (r, x1) -> incr r map1)))
    173     | Joint.Final x0 -> map1
     168                | ERTL.Ertl_new_frame -> map
     169                | ERTL.Ertl_del_frame -> map
     170                | ERTL.Ertl_frame_size r -> incr r map)
     171             | ERTLptr.LOW_ADDRESS (r, x1) -> incr r map
     172             | ERTLptr.HIGH_ADDRESS (r, x1) -> incr r map)))
     173    | Joint.Final x0 -> map
    174174    | Joint.FCOND (x0, x1, x2) -> assert false (* absurd case *)
    175175  in
    176   Identifiers.foldi0 PreIdentifiers.LabelTag f
     176  Identifiers.foldi PreIdentifiers.LabelTag f
    177177    (Obj.magic fun0.Joint.joint_if_code)
    178178    (Identifiers.empty_map PreIdentifiers.RegisterTag)
Note: See TracChangeset for help on using the changeset viewer.