Commit 49eeed6d authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files

No commit message

No commit message
parent 2736311c
signature CVG =
NP_S_S,NP,S:type;
G_quant:NP_S_S -> (NP -> S) -> S;
EV,SO:NP_S_S;
CHRIS,KIM,DANA,SANDY:NP;
LIKE:NP -> NP -> S;
end
signature simple_syntax =
NP,S:type;
everybody,somebody:NP;
liked:NP -> NP -> S;
Chris,Kim,Dana,Sandy : NP;
end
lexicon CVG_syntax (CVG) : simple_syntax =
NP_S_S := NP;
NP := NP;
S := S;
G_quant := lambda q r.r q;
EV := everybody;
SO := somebody;
LIKE := liked;
SANDY := Sandy;
DANA := Dana;
KIM := Kim;
CHRIS := Chris;
end
lexicon CVG_strings (simple_syntax) : strings =
NP := string;
S := string;
everybody := everybody;
somebody := somebody;
liked := lambda o s. s + liked + o;
Sandy := Sandy;
Dana := Dana ;
Kim := Kim;
Chris := Chris;
end
signature semantics =
e,t:type;
chris',kim',dana',sandy':e;
like' : e -> e -> t;
binder All : (e =>t) -> t;
binder Ex : (e =>t) -> t;
infix & : t -> t -> t;
infix > : t -> t -> t;
person' : e -> t;
everybody' = lambda P.All x. (person' x) > (P x): (e->t) -> t;
somebody' = lambda P. Ex x. (person' x) & (P x): (e->t) -> t;
end
lexicon CVG_semantics (CVG) : semantics =
NP_S_S := (e -> t) -> t;
NP := e;
S := t;
G_quant := lambda q r.q r;
EV := everybody';
SO := somebody';
CHRIS := chris';
KIM := kim';
DANA := dana';
SANDY := sandy';
LIKE := lambda o s. like' s o ;
end
load d ../data/cvg.acg;
CVG_syntax CVG_semantics analyse G_sem EV (lambda x.G_sem SO (lambda y.LIKE x y)) : S;
CVG_syntax CVG_semantics analyse G_sem SO (lambda y.G_sem EV (lambda x.LIKE x y)) : S;
CVG_syntax analyse WHETHER (LIKE SANDY KIM): S_k ;
CVG_syntax analyse G_filler WHAT_FILLER (lambda t. LIKE KIM t) :Q ;
CVG_syntax analyse G_syn WHO_FILLER (lambda t. G_situ_1 (lambda y . LIKE y t)) :Q ;
CVG_syntax analyse G_syn WHO_FILLER (lambda t. WONDERED (G_syn WHO_FILLER ( lambda t'. LIKE WHAT_IN_SITU t')) t) :Q ;
load d ../data/strings.acg;
load d ../data/cvg-quantification.acg;
compose CVG_strings CVG_syntax as CVG_phonology;
CVG_phonology CVG_syntax CVG_semantics analyse G_quant EV (lambda x.G_quant SO (lambda y.LIKE y x)) : S;
CVG_phonology CVG_syntax CVG_semantics analyse G_quant SO (lambda y.G_quant EV (lambda x.LIKE y x)) : S;
load d ../data/strings.acg;
load d ../data/cvg-topicalisation-in-situ.acg;
compose CVG_strings CVG_syntax as CVG_phonology;
CVG_phonology CVG_simple_semantics analyse G_top_in_situ (" SANDY) (lambda y . LIKE y KIM) : S;
CVG_phonology CVG_simple_semantics analyse G_top (^ SANDY) (lambda y . LIKE y KIM) : T;
signature syntax =
NP,S,T,NP_S_T,NP_S_T_in_situ : type;
G_top : NP_S_T -> (NP -> S) -> T;
G_top_in_situ : NP_S_T_in_situ -> (NP -> S) -> S;
CHRIS,KIM,DANA,SANDY:NP;
LIKE:NP -> NP -> S;
prefix ^ : NP -> NP_S_T ;
prefix " : NP -> NP_S_T_in_situ ;
end
signature simple_syntax =
NP,S,T:type;
liked:NP -> NP -> S;
Chris,Kim,Dana,Sandy : NP;
prefix ^ : NP -> (NP -> S) -> T ;
prefix " : NP -> NP ;
end
lexicon CVG_syntax (syntax) : simple_syntax =
NP := NP;
S := S;
T := T;
NP_S_T := (NP -> S)-> T;
NP_S_T_in_situ := NP ;
G_top := lambda q r.q r;
G_top_in_situ := lambda t r .r t;
LIKE := liked;
SANDY := Sandy;
DANA := Dana;
KIM := Kim;
CHRIS := Chris;
^ := lambda n . ^ n ;
" := lambda n . " n ;
end
lexicon CVG_strings (simple_syntax) : strings =
NP,S,T:= string;
liked := lambda o s . s + liked + o ;
Chris := Chris ;
Kim := Kim;
Dana := Dana ;
Sandy := Sandy ;
^ := lambda s r. s ! (r E) ;
" := lambda n . " n ;
end
signature simple_semantics =
e,t:type;
everybody',somebody': e ;
chris',kim',dana',sandy':e;
like' : e -> e -> t;
top' : e -> (e ->t) -> t
end
lexicon CVG_simple_semantics (syntax) : simple_semantics =
NP := e;
S := t;
T := t;
NP_S_T := (e -> t) -> t ;
NP_S_T_in_situ := (e -> t) -> t ;
G_top := lambda q r.q r;
G_top_in_situ := lambda q r.q r;
CHRIS := chris';
KIM := kim';
DANA := dana';
SANDY := sandy';
LIKE := lambda o s .like' s o;
^ := lambda n. top' n;
" := lambda n. top' n;
end
signature syntax =
NP,S,T,NP_S_T : type;
G_top : NP_S_T -> (NP -> S) -> T;
CHRIS,KIM,DANA,SANDY:NP;
LIKE:NP -> NP -> S;
prefix ^ : NP -> NP_S_T ;
end
signature simple_syntax =
NP,S,T:type;
liked:NP -> NP -> S;
Chris,Kim,Dana,Sandy : NP;
prefix ^ : NP -> (NP -> S) -> T ;
end
lexicon CVG_syntax (syntax) : simple_syntax =
NP := NP;
S := S;
T := T;
NP_S_T := (NP -> S)-> T;
G_top := lambda q r.q r;
LIKE := liked;
SANDY := Sandy;
DANA := Dana;
KIM := Kim;
CHRIS := Chris;
^ := lambda n . ^ n ;
end
lexicon CVG_strings (simple_syntax) : strings =
NP,S,T:= string;
liked := lambda o s . s + liked + o ;
Chris := Chris ;
Kim := Kim;
Dana := Dana ;
Sandy := Sandy ;
^ := lambda s r. s ! (r E) ;
end
signature simple_semantics =
e,t:type;
everybody',somebody': e ;
chris',kim',dana',sandy':e;
like' : e -> e -> t;
top' : e -> (e ->t) -> t
end
lexicon CVG_simple_semantics (syntax) : simple_semantics =
NP := e;
S := t;
T := t;
NP_S_T := (e -> t) -> t ;
G_top := lambda q r.q r;
CHRIS := chris';
KIM := kim';
DANA := dana';
SANDY := sandy';
LIKE := lambda o s .like' s o;
^ := lambda n. top' n;
end
CVG_syntax CVG_simple_semantics analyse LIKE EV SO :S ;
CVG_semantics analyse G_q everybody' (lambda x.G_q somebody'(lambda y. like' x y)) : t;
CVG_semantics analyse G_q somebody' (lambda y.G_q everybody'(lambda x. like' x y)) : t;
CVG_syntax CVG_simple_semantics analyse WHETHER (LIKE SANDY KIM): S ;
CVG_syntax CVG_simple_semantics analyse G WHAT_FILLER (lambda t. LIKE KIM t) :Q ;
CVG_syntax CVG_simple_semantics analyse G WHO_FILLER (lambda y . LIKE y WHAT_IN_SITU) :Q ;
CVG_syntax CVG_simple_semantics analyse G WHO_FILLER (lambda x. WONDERED (G WHO_FILLER ( lambda y. LIKE WHAT_IN_SITU y)) x) :Q ;
load d ../data/strings.acg;
load d ../data/cvg2.acg;
compose CVG_strings CVG_syntax as CVG_phonology;
# Scope ambiguity
CVG_phonology CVG_syntax CVG_simple_semantics analyse LIKE SO EV :S ;
# Semantics
CVG_semantics RC_ty analyse G_q everybody' (lambda x.G_q somebody'(lambda y. like' x y)) : t;
CVG_semantics RC_ty analyse G_q somebody' (lambda y.G_q everybody'(lambda x. like' x y)) : t;
# Embedded polar question
CVG_phonology CVG_syntax CVG_simple_semantics analyse WHETHER (LIKE SANDY KIM): S ;
# Semantics
CVG_semantics RC_ty analyse whether' (like' kim' sandy') : k;
# Embedded consituent question
CVG_phonology CVG_syntax CVG_simple_semantics analyse G WHAT_FILLER (lambda t. LIKE t KIM) :Q ;
# Semantics
CVG_semantics RC_ty analyse what_filler (lambda y.like' kim' y) : k1;
# Embedded consituent question
CVG_phonology CVG_syntax CVG_simple_semantics analyse LIKE WHAT_IN_SITU KIM : S ;
# Semantics
CVG_semantics RC_ty analyse G_w12 what_in_situ12 (lambda y.like' kim' y) : k2;
# Binary consituent question
CVG_phonology CVG_syntax CVG_simple_semantics analyse G WHO_FILLER (lambda y . LIKE WHAT_IN_SITU y) :Q ;
# Semantics
CVG_semantics RC_ty analyse G_w12 what_in_situ12 (lambda y. who_filler (lambda x. like' x y)) : k2 ;
# Baker ambiguity
CVG_phonology CVG_syntax CVG_simple_semantics analyse G WHO_FILLER (lambda x. WONDERED (G WHO_FILLER ( lambda y. LIKE WHAT_IN_SITU y)) x) :Q ;
# Semantics
CVG_semantics RC_ty analyse who_filler (lambda z.(wonder2' (G_w12 what_in_situ12 (lambda y. who_filler (lambda x.like' x y))) z)) : k1 ;
CVG_semantics RC_ty analyse G_w12 what_in_situ12 (lambda y.who_filler (lambda z.wonder1' (who_filler (lambda x.like' x y)) z)) : k2 ;
......@@ -17,6 +17,7 @@ signature syntax =
WHAT_IN_SITU : NP;
WHO_FILLER,WHAT_FILLER: NP_S_Q;
end
signature simple_syntax =
......@@ -33,7 +34,6 @@ signature simple_syntax =
who_in_situ,what_in_situ:NP;
who_filler,what_filler: (NP -> S) -> Q;
end
......@@ -65,8 +65,31 @@ lexicon CVG_syntax (syntax) : simple_syntax =
WHAT_FILLER := lambda r. what_filler (lambda x .r x);
WHO_FILLER := lambda r. who_filler (lambda x .r x);
end
lexicon CVG_strings (simple_syntax) : strings =
NP,S,Q:= string;
everybody := everyone;
somebody := someone;
barked := lambda x. x + barked;
liked := lambda o s . s + liked + o ;
thought := lambda s x. x + thought + s;
wondered := lambda s x.x+wondered+s ;
whether := lambda s.whether+s ;
Chris := Chris ;
Kim := Kim;
Dana := Dana ;
Sandy := Sandy ;
who_in_situ := who;
who_filler := lambda P . who + (P E);
what_in_situ := what;
what_filler := lambda P. what + (P E);
end
signature simple_semantics =
e,t:type;
......@@ -104,7 +127,7 @@ lexicon CVG_simple_semantics (syntax) : simple_semantics =
DANA := dana';
SANDY := sandy';
LIKE := like';
LIKE := lambda o s .like' s o;
BARKE := barke' ;
THOUGHT := think' ;
WONDERED := wonder' ;
......@@ -127,8 +150,8 @@ signature semantics =
k,k1,k2,k3,e_t_k1,e_k1_k2,e_k2_k3:type;
G_q : e_t_t -> (e ->t) -> t;
G_w12 : e_t_k1 -> (e -> k1) -> k2;
G_w23 : e_t_k1 -> (e -> k2) -> k3;
G_w12 : e_k1_k2 -> (e -> k1) -> k2;
G_w23 : e_k2_k3 -> (e -> k2) -> k3;
everybody',somebody': e_t_t;
......@@ -147,11 +170,12 @@ signature semantics =
who_filler : (e -> t) -> k1;
who_in_situ12 : e_k1_k2 ;
who_in_situ23 : e_k2_k3 ;
what_filler : (e -> t) -> k1;
what_filler : (e -> t) -> k1;
what_in_situ12 : e_k1_k2 ;
what_in_situ23 : e_k2_k3 ;
end
lexicon CVG_semantics (semantics):simple_semantics =
e:=e;
t:=t;
......@@ -187,3 +211,92 @@ lexicon CVG_semantics (semantics):simple_semantics =
what_in_situ12 := what_in_situ ;
what_in_situ23 := what_in_situ ;
end
signature ty_n =
e,t:type;
everybody',somebody': (e -> t) -> t ;
chris',kim',dana',sandy':e;
person',thing' : e -> t;
whether' : t -> t -> t;
infix & : t -> t -> t;
infix | : t -> t -> t;
which0 : (e ->t) -> (e -> t) -> e -> t -> t ;
which1 : (e ->t) -> (e -> e -> t -> t) -> e -> e -> t -> t ;
which2 : (e ->t) -> (e -> e -> e -> t -> t) -> e -> e -> e -> t -> t ;
who = which0 person' : (e -> t) -> e -> t -> t ;
who12 = which1 person' : (e -> e -> t -> t) -> e -> e -> t -> t;
who23 = which2 person' : (e -> e -> e -> t -> t ) -> e -> e -> e -> t -> t;
what = which0 thing' : (e -> t) -> e -> t -> t ;
what12 = which1 thing' : (e -> e -> t -> t) -> e -> e -> t -> t;
what23 = which2 thing' : (e -> e -> e -> t -> t) -> e -> e -> e -> t -> t;
like' : e -> e -> t;
barke' : e -> t;
think' : t -> e -> t;
k = t -> t:type;
k1 = e -> t -> t:type;
k2 = e -> e -> t -> t:type;
k3 = e -> e -> e -> t -> t:type;
wonder1' : k1 -> e -> t;
wonder2' : k2 -> e -> t;
(* who : (e -> t) -> k1;
who12 : (e -> k1) -> k2 ;
who23 : (e -> k2) -> k3 ;
what : (e -> t) -> k1;
what12 : (e -> k1) -> k2;
what23 : (e -> k2) -> k3 ; *)
end
lexicon RC_ty (semantics) : ty_n =
e := e;
t :=t;
e_t_t:= (e ->t) -> t;
k := k;
k1 := k1;
k2 := k2;
k3 := k3;
e_t_k1 := (e -> t) -> k1;
e_k1_k2 := (e -> k1) -> k2;
e_k2_k3 := (e -> k2) -> k3;
G_q := lambda Q r. Q r;
G_w12 := lambda Q r. Q r;
G_w23 := lambda Q r. Q r;
everybody':= everybody';
somebody' := somebody';
chris':= chris';
kim':= kim';
dana':= dana';
sandy':= sandy';
like' := like' ;
barke' := barke';
think' := think';
wonder1' := wonder1' ;
wonder2' := wonder2' ;
whether' := whether' ;
who_filler := who ;
who_in_situ12 := who12 ;
who_in_situ23 := who23 ;
what_filler := what ;
what_in_situ12 := what12;
what_in_situ23 := what23 ;
end
\ No newline at end of file
signature strings =
(* s:type ;
string = s->s : type;
infix + = lambda g f x.g(f x) : string -> string -> string; *)
string: type;
infix + : string -> string -> string;
E:string;
infix ! : string -> string -> string;
prefix " : string -> string;
every,dog,chases,a,cat,sleeps,slowly,new,big,black,seems,John,Mary,Bill,Paul,Kim,Dana,Chris,
Sandy,everyone,someone,everybody,somebody,
claims,loves,to,love,who,said,liked,does,think,thinks,thought,likes,wondered,whether,what,barked:string;
end
......@@ -349,7 +349,7 @@ let build_expectation lst =
| Lex Abstract_sig_closing -> build_expectation [Colon,Lex Object_sig_opening]
| Lex Object_sig_opening -> build_expectation [Id,Lex Object_sig_name]
| Lex Object_sig_name -> build_expectation [Equal,Lex (Lex_def No_lex_entry)]
| Lex (Lex_def No_lex_entry) -> build_expectation [Id,Lex (Lex_def (Lex_entry_id No_interpretation));End_kwd,No_dec]
| Lex (Lex_def No_lex_entry) -> build_expectation [Id,Lex (Lex_def (Lex_entry_id No_interpretation));End_kwd,No_dec;Sym,Lex (Lex_def (Lex_entry_id No_interpretation))]
| Lex (Lex_def (Lex_entry_id No_interpretation)) ->
build_expectation [Comma,Lex (Lex_def No_lex_entry);
Colon_equal,Lex (Lex_def (Lex_entry_id (Interpretation No_type_or_term_in_def)))]
......
......@@ -87,7 +87,7 @@ sig
| Signature of Signature1.t
| Lexicon of Lexicon.t
val empty : t
val insert : entry -> t -> t
val insert : ?override:bool -> entry -> t -> t
val get_signature : string -> t -> Signature1.t
val get_lexicon : string -> t -> Lexicon.t
val get : string -> t -> entry
......@@ -125,15 +125,15 @@ struct
let empty = {map=Env.empty;sig_number=0;lex_number=0;focus=None}
let insert d e = match d with
let insert ?(override=false) d e = match d with
| Signature s -> let name,(p1,p2) = Sg.name s in
if not (Env.mem name e.map)
if (not (Env.mem name e.map))||override
then
{e with map=Env.add name d e.map ;sig_number=e.sig_number+1}
else
raise (Error.Error (Error.Env_error (Error.Duplicated_signature name,(p1,p2))))
| Lexicon l -> let name,(p1,p2) = Lex.name l in
if not (Env.mem name e.map)
if not (Env.mem name e.map)||override
then
{e with map=Env.add name d e.map ;lex_number=e.lex_number+1}
else
......
......@@ -107,7 +107,7 @@ sig
(** [insert c e] adds the content [c] into the environment [e] and
returns the resulting environmnent *)
val insert : entry -> t -> t
val insert : ?override:bool -> entry -> t -> t
(** [get_signature name e] returns the signature of name [name] in
the environment [e]. Raise
......
......@@ -29,6 +29,7 @@ type lex_error =
| Mismatch_parentheses
| Unclosed_comment
| Expect of string
| Bad_token
type parse_error =
| Duplicated_term of string
......@@ -72,6 +73,7 @@ type error =
| Type_error of type_error * (Lexing.position * Lexing.position)
| Env_error of env_error * (Lexing.position * Lexing.position)
| Lexicon_error of lexicon_error * (Lexing.position * Lexing.position)
| System_error of string
......@@ -99,6 +101,7 @@ let lex_error_to_string = function
| Unclosed_comment -> "Syntax error: Unclosed comment"
| Mismatch_parentheses -> "Syntax error: Unclosed parenthesis"
| Expect s -> Printf.sprintf "Syntax error: %s expected" s
| Bad_token -> "Lexing error: no such token allowed"
let parse_error_to_string = function
| Duplicated_type ty -> Printf.sprintf "Syntax error: Type \"%s\" has already been defined" ty
......@@ -107,7 +110,7 @@ let parse_error_to_string = function
| Unknown_constant id -> Printf.sprintf "Syntax error: Unknown constant \"%s\"" id
| Unknown_type id -> Printf.sprintf "Syntax error: Unknown atomic type \"%s\"" id
| Missing_arg_of_Infix id -> Printf.sprintf "Syntax error: \"%s\" is defined as infix but used here with less than two arguments" id
| No_such_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" not in the current< environment" s
| No_such_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" not in the current environment" s
| Dyp_error -> "Dyp: Syntax error"
let type_error_to_string = function
......@@ -149,12 +152,15 @@ let warning_to_string w =
let error_msg e input_file =
let msg,location_msg =
match e with
| Parse_error (er,(s,e)) -> parse_error_to_string er,compute_comment_for_position s e
| Lexer_error (er,(s,e)) -> lex_error_to_string er,compute_comment_for_position s e
| Type_error (er,(s,e)) -> type_error_to_string er,compute_comment_for_position s e