Revision ca7ff3f7
Added by Lélio Brun 7 months ago
| src/utils/dimension.ml | ||
|---|---|---|
| 11 | 11 |
|
| 12 | 12 |
open Format |
| 13 | 13 |
|
| 14 |
type dim_expr = |
|
| 15 |
{mutable dim_desc: dim_desc;
|
|
| 16 |
dim_loc: Location.t; |
|
| 17 |
dim_id: int} |
|
| 14 |
type dim_expr = {
|
|
| 15 |
mutable dim_desc : dim_desc; |
|
| 16 |
dim_loc : Location.t; |
|
| 17 |
dim_id : int; |
|
| 18 |
} |
|
| 18 | 19 |
|
| 19 | 20 |
and dim_desc = |
| 20 |
| Dbool of bool |
|
| 21 |
| Dint of int
|
|
| 22 |
| Dident of Utils.ident |
|
| 23 |
| Dappl of Utils.ident * dim_expr list |
|
| 24 |
| Dite of dim_expr * dim_expr * dim_expr |
|
| 25 |
| Dlink of dim_expr |
|
| 26 |
| Dvar |
|
| 27 |
| Dunivar |
|
| 21 |
| Dbool of bool
|
|
| 22 |
| Dint of int
|
|
| 23 |
| Dident of Utils.ident
|
|
| 24 |
| Dappl of Utils.ident * dim_expr list
|
|
| 25 |
| Dite of dim_expr * dim_expr * dim_expr
|
|
| 26 |
| Dlink of dim_expr
|
|
| 27 |
| Dvar
|
|
| 28 |
| Dunivar
|
|
| 28 | 29 |
|
| 29 | 30 |
exception Unify of dim_expr * dim_expr |
| 31 |
|
|
| 30 | 32 |
exception InvalidDimension |
| 31 | 33 |
|
| 32 | 34 |
let new_id = ref (-1) |
| 33 | 35 |
|
| 34 | 36 |
let mkdim loc dim = |
| 35 | 37 |
incr new_id; |
| 36 |
{ dim_loc = loc;
|
|
| 37 |
dim_id = !new_id; |
|
| 38 |
dim_desc = dim;} |
|
| 38 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = dim }
|
|
| 39 | 39 |
|
| 40 | 40 |
let mkdim_var () = |
| 41 | 41 |
incr new_id; |
| 42 |
{ dim_loc = Location.dummy_loc;
|
|
| 43 |
dim_id = !new_id; |
|
| 44 |
dim_desc = Dvar;} |
|
| 42 |
{ dim_loc = Location.dummy_loc; dim_id = !new_id; dim_desc = Dvar }
|
|
| 45 | 43 |
|
| 46 | 44 |
let mkdim_ident loc id = |
| 47 | 45 |
incr new_id; |
| 48 |
{ dim_loc = loc;
|
|
| 49 |
dim_id = !new_id; |
|
| 50 |
dim_desc = Dident id;} |
|
| 46 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dident id }
|
|
| 51 | 47 |
|
| 52 | 48 |
let mkdim_bool loc b = |
| 53 | 49 |
incr new_id; |
| 54 |
{ dim_loc = loc;
|
|
| 55 |
dim_id = !new_id; |
|
| 56 |
dim_desc = Dbool b;} |
|
| 50 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dbool b }
|
|
| 57 | 51 |
|
| 58 | 52 |
let mkdim_int loc i = |
| 59 | 53 |
incr new_id; |
| 60 |
{ dim_loc = loc;
|
|
| 61 |
dim_id = !new_id; |
|
| 62 |
dim_desc = Dint i;} |
|
| 54 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dint i }
|
|
| 63 | 55 |
|
| 64 | 56 |
let mkdim_appl loc f args = |
| 65 | 57 |
incr new_id; |
| 66 |
{ dim_loc = loc;
|
|
| 67 |
dim_id = !new_id; |
|
| 68 |
dim_desc = Dappl (f, args);} |
|
| 58 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dappl (f, args) }
|
|
| 69 | 59 |
|
| 70 | 60 |
let mkdim_ite loc i t e = |
| 71 | 61 |
incr new_id; |
| 72 |
{ dim_loc = loc;
|
|
| 73 |
dim_id = !new_id; |
|
| 74 |
dim_desc = Dite (i, t, e);} |
|
| 62 |
{ dim_loc = loc; dim_id = !new_id; dim_desc = Dite (i, t, e) }
|
|
| 75 | 63 |
|
| 76 | 64 |
let rec pp_dimension fmt dim = |
| 77 |
(*fprintf fmt "<%d>" (Obj.magic dim: int);*) |
|
| 78 |
match dim.dim_desc with |
|
| 79 |
| Dident id -> |
|
| 80 |
fprintf fmt "%s" id |
|
| 81 |
| Dint i -> |
|
| 82 |
fprintf fmt "%d" i |
|
| 83 |
| Dbool b -> |
|
| 84 |
fprintf fmt "%B" b |
|
| 85 |
| Dite (i, t, e) -> |
|
| 86 |
fprintf fmt "if %a then %a else %a" |
|
| 87 |
pp_dimension i pp_dimension t pp_dimension e |
|
| 88 |
| Dappl (f, [arg]) -> |
|
| 89 |
fprintf fmt "(%s%a)" f pp_dimension arg |
|
| 90 |
| Dappl (f, [arg1; arg2]) -> |
|
| 91 |
fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 |
|
| 92 |
| Dappl (_, _) -> assert false |
|
| 93 |
| Dlink dim' -> fprintf fmt "%a" pp_dimension dim' |
|
| 94 |
| Dvar -> fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) |
|
| 95 |
| Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) |
|
| 65 |
(*fprintf fmt "<%d>" (Obj.magic dim: int);*) |
|
| 66 |
match dim.dim_desc with |
|
| 67 |
| Dident id -> |
|
| 68 |
fprintf fmt "%s" id |
|
| 69 |
| Dint i -> |
|
| 70 |
fprintf fmt "%d" i |
|
| 71 |
| Dbool b -> |
|
| 72 |
fprintf fmt "%B" b |
|
| 73 |
| Dite (i, t, e) -> |
|
| 74 |
fprintf fmt "if %a then %a else %a" pp_dimension i pp_dimension t |
|
| 75 |
pp_dimension e |
|
| 76 |
| Dappl (f, [ arg ]) -> |
|
| 77 |
fprintf fmt "(%s%a)" f pp_dimension arg |
|
| 78 |
| Dappl (f, [ arg1; arg2 ]) -> |
|
| 79 |
fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2 |
|
| 80 |
| Dappl (_, _) -> |
|
| 81 |
assert false |
|
| 82 |
| Dlink dim' -> |
|
| 83 |
fprintf fmt "%a" pp_dimension dim' |
|
| 84 |
| Dvar -> |
|
| 85 |
fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) |
|
| 86 |
| Dunivar -> |
|
| 87 |
fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) |
|
| 96 | 88 |
|
| 97 | 89 |
let rec multi_dimension_product loc dim_list = |
| 98 |
match dim_list with |
|
| 99 |
| [] -> mkdim_int loc 1 |
|
| 100 |
| [d] -> d |
|
| 101 |
| d::q -> mkdim_appl loc "*" [d; multi_dimension_product loc q] |
|
| 90 |
match dim_list with |
|
| 91 |
| [] -> |
|
| 92 |
mkdim_int loc 1 |
|
| 93 |
| [ d ] -> |
|
| 94 |
d |
|
| 95 |
| d :: q -> |
|
| 96 |
mkdim_appl loc "*" [ d; multi_dimension_product loc q ] |
|
| 102 | 97 |
|
| 103 | 98 |
(* Builds a dimension expr representing 0<=d *) |
| 104 |
let check_bound loc d = |
|
| 105 |
mkdim_appl loc "<=" [mkdim_int loc 0; d] |
|
| 99 |
let check_bound loc d = mkdim_appl loc "<=" [ mkdim_int loc 0; d ] |
|
| 106 | 100 |
|
| 107 | 101 |
(* Builds a dimension expr representing 0<=i<d *) |
| 108 | 102 |
let check_access loc d i = |
| 109 |
mkdim_appl loc "&&" |
|
| 110 |
[mkdim_appl loc "<=" [mkdim_int loc 0; i]; |
|
| 111 |
mkdim_appl loc "<" [i; d]] |
|
| 103 |
mkdim_appl loc "&&" |
|
| 104 |
[ mkdim_appl loc "<=" [ mkdim_int loc 0; i ]; mkdim_appl loc "<" [ i; d ] ] |
|
| 112 | 105 |
|
| 113 |
let rec repr dim = |
|
| 114 |
match dim.dim_desc with |
|
| 115 |
| Dlink dim' -> repr dim' |
|
| 116 |
| _ -> dim |
|
| 106 |
let rec repr dim = match dim.dim_desc with Dlink dim' -> repr dim' | _ -> dim |
|
| 117 | 107 |
|
| 118 | 108 |
let rec is_eq_dimension d1 d2 = |
| 119 | 109 |
let d1 = repr d1 in |
| 120 | 110 |
let d2 = repr d2 in |
| 121 |
d1.dim_id = d2.dim_id || |
|
| 111 |
d1.dim_id = d2.dim_id |
|
| 112 |
|| |
|
| 122 | 113 |
match d1.dim_desc, d2.dim_desc with |
| 123 | 114 |
| Dappl (f1, args1), Dappl (f2, args2) -> |
| 124 |
f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2 |
|
| 115 |
f1 = f2 |
|
| 116 |
&& List.length args1 = List.length args2 |
|
| 117 |
&& List.for_all2 is_eq_dimension args1 args2 |
|
| 125 | 118 |
| Dite (c1, t1, e1), Dite (c2, t2, e2) -> |
| 126 | 119 |
is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2 |
| 127 |
| Dint i1 , Dint i2 -> i1 = i2 |
|
| 128 |
| Dbool b1 , Dbool b2 -> b1 = b2 |
|
| 129 |
| Dident id1, Dident id2 -> id1 = id2 |
|
| 130 |
| _ -> false |
|
| 120 |
| Dint i1, Dint i2 -> |
|
| 121 |
i1 = i2 |
|
| 122 |
| Dbool b1, Dbool b2 -> |
|
| 123 |
b1 = b2 |
|
| 124 |
| Dident id1, Dident id2 -> |
|
| 125 |
id1 = id2 |
|
| 126 |
| _ -> |
|
| 127 |
false |
|
| 131 | 128 |
|
| 132 | 129 |
let is_dimension_const dim = |
| 133 |
match (repr dim).dim_desc with |
|
| 134 |
| Dint _ |
|
| 135 |
| Dbool _ -> true |
|
| 136 |
| _ -> false |
|
| 130 |
match (repr dim).dim_desc with Dint _ | Dbool _ -> true | _ -> false |
|
| 137 | 131 |
|
| 138 | 132 |
let size_const_dimension dim = |
| 139 | 133 |
match (repr dim).dim_desc with |
| 140 |
| Dint i -> i |
|
| 141 |
| Dbool b -> if b then 1 else 0 |
|
| 142 |
| _ -> (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false) |
|
| 134 |
| Dint i -> |
|
| 135 |
i |
|
| 136 |
| Dbool b -> |
|
| 137 |
if b then 1 else 0 |
|
| 138 |
| _ -> |
|
| 139 |
Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; |
|
| 140 |
assert false |
|
| 143 | 141 |
|
| 144 | 142 |
let rec is_polymorphic dim = |
| 145 | 143 |
match dim.dim_desc with |
| 146 |
| Dident _ |
|
| 147 |
| Dint _ |
|
| 148 |
| Dbool _ |
|
| 149 |
| Dvar -> false |
|
| 150 |
| Dite (i, t, e) -> |
|
| 151 |
is_polymorphic i || is_polymorphic t || is_polymorphic e |
|
| 152 |
| Dappl (_, args) -> List.exists is_polymorphic args |
|
| 153 |
| Dlink dim' -> is_polymorphic dim' |
|
| 154 |
| Dunivar -> true |
|
| 144 |
| Dident _ | Dint _ | Dbool _ | Dvar -> |
|
| 145 |
false |
|
| 146 |
| Dite (i, t, e) -> |
|
| 147 |
is_polymorphic i || is_polymorphic t || is_polymorphic e |
|
| 148 |
| Dappl (_, args) -> |
|
| 149 |
List.exists is_polymorphic args |
|
| 150 |
| Dlink dim' -> |
|
| 151 |
is_polymorphic dim' |
|
| 152 |
| Dunivar -> |
|
| 153 |
true |
|
| 155 | 154 |
|
| 156 | 155 |
(* Normalizes a dimension expression, i.e. canonicalize all polynomial |
| 157 |
sub-expressions, where unsupported operations (eg. '/') are treated |
|
| 158 |
as variables. |
|
| 159 |
*) |
|
| 156 |
sub-expressions, where unsupported operations (eg. '/') are treated as |
|
| 157 |
variables. *) |
|
| 160 | 158 |
|
| 161 | 159 |
let rec factors dim = |
| 162 | 160 |
match dim.dim_desc with |
| 163 |
| Dappl (f, args) when f = "*" -> List.flatten (List.map factors args) |
|
| 164 |
| _ -> [dim] |
|
| 161 |
| Dappl (f, args) when f = "*" -> |
|
| 162 |
List.flatten (List.map factors args) |
|
| 163 |
| _ -> |
|
| 164 |
[ dim ] |
|
| 165 | 165 |
|
| 166 | 166 |
let rec factors_constant fs = |
| 167 | 167 |
match fs with |
| 168 |
| [] -> 1 |
|
| 169 |
| f::q -> |
|
| 168 |
| [] -> |
|
| 169 |
1 |
|
| 170 |
| f :: q -> ( |
|
| 170 | 171 |
match f.dim_desc with |
| 171 |
| Dint i -> i * (factors_constant q) |
|
| 172 |
| _ -> factors_constant q |
|
| 172 |
| Dint i -> |
|
| 173 |
i * factors_constant q |
|
| 174 |
| _ -> |
|
| 175 |
factors_constant q) |
|
| 173 | 176 |
|
| 174 | 177 |
let norm_factors fs = |
| 175 | 178 |
let k = factors_constant fs in |
| 176 | 179 |
let nk = List.filter (fun d -> not (is_dimension_const d)) fs in |
| 177 |
(k, List.sort compare nk)
|
|
| 180 |
k, List.sort compare nk
|
|
| 178 | 181 |
|
| 179 | 182 |
let rec terms dim = |
| 180 |
match dim.dim_desc with |
|
| 181 |
| Dappl (f, args) when f = "+" -> List.flatten (List.map terms args) |
|
| 182 |
| _ -> [dim] |
|
| 183 |
|
|
| 184 |
let normalize dim = |
|
| 185 |
dim |
|
| 186 |
(* |
|
| 187 |
let rec unnormalize loc l = |
|
| 188 |
let l = List.sort (fun (k, l) (k', l') -> compare l l') (List.map (fun (k, l) -> (k, List.sort compare l)) l) in |
|
| 189 |
match l with |
|
| 190 |
| [] -> mkdim_int loc 0 |
|
| 191 |
| t::q -> |
|
| 192 |
List.fold_left (fun res (k, l) -> mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q |
|
| 193 |
*) |
|
| 194 |
let copy copy_dim_vars dim = |
|
| 195 |
let rec cp dim = |
|
| 196 | 183 |
match dim.dim_desc with |
| 197 |
| Dbool _ |
|
| 198 |
| Dint _ -> dim |
|
| 199 |
| Dident id -> mkdim_ident dim.dim_loc id |
|
| 200 |
| Dite (c, t, e) -> mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) |
|
| 201 |
| Dappl (id, args) -> mkdim_appl dim.dim_loc id (List.map cp args) |
|
| 202 |
| Dlink dim' -> cp dim' |
|
| 203 |
| Dunivar -> assert false |
|
| 204 |
| Dvar -> |
|
| 205 |
try |
|
| 206 |
List.assoc dim.dim_id !copy_dim_vars |
|
| 207 |
with Not_found -> |
|
| 208 |
let var = mkdim dim.dim_loc Dvar in |
|
| 209 |
copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars; |
|
| 210 |
var |
|
| 211 |
in cp dim |
|
| 184 |
| Dappl (f, args) when f = "+" -> |
|
| 185 |
List.flatten (List.map terms args) |
|
| 186 |
| _ -> |
|
| 187 |
[ dim ] |
|
| 188 |
|
|
| 189 |
let normalize dim = dim |
|
| 212 | 190 |
|
| 213 |
(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool |
|
| 214 |
constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified in-place. |
|
| 215 |
*) |
|
| 191 |
(* let rec unnormalize loc l = let l = List.sort (fun (k, l) (k', l') -> compare |
|
| 192 |
l l') (List.map (fun (k, l) -> (k, List.sort compare l)) l) in match l with | |
|
| 193 |
[] -> mkdim_int loc 0 | t::q -> List.fold_left (fun res (k, l) -> mkdim_appl |
|
| 194 |
loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q *) |
|
| 195 |
let copy copy_dim_vars dim = |
|
| 196 |
let rec cp dim = |
|
| 197 |
match dim.dim_desc with |
|
| 198 |
| Dbool _ | Dint _ -> |
|
| 199 |
dim |
|
| 200 |
| Dident id -> |
|
| 201 |
mkdim_ident dim.dim_loc id |
|
| 202 |
| Dite (c, t, e) -> |
|
| 203 |
mkdim_ite dim.dim_loc (cp c) (cp t) (cp e) |
|
| 204 |
| Dappl (id, args) -> |
|
| 205 |
mkdim_appl dim.dim_loc id (List.map cp args) |
|
| 206 |
| Dlink dim' -> |
|
| 207 |
cp dim' |
|
| 208 |
| Dunivar -> |
|
| 209 |
assert false |
|
| 210 |
| Dvar -> ( |
|
| 211 |
try List.assoc dim.dim_id !copy_dim_vars |
|
| 212 |
with Not_found -> |
|
| 213 |
let var = mkdim dim.dim_loc Dvar in |
|
| 214 |
copy_dim_vars := (dim.dim_id, var) :: !copy_dim_vars; |
|
| 215 |
var) |
|
| 216 |
in |
|
| 217 |
cp dim |
|
| 218 |
|
|
| 219 |
(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing |
|
| 220 |
only int and bool constructs, with conditionals. [eval_const] is a typing |
|
| 221 |
environment for static values. [eval_op] is an evaluation env for basic |
|
| 222 |
operators. The argument [dim] is modified in-place. *) |
|
| 216 | 223 |
let rec eval eval_op eval_const dim = |
| 217 | 224 |
match dim.dim_desc with |
| 218 |
| Dbool _ |
|
| 219 |
| Dint _ -> () |
|
| 220 |
| Dident id -> |
|
| 221 |
(match eval_const id with |
|
| 222 |
| Some val_dim -> dim.dim_desc <- Dlink val_dim |
|
| 223 |
| None -> (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension)) |
|
| 224 |
| Dite (c, t, e) -> |
|
| 225 |
begin |
|
| 226 |
eval eval_op eval_const c; |
|
| 227 |
eval eval_op eval_const t; |
|
| 228 |
eval eval_op eval_const e; |
|
| 229 |
match (repr c).dim_desc with |
|
| 230 |
| Dbool b -> dim.dim_desc <- Dlink (if b then t else e) |
|
| 231 |
| _ -> () |
|
| 232 |
end |
|
| 225 |
| Dbool _ | Dint _ -> |
|
| 226 |
() |
|
| 227 |
| Dident id -> ( |
|
| 228 |
match eval_const id with |
|
| 229 |
| Some val_dim -> |
|
| 230 |
dim.dim_desc <- Dlink val_dim |
|
| 231 |
| None -> |
|
| 232 |
Format.eprintf "invalid %a@." pp_dimension dim; |
|
| 233 |
raise InvalidDimension) |
|
| 234 |
| Dite (c, t, e) -> ( |
|
| 235 |
eval eval_op eval_const c; |
|
| 236 |
eval eval_op eval_const t; |
|
| 237 |
eval eval_op eval_const e; |
|
| 238 |
match (repr c).dim_desc with |
|
| 239 |
| Dbool b -> |
|
| 240 |
dim.dim_desc <- Dlink (if b then t else e) |
|
| 241 |
| _ -> |
|
| 242 |
()) |
|
| 233 | 243 |
| Dappl (id, args) -> |
| 234 |
begin |
|
| 235 |
List.iter (eval eval_op eval_const) args; |
|
| 236 |
if List.for_all is_dimension_const args |
|
| 237 |
then dim.dim_desc <- Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args) |
|
| 238 |
end |
|
| 244 |
List.iter (eval eval_op eval_const) args; |
|
| 245 |
if List.for_all is_dimension_const args then |
|
| 246 |
dim.dim_desc <- |
|
| 247 |
Env.lookup_value eval_op id (List.map (fun d -> (repr d).dim_desc) args) |
|
| 239 | 248 |
| Dlink dim' -> |
| 240 |
begin
|
|
| 241 |
eval eval_op eval_const dim';
|
|
| 242 |
dim.dim_desc <- Dlink (repr dim')
|
|
| 243 |
end
|
|
| 244 |
| Dvar -> ()
|
|
| 245 |
| Dunivar -> assert false
|
|
| 249 |
eval eval_op eval_const dim';
|
|
| 250 |
dim.dim_desc <- Dlink (repr dim')
|
|
| 251 |
| Dvar ->
|
|
| 252 |
()
|
|
| 253 |
| Dunivar ->
|
|
| 254 |
assert false
|
|
| 246 | 255 |
|
| 247 | 256 |
let uneval const univar = |
| 248 | 257 |
let univar = repr univar in |
| 249 | 258 |
match univar.dim_desc with |
| 250 |
| Dunivar -> univar.dim_desc <- Dident const |
|
| 251 |
| _ -> assert false |
|
| 259 |
| Dunivar -> |
|
| 260 |
univar.dim_desc <- Dident const |
|
| 261 |
| _ -> |
|
| 262 |
assert false |
|
| 252 | 263 |
|
| 253 | 264 |
(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in |
| 254 | 265 |
dimension expression [dim]. False otherwise. *) |
| 255 | 266 |
let rec occurs dvar dim = |
| 256 | 267 |
let dim = repr dim in |
| 257 | 268 |
match dim.dim_desc with |
| 258 |
| Dvar -> dim.dim_id = dvar.dim_id |
|
| 259 |
| Dident _ |
|
| 260 |
| Dint _ |
|
| 261 |
| Dbool _ |
|
| 262 |
| Dunivar -> false |
|
| 263 |
| Dite (i, t, e) -> |
|
| 264 |
occurs dvar i || occurs dvar t || occurs dvar e |
|
| 265 |
| Dappl (_, args) -> List.exists (occurs dvar) args |
|
| 266 |
| Dlink _ -> assert false |
|
| 267 |
|
|
| 268 |
(* Promote monomorphic dimension variables to polymorphic variables. |
|
| 269 |
Generalize by side-effects *) |
|
| 269 |
| Dvar -> |
|
| 270 |
dim.dim_id = dvar.dim_id |
|
| 271 |
| Dident _ | Dint _ | Dbool _ | Dunivar -> |
|
| 272 |
false |
|
| 273 |
| Dite (i, t, e) -> |
|
| 274 |
occurs dvar i || occurs dvar t || occurs dvar e |
|
| 275 |
| Dappl (_, args) -> |
|
| 276 |
List.exists (occurs dvar) args |
|
| 277 |
| Dlink _ -> |
|
| 278 |
assert false |
|
| 279 |
|
|
| 280 |
(* Promote monomorphic dimension variables to polymorphic variables. Generalize |
|
| 281 |
by side-effects *) |
|
| 270 | 282 |
let rec generalize dim = |
| 271 | 283 |
match dim.dim_desc with |
| 272 |
| Dvar -> dim.dim_desc <- Dunivar |
|
| 273 |
| Dident _ |
|
| 274 |
| Dint _ |
|
| 275 |
| Dbool _ |
|
| 276 |
| Dunivar -> () |
|
| 277 |
| Dite (i, t, e) -> |
|
| 278 |
generalize i; generalize t; generalize e |
|
| 279 |
| Dappl (_, args) -> List.iter generalize args |
|
| 280 |
| Dlink dim' -> generalize dim' |
|
| 281 |
|
|
| 282 |
(* Instantiate polymorphic dimension variables to monomorphic variables. |
|
| 283 |
Also duplicates the whole term structure (but the constant sub-terms). |
|
| 284 |
*) |
|
| 284 |
| Dvar -> |
|
| 285 |
dim.dim_desc <- Dunivar |
|
| 286 |
| Dident _ | Dint _ | Dbool _ | Dunivar -> |
|
| 287 |
() |
|
| 288 |
| Dite (i, t, e) -> |
|
| 289 |
generalize i; |
|
| 290 |
generalize t; |
|
| 291 |
generalize e |
|
| 292 |
| Dappl (_, args) -> |
|
| 293 |
List.iter generalize args |
|
| 294 |
| Dlink dim' -> |
|
| 295 |
generalize dim' |
|
| 296 |
|
|
| 297 |
(* Instantiate polymorphic dimension variables to monomorphic variables. Also |
|
| 298 |
duplicates the whole term structure (but the constant sub-terms). *) |
|
| 285 | 299 |
let rec instantiate inst_dim_vars dim = |
| 286 | 300 |
let dim = repr dim in |
| 287 | 301 |
match dim.dim_desc with |
| 288 |
| Dvar |
|
| 289 |
| Dident _ |
|
| 290 |
| Dint _ |
|
| 291 |
| Dbool _ -> dim |
|
| 292 |
| Dite (i, t, e) -> |
|
| 293 |
mkdim_ite dim.dim_loc |
|
| 294 |
(instantiate inst_dim_vars i) |
|
| 295 |
(instantiate inst_dim_vars t) |
|
| 296 |
(instantiate inst_dim_vars e) |
|
| 297 |
| Dappl (f, args) -> mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) |
|
| 298 |
| Dlink _ -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) |
|
| 299 |
| Dunivar -> |
|
| 300 |
try |
|
| 301 |
List.assoc dim.dim_id !inst_dim_vars |
|
| 302 |
with Not_found -> |
|
| 303 |
let var = mkdim dim.dim_loc Dvar in |
|
| 304 |
inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars; |
|
| 305 |
var |
|
| 306 |
|
|
| 307 |
(** destructive unification of [dim1] and [dim2]. |
|
| 308 |
Raises [Unify (t1,t2)] if the types are not unifiable. |
|
| 309 |
if [semi] unification is required, |
|
| 310 |
[dim1] should furthermore be an instance of [dim2] *) |
|
| 311 |
let unify ?(semi=false) dim1 dim2 = |
|
| 302 |
| Dvar | Dident _ | Dint _ | Dbool _ -> |
|
| 303 |
dim |
|
| 304 |
| Dite (i, t, e) -> |
|
| 305 |
mkdim_ite dim.dim_loc |
|
| 306 |
(instantiate inst_dim_vars i) |
|
| 307 |
(instantiate inst_dim_vars t) |
|
| 308 |
(instantiate inst_dim_vars e) |
|
| 309 |
| Dappl (f, args) -> |
|
| 310 |
mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args) |
|
| 311 |
| Dlink _ -> |
|
| 312 |
assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*) |
|
| 313 |
| Dunivar -> ( |
|
| 314 |
try List.assoc dim.dim_id !inst_dim_vars |
|
| 315 |
with Not_found -> |
|
| 316 |
let var = mkdim dim.dim_loc Dvar in |
|
| 317 |
inst_dim_vars := (dim.dim_id, var) :: !inst_dim_vars; |
|
| 318 |
var) |
|
| 319 |
|
|
| 320 |
(** destructive unification of [dim1] and [dim2]. Raises [Unify (t1,t2)] if the |
|
| 321 |
types are not unifiable. if [semi] unification is required, [dim1] should |
|
| 322 |
furthermore be an instance of [dim2] *) |
|
| 323 |
let unify ?(semi = false) dim1 dim2 = |
|
| 312 | 324 |
let rec unif dim1 dim2 = |
| 313 | 325 |
let dim1 = repr dim1 in |
| 314 | 326 |
let dim2 = repr dim2 in |
| 315 |
if dim1.dim_id = dim2.dim_id then () else |
|
| 327 |
if dim1.dim_id = dim2.dim_id then () |
|
| 328 |
else |
|
| 316 | 329 |
match dim1.dim_desc, dim2.dim_desc with |
| 317 |
| Dunivar, _ |
|
| 318 |
| _ , Dunivar -> assert false |
|
| 319 |
| Dvar , Dvar -> |
|
| 320 |
if dim1.dim_id < dim2.dim_id |
|
| 321 |
then dim2.dim_desc <- Dlink dim1 |
|
| 322 |
else dim1.dim_desc <- Dlink dim2 |
|
| 323 |
| Dvar , _ when (not semi) && not (occurs dim1 dim2) -> |
|
| 324 |
dim1.dim_desc <- Dlink dim2 |
|
| 325 |
| _ , Dvar when not (occurs dim2 dim1) -> |
|
| 326 |
dim2.dim_desc <- Dlink dim1 |
|
| 327 |
| Dite(i1, t1, e1), Dite(i2, t2, e2) -> |
|
| 328 |
begin |
|
| 329 |
unif i1 i2; |
|
| 330 |
unif t1 t2; |
|
| 331 |
unif e1 e2 |
|
| 332 |
end |
|
| 333 |
| Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 -> |
|
| 334 |
List.iter2 unif args1 args2 |
|
| 335 |
| Dbool b1, Dbool b2 when b1 = b2 -> () |
|
| 336 |
| Dint i1 , Dint i2 when i1 = i2 -> () |
|
| 337 |
| Dident id1, Dident id2 when id1 = id2 -> () |
|
| 338 |
| _ -> raise (Unify (dim1, dim2)) |
|
| 339 |
in unif dim1 dim2 |
|
| 340 |
|
|
| 341 |
let rec rename fnode fvar e = |
|
| 342 |
{ e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }
|
|
| 330 |
| Dunivar, _ | _, Dunivar -> |
|
| 331 |
assert false |
|
| 332 |
| Dvar, Dvar -> |
|
| 333 |
if dim1.dim_id < dim2.dim_id then dim2.dim_desc <- Dlink dim1 |
|
| 334 |
else dim1.dim_desc <- Dlink dim2 |
|
| 335 |
| Dvar, _ when (not semi) && not (occurs dim1 dim2) -> |
|
| 336 |
dim1.dim_desc <- Dlink dim2 |
|
| 337 |
| _, Dvar when not (occurs dim2 dim1) -> |
|
| 338 |
dim2.dim_desc <- Dlink dim1 |
|
| 339 |
| Dite (i1, t1, e1), Dite (i2, t2, e2) -> |
|
| 340 |
unif i1 i2; |
|
| 341 |
unif t1 t2; |
|
| 342 |
unif e1 e2 |
|
| 343 |
| Dappl (f1, args1), Dappl (f2, args2) |
|
| 344 |
when f1 = f2 && List.length args1 = List.length args2 -> |
|
| 345 |
List.iter2 unif args1 args2 |
|
| 346 |
| Dbool b1, Dbool b2 when b1 = b2 -> |
|
| 347 |
() |
|
| 348 |
| Dint i1, Dint i2 when i1 = i2 -> |
|
| 349 |
() |
|
| 350 |
| Dident id1, Dident id2 when id1 = id2 -> |
|
| 351 |
() |
|
| 352 |
| _ -> |
|
| 353 |
raise (Unify (dim1, dim2)) |
|
| 354 |
in |
|
| 355 |
unif dim1 dim2 |
|
| 356 |
|
|
| 357 |
let rec rename fnode fvar e = |
|
| 358 |
{ e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }
|
|
| 359 |
|
|
| 343 | 360 |
and expr_replace_var_desc fnode fvar e = |
| 344 | 361 |
let re = rename fnode fvar in |
| 345 | 362 |
match e with |
| 346 |
| Dvar |
|
| 347 |
| Dunivar |
|
| 348 |
| Dbool _ |
|
| 349 |
| Dint _ -> e |
|
| 350 |
| Dident v -> Dident (fvar v) |
|
| 351 |
| Dappl (id, el) -> Dappl (fnode id, List.map re el) |
|
| 352 |
| Dite (g,t,e) -> Dite (re g, re t, re e) |
|
| 353 |
| Dlink e -> Dlink (re e) |
|
| 354 |
|
|
| 355 |
let rec expr_replace_expr fvar e = |
|
| 356 |
{ e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
|
|
| 363 |
| Dvar | Dunivar | Dbool _ | Dint _ -> |
|
| 364 |
e |
|
| 365 |
| Dident v -> |
|
| 366 |
Dident (fvar v) |
|
| 367 |
| Dappl (id, el) -> |
|
| 368 |
Dappl (fnode id, List.map re el) |
|
| 369 |
| Dite (g, t, e) -> |
|
| 370 |
Dite (re g, re t, re e) |
|
| 371 |
| Dlink e -> |
|
| 372 |
Dlink (re e) |
|
| 373 |
|
|
| 374 |
let rec expr_replace_expr fvar e = |
|
| 375 |
{ e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
|
|
| 376 |
|
|
| 357 | 377 |
and expr_replace_expr_desc fvar e = |
| 358 | 378 |
let re = expr_replace_expr fvar in |
| 359 | 379 |
match e with |
| 360 |
| Dvar |
|
| 361 |
| Dunivar |
|
| 362 |
| Dbool _ |
|
| 363 |
| Dint _ -> e |
|
| 364 |
| Dident v -> (fvar v).dim_desc |
|
| 365 |
| Dappl (id, el) -> Dappl (id, List.map re el) |
|
| 366 |
| Dite (g,t,e) -> Dite (re g, re t, re e) |
|
| 367 |
| Dlink e -> Dlink (re e) |
|
| 380 |
| Dvar | Dunivar | Dbool _ | Dint _ -> |
|
| 381 |
e |
|
| 382 |
| Dident v -> |
|
| 383 |
(fvar v).dim_desc |
|
| 384 |
| Dappl (id, el) -> |
|
| 385 |
Dappl (id, List.map re el) |
|
| 386 |
| Dite (g, t, e) -> |
|
| 387 |
Dite (re g, re t, re e) |
|
| 388 |
| Dlink e -> |
|
| 389 |
Dlink (re e) |
|
Also available in: Unified diff
reformatting