Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2002-05-16 18:58:35 -0700 (Thu, 16 May 2002)
Revision: 3657
Log message:
Change the grammar for terms a little bit.
Now the grammar understands
(1) Expression for records:
- Record types:
{x:A; y:B; ... z:C}
- Records
{x=a; y=b; ... z=c}
- Field selections:
r^x
where x,y,z are words or strings, A,B,C,a,b,c,r are terms.
Actually type {x_1:A_1;x_2:A_2;...x_n:A_n} is a depend typed record.
It bounds the variable "self" inside terms A_2, ..., A_n. The type of
self in A_k is {x_1:A_1, ..., x_k-1:A_k-1}. So, you can write, e.g.,
{car : univ[l:l];
"*" : 'self^car -> 'self^car -> 'self^car
}
This form a type that contains, for example,
{car = int;
"*" = lambda{x.lambda{y. 'x+@ 'y}}
}
(2) Syntax sugar for self.
You may omit self, in the expressions like self^x.
That is, you can write ^x instead of self^x.
So, the following type is equivalent to the previous one.
{car : univ[l:l];
"*" : ^car -> ^car -> ^car
}
(3) Binary operations ^*, ^+, ^=, ^/, ^-, ^<, ^> ,^<>
x ^* y stands for self^"*" x y
x ^= y stands for self^"=" x y
and so on.
So you may write
{car : univ[l:l];
"*" : ^car -> ^car -> ^car;
axm : all x,y,z : ^car. ('x ^* 'y) ^* 'z = 'x ^* ('y ^* 'z) in ^car
}
(4) Let and with operators.
Now (let x=term1 in term2) and (term2 where x=term1) are both expression for
the let{term1;x.term2} term defined now in itt_rfun.
(5) Open operators.
(open e1 in e2) stands for (let self=e1 in e2)
(forany T. e) stands for (all self:T. e)
(thereis T. e) stands for (exsts self:T. e)
So you may write something like this
open 'g in 'x ^* ^y ^* 'z
forany group. all 'x in ^car. 'x ^* ^e = 'x in ^car
(6) Changed associativity and priority of some operators.
Now the priority is the following (from the lowest priority):
- operators like if-then-else and let
- logical operators (in usual order)
- relations (first =,in,~, then all other relations)
- type and arithmetic operators in usual order
- application
- record field selection
For example
'x in 'y and 'z stands for ('x in 'y) and 'z
but
'x in 'y * 'z stands for 'x in ('y * 'z)
I think this is natural.
Corrected a couple of proofs that was broken.
TODO:
- make sure that display forms respect the new grammar.