check.makam

check : term -> term -> prop.
multistep : term -> term -> prop.

(* Allow User Defined Axioms *)
check (axiom _ A) A.

check set typ.

(* Functions/Dependent Products *)
check (forall A B) L :-
    check A _,
    (x:term -> check x A -> check (B x) L).

check (lam A N) (forall A B) :-
    check A _,
    (x:term -> check x A -> check (N x) (B x)).

check (app M N) (B N) :-
    check M (forall A B),
    check N A.

(* Normalization Rule *)

(* FIXME

 check M B :-
    check M A,
    multistep A B,
    check B _. *)

(* Normalization *)

step : term -> term -> prop.
step_ : term -> term -> prop.

multistep X Z :-
    if step X Y
    then multistep Y Z
    else unify X Z.

step X Y :-
    if step_ X Y
    then success
    else structural @step_ X Y.

step_ (app (lam A F) X) (F X) :-
    check X A.