Changeset 2733


Ignore:
Timestamp:
Feb 25, 2013, 11:04:57 PM (6 years ago)
Author:
sacerdot
Message:

All axioms in set_adt implemented by hand.

Location:
extracted
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • extracted/PROBLEMS

    r2730 r2733  
    2828
    2929a) two in compiler.ml (the backend and the compiler itself)
     30b) set_adt currently implemented by cut&paste from OCaml's set.ml, but
     31   using Pervasives.compare: the equality function taken in input is ignored!
  • extracted/set_adt.ml

    r2731 r2733  
     1(* Copied from OCaml's set.ml *)
     2
    13    type 'a set = Empty | Node of 'a set * 'a * 'a set * int
    24
     
    4749         if c < 0 then bal (add x l) v r else bal l v (add x r)
    4850
     51    let rec min_elt = function
     52        Empty -> raise Not_found
     53      | Node(Empty, v, r, _) -> v
     54      | Node(l, v, r, _) -> min_elt l
     55
     56    let rec remove_min_elt = function
     57        Empty -> invalid_arg "Set.remove_min_elt"
     58      | Node(Empty, v, r, _) -> r
     59      | Node(l, v, r, _) -> bal (remove_min_elt l) v r
     60
     61    let merge t1 t2 =
     62      match (t1, t2) with
     63        (Empty, t) -> t
     64      | (t, Empty) -> t
     65      | (_, _) -> bal t1 (min_elt t2) (remove_min_elt t2)
     66
     67    let rec join l v r =
     68      match (l, r) with
     69        (Empty, _) -> add v r
     70      | (_, Empty) -> add v l
     71      | (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) ->
     72          if lh > rh + 2 then bal ll lv (join lr v r) else
     73          if rh > lh + 2 then bal (join l v rl) rv rr else
     74          create l v r
     75
     76    let rec split x = function
     77        Empty ->
     78          (Empty, false, Empty)
     79      | Node(l, v, r, _) ->
     80          let c = compare x v in
     81          if c = 0 then (l, true, r)
     82          else if c < 0 then
     83            let (ll, pres, rl) = split x l in (ll, pres, join rl v r)
     84          else
     85            let (lr, pres, rr) = split x r in (join l v lr, pres, rr)
     86
     87    let rec union s1 s2 =
     88      match (s1, s2) with
     89        (Empty, t2) -> t2
     90      | (t1, Empty) -> t1
     91      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
     92          if h1 >= h2 then
     93            if h2 = 1 then add v2 s1 else begin
     94              let (l2, _, r2) = split v1 s2 in
     95              join (union l1 l2) v1 (union r1 r2)
     96            end
     97          else
     98            if h1 = 1 then add v1 s2 else begin
     99              let (l1, _, r1) = split v2 s1 in
     100              join (union l1 l2) v2 (union r1 r2)
     101            end
     102
     103    let concat t1 t2 =
     104      match (t1, t2) with
     105        (Empty, t) -> t
     106      | (t, Empty) -> t
     107      | (_, _) -> join t1 (min_elt t2) (remove_min_elt t2)
     108
     109    let rec mem x = function
     110        Empty -> false
     111      | Node(l, v, r, _) ->
     112          let c = compare x v in
     113          c = 0 || mem x (if c < 0 then l else r)
     114
     115    let rec for_all p = function
     116        Empty -> true
     117      | Node(l, v, r, _) -> p v && for_all p l && for_all p r
     118
     119    let rec exists p = function
     120        Empty -> false
     121      | Node(l, v, r, _) -> p v || exists p l || exists p r
     122
     123    let rec subset s1 s2 =
     124      match (s1, s2) with
     125        Empty, _ ->
     126          true
     127      | _, Empty ->
     128          false
     129      | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
     130          let c = compare v1 v2 in
     131          if c = 0 then
     132            subset l1 l2 && subset r1 r2
     133          else if c < 0 then
     134            subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
     135          else
     136            subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
     137
     138    let rec diff s1 s2 =
     139      match (s1, s2) with
     140        (Empty, t2) -> Empty
     141      | (t1, Empty) -> t1
     142      | (Node(l1, v1, r1, _), t2) ->
     143          match split v1 t2 with
     144            (l2, false, r2) ->
     145              join (diff l1 l2) v1 (diff r1 r2)
     146          | (l2, true, r2) ->
     147              concat (diff l1 l2) (diff r1 r2)
     148
     149    type 'a enumeration = End | More of 'a * 'a set * 'a enumeration
     150
     151    let rec cons_enum s e =
     152      match s with
     153        Empty -> e
     154      | Node(l, v, r, _) -> cons_enum l (More(v, r, e))
     155
     156    let rec compare_aux e1 e2 =
     157        match (e1, e2) with
     158        (End, End) -> 0
     159      | (End, _)  -> -1
     160      | (_, End) -> 1
     161      | (More(v1, r1, e1), More(v2, r2, e2)) ->
     162          let c = compare v1 v2 in
     163          if c <> 0
     164          then c
     165          else compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
     166
     167    let compare s1 s2 =
     168      compare_aux (cons_enum s1 End) (cons_enum s2 End)
     169
     170    let equal s1 s2 =
     171      compare s1 s2 = 0
     172
     173    let matitabool_of_bool b = if b then Bool.True else Bool.False
     174
    49175(** val set_empty : 'a1 set0 **)
    50176let set_empty = Empty
    51177
    52 (** val set_size : 'a1 set0 -> Nat.nat **)
    53 let set_size _ =
    54   failwith "AXIOM TO BE REALIZED"
    55 
    56 (** val set_to_list : 'a1 set0 -> 'a1 List.list **)
    57 let set_to_list _ =
    58   failwith "AXIOM TO BE REALIZED"
    59 
    60 (** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **)
    61 let set_insert = add
    62 
    63 (** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **)
    64 let set_remove _ =
    65   failwith "AXIOM TO BE REALIZED"
    66 
    67178(** val set_member :
    68179    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
    69 let set_member _ =
    70   failwith "AXIOM TO BE REALIZED"
    71 
    72 (** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
    73 let set_forall _ =
    74   failwith "AXIOM TO BE REALIZED"
    75 
    76 (** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
    77 let set_exists _ =
    78   failwith "AXIOM TO BE REALIZED"
    79 
    80 (** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **)
    81 let set_filter _ =
    82   failwith "AXIOM TO BE REALIZED"
    83 
    84 (** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **)
    85 let set_map _ =
    86   failwith "AXIOM TO BE REALIZED"
    87 
    88 (** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **)
    89 let set_fold _ =
    90   failwith "AXIOM TO BE REALIZED"
     180let set_member _ x s = matitabool_of_bool (mem x s)
    91181
    92182(** val set_equal :
    93183    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    94 let set_equal _ =
    95   failwith "AXIOM TO BE REALIZED"
     184let set_equal _ s1 s2 = matitabool_of_bool (equal s1 s2)
    96185
    97186(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    98 let set_diff _ =
    99   failwith "AXIOM TO BE REALIZED"
    100 
    101 (** val set_is_empty : 'a1 set0 -> Bool.bool **)
    102 let set_is_empty set1 =
    103   Util.eq_nat (set_size set1) Nat.O
     187let set_diff = diff
    104188
    105189(** val set_singleton : 'a1 -> 'a1 set0 **)
    106190let set_singleton elt =
    107   set_insert elt set_empty
     191  add elt set_empty
    108192
    109193(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
    110194let set_from_list the_list =
    111   List.foldr set_insert set_empty the_list
    112 
    113 (** val set_split :
    114     ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod **)
    115 let set_split pred0 the_set =
    116   let left = set_filter pred0 the_set in
    117   let npred = fun x -> Bool.notb (pred0 x) in
    118   let right = set_filter npred the_set in
    119   { Types.fst = left; Types.snd = right }
     195  List.foldr add set_empty the_list
    120196
    121197(** val set_subset :
    122198    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    123 let set_subset eq left right =
    124   set_forall (fun elt -> set_member eq elt right) left
    125 
    126 (** val set_subseteq :
    127     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    128 let set_subseteq eq left right =
    129   Bool.andb (set_equal eq left right) (set_subset eq left right)
     199let set_subset _ s1 s2 = matitabool_of_bool (subset s1 s2)
    130200
    131201(** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    132 let set_union left right =
    133   set_fold set_insert left right
    134 
    135 (** val set_intersection :
    136     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    137 let set_intersection eq left right =
    138   set_filter (fun elt -> set_member eq elt right) left
     202let set_union = union
  • extracted/set_adt.mli

    r2730 r2733  
    33val set_empty : 'a1 set
    44
    5 val set_size : 'a1 set -> Nat.nat
    6 
    7 val set_to_list : 'a1 set -> 'a1 List.list
    8 
    9 val set_insert : 'a1 -> 'a1 set -> 'a1 set
    10 
    11 val set_remove : 'a1 -> 'a1 set -> 'a1 set
    12 
    135val set_member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set -> Bool.bool
    14 
    15 val set_forall : ('a1 -> Bool.bool) -> 'a1 set -> Bool.bool
    16 
    17 val set_exists : ('a1 -> Bool.bool) -> 'a1 set -> Bool.bool
    18 
    19 val set_filter : ('a1 -> Bool.bool) -> 'a1 set -> 'a1 set
    20 
    21 val set_map : ('a1 -> 'a2) -> 'a1 set -> 'a2 set
    22 
    23 val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set -> 'a2 -> 'a2
    246
    257val set_equal :
     
    2810val set_diff : 'a1 set -> 'a1 set -> 'a1 set
    2911
    30 val set_is_empty : 'a1 set -> Bool.bool
    31 
    3212val set_singleton : 'a1 -> 'a1 set
    3313
    3414val set_from_list : 'a1 List.list -> 'a1 set
    3515
    36 val set_split :
    37   ('a1 -> Bool.bool) -> 'a1 set -> ('a1 set, 'a1 set) Types.prod
    38 
    3916val set_subset :
    4017  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
    4118
    42 val set_subseteq :
    43   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
    44 
    4519val set_union : 'a1 set -> 'a1 set -> 'a1 set
    46 
    47 val set_intersection :
    48   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> 'a1 set
    49 
Note: See TracChangeset for help on using the changeset viewer.