372 |
[Ty.T_Tensor(Ty.ShapeVar s1), Ty.T_Tensor(Ty.ShapeVar s2)] |
[Ty.T_Tensor(Ty.ShapeVar s1), Ty.T_Tensor(Ty.ShapeVar s2)] |
373 |
--> Ty.T_Tensor(Ty.ShapeVar s3))) |
--> Ty.T_Tensor(Ty.ShapeVar s3))) |
374 |
|
|
375 |
|
|
376 |
|
val op_innerField = polyVar (N.op_dot, all([DK, NK, SK], |
377 |
|
fn [Ty.DIFF k, Ty.DIM d, Ty.SHAPE dd] => let |
378 |
|
val t = Ty.T_Field{diff = Ty.DiffVar(k, 0), dim = Ty.DimVar d, shape = Ty.ShapeVar dd} |
379 |
|
val t2 = Ty.T_Field{diff = Ty.DiffVar(k, 0), dim = Ty.DimVar d, shape = Ty.Shape[]} |
380 |
|
in |
381 |
|
[t, t] --> t2 |
382 |
|
end)) |
383 |
|
|
384 |
|
|
385 |
|
|
386 |
|
|
387 |
|
|
388 |
(* the colon (or double-dot) product operator is treated as a special case in the |
(* the colon (or double-dot) product operator is treated as a special case in the |
389 |
* typechecker. It is not included in the basis environment, but we define its type |
* typechecker. It is not included in the basis environment, but we define its type |
390 |
* schemehere. There is an implicit constraint on its type to have the following scheme: |
* schemehere. There is an implicit constraint on its type to have the following scheme: |
454 |
val op_outer = polyVar (N.op_outer, all([NK, NK], mkOuter)) |
val op_outer = polyVar (N.op_outer, all([NK, NK], mkOuter)) |
455 |
end |
end |
456 |
|
|
457 |
|
(* |
458 |
|
|
459 |
|
fun field' (k, d, dd) = field(k, Ty.DimConst d, Ty.Shape(List.map Ty.DimConst dd)) |
460 |
|
|
461 |
|
local |
462 |
|
fun mkOuterField [Ty.DIFF k, Ty.DIM d, Ty.SHAPE dd1, Ty.SHAPE dd2] = let |
463 |
|
val d1 = Ty.ShapeVar dd1 |
464 |
|
val d2 = Ty.ShapeVar dd2 |
465 |
|
val f = field(Ty.DiffVar(k, 0), d, d1) |
466 |
|
val g = field(Ty.DiffVar(k, 0), d, d2) |
467 |
|
val h = field'(Ty.DiffVar(k, 0), 3, [2,2]) |
468 |
|
|
469 |
|
|
470 |
|
in |
471 |
|
[f, g] --> h |
472 |
|
end |
473 |
|
in |
474 |
|
val op_outerField = polyVar (N.op_outer, all([DK,NK, SK,SK], mkOuterField)) |
475 |
|
end |
476 |
|
*) |
477 |
|
|
478 |
val fn_principleEvec = polyVar (N.fn_principleEvec, all([NK], |
val fn_principleEvec = polyVar (N.fn_principleEvec, all([NK], |
479 |
fn [Ty.DIM d] => let |
fn [Ty.DIM d] => let |
480 |
val d = Ty.DimVar d |
val d = Ty.DimVar d |