 Timestamp:
 Feb 25, 2013, 10:17:34 PM (8 years ago)
 Location:
 extracted
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

extracted/build
r2620 r2731 3 3 # Uses a GNU sed extension 4 4 ls *.ml  sed e 's/\(.\)\(.*\)\.ml/\U\1\E\2/' > extracted.mlpack 5 ocamlbuild extracted.cmo5 ocamlbuild cflag g extracted.cmo 
extracted/compiler.ml
r2730 r2731 271 271 272 272 (** val compute_fixpoint : Fixpoints.fixpoint_computer **) 273 let compute_fixpoint =273 let compute_fixpoint _ = 274 274 failwith "AXIOM TO BE REALIZED" 275 275 276 276 (** val colour_graph : Interference.coloured_graph_computer **) 277 let colour_graph =277 let colour_graph _ = 278 278 failwith "AXIOM TO BE REALIZED" 279 279 
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) 2 48 3 49 (** val set_empty : 'a1 set0 **) 4 let set_empty = 5 failwith "AXIOM TO BE REALIZED" 50 let set_empty = Empty 6 51 7 52 (** val set_size : 'a1 set0 > Nat.nat **) 8 let set_size =53 let set_size _ = 9 54 failwith "AXIOM TO BE REALIZED" 10 55 11 56 (** val set_to_list : 'a1 set0 > 'a1 List.list **) 12 let set_to_list =57 let set_to_list _ = 13 58 failwith "AXIOM TO BE REALIZED" 14 59 15 60 (** val set_insert : 'a1 > 'a1 set0 > 'a1 set0 **) 16 let set_insert = 17 failwith "AXIOM TO BE REALIZED" 61 let set_insert = add 18 62 19 63 (** val set_remove : 'a1 > 'a1 set0 > 'a1 set0 **) 20 let set_remove =64 let set_remove _ = 21 65 failwith "AXIOM TO BE REALIZED" 22 66 23 67 (** val set_member : 24 68 ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set0 > Bool.bool **) 25 let set_member =69 let set_member _ = 26 70 failwith "AXIOM TO BE REALIZED" 27 71 28 72 (** val set_forall : ('a1 > Bool.bool) > 'a1 set0 > Bool.bool **) 29 let set_forall =73 let set_forall _ = 30 74 failwith "AXIOM TO BE REALIZED" 31 75 32 76 (** val set_exists : ('a1 > Bool.bool) > 'a1 set0 > Bool.bool **) 33 let set_exists =77 let set_exists _ = 34 78 failwith "AXIOM TO BE REALIZED" 35 79 36 80 (** val set_filter : ('a1 > Bool.bool) > 'a1 set0 > 'a1 set0 **) 37 let set_filter =81 let set_filter _ = 38 82 failwith "AXIOM TO BE REALIZED" 39 83 40 84 (** val set_map : ('a1 > 'a2) > 'a1 set0 > 'a2 set0 **) 41 let set_map =85 let set_map _ = 42 86 failwith "AXIOM TO BE REALIZED" 43 87 44 88 (** val set_fold : ('a1 > 'a2 > 'a2) > 'a1 set0 > 'a2 > 'a2 **) 45 let set_fold =89 let set_fold _ = 46 90 failwith "AXIOM TO BE REALIZED" 47 91 48 92 (** val set_equal : 49 93 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **) 50 let set_equal =94 let set_equal _ = 51 95 failwith "AXIOM TO BE REALIZED" 52 96 53 97 (** val set_diff : 'a1 set0 > 'a1 set0 > 'a1 set0 **) 54 let set_diff =98 let set_diff _ = 55 99 failwith "AXIOM TO BE REALIZED" 56 100 … … 93 137 let set_intersection eq left right = 94 138 set_filter (fun elt > set_member eq elt right) left 95
Note: See TracChangeset
for help on using the changeset viewer.