Changeset 2731


Ignore:
Timestamp:
Feb 25, 2013, 10:17:34 PM (6 years ago)
Author:
sacerdot
Message:

Minimal set of axioms implemented to make the driver run.

Location:
extracted
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • extracted/build

    r2620 r2731  
    33# Uses a GNU sed extension
    44ls *.ml | sed -e 's/\(.\)\(.*\)\.ml/\U\1\E\2/' > extracted.mlpack
    5 ocamlbuild extracted.cmo
     5ocamlbuild -cflag -g extracted.cmo
  • extracted/compiler.ml

    r2730 r2731  
    271271
    272272(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
    273 let compute_fixpoint =
     273let compute_fixpoint _ =
    274274  failwith "AXIOM TO BE REALIZED"
    275275
    276276(** val colour_graph : Interference.coloured_graph_computer **)
    277 let colour_graph =
     277let colour_graph _ =
    278278  failwith "AXIOM TO BE REALIZED"
    279279
  • extracted/set_adt.ml

    r2730 r2731  
    1 type 'x set (* AXIOM TO BE REALIZED *)
     1    type 'a set = Empty | Node of 'a set * 'a * 'a set * int
     2
     3    let height = function
     4        Empty -> 0
     5      | Node(_, _, _, h) -> h
     6
     7    let create l v r =
     8      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
     9      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
     10      Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
     11
     12    let bal l v r =
     13      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
     14      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
     15      if hl > hr + 2 then begin
     16        match l with
     17          Empty -> invalid_arg "Set.bal"
     18        | Node(ll, lv, lr, _) ->
     19            if height ll >= height lr then
     20              create ll lv (create lr v r)
     21            else begin
     22              match lr with
     23                Empty -> invalid_arg "Set.bal"
     24              | Node(lrl, lrv, lrr, _)->
     25                  create (create ll lv lrl) lrv (create lrr v r)
     26            end
     27      end else if hr > hl + 2 then begin
     28        match r with
     29          Empty -> invalid_arg "Set.bal"
     30        | Node(rl, rv, rr, _) ->
     31            if height rr >= height rl then
     32              create (create l v rl) rv rr
     33            else begin
     34              match rl with
     35                Empty -> invalid_arg "Set.bal"
     36              | Node(rll, rlv, rlr, _) ->
     37                  create (create l v rll) rlv (create rlr rv rr)
     38            end
     39      end else
     40        Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
     41
     42    let rec add x = function
     43       Empty -> Node(Empty, x, Empty, 1)
     44     | Node(l, v, r, _) as t ->
     45         let c = compare x v in
     46         if c = 0 then t else
     47         if c < 0 then bal (add x l) v r else bal l v (add x r)
    248
    349(** val set_empty : 'a1 set0 **)
    4 let set_empty =
    5   failwith "AXIOM TO BE REALIZED"
     50let set_empty = Empty
    651
    752(** val set_size : 'a1 set0 -> Nat.nat **)
    8 let set_size =
     53let set_size _ =
    954  failwith "AXIOM TO BE REALIZED"
    1055
    1156(** val set_to_list : 'a1 set0 -> 'a1 List.list **)
    12 let set_to_list =
     57let set_to_list _ =
    1358  failwith "AXIOM TO BE REALIZED"
    1459
    1560(** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **)
    16 let set_insert =
    17   failwith "AXIOM TO BE REALIZED"
     61let set_insert = add
    1862
    1963(** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **)
    20 let set_remove =
     64let set_remove _ =
    2165  failwith "AXIOM TO BE REALIZED"
    2266
    2367(** val set_member :
    2468    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
    25 let set_member =
     69let set_member _ =
    2670  failwith "AXIOM TO BE REALIZED"
    2771
    2872(** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
    29 let set_forall =
     73let set_forall _ =
    3074  failwith "AXIOM TO BE REALIZED"
    3175
    3276(** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
    33 let set_exists =
     77let set_exists _ =
    3478  failwith "AXIOM TO BE REALIZED"
    3579
    3680(** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **)
    37 let set_filter =
     81let set_filter _ =
    3882  failwith "AXIOM TO BE REALIZED"
    3983
    4084(** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **)
    41 let set_map =
     85let set_map _ =
    4286  failwith "AXIOM TO BE REALIZED"
    4387
    4488(** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **)
    45 let set_fold =
     89let set_fold _ =
    4690  failwith "AXIOM TO BE REALIZED"
    4791
    4892(** val set_equal :
    4993    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    50 let set_equal =
     94let set_equal _ =
    5195  failwith "AXIOM TO BE REALIZED"
    5296
    5397(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    54 let set_diff =
     98let set_diff _ =
    5599  failwith "AXIOM TO BE REALIZED"
    56100
     
    93137let set_intersection eq left right =
    94138  set_filter (fun elt -> set_member eq elt right) left
    95 
Note: See TracChangeset for help on using the changeset viewer.