Changeset 2718


Ignore:
Timestamp:
Feb 23, 2013, 1:19:21 AM (6 years ago)
Author:
sacerdot
Message:

set_empty turned from a value to a function because it is not implemented yet

Location:
extracted
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • extracted/liveness.ml

    r2717 r2718  
    116116let register_lattice =
    117117  { Fixpoints.l_bottom =
    118     (Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
    119       Set_adt.set_empty }); Fixpoints.l_equal = (fun left right ->
     118    (Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
     119      Set_adt.set_empty () }); Fixpoints.l_equal = (fun left right ->
    120120    Bool.andb
    121121      (Set_adt.set_equal
     
    140140let rl_psingleton r =
    141141  Obj.magic { Types.fst = (Set_adt.set_singleton r); Types.snd =
    142     Set_adt.set_empty }
     142    Set_adt.set_empty () }
    143143
    144144(** val rl_hsingleton : I8051.register -> __ **)
    145145let rl_hsingleton r =
    146   Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
     146  Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
    147147    (Set_adt.set_singleton r) }
    148148
     
    167167   | Joint.COST_LABEL clabel -> rl_bottom
    168168   | Joint.CALL (x, x0, x1) ->
    169      Obj.magic { Types.fst = Set_adt.set_empty; Types.snd =
     169     Obj.magic { Types.fst = Set_adt.set_empty (); Types.snd =
    170170       (Set_adt.set_from_list I8051.registerCallerSaved) }
    171171   | Joint.COND (r, lbl_true) -> rl_bottom
     
    238238   | Joint.COST_LABEL clabel -> Obj.magic rl_bottom
    239239   | Joint.CALL (x, nparams, x0) ->
    240      { Types.fst = Set_adt.set_empty; Types.snd =
     240     { Types.fst = Set_adt.set_empty (); Types.snd =
    241241       (Set_adt.set_from_list
    242242         (Util.prefix (Obj.magic nparams) I8051.registerParams)) }
     
    297297   | Joint.GOTO l -> Obj.magic rl_bottom
    298298   | Joint.RETURN ->
    299      { Types.fst = Set_adt.set_empty; Types.snd =
     299     { Types.fst = Set_adt.set_empty (); Types.snd =
    300300       (Set_adt.set_union (Set_adt.set_from_list I8051.registerCalleeSaved)
    301301         ret_regs) }
  • extracted/set_adt.ml

    r2717 r2718  
    128128
    129129(** val set_empty : 'a1 set0 **)
    130 let set_empty =
     130let set_empty _ =
    131131  failwith "AXIOM TO BE REALIZED"
    132132
     
    187187(** val set_singleton : 'a1 -> 'a1 set0 **)
    188188let set_singleton elt =
    189   set_insert elt set_empty
     189  set_insert elt (set_empty ())
    190190
    191191(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
    192192let set_from_list the_list =
    193   List.foldr set_insert set_empty the_list
     193  List.foldr set_insert (set_empty ()) the_list
    194194
    195195(** val set_split :
  • extracted/set_adt.mli

    r2717 r2718  
    7777val set_jmdiscr : 'a1 set0 -> 'a1 set0 -> __
    7878
    79 val set_empty : 'a1 set0
     79val set_empty : unit -> 'a1 set0
    8080
    8181val set_size : 'a1 set0 -> Nat.nat
Note: See TracChangeset for help on using the changeset viewer.