Ignore:
Timestamp:
Oct 7, 2011, 1:48:26 PM (9 years ago)
Author:
tranquil
Message:

indexing branch is compiling again:

  • clight interpreter updated
  • clight labeller yet to be completed with single-entry loop detection
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051-indexed-labels-branch/src/common/costLabel.ml

    r1310 r1319  
    1212let sexpr_id = Sexpr(1, 0)
    1313
     14let const_sexpr n = Sexpr(0, n)
     15
    1416type index = int
    1517
     
    1820type indexing = sexpr list
    1921
    20 type const_indexing = int ref list
     22type const_indexing = int array
    2123
    2224(** [enter_loop n indexing] is used to update indexing when one is entering a
    2325    loop indexed by [n].
    2426                The function recycles the same constant indexing *)
    25 let rec enter_loop n indexing = match n, indexing with
    26         | None, _ -> indexing (* entering a multi-entry loop *)
    27         | Some 0, [] -> [ref 0] (* entering a single entry loop, current depth *)
    28         | Some 0, hd :: tl -> hd := 0; indexing (* as above, reusing slot *)
    29         | Some x, hd :: tl -> hd :: enter_loop (Some (x-1)) tl (* lower depth *)
    30         | Some x, [] -> assert false(* means I'm entering a single entry loop *)
    31                                     (* without having entered the one containing it *)       
     27let rec enter_loop n indexing = match n with
     28        | None -> ()
     29        | Some x -> indexing.(x) <- 0
    3230
    3331(** [enter_loop n indexing] is used to update indexing when one is continuing a
    3432    loop indexed by [n]. *)
    35 let rec continue_loop n indexing = match n, indexing with
    36         | None, _ -> indexing (* continuing a multi-entry loop *)
    37         | Some 0, hd :: tl -> hd := !hd + 1; indexing (* incrementing index *)
    38         | Some x, hd :: tl -> hd :: continue_loop (Some (x-1)) tl (* lower depth *)
    39         | Some _, [] -> assert false (* means I'm continuing a single entry loop *)
    40                                      (* without having entered it *)       
     33let rec continue_loop n indexing = match n with
     34        | None -> ()
     35        | Some x -> indexing.(x) <- indexing.(x) + 1
    4136
    4237let sexpr_of i l =
     
    4742      | Invalid_argument _ -> invalid_arg "costLabel.sexpr_of"
    4843
    49 let rec id_indexing = function
    50         | 0 -> []
    51         | n -> sexpr_id :: id_indexing (n-1)
     44let empty_indexing = []
     45
     46let add_id_indexing ind = sexpr_id :: ind
    5247
    5348(* a*_+b is composed with c*_+d by substitution: *)
     
    7065        | _ -> n 
    7166
    72 let rec compose_const_indexing c m = match c, m with
    73         | i1 :: l1, s2 :: l2 -> ev_sexpr !i1 s2 :: compose_const_indexing l1 l2
    74         | _, [] -> [] (* that's ok as current indexings will not be shrinked *)
    75         | [], _ -> assert false (* means an indexed label is not in the right ctx *)
     67let rec compose_const_indexing_i i c = function
     68        | [] -> []
     69        | s :: l ->
     70                const_sexpr (ev_sexpr c.(i) s) :: compose_const_indexing_i (i+1) c l
    7671
    7772module IndexingSet = Set.Make(struct
     
    8075        end)
    8176
    82 
    8377type t = {
    8478    name : Atom.t;
    8579    i : indexing
    8680}
     81
     82let apply_const_indexing c lbl =
     83    {lbl with i = compose_const_indexing_i 0 c lbl.i}
    8784
    8885
Note: See TracChangeset for help on using the changeset viewer.