Commit 131682fe authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

No commit message

No commit message
parent b92a595c
......@@ -60,3 +60,75 @@ then on the prompt type
Example files are given in the ./examples directory. Read the
./examples/README file
************************************
* Syntax of signature and lexicons *
************************************
(see the examples/tag.acg file for an example)
Signatures are defined by:
signature my_sig_name=
sig_entries
end
Sig_entries always ends with a ; and can be:
+ type declaration as in
NP,S : type;
+ type definition as in
o :type;
string = o -> o;
Note that type constructors are -> and => for the linear and
intuitionnistic arrow respectively.
+ constant declarations as in
foo:NP;
bar,dummy:NP -> S;
infix + : string -> string -> string;
prefix - : bool -> bool;
binder All : (e =>t) -> t;
infix > : bool -> bool -> bool; (*This means implication*)
Note that infix and prefix are keywords to introduce symbols (of
length 1. This probably will change).
Also notes that comments are surrounded by (* and *)
+ constant definitions as in
n = lambda n. bar n : NP -> S;
infix + = lambda x y z.x(y z): string -> string -> string;
prefix - = lambda p.not p:bool -> bool;
everyone = lambda P. All x. (human x) > (P x) ;
Note the syntax for binders (All in the last example). Available
construction for terms are:
lambda x y z.t
for linear abstraction
Lambda x y z.t
for non-linear abstraction
t u v
for application (eauql to (t u) v)
t SYM u
if SYM is a infix symbol (lowest priority)
SYM t
if SYM is a prefic symbol (highest priority)
BINDER x y z.t
if BINDER is a binder
Lexicons are defined by:
lexicon my_lex_name(abstract_sig_name) : object_sig_name =
lex_entries
end
Lex_entries always ends with a ; and have the following form:
abstract_atomic_type1, abstract_atomic_type2 := object_type;
abstract_const1, abstract_const2 := object_term;
......@@ -17,6 +17,8 @@
# #
##########################################################################
# Comments are from # symbols to the end of the line
# First print the help messasge that describes the commands
help;
......
......@@ -26,6 +26,11 @@ for adjunction. See https://hal.inria.fr/inria-00141913 for further
explanation of the TAG into ACG encoding *)
Sa,Na, Na_d, N, VPa, S,WH : type;
(* Declatiation of abstract constants together with their
types. -> stands for the linear implication and => (not used in this
signature) stands for the intuituinnistic implication *)
C_dog,C_cat:Na_d -> Na-> N;
C_sleeps:Sa -> VPa -> N -> S;
C_chases, C_loves, C_to_love:Sa -> VPa -> N -> N -> S;
......@@ -82,6 +87,9 @@ end
signature strings =
string: type;
(* we can define infix and prefix symbols. Note that as for now, the length of symbols can only be 1 *)
infix + : string -> string -> string;
every,dog,chases,a,cat,sleeps,slowly,new,big,black,seems,john,mary,bill,paul,
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment