Type related passes

doc/ops.pl

@@ -0,0 +1,6 @@
+:- op(700, xfy, user:(≤)).
+:- op(700, xfy, user:(≥)).
+:- op(700, xfy, user:(<:)).
+:- op(700, xfy, user:(∈)).
+:- op(700, xfy, user:(⋮)).
+:- op(700, xfy, user:(⋅)).

doc/razbor.pl

@@ -0,0 +1,378 @@
+:- use_module(library(pprint)).
+:- use_module(library(yall)).
+
+:- [tox].
+
+:- op(1100, xfy, user:(//)).
+:- op(990, xfy, user:(→)).
+:- op(700, xfy, user:(≠)).
+
+X ≠ Y :- dif(X, Y).
+
+L // R :- L *-> true ; R.
+
+match(X, [V|Cases]) :-
+    ( V = (Val → Goal), X = Val *->
+        call(Goal)
+    ; X = V *->
+        true
+    ;
+        match(X, Cases)
+    ).
+
+% def path: type.
+% def path: list string -> list string -> path.
+
+% def endinanness: type.
+% def big_endian: endinanness.
+% def little_endian: endinanness.
+
+% def rel: type.
+% def rexpr: type.
+
+% def hole: rexpr.
+% def sizeof: rexpr.
+% def rint: int -> rexpr.
+% def ref: path -> rexpr.
+% def size: list rel -> rexpr.
+
+% def (<): rexpr -> rexpr -> rel.
+% def (≤): rexpr -> rexpr -> rel.
+% def (=): rexpr -> rexpr -> rel.
+% def (≥): rexpr -> rexpr -> rel.
+% def (>): rexpr -> rexpr -> rel.
+
+% def value: type.
+% def vbool: bool -> value.
+% def vint: int -> value.
+
+% def ty: type.
+% def top: ty.
+% def bottom: ty.
+
+% def boolean: ty.
+% def integer: ty.
+
+% def u: int -> endinanness -> ty.
+% def s: int -> endinanness -> ty.
+
+% def arr: ty -> list rel -> ty.
+% def str: list rel -> ty.
+
+% def meet: list ty -> ty.
+% def join: list ty -> ty.
+
+% def ref: path -> ty.
+
+% def (⋮): ty -> list rel -> ty.
+% def (∈): value -> ty -> ty.
+
+% def prod: list path -> ty.
+
+% def reduced: ty -> ty.
+
+% def (<:): path -> ty -> o.
+% def ctypeof: path -> ty -> o.
+
+% def simpl: ty -> ty -> o.
+% def subst: ty -> ty -> o.
+% def reduce_meet: ty -> ty -> ty -> o.
+% def reduce_join: list ty -> list ty -> o.
+
+as_path(S, path(Mods, Data)) :-
+    split_string(S, " ", "", [ModsStr, DataStr]) *->
+        split_string(ModsStr, ".", "", Mods),
+        split_string(DataStr, ".", "", Data)
+    ;
+        split_string(S, ".", "", Mods),
+        Data = [].
+
+ctypeof(P, T) :-
+    P <: Tx,
+    subst(Tx, Ty),
+    simpl(Ty, T).
+
+print_t(T) :-
+    WriteOps = [spacing(next_argument)],
+    print_term(T, [write_options(WriteOps)]).
+
+print_tox_ctypeof :-
+    findall(P, P <: _, RawTypes),
+    maplist(ctypeof_pair, RawTypes, CTypes),
+    WriteOps = [spacing(next_argument)],
+    print_term(CTypes, [write_options(WriteOps)]).
+
+ctypeof_pair(P, P <: T) :- ctypeof(P, T).
+
+print_ctypeof(PathStr) :-
+    as_path(PathStr, Path),
+    ctypeof(Path, T),
+    WriteOps = [
+        right_margin(60),
+        write_options([
+            spacing(next_argument)
+        ])
+    ],
+    print_term(T, WriteOps).
+
+is_simple(E) :-
+    dif(E, prod(_)),
+    dif(E, join(_)).
+
+subst_(meet([X|Xs]), meet([Y|Ys])) :-
+    subst(X, Y),
+    subst(meet(Xs), meet(Ys)).
+subst_(Tx ⋮ P, Ty ⋮ P) :-
+    subst(Tx, Ty).
+subst_(V ∈ Tx, V ∈ Ty) :-
+    subst(Tx, Ty).
+subst_(ref(P), T) :-
+    ctypeof(P, Tx),
+    ( is_simple(Tx) *->
+        T = (Tx ⋅ [P])
+    ;
+        T = ref(P)
+    ).
+subst(Tx, Ty) :-
+    subst_(Tx, Ty) // Tx = Ty.
+
+simpl_(Tx ⋮ P, Ty ⋮ P) :-
+    simpl(Tx, Ty).
+simpl_(V ∈ Tx, V ∈ Ty) :-
+    simpl(Tx, Ty).
+simpl_(meet([]), top).
+simpl_(meet([T]), T).
+simpl_(meet([X|Xs]), T) :-
+    reduce_meet(X, meet(Xs), M),
+    simpl(M, T).
+simpl_(join([X|[]]), Y) :-
+    simpl(X, Y).
+simpl_(join([X|Xs]), join(Z)) :-
+    simpl(X, Y),
+    simpl(join(Xs), join(Ys)),
+    reduce_join([Y|Ys], Z).
+simpl(Tx, Ty) :-
+    simpl_(Tx, Ty) // Tx = Ty.
+
+reduce_join(join([X|Xs]), Y) :-
+    append(X, Xs, Z),
+    reduce_join(Z, Y).
+reduce_join([X|Ys], [X|Zs]) :-
+    reduce_join(Ys, Zs).
+reduce_join([], []).
+
+reduce_meet(L, R, M) :- match((L, R, M), [
+    (T, T, T),
+    (top, T, T),
+    (T, top, T),
+    (bottom, _, bottom),
+    (integer, u(S, E), u(S, E)),
+    (u(S, E), integer, u(S, E)),
+
+    (Tx ⋮ Px, Ty ⋮ Py, T ⋮ P) → (
+        reduce_meet(Tx, Ty, T),
+        append(Px, Py, P)
+    ),
+    (Tx ⋮ P, V ∈ Ty, V ∈ (T ⋮ P)) → 
+        reduce_meet(Tx, Ty, T),
+    (V ∈ Tx, Ty ⋮ P, V ∈ (T ⋮ P)) → 
+        reduce_meet(Tx, Ty, T),
+    (Tx ⋮ P, Ty, T ⋮ P) →
+        reduce_meet(Tx, Ty, T),
+    (Tx, Ty ⋮ P, T ⋮ P) →
+        reduce_meet(Tx, Ty, T),
+    (Vx ∈ Tx, Vy ∈ Ty, V ∈ T) → (
+        meet_values(Vx, Vy, V),
+        reduce_meet(Tx, Ty, T)
+    ),
+    (Tx, V ∈ Ty, V ∈ T) →
+        reduce_meet(Tx, Ty, T),
+    (V ∈ Tx, Ty, V ∈ T) →
+        reduce_meet(Tx, Ty, T),
+
+    (meet([]), T, T),
+    (T, meet([]), T),
+    (meet([X|Xs]), meet(Y), Z) → (
+        append(Xs, Y, Ts),
+        reduce_meet(X, meet(Ts), Z)
+    ),
+    (meet([X]), Y, Z) →
+        reduce_meet(X, Y, Z),
+    (X, meet([Y]), Z) →
+        reduce_meet(X, Y, Z),
+    (meet([X|Xs]), Y, Z) → (
+        append(Xs, [Y], Ts),
+        reduce_meet(X, meet(Ts), Z)
+    ),
+    (X, meet([Y|Ys]), Z) → (
+        reduce_meet(X, Y, T),
+        reduce_meet(T, meet(Ys), Z)
+    ),
+
+    (X, join([Y]), Z) → 
+        reduce_meet(X, Y, Z),
+    (X, join([Y|Ys]), join([Z|Zs])) → (
+        reduce_meet(X, Y, Z),
+        reduce_meet(X, join(Ys), join(Zs))
+    ),
+    (join([X]), Y, Z) → 
+        reduce_meet(X, Y, Z),
+    (join([X|Xs]), Y, join([Z|Zs])) → (
+        reduce_meet(X, Y, Z),
+        reduce_meet(join(Xs), Y, join(Zs))
+    ),
+
+    (ref(X), Y, reduced(meet([ref(X), Y]))),
+    (X, ref(Y), reduced(meet([X, ref(Y)]))),
+
+    (prod(X), Y, Z) → fail,
+    (X, prod(Y), Z) → fail
+]) // M = bottom.
+
+meet_values(V, V, V).
+
+sizeof(P, S) :-
+    ctypeof(P, T),
+    sizeof_type(T, S).
+
+size_sum(Sx, Sy, S) :- fail.
+
+size_join(Sx, Sy, S) :- match((Sx, Sy, S), [
+    (bottom, Y, Y),
+    (X, bottom, X),
+    (join(Xs), join(Ys), join(Zs)) →
+        append(Xs, Ys, Zs),
+    (X, join(Ys), join([X|Ys])),
+    (join(Xs), Y, join([Y|Xs])),
+    (X, Y, join([X, Y])) 
+]).
+
+size_mul(Sx, Sy, S) :- fail.
+size_unify(Sx, Sy, S) :- fail.
+
+exact_size(S, E) :-
+    member(hole=E, S).
+
+size_constraint([], []).
+size_constraint([P|Ps], [S|Ss]) :-
+    (P, S) = (sizeof=C, hole=C) *->
+        size_constraint(Ps, Ss)
+    ;
+        size_constraint(Ps, [S|Ss]).
+
+sizeof_type(prod(Ts), S) :-
+    maplist(
+        [T, S] >> sizeof_type(T, S),
+        Ts, Ss
+    ),
+    foldl(
+        [Sx, Sy, S] >> size_sum(Sx, Sy, S),
+        Ss, [], S
+    ).
+
+sizeof_type(join(Ts), S) :-
+    maplist(
+        [T, S] >> sizeof_type(T, S),
+        Ts, Ss
+    ),
+    foldl(
+        [Sx, Sy, S] >> size_join(Sx, Sy, S),
+        Ss, bottom, S
+    ).
+
+sizeof_type(T, []) :-
+    T = top ; T = integer.
+
+sizeof_type(bottom, bottom).
+
+sizeof_type(u(S, _), [hole=rint(S)]).
+sizeof_type(_ ∈ T, S) :-
+    sizeof_type(T, S).
+sizeof_type(arr(T, N), S) :-
+    sizeof_type(T, St),
+    Sn = N,
+    size_mul(St, Sn, S).
+sizeof_type(T ⋅ _, S) :-
+    sizeof_type(T, S).
+sizeof_type(ref(Path), S) :-
+    sizeof(Path, S).
+sizeof_type(T ⋮ P, S) :-
+    sizeof_type(T, Sx),
+    size_constraint(P, Sy),
+    size_unify(Sx, Sy, S).
+
+is_name(path(_, Data)) :-
+    last(Data, Name),
+    \+ atom_number(Name, _).
+
+has_name(P, N) :-
+    nameof(P, N),
+    is_name(N).
+
+short_nameof(P, S) :-
+    nameof(P, path(_, D)),
+    last(D, S).
+
+constant(V ∈ _, V).
+
+root_path(path(_, [_])).
+
+print_mtype(Path) :-
+    mtype(Path, T), print_t(T)
+    // ctypeof(Path, T), print_t(T).
+
+% as_datatype(T, DataType)
+mtype(Path, MT) :-
+    ctypeof(Path, T),
+    as_mtype(Path, T, MT).
+
+as_mtype(Path, prod(Prod), struct(Path, Fields)) :- 
+    root_path(Path),
+    maplist(
+        ([P, T] >> mtype(P, T)),
+        Prod, Fields
+    ).
+
+as_mtype(Path, join(Join), enum(Path, Fields)) :-
+    root_path(Path),
+    maplist(
+        [R, F] >> (
+            ref(P) = R,
+            short_nameof(P, N),
+            F = N : P
+        ),
+        Join, Fields    
+    ).
+
+as_mtype(Path, Type, data(Path, F)) :-
+    root_path(Path),
+    Type \= prod(_), Type \= join(_),
+    forget(Type, F).
+
+as_mtype(Path, Type, ShortName : F) :-
+    \+ root_path(Path),
+    Type \= prod(_), Type \= join(_),
+    nameof(Path, Name),    % TODO: use has_name
+    path(_, D) = Name,
+    last(D, ShortName),
+    forget(Type, F).
+
+forget(T, F) :- match((T, F), [
+    (_ ⋅ [Path], Path),
+    (X ⋮ _, Y) → 
+        forget(X, Y),
+    (_ ∈ X, Y) →
+        forget(X, Y),
+    (arr(Tx, Nx), Y) →
+        forget_arr(arr(Tx, Nx), Y),
+    (X, X)
+]).
+
+forget_arr(arr(Tx, Nx), F) :-
+    forget(Tx, Ty),
+    % TODO: support ref constants
+    (exact_size(Nx, rint(Ny)) *->
+        F = arr(Ty, Ny)
+    ;
+        F = vec(Ty)
+    ).