%%% Intersection type checking from ICFP'00 paper
%%% No refinement restriction
%%% No polymorphism
%%% Included Top (t)
%%% Author: Frank Pfenning
%%% Extended: Brigitte Pientka

% Types
tp : type.				%name tp A.

% bp Tue Feb 26 20:36:02 2002
bool: tp.

zero : tp.  % bp Wed Feb 27 11:51:24 2002
bit : tp.
nat : tp.
pos : tp.
=>  : tp -> tp -> tp.			%infix right 10 =>.
&   : tp -> tp -> tp.			%infix right 9 &.
t   : tp.

%{
% Declarative Subtyping
<= : tp -> tp -> type.			%infix none 8 <=.
					%name <= S.
%mode <= *A *B.

refl : A <= A.
trans : A <= B
	 -> B <= C
	 -> A <= C.


z<=n : zero <= nat.
p<=n : pos <= nat.
n<=b : nat <= bit.

&<=1 : A1 & A2 <= A1.
&<=2 : A1 & A2 <= A2.
<=&  : A <= B1
	-> A <= B2
	-> A <= B1 & B2.
<=t  : A <= t.

<==> : B1 <= A1
	-> A2 <= B2
	-> A1 => A2 <= B1 => B2.
}%
% Ordinary Types
ord : tp -> type.
%mode ord +A.

ord_bo: ord bool.

ord_b : ord bit.
ord_n : ord nat.
ord_p : ord pos.
ord_z : ord zero.
ord_=> : ord (A => B).
% t and & are not ordinary.
%terminates [] (ord _).

% Extracting conjuncts
conj : tp -> tp -> type.
%mode conj +A -Ao.
conj0 : conj Ao Ao
	 <- ord Ao.
conjl : conj (A & B) Ao
	 <- conj A Ao.
conjr : conj (A & B) Bo
	 <- conj B Bo.
%terminates A (conj A _).

% Algorithmic Subtyping
% Duplicated for the termination checker only!
<| : tp -> tp -> type.			%infix none 8 <|.
|> : tp -> tp -> type.			%infix none 8 |>.
%mode <| +A +B.
%mode |> +A +B.

bo<|bo: bool <| bool.

b<|b : bit <| bit.
n<|n : nat <| nat.
p<|p : pos <| pos.
p<|n : pos <| nat.
z<|z : zero <| zero.
z<|n : zero <| nat.
n<|b : nat <| bit.
p<|b : pos <| bit.

&1<|o : A1 & A2 <| Bo
	 <- ord Bo
	 <- A1 <| Bo.
&2<|o : A1 & A2 <| Bo
	 <- ord Bo
	 <- A2 <| Bo.

<|& : A <| B1 & B2
       <- A <| B1
       <- A <| B2.

<|t : A <| t.

=><|=> : A1 |> B1
	-> A2 <| B2
	-> A1 => A2 <| B1 => B2.

b|>b : bit |> bit.
n|>n : nat |> nat.
p|>p : pos |> pos.
n|>p : nat |> pos.
z|>z : zero |> zero.
n|>z : nat |> zero.
b|>b : bit |> nat.
b|>p : bit |> pos.

o|>&1 : Bo |> A1 & A2
	 <- ord Bo
	 <- Bo |> A1.
o|>&2 : Bo |> A1 & A2
	 <- ord Bo
	 <- Bo |> A2.

&|> : B1 & B2 |> A
       <- B1 |> A
       <- B2 |> A.

t|> : t |> A.

=>|>=> : B1 <| A1
	-> B2 |> A2
	-> B1 => B2 |> A1 => A2.

%terminates [(A A') (B B')] (|> A' B') (<| A B).

% Note to Brigitte
% %terminates [(A A') (B B')] (<| A B) (<| B' A').

% Terms
term : type.				%name term M x.

% Type ascription
# : term -> tp -> term.			%infix none 8 #.

% integers
z: term.
s: term -> term.

casen : term
	-> term
	-> (term -> term)
	-> term.

% Functions
lam : (term -> term) -> term.
app : term -> term -> term.

if : term -> term -> term -> term.
true: term.
false: term.

% Bits
e : term.
0 : term -> term.			%postfix 10 0.
1 : term -> term.			%postfix 10 1.
case : term
	-> term
	-> (term -> term)
	-> (term -> term)
	-> term.

% Let and recursion
let : term -> (term -> term) -> term.
fix : (term -> term) -> term.

% Values

value : term -> type.			%name value W.
%mode value +M.

val_lam : value (lam [x] M x).
val_e : value (e).
val_0 : value (M 0) <- value M.
val_1 : value (M 1) <- value M.
val_t: value true.
val_f: value false.
val_z: value z.
val_s: value (s E) <- value E.

%terminates M (value M).

nonvalue : term -> type.
%mode nonvalue +M.
nv_app : nonvalue (app M N).
nv_0 : nonvalue (M 0)
	<- nonvalue M.
nv_1 : nonvalue (M 1)
	<- nonvalue M.
nv_case : nonvalue (case M Me M0 M1).
nv_casen : nonvalue (casen M Mz Ms).
nv_let : nonvalue (let M N).
nv_fix : nonvalue (fix M).
nv_if  : nonvalue (if M M1 M2).
%terminates M (nonvalue M).

% Typing Rules; Values
%{
of : term -> tp -> type.		%name of D.
%mode of +M *A.

of<= : of M A
	-> A <= B
	-> of M B.

of& : of V A
       -> of V B
       -> value V
       -> of V (A & B).

of_true: of true bool.
of_false: of false bool.
of_if : of (if M M1 M2) T
	 <- of M bool
	 <- of M1 T
	 <- of M2 T.

of_lam : ({x} of x A -> of (M x) B)
	  -> of (lam [x] M x) (A => B).

of_app : of M (A => B)
	  -> of N A
	  -> of (app M N) B.

of_e : of e nat.
of_ez : of e zero.
of_0b : of M bit -> of (M 0) bit.
of_0p : of M pos -> of (M 0) pos.
of_1b : of M bit -> of (M 1) bit.
of_1p : of M nat -> of (M 1) pos.

of_case_b : of M bit
	     -> of Me A
	     -> ({x} of x bit -> of (M0 x) A)
	     -> ({y} of y bit -> of (M1 y) A)
	     -> of (case M Me ([x] M0 x) ([y] M1 y)) A.
of_case_n : of M nat
	     -> of Me A
	     -> ({x} of x pos -> of (M0 x) A)
	     -> ({y} of y nat -> of (M1 y) A)
	     -> of (case M Me ([x] M0 x) ([y] M1 y)) A.
of_case_p : of M pos
	     -> ({x} of x pos -> of (M0 x) A)
	     -> ({y} of y nat -> of (M1 y) A)
	     -> of (case M Me ([x] M0 x) ([y] M1 y)) A.

% bp Wed Feb 27 11:54:12 2002
of_case_z : of M zero
	     -> of Me A
	     -> of (case M Me ([x] M0 x) ([y] M1 y)) A.

of_fix : of (fix M) A
	  <- ({x:term} of x A -> of (M x) A).

of_let : of (let M N) A
	  <- of M B
	  <- ({x:term} of x B -> of (N x) A).
}%
% Bi-Directional Type Checking
synth : term -> tp -> type.		%name synth S s.
check : term -> tp -> type.		%name check C c.
%mode synth +I -A.
%mode check +C +A.

% there is a bug -- if -- bp Mon Feb 18 13:54:00 2002 fixed
% tabled synth.
%tabled check.

% Coercions
s_# : synth (C # A) A
       <- check C A.

c_s : check I Ao
       <- ord Ao
       <- synth I A'
       <- A' <| Ao.

cnv_& : check I (A & B)
	 <- nonvalue I
	 <- synth I A'
	 <- A' <| A & B.
cnv_t : check I t
	 <- nonvalue I.
%	 <- synth I A'			% redundant?
%	 <- A' <| t.			% always succeeds

%% Intersections
c_& : check CV (A & B)
       <- value CV
       <- check CV A
       <- check CV B.

c_t : check CV t
       <- value CV.
       % checkable CV?


% Functions
s_app : synth (app I C) B
	 <- synth I A'
	 <- conj A' (A => B)
	 <- check C A.

c_lam : check (lam [x] C x) (A => B)
	 <- ({x:term} value x -> synth x A -> check (C x) B).

c_true: check true bool.
c_false: check false bool.
c_if : check (if M M1 M2) A
	<- check M bool
	<- check M1 A
	<- check M2 A.

% e : nat [& bit]
c_b : check e bit.
c_e : check e nat.
c_z : check e zero. % bp Wed Feb 27 11:58:16 2002
% no c_p

% _ 0 : bit -> bit & pos -> pos [& nat -> bit]
s_0_b : check (C 0) bit <- check C bit.
s_0_n : check (C 0) nat <- check C pos.
s_0_p : check (C 0) pos <- check C pos.

% _ 1 : bit -> bit & nat -> pos [& pos -> pos]
s_1_b : check (C 1) bit <- check C bit.
s_1_n : check (C 1) nat <- check C nat.
s_1_p : check (C 1) pos <- check C nat.

c_case_b : check (case I Ce ([x] C0 x) ([y] C1 y)) A
	     <- synth I B'
	     <- conj B' bit
	     <- check Ce A
	     <- ({x} value x -> synth x bit -> check (C0 x) A)
	     <- ({y} value y -> synth y bit -> check (C1 y) A).

c_case_n : check (case I Ce ([x] C0 x) ([y] C1 y)) A
	     <- synth I B'
	     <- conj B' nat
	     <- check Ce A
	     <- ({x} value x -> synth x pos -> check (C0 x) A)
	     <- ({y} value y -> synth y nat -> check (C1 y) A).

c_case_p : check (case I Ce ([x] C0 x) ([y] C1 y)) A
	     <- synth I B'
	     <- conj B' pos
	     <- check Ce t		% to be pedantic
	     <- ({x} value x -> synth x pos -> check (C0 x) A)
	     <- ({y} value y -> synth y nat -> check (C1 y) A).


c_case_z : check (case I Ce ([x] C0 x) ([y] C1 y)) A
	     <- synth I B'
	     <- conj B' zero
	     <- check Ce A.

% Definitions
c_let : check (let I C) A
	 <- synth I B
	 <- ({x:term} value x -> synth x B -> check (C x) A).

% Recursion
c_fix : check (fix C) A
	 <- ({x:term} nonvalue x -> synth x A -> check (C x) A).



% Note to Carsten: cannot termination check this!!

% %terminates {(I C) A} (synth I _) (check C A).
% %terminates {(I C) (A' A)} (synth I A') (check C A).
% Need to comment out offending clause and use spec below
% %terminates (I C) (synth I A') (check C A).