Messing with dependent type systems in makam (http://astampoulis.github.io/makam/)

dependent.makam

(* terms *)

term : type.

universe : term.
annotate : term -> term -> term.
unitType : term.
unitTerm : term.
pairType : term -> (term -> term) -> term.
pairTerm : term -> term -> term.
pairElim : term -> (term -> term -> term) -> term.
funType  : term -> (term -> term) -> term.
funTerm  : (term -> term) -> term.
funElim  : term -> term -> term.


(* values *)

neu : type.
whnf : type.

whnf_neu : neu -> whnf.
whnf_universe : whnf.
whnf_unitType : whnf.
whnf_unitTerm : whnf.
whnf_pairTerm : whnf -> whnf -> whnf.


(* semantics *)

eval : term -> whnf -> prop.

eval universe whnf_universe.
eval (annotate Term _) Term' :-
    eval Term Term'.
eval unitTerm whnf_unitType.
eval unitType whnf_universe.
eval (pairType First Second) _ :-
    eval First First',
    TODO.
eval (pairTerm First Second) (whnf_pairTerm First' Second') :-
    eval First First',
    eval Second Second'.
eval (pairElim _ _) _ :- TODO.
eval (funType ParamType BodyType) _ :-
    eval ParamType ParamType',
    TODO.
eval (funTerm _) _ :- TODO.
eval (funElim _ _) _ :- TODO.

equal : whnf -> whnf -> prop.

equal whnf_universe whnf_universe.
equal whnf_unitType whnf_unitType.
equal whnf_unitTerm whnf_unitTerm.
equal (whnf_pairTerm First0 Second0) (whnf_pairTerm First1 Second1) :-
    equal First0 First1,
    equal Second0 Second1.


(* typing *)

check : term -> whnf -> prop.
synth : term -> whnf -> prop.

check (pairTerm First Second) _ :- TODO.
check (funTerm Body) _ :- TODO.
check Term Type :-
    synth Term Type',
    equal Type Type'.

synth universe whnf_universe.
synth (annotate Term Type) Type' :-
    eval Type Type',
    check Term Type'.
synth unitTerm whnf_unitType.
synth unitType whnf_universe.
synth (pairType FirstType SecondType) _ :- TODO.
synth (pairElim Head Body) _ :- TODO.
synth (funType ParamType BodyType) _ :- TODO.
synth (funElim Head Arg) _ :- TODO.


(* -------------------------------------------------------------------------- *)
(* tests *)

check universe Type ?

dependent : testsuite.
%testsuite dependent.

>> check universe whnf_universe ?
>> Yes.

>> check unitTerm whnf_unitType ?
>> Yes.

>> check universe (whnf_neu Type) ?
>> Yes.

>> synth (pairTerm _ _) _ ?
>> Impossible.

>> synth (funTerm _) _ ?
>> Impossible.