Calcom/arrayOL.ml

   1 open SPPoC;;
   2 (* fonctions auxiliaires *)
   3
   4 let build_string_vect var dim =
   5   let rec it n =
   6     if n > dim then []
   7     else (var^(string_of_int n))::(it (succ n))
   8   in it 1;;
   9
  10 let build_vect var dim =
  11   List.map Expr.read (build_string_vect var dim);;
  12
  13 let rec const_vect value dim =
  14   if dim = 0 then []
  15   else (Expr.read value)::(const_vect value (pred dim));;
  16
  17 let build_matrix var dim_i dim_j =
  18   let rec it n =
  19     if n > dim_i then []
  20     else (build_vect (var^(string_of_int n)^"_") dim_j)::(it (succ n))
  21   in it 1;;
  22
  23 let matrix_vect_mult m v =
  24   List.map (fun c -> Expr.add_list (List.map2 Expr.mult v c)) m;;
  25
  26 let int_vect l = List.map (fun i -> Expr.of_form (Form.of_int i)) l;;
  27
  28 let int_matrix l = List.map int_vect l;;
  29
  30 let (|+) v1 v2 = List.map2 Expr.add v1 v2 ;;
  31 let (|-) v1 v2 = List.map2 Expr.sub v1 v2 ;;
  32 let (|*) v1 v2 = List.map2 Expr.mult v1 v2 ;;
  33 let (|:) v1 v2 = List.map2 Expr.div v1 v2 ;;
  34 let (|/) v1 v2 = List.map2 Expr.quo v1 v2 ;;
  35 let (|%) v1 v2 = List.map2 Expr.modulo v1 v2 ;;
  36
  37 let (|>=) v1 v2 = List.map2 Ineq.build_ge v1 v2 ;;
  38 let (|<=) v1 v2 = List.map2 Ineq.build_le v1 v2 ;;
  39 let (|>) v1 v2 = List.map2 Ineq.build_gt v1 v2 ;;
  40 let (|<) v1 v2 = List.map2 Ineq.build_lt v1 v2 ;;
  41 let (|=) v1 v2 = List.map2 Ineq.build_eq v1 v2 ;;
  42
  43 (* construction de la description d'un motif
  44    - [var] est le point du motif
  45    - [init] est le point initial du motif
  46    - [index] est l'index dans le motif
  47    - [F] est la matrice d'ajustage
  48    - [sf] est le vecteur de taille du motif
  49    - [S] est la taille du tableau
  50 *)
  51 let make_pattern var init index dim =
  52   let index_vect = build_vect index dim
  53   and zero_vect = const_vect "0" dim
  54   and size_vect = build_vect "sf" dim
  55   and array_size_vect = build_vect "S" dim
  56   and fitting_matrix = build_matrix "F" dim dim
  57   and var_vect = build_vect var dim
  58   and init_vect = build_vect init dim
  59   in
  60     System.make
  61       ((index_vect |>= zero_vect)@
  62        (size_vect |> index_vect)@
  63        (var_vect |=
  64           ((init_vect |+ (matrix_vect_mult fitting_matrix index_vect))
  65            |% array_size_vect)));;
  66
  67 let make_pattern2 var init index dim =
  68   let index_vect = build_vect index dim
  69   and inf_vect = build_vect "-sf" dim
  70   and size_vect = build_vect "sf" dim
  71   and array_size_vect = build_vect "S" dim
  72   and fitting_matrix = build_matrix "F" dim dim
  73   and var_vect = build_vect var dim
  74   and init_vect = build_vect init dim
  75   in
  76     System.make
  77       ((index_vect |> inf_vect)@
  78        (size_vect |> index_vect)@
  79        (var_vect |=
  80           ((init_vect |+ (matrix_vect_mult fitting_matrix index_vect))
  81            |% array_size_vect)));;
  82
  83 (* construction de la description du pavage (calcul du point initial
  84    du motif)
  85    - [init] est le point initial du motif
  86    - [index] est l'indice de l'itérateur
  87    - [orig] est l'origine du pavage
  88    - [P] est la matrice de pavage
  89    - [sp] est la borne de l'itérateur
  90 *)
  91 let make_iterator init index dim =
  92   let init_vect = build_vect init dim
  93   and index_vect = build_vect index dim
  94   and orig_vect = build_vect "orig" dim
  95   and zero_vect = const_vect "0" dim
  96   and sup_vect = build_vect "sp" dim
  97   and paving_matrix = build_matrix "P" dim dim
  98   in
  99     System.make
 100       ((index_vect |>= zero_vect)@
 101        (index_vect |< sup_vect)@
 102        (init_vect |=
 103           (orig_vect |+ (matrix_vect_mult paving_matrix index_vect))));;
 104
 105 let make_iterator2 init index dim =
 106   let init_vect = build_vect init dim
 107   and index_vect = build_vect index dim
 108   and orig_vect = build_vect "orig" dim
 109   and inf_vect = build_vect "-sp" dim
 110   and sup_vect = build_vect "sp" dim
 111   and paving_matrix = build_matrix "P" dim dim
 112   in
 113     System.make
 114       ((index_vect |> inf_vect)@
 115        (index_vect |< sup_vect)@
 116        (init_vect |=
 117           (orig_vect |+ (matrix_vect_mult paving_matrix index_vect))));;
 118
 119 (* mise en commun des deux systèmes précédents pour décrire un point
 120 *)
 121 let make_point point paving_index init fitting_index dim =
 122   System.combine
 123     (make_iterator init paving_index dim)
 124     (make_pattern point init fitting_index dim);;
 125
 126 let make_point2 point paving_index init fitting_index dim =
 127   System.combine
 128     (make_iterator2 init paving_index dim)
 129     (make_pattern2 point init fitting_index dim);;
 130
 131 (* fonctions de définition des paramètres *)
 132 let def_array_size l =
 133   let dim = List.length l in
 134   let array_size_vect = build_vect "S" dim in
 135     System.make (array_size_vect |= l);;
 136
 137 let def_fitting_size l =
 138   let dim = List.length l in
 139   let pattern_size_vect = build_vect "sf" dim in
 140     System.make (pattern_size_vect |= l);;
 141
 142 let def_origin l =
 143   let dim = List.length l in
 144   let orig_vect = build_vect "orig" dim in
 145     System.make (orig_vect |= l);;
 146
 147 let def_paving_size l =
 148   let dim = List.length l in
 149   let paving_size_vect = build_vect "sp" dim in
 150     System.make (paving_size_vect |= l);;
 151
 152 let def_fitting l =
 153   let dim_i = List.length l
 154   and dim_j = List.length (List.hd l) in
 155     if dim_i <> dim_j then invalid_arg "non square matrix!";
 156     let fitting_matrix = build_matrix "F" dim_i dim_j in
 157       System.make ((List.flatten fitting_matrix) |=
 158                      (List.flatten l));;
 159
 160 let def_paving l =
 161   let dim_i = List.length l
 162   and dim_j = List.length (List.hd l) in
 163     if dim_i <> dim_j then invalid_arg "non square matrix!";
 164     let paving_matrix = build_matrix "P" dim_i dim_j in
 165       System.make ((List.flatten paving_matrix) |=
 166                      (List.flatten l));;
 167
 168 (* problème de non recouvrement *)
 169 let test_overlap
 170   (array_size, fitting, fitting_size, origin, paving, paving_size) =
 171   let dim = List.length (System.to_ineq_list array_size) in
 172   let x = build_vect "x" dim
 173   and i = build_vect "i" dim
 174   and j = build_vect "j" dim
 175   and k = build_vect "k" dim
 176   and x' = build_vect "x'" dim
 177   and i' = build_vect "i'" dim
 178   and j' = build_vect "j'" dim
 179   and k' = build_vect "k'" dim in
 180   let common =
 181     System.combine_list
 182       [array_size; fitting; fitting_size; origin; paving; paving_size;
 183        make_point "x" "i" "j" "k" dim;
 184        make_point "x'" "i'" "j'" "k'" dim;
 185        System.make (x |= x')] in
 186   let vars = (build_string_vect "x" dim)@
 187              (build_string_vect "x'" dim)@
 188              (build_string_vect "i" dim)@
 189              (build_string_vect "k" dim)@
 190              (build_string_vect "i'" dim)@
 191              (build_string_vect "k'" dim) in
 192   let rec lexico eqs = function
 193     | [] -> EQuast.of_quast Quast.bottom
 194     | (i,i')::r ->
 195         let res = PIP.solve (PIP.make
 196                                (System.simplify_vars vars
 197                                   (System.combine common
 198                                      (System.make
 199                                         ((Ineq.build_lt i i')::eqs))))
 200                                (Question.min_lex vars)) in
 201         if Quast.is_bottom (EQuast.get_quast res)
 202         then lexico ((Ineq.build_eq i i')::eqs) r
 203         else res in
 204     lexico [] (List.combine (i@k) (i'@k'));;
 205
 206 let test_overlap2
 207   (array_size, fitting, fitting_size, origin, paving, paving_size) =
 208   let dim = List.length (System.to_ineq_list array_size) in
 209   let x = build_vect "x" dim
 210   and i = build_vect "i" dim
 211   and j = build_vect "j" dim
 212   and k = build_vect "k" dim
 213   and z = const_vect "0" dim in
 214   let common =
 215     System.combine_list
 216       [array_size; fitting; fitting_size; origin; paving; paving_size;
 217        make_point2 "x" "i" "j" "k" dim;
 218        System.make (x |= z)] in
 219   let vars = (build_string_vect "i" dim)@
 220              (build_string_vect "k" dim) in
 221   let rec lexico eqs = function
 222     | [] -> EQuast.of_quast Quast.bottom
 223     | (is,i)::r as vl ->
 224         let v = fst (List.split vl) in
 225         let res = PIP.solve (PIP.make
 226                                (System.simplify_vars v
 227                                   (System.combine common
 228                                      (System.make
 229                                         ((Ineq.build_gt i <:e<0>>)::eqs))))
 230                                (Question.min_lex v)) in
 231         if Quast.is_bottom (EQuast.get_quast res)
 232         then lexico ((Ineq.build_eq i <:e<0>>)::eqs) r
 233         else res in
 234     lexico [] (List.combine vars (i@k));;
 235
 236 (* Easy QD definition and manipulation *)
 237
 238 type qd =
 239     {array_size : int list;
 240      fitting : int list list;
 241      fitting_size : int list;
 242      origin : int list;
 243      paving : int list list;
 244      paving_size : int list};;
 245
 246 let def_qd qd =
 247   let dim = List.length qd.array_size in
 248   let check_vect v =
 249     if List.length v <> dim then invalid_arg "def_qd"
 250     else int_vect v
 251   and check_matrix m =
 252     if List.length m <> dim or
 253       List.exists (fun v -> List.length v <> dim) m
 254     then invalid_arg "def_qd"
 255     else int_matrix m
 256   in
 257     (def_array_size (check_vect qd.array_size)),
 258     (def_fitting (check_matrix qd.fitting)),
 259     (def_fitting_size (check_vect qd.fitting_size)),
 260     (def_origin (check_vect qd.origin)),
 261     (def_paving (check_matrix qd.paving)),
 262     (def_paving_size (check_vect qd.paving_size));;
 263
 264 let overlap qd = test_overlap (def_qd qd);;
 265 let overlap2 qd = test_overlap2 (def_qd qd);;
 266
 267
 268
 269 (***********************)
 270 (*       T E S T       *)
 271 (***********************)
 272 let qdcompact = {array_size = [9;9];
 273                  fitting = [[1;0];[0;1]];
 274                  fitting_size = [3;3];
 275                  origin = [0;0];
 276                  paving = [[0;3];[3;0]];
 277                  paving_size = [3;3]};;
 278
 279 let qdtrous = {array_size = [10;10];
 280                fitting = [[2;0];[0;2]];
 281                fitting_size = [2;2];
 282                origin = [0;0];
 283                paving = [[0;3];[3;0]];
 284                paving_size = [4;4]};;
 285
 286 let qdoverlap = {array_size = [8;4];
 287                  fitting = [[0;1];[1;0]];
 288                  fitting_size = [4;1];
 289                  origin = [0;0];
 290                  paving = [[2;1];[1;2]];
 291                  paving_size = [4;4]};;
 292
 293 overlap2 qdcompact;;
 294 overlap qdcompact;;
 295 overlap2 qdtrous;;
 296 overlap qdtrous;;
 297 overlap2 qdoverlap;;
 298 overlap qdoverlap;;