Commit a9d70173 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Associativity and precedence specifications have been added.

parent 6379ff57
......@@ -3,10 +3,10 @@
** The acgc.opt/acgc compiler and the acg.opt/acg interpreter:
+ Some syntax changes:
1. Prefix operators have the highest priority
2. Infix operators have a higher priority than application (*Note:
this may break existing code*)
2. application has precedence over infix operators
3. An associativity property (none, left, right) can be set to infix
operators (left is the default), and a precedence level as well
operators (left is the default), and a precedence level as
well. See associativity and the precedence section in the README.
+ Removed the dependency to BOLT (replaced by Logs) and dypgen (replaced by menhir)
* Version 1.4.0
......
......@@ -3,8 +3,9 @@
* Removed the dependency to BOLT (replaced by Logs) and dypgen (replaced by menhir)
* Some syntax changes:
1. Prefix operators have the highest priority
2. Infix operators have a higher priority than application (*Note: this may break existing code*)
3. An associativity property (none, left, right) can be set to infix operators (left is the default), and a precedence level as well
2. Application has precedence over infix operators
3. An associativity property (none, left, right) can be set to infix operators (left is the default), and a precedence level as well. See the associativity and the precedence section in the [README](README.me).
* Removed the dependency to BOLT (replaced by Logs) and dypgen (replaced by menhir)
# Version 1.4.0
## The acgc.opt/acgc compiler and the acg.opt/acg interpreter:
......
......@@ -205,9 +205,9 @@ acgc.opt)
************************************
* Syntax of signature and lexicons *
************************************
************************
* Syntax of signatures *
************************
(see the examples/tag.acg file for an example)
......@@ -266,6 +266,43 @@ if SYM is a prefic symbol (highest priority)
BINDER x y z.t
if BINDER is a binder
+ About associativity and precedence of operators
Prefix operators have precedence over application, and application has
precedence over infix operators. Relative precedence among infix
operators can be defined.
When no associativity specification is set, the default is left
associative.
When no precedece definition is given, the default is higher
precedence over any infix operator defined so far.
When declaring or defining an infix operator with the keyword 'infix',
the optional specification for the associativity and the relative
precedence can be set.
A specification is given between square brackets. The syntax is as
follows:
infix [specification] SYM …
(the remaining part of the declaration is the same as without the specification)
A specification is non-empty comma-separated list of:
+ an (optional) associativity specification, given by one of the
keywords 'Left', 'Right', or 'NonAssoc'. If not present, left
associativity is set by default to infix operators
+ an (optional) precedence declaration (if not present, the highest
precedence over all the infix operators defined so far is given). It
is defined as '< SYM' (where SYM is a symbol). It assigns to the
operator being declared or defined the greates precedence *below* the precedence of SYM.
***********************
* Syntax of lexicons *
***********************
There are two ways to define a lexicon:
1. By using the keyword `lexicon` or `nl_lexicon` as in :
......
......@@ -187,6 +187,28 @@ end
* `SYM t` if `SYM` is a prefix symbol (highest priority)
* `BINDER x y z.t` if `BINDER` is a binder
* About associativity and precedence of operators
Prefix operators have precedence over application, and application has precedence over infix operators. Relative precedence among infix operators can be defined.
When no associativity specification is set, the default is left associative.
When no precedece definition is given, the default is higher precedence over any infix operator defined so far.
When declaring or defining an infix operator with the keyword 'infix', the optional specification for the associativity and the relative precedence can be set.
A specification is given between square brackets. The syntax is as follows:
```
infix [specification] SYM …
```
(the remaining part of the declaration is the same as without the specification)
A specification is non-empty comma-separated list of:
+ an (optional) associativity specification, given by one of the keywords `Left`, `Right`, or `NonAssoc`. If not present, left associativity is set by default to infix operators
+ an (optional) precedence declaration (if not present, the highest precedence over all the infix operators defined so far is given). It is defined as `< SYM` (where `SYM` is a symbol). It assigns to the operator being declared or defined the greates precedence *below* the precedence of `SYM`.
### Lexicons
......
......@@ -41,7 +41,7 @@ signature francais =
string : type;
(* the infix concatenation operator + *)
infix + : string -> string -> string;
infix [Right] + : string -> string -> string;
(* the empty string e *)
e : string;
......@@ -65,7 +65,7 @@ lexicon realisation_francais (syntax) : francais =
returns the concatenation subject+loves+object *)
AIMER := lambda o s.s + aime + o;
VOULOIR_CV := lambda vp. Lambda s. s + veut + (vp e);
VOULOIR_CV := lambda vp. Lambda s. s + veut + vp e;
VOULOIR_SC := lambda sc s. s + veut + sc;
CHAQUE := lambda n P. P (chaque + n);
......@@ -111,7 +111,7 @@ lexicon realisation_anglais (syntax) : anglais =
(* LOVE is interpreted as a function taking two arguments. The first one is the object and the second one is the subject. It returns the concatenation subject+loves+object *)
AIMER := lambda o s.s + loves + o;
VOULOIR_CV := lambda vp. Lambda s. s + wants + to + (vp e);
VOULOIR_CV := lambda vp. Lambda s. s + wants + to + vp e;
VOULOIR_SC := lambda sc s. s + wants + sc;
CHAQUE := lambda n P. P (every + n);
......
......@@ -27,7 +27,7 @@ signature strings =
string : type;
(* the infix concatenation operator + *)
infix + : string -> string -> string;
infix [Right] + : string -> string -> string;
(* the empty string e *)
e : string;
......
......@@ -108,7 +108,7 @@ signature strings =
(* We can define infix and prefix symbols.
Note that as for now, the length of symbols can only be 1. *)
infix + = lambda a b. lambda z. a (b z) : string -> string -> string;
infix [Right] + = lambda a b. lambda z. a (b z) : string -> string -> string;
every, dog, chases, a, cat, sleeps, slowly, new, big, black, seems,
john, mary, bill, paul, claims, loves, to, love, who, said, liked,
......@@ -152,6 +152,7 @@ lexicon tag_strings (derived_trees) : strings =
WH1, N1, VP1 := lambda f. f;
N2, S2, VP2 := lambda f g. f + g;
VP2 := (+);
end
......@@ -177,8 +178,8 @@ signature semantics =
(* And finally, here are the logical constants *)
infix & : t -> t -> t;
infix > : t -> t -> t;
infix [Right] & : t -> t -> t;
infix [Right, < & ] > : t -> t -> t;
binder All : (e => t) -> t;
binder Ex : (e => t) -> t;
......@@ -208,7 +209,9 @@ lexicon tag_semantics (derivation_trees) : semantics =
C_to_love := lambda s a O S. s (S (a (lambda x. O (lambda y. love x y))));
C_slowly := lambda vp r. vp (lambda x. slowly (r x));
C_seems := lambda vp r. vp (lambda x. seem r x);
C_new := lambda a n. a (Lambda x. (new x) & (n x));
C_new := lambda a n. a (Lambda x. new x & n x);
(* Application has precedence over operators such as & *)
(* So we can drop the parenthesis *)
C_big := lambda a n. a (Lambda x. (big x) & (n x));
C_black := lambda a n. a (Lambda x. (black x) & (n x));
C_claims := lambda sa a S comp. sa (S (a (lambda x. claim x comp)));
......
......@@ -45,7 +45,7 @@ let bad_infix_usage () = !infix_as_prefix
type lex_error =
| Unstarted_comment
| Unstarted_bracket
| Mismatch_parentheses
| Mismatch_parentheses of char
| Unclosed_comment
| Expect of string
| Bad_token
......@@ -56,6 +56,7 @@ type parse_error =
| Duplicated_type of string
| Binder_expected of string
| Unknown_constant of string
| Not_def_as_infix of string
| Unknown_constant_nor_variable of string
| Unknown_constant_nor_type of string
| Unknown_type of string
......@@ -131,7 +132,7 @@ let lex_error_to_string = function
| Unstarted_comment -> "Syntax error: No comment opened before this closing of comment"
| Unstarted_bracket -> "Syntax error: No bracket opened before this right bracket"
| Unclosed_comment -> "Syntax error: Unclosed comment"
| Mismatch_parentheses -> "Syntax error: Unclosed parenthesis"
| Mismatch_parentheses c -> Printf.sprintf "Syntax error: Unclosed parenthesis '%c'" c
| Expect s -> Printf.sprintf "Syntax error: %s expected" s
| Bad_token -> "Lexing error: no such token allowed"
......@@ -141,6 +142,7 @@ let parse_error_to_string = function
| Duplicated_term te -> Printf.sprintf "Syntax error: Term \"%s\" has already been defined" te
| Binder_expected id -> Printf.sprintf "Syntax error: Unknown binder \"%s\"" id
| Unknown_constant id -> Printf.sprintf "Syntax error: Unknown constant \"%s\"" id
| Not_def_as_infix id -> Printf.sprintf "Syntax error: \"%s\" is not an infix operator" id
| Unknown_constant_nor_variable id -> Printf.sprintf "Syntax error: Unknown constant or variable \"%s\"" id
| Unknown_constant_nor_type id -> Printf.sprintf "Syntax error: Unknown constant or type \"%s\"" id
| Unknown_type id -> Printf.sprintf "Syntax error: Unknown atomic type \"%s\"" id
......@@ -148,7 +150,7 @@ let parse_error_to_string = function
| No_such_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" not in the current environment" s
| No_such_lexicon s -> Printf.sprintf "Syntax error: Lexicon id \"%s\" not in the current environment" s
| Not_associative s -> Printf.sprintf "Syntax error: Operator \"%s\" is not associative but is used without parenthesis" s
| Not_infix s -> Printf.sprintf "Syntax error: Operator \"%s\" is not infix bus is used as infix" s
| Not_infix s -> Printf.sprintf "Syntax error: Operator \"%s\" is not infix but is used as infix" s
| Prefix_missing_arg s -> Printf.sprintf "Syntax error: The prefix operator \"%s\" is missing its argument" s
| Infix_missing_first_arg s -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s
| Infix_missing_second_arg s -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s
......
......@@ -26,7 +26,7 @@
type lex_error =
| Unstarted_comment
| Unstarted_bracket
| Mismatch_parentheses
| Mismatch_parentheses of char
| Unclosed_comment
| Expect of string
| Bad_token
......@@ -39,6 +39,7 @@ type parse_error =
| Duplicated_type of string
| Binder_expected of string
| Unknown_constant of string
| Not_def_as_infix of string
| Unknown_constant_nor_variable of string
| Unknown_constant_nor_type of string
| Unknown_type of string
......
......@@ -43,9 +43,9 @@ sig
(* val find_type : string -> t -> stype *)
val find_term : string -> t -> term * stype
val is_type : string -> t -> bool
val is_constant : string -> t -> bool*Abstract_syntax.syntactic_behavior option
val precedence : string -> t -> (float*Abstract_syntax.associativity) option
val new_precedence : t -> (float * t)
val is_constant : string -> t -> bool * Abstract_syntax.syntactic_behavior option
(*val precedence : string -> t -> (float*Abstract_syntax.associativity) option *)
val new_precedence : ?before:string -> string -> t -> (float * t)
val type_to_string : stype -> t -> string
val term_to_string : term -> t -> string
val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string
......
......@@ -80,20 +80,23 @@ sig
atomic type in [s] and [false] oterwise *)
val is_type : string -> t -> bool
(** [is_constant id s] returns [(true,Some b)] together with its
syntactic behaviour [b] if [id] is the name of a constant in [s]
and [false,None] oterwise *)
(** [is_constant id s] returns [(true,Some (b,pred))] together with
its syntactic behaviour [b] and its precedence [pred] if [id] is
the name of a constant in [s] and [false,None] oterwise *)
val is_constant : string -> t -> bool * Abstract_syntax.syntactic_behavior option
(** [precedence id s] returns a [Some f] where [f] is float
indicating the precedence of the infix operator [id]. It returns
[None] if [id] is not an infix operator. *)
val precedence : string -> t -> (float * Abstract_syntax.associativity) option
(** [new_precedence s] returns a pair consisting of a new precedence
value, higher thant any other one in the signature [s], and the
new signature taking this new value into account. *)
val new_precedence : t -> (float * t)
(* val precedence : string -> t -> (float * Abstract_syntax.associativity) option *)
(** [new_precedence ?before id s] returns a pair consisting of a new
precedence value associated to [id], and the new signature
taking this new value into account. If the optional string
argument [before] is not provided, then [id] is given the
highest precedence so far. Otherwise, it is given the precedence
just below [before].*)
val new_precedence : ?before:string -> string -> t -> (float * t)
(** [type_to_string ty sg] returns the string corresponding to a
type [ty] of type {!Logic.Lambda.Lambda.stype}) with respect to the
......
......@@ -49,9 +49,10 @@ struct
size:int;
terms:entry Symbols.t;
types:entry Symbols.t;
precedence: (float * string option) Symbols.t ; (* indicates the precedence and a link to the previous one *)
max_pred : float * string option ; (* indicates the greatest precedence and a link to the previous one *)
ids:entry Id.t;
is_2nd_order:bool;
precedence:float;
extension_timestamp:float;
definition_timestamp:float}
......@@ -98,7 +99,8 @@ struct
types=Symbols.empty;
ids=Id.empty;
is_2nd_order=true;
precedence = 0.;
precedence = Symbols.empty;
max_pred = 0., None ;
definition_timestamp=timestamp;
extension_timestamp=timestamp}
......@@ -288,23 +290,56 @@ struct
| _ -> false
| exception Symbols.Not_found -> false
let is_constant s {terms=syms} =
let is_constant s {terms=syms;precedence} =
match Symbols.find s syms with
| Term_declaration (_,_,behavior,_) -> true,Some behavior
| Term_definition (_,_,behavior,_,_) -> true,Some behavior
| _ -> false,None
| exception Symbols.Not_found -> false,None
let precedence s {terms=syms} =
match Symbols.find s syms with
| Term_declaration (_,_,Infix f,_) -> Some f
| Term_definition (_,_,Infix f,_,_) -> Some f
| _ -> None
let precedence s {precedence} =
match Symbols.find s precedence with
| f,_ -> Some f
| exception Symbols.Not_found -> None
let new_precedence sg =
let p = sg.precedence +. 1. in
p,{sg with precedence = p}
let new_precedence ?before id sg =
match before, sg.max_pred with
| None, (f, None) ->
let p = f +. 1. in
p, {sg with
max_pred = p, Some id;
precedence = Symbols.add id (p,None) sg.precedence}
| None, (f, (Some _ as max)) ->
let p = f +. 1. in
p, {sg with
max_pred = p, Some id;
precedence = Symbols.add id (p,max) sg.precedence}
| Some upper_bound, (f, None) ->
(* Strange to give an upper bound when there is no max. Behaves
like introducing the first element *)
let p = f +. 1. in
p, {sg with
max_pred = p, Some id;
precedence = Symbols.add id (p,None) sg.precedence}
| Some upper_bound, _ ->
(match Symbols.find upper_bound sg.precedence with
| f_up, None ->
let f_down = 0. in
let p = (f_up +. f_down)/. 2. in
let new_pred =
Symbols.add ~overwrite:true upper_bound
(f_up,Some id)
(Symbols.add id (p,None) sg.precedence) in
p, {sg with precedence = new_pred}
| f_up, Some lower_bound ->
let f_down,_ = Symbols.find lower_bound sg.precedence in
let p = (f_up +. f_down)/. 2. in
let new_pred =
Symbols.add upper_bound
(f_up,Some id)
(Symbols.add id (p,Some lower_bound) sg.precedence) in
p, {sg with precedence = new_pred}
| exception Not_found -> failwith "Bug: Shouldn't happen")
let add_warnings _ sg = sg
......@@ -430,10 +465,10 @@ module Table = Table.Make_table(struct let b = 10 end)
exception Conflict
let empty = IntMap.empty
let add ?(override=false) k v t =
let add ?(overwrite=false) k v t =
try
let _ = IntMap.find k t in
if override then IntMap.add k v t else raise Conflict
if overwrite then IntMap.add k v t else raise Conflict
with
| Not_found -> IntMap.add k v t
......
signature Integer =
int : type;
infix [Right] + : int -> int -> int ;
infix [Left, < +] - : int -> int -> int ;
infix [Right] * : int -> int -> int ;
infix [NonAssoc] / : int -> int -> int;
infix @ : int -> int -> int ;
prefix | : int -> int ;
prefix ! : int -> int ;
a, b, c, d : int;
x, y, z : int -> int;
end
\ No newline at end of file
......@@ -2,14 +2,14 @@
* DONE Add an optional ";" before the "end" keyword
* DONE Change lexers to avoid problems with keywords
* TODO Add precedence values and management in the signature
* DONE Add precedence values and management in the signature
* TODO Add (+) notation style to prevent the infix use of +
* TODO Add syntactic extensions to handle associativity and precedence of infix operators
* DONE Add syntactic extensions to handle associativity and precedence of infix operators
* TODO Add error (and warning) messages management to the Error module, and make a difference between "real" parsing errors and errors resulting from evaluating the parsing against some environment. The latter can be output all together (may be some limit to be set)
* DONE Move from dypgen to menhir in scripts
* TODO change README and INSTALL files:
* DONE change README and INSTALL files:
+ [X] to indicate new dependencies (menhir, logs...)
+ [ ] to document syntax extensions for infix operators, precedence of the latter over application. Highest precedence for prefix operators
* TODO What about lexicon composition when one lexicon at least is non-linear?
+ [X] to document syntax extensions for infix operators, precedence of the latter over application. Highest precedence for prefix operators
* DONE What about lexicon composition when one lexicon at least is non-linear?
* TODO Add debug flag (+ flag for log sources?)
* TODO Change command line parsing to use Cmd
......@@ -25,19 +25,34 @@
let loc lexbuf = Lexing.lexeme_start_p lexbuf,Lexing.lexeme_end_p lexbuf
type brackets =
| Round
| Square
| Curly
let brackets = ref []
let add_bracket loc = brackets:=loc::!brackets
let kind_to_char = function
| Round -> '('
| Square -> '['
| Curly -> '{'
let add_bracket br loc =
brackets:=(loc,br)::!brackets
let remove_bracket l = match !brackets with
let remove_bracket br l =
match !brackets with
| [] -> raise (Error.Error (Error.Lexer_error (Error.Unstarted_bracket, l)))
| _::tl -> brackets := tl
| (_,k)::tl when k = br -> brackets := tl
| (l,k)::_ ->
raise (Error.Error (Error.Lexer_error (Error.Mismatch_parentheses (kind_to_char k),l)))
let check_brackets () =
match !brackets with
| [] -> ()
| (p1,p2)::__ -> let () = brackets := [] in
raise (Error.Error (Error.Lexer_error (Error.Mismatch_parentheses,(p1,p2))))
| (loc,c)::_ ->
let () = brackets := [] in
raise (Error.Error (Error.Lexer_error (Error.Mismatch_parentheses (kind_to_char c),loc)))
type context =
| NoContext
......@@ -61,7 +76,7 @@ let letter = ['a'-'z' 'A'-'Z' '
let digit = ['0'-'9']
let string = (letter|digit|'_')*'\''*
let symbol = ['|' '!' '"' '#' '$' '%' '&' '\'' '*' '+' '-' '/' '<' '>' '?' '@' '[' '\\' ']' '^' '`' '{' '}' '~' ]
let symbol = ['|' '!' '"' '#' '$' '%' '&' '\'' '*' '+' '-' '/' '<' '>' '?' '@' '\\' '^' '`' '~' ]
let keyword = ("end" | "type" | "prefix" | "infix" | "binder" | "lambda" | "Lambda")
rule lexer =
......@@ -118,16 +133,24 @@ rule lexer =
let () = check_brackets () in
Data_parser.COLON(loc lexbuf)}
| [','] {
let () = check_brackets () in
(* let () = check_brackets () in *)
Data_parser.COMMA(loc lexbuf)}
| ['('] {
let l = loc lexbuf in
let () = add_bracket l in
let () = add_bracket Round l in
Data_parser.LPAREN l}
| [')'] {
let brac_loc = loc lexbuf in
let () = remove_bracket brac_loc in
let () = remove_bracket Round brac_loc in
Data_parser.RPAREN brac_loc}
| ['['] {
let l = loc lexbuf in
let () = add_bracket Square l in
Data_parser.LSQBRACKET l}
| [']'] {
let brac_loc = loc lexbuf in
let () = remove_bracket Square brac_loc in
Data_parser.RSQBRACKET brac_loc}
| ['.'] {
Data_parser.DOT(loc lexbuf)}
| "end" {
......
This diff is collapsed.
......@@ -9,9 +9,8 @@
(modules term_parser_test))
(menhir
; (flags (--explain --table --compile-errors /home/pogodall/work/dev/ACGtk/src/grammars/data_parser.messages))
(merge_into data_parser)
(flags (--explain --table))
(flags (--explain --table --strict))
(modules file_parser sig_parser lex_parser type_parser term_parser))
......
......@@ -44,95 +44,109 @@ let message =
"A type expression is expected.\n"
| 77 ->
"An equality symbol '=' is expected.\n"
| 124 | 78 ->
| 141 | 78 ->
"A signature entry (type declaration, type definition, term declaration, or term definition) is expected.\n"
| 75 ->
"A declaration of a signature (keyword 'signature') or of a lexicon (keyword 'lexicon' or 'nl_lexicon') is expected.\n"
| 133 ->
| 150 ->
"An identifier (the name of a new lexicon) is expected.\n"
| 134 ->
| 151 ->
"A left parenthesis '(' is expected.\n"
| 136 ->
| 153 ->
"A right parenthesis ')' is expected.\n"
| 137 ->
| 154 ->
"A colon ':' is expected.\n"
| 138 ->
| 155 ->
"An identifier (the name of a signature) is expected.\n"
| 139 ->
| 156 ->
"An equality symbol '=' is expected.\n"
| 141 ->
| 158 ->
"A semi-colon ';' or the 'end' keyword are expected.\n"
| 147 ->
| 164 ->
"An identifier (the name of a new lexicon) is expected\n"
| 148 ->
| 165 ->
"A left parenthesis '(' is expected.\n"
| 149 ->
| 166 ->
"An identifier (the name of a signature) is expected.\n"
| 150 ->
| 167 ->
"A right parenthesis ')' is expected.\n"
| 151 ->
| 168 ->
"A expression in the form of \": <identifier> =\" where the identifier is the name of a signature is expected.\n"
| 152 | 135 | 76 ->
| 169 | 152 | 76 ->
"An identifier (the name of a signature) is expected.\n"
| 153 ->
| 170 ->
"An equality symbold '=' is expected.\n"
| 154 | 142 | 140 ->
| 171 | 159 | 157 ->
"A lexicon entry of the form \"<term> := <term>;\" or \"<type> := <type>\" is expected.\n"
| 157 | 156 ->
| 174 | 173 ->
"An expression representing the composition of lexicons is expected.\n"
| 162 ->
| 179 ->
"The composition operator '<<' or a right parenthesis ')' is expected.\n"
| 159 | 166 ->
| 176 | 183 ->
"The composition operator '<<' is expected.\n"
| 160 ->
| 177 ->
"An identifier (the name of a lexicon), or an expression representing the composition of lexicons is expected.\n"
| 172 ->
| 189 ->
"An identifier or a keyword ('infix', 'prefix', or 'binder') is expected.\n"
| 87 | 79 ->
| 79 ->
"A symbol is expected.\n"
| 88 | 80 ->
"A typing judgmenet in the form of \": <type>;\" or a defintion in the form of \"= <term>: <type>;\" is expected.\n"
| 89 | 81 ->
| 95 ->
"An associativity specification (one of the keywords 'Left', 'Right', or 'NonAssoc') or a precedence specification in the form of \"< <sym>\" where \"<sym>\" is an other infix symbol are expected.\n"
| 99 ->
"A right square bracket ']' or a comma \",\" followed by a precedence specification in the form of \"< <sym>\" where \"<sym>\" is an other infix symbol are expected.\n"
| 98 ->
"An associativity specification (one of the keywords 'Left', 'Right', or 'NonAssoc') is expected.\n"
| 100 ->
"A precedence specification in the form of \"< <sym>\" where \"<sym>\" is an other infix symbol is expected.\n"
| 97 ->
"A right square bracket ']' or a comma ',' followed by an associativity specification (one of the keywords 'Left', 'Right', or 'NonAssoc') are expected.\n"
| 96 ->
"An identifier is expected.\n"
| 87 | 104 ->
"A symbol or a declaration of associativity an precedence property are expected.\n"
| 88 | 80 | 105 ->
"A typing judgement in the form of \": <type>;\" or a defintion in the form of \"= <term>: <type>;\" is expected.\n"
| 89 | 81 | 106 ->
"A typing judgment in the form \"<term> : <type>;\" is expected.\n"
| 90 | 82 ->
| 90 | 82 | 107 ->
"A typing judgment in the form \": <type>;\" is expected.\n"
| 93 | 91 | 85 | 83 ->
| 93 | 91 | 85 | 83 | 108 | 110 ->
"A type is expected after the colon ':'.\n"
| 95 ->
| 112 ->
"A comma ',' or a colon ':' are expected in a type or term declaration. An equality symbol '=' is expected in a type or term definition.\n"
| 96 ->
| 113 ->
"A definition in the form of \"<term> : <type>;\" or a type definition of the form \"<type> : type;\" (with the keyword 'type') is expected after a term or a type defintion, resp.\n"
| 100 ->
| 117 ->
"A typing judgement in the form of \": <type>\" is expected in a term definition.\n"
| 101 ->
| 118 ->
"A type is expected in a term definition.\n"
| 103 ->
| 120 ->
"A typing judgement in the form of \": <type>;\" or a type definition with a colon ':' and the 'type' keyword in the form of \": type;\" is expected in a term or a type definition.\n"
| 116 ->
| 133 ->
"The 'type' keyword or a typing judgement in the form of \": <type>;\" is expected after the definition of a type or a term, resp.\n"
| 97 ->
| 114 ->
"In a type definition, a colon ':' is expeced before the keyword 'type'.\n"
| 98 ->
| 115 ->
"In a type definition, the keyword 'type' is expected after the colon ':'.\n"
| 106 | 105 ->
| 123 | 122 ->
"After a term or type declaration of the form \"<ident1>, <ident2>\", a type declaration of the form \": type;\" (with the keyword 'type') or a typing judgment of the form \": <type>;\" is expected.\n"
| 126 ->
| 143 ->
"After a term declaration of the form \"<term>: \", a type expression and a semicolon \"<type> ;\" are expected.\n"
| 174 ->
| 191 ->
"After a term declaration of the form \"<term>: <type>\", a semicolon ';' is expected.\n"
| 108 ->
| 125 ->
"An identidier (the name of the binder) is expected after the keyword 'binder'.\n"
| 109 ->
| 126 ->
"A typing judgement in the form of \": <type>\" or a definition in the form of \"= <term> : <type>\" is expected after the declaration of a binder.\n"
| 110 ->
| 127 ->
"A term is expected as right hand side of a term definition.\n"
| 111 ->
| 128 ->
"A typing judgment in the form of \": <type>\" is expected after defining a binder.\n"
| 176 | 8 ->
| 193 | 8 ->
"A typing judgment in the form of \"<term> : <type>\" is expected.\n"
| 178 ->
| 195 ->
"A typing judgement in the form of \": <type>\" is expected after a term.\n"
| 180 | 179 | 114 | 112 | 123 ->
| 197 | 196 | 131 | 129 | 140 ->
"A type expression is expected after ':'.\n"
| _ ->
raise Not_found
......@@ -10,6 +10,8 @@ let tok_to_string = function
| Data_parser.EOI -> "EOI"
| Data_parser.LPAREN _ -> "LPAREN"
| Data_parser.RPAREN _ -> "RPAREN"
| Data_parser.RSQBRACKET _ -> "RSQBRACKET"
| Data_parser.LSQBRACKET _ -> "LSQBRACKET"
| Data_parser.SIG_OPEN _ -> "SIG_OPEN"
| Data_parser.LEX_OPEN _ -> "LEX_OPEN"
| Data_parser.NL_LEX_OPEN _ -> "NL_LEX_OPEN"
......
%{
type fixity = {prec_spec : string option ;
(* if not [None], specifies the operator with an immediately higher precedence *)
assoc : Logic.Abstract_syntax.Abstract_syntax.associativity option ;
}
let build_infix opt sym sg =
let sym_id,_ = sym in
match opt {assoc = None ; prec_spec = None } sg with
| {assoc = None ; prec_spec = None } ->
let p,sg' = Environment.Signature1.new_precedence sym_id sg in
sym,Abstract_syntax.Infix (Abstract_syntax.Left,p),sg'
| {assoc = None ; prec_spec = Some id } ->
let p,sg' = Environment.Signature1.new_precedence ~before:id sym_id sg in
sym,Abstract_syntax.Infix (Abstract_syntax.Left,p),sg'
| {assoc = Some a ; prec_spec = None} ->
let p,sg' = Environment.Signature1.new_precedence sym_id sg in
sym,Abstract_syntax.Infix (a,p),sg'
| {assoc = Some a ; prec_spec = Some id} ->
let p,sg' = Environment.Signature1.new_precedence ~before:id sym_id sg in
sym,Abstract_syntax.Infix (a,p),sg'
%}
%token <Logic.Abstract_syntax.Abstract_syntax.location> LSQBRACKET RSQBRACKET
%token <(string*Logic.Abstract_syntax.Abstract_syntax.location)> SYMBOL
%token <Logic.Abstract_syntax.Abstract_syntax.location> COMMA
......@@ -9,6 +35,7 @@
%start < AcgData.Environment.Environment.Signature1.t -> AcgData.Environment.Environment.t -> AcgData.Environment.Environment.Signature1.t> sig_entry_eoi
%%
sig_entry_eoi :
......@@ -92,8 +119,17 @@ sig_entry_eoi :
| ids = separated_nonempty_list(COMMA,IDENT) { fun sg -> List.map (fun id -> (id,Abstract_syntax.Default)) ids,sg }
| PREFIX sym = SYMBOL { fun sg -> [sym,Abstract_syntax.Prefix],sg }