Commit 5f509c82 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Simplified parsers for terms and types. Compiles, and test seem ok. Still needs a bit of cleaning

parent 67d9d8f2
......@@ -7,6 +7,8 @@
3. An associativity property (none, left, right) can be set to infix
operators (left is the default), and a precedence level as
well. See associativity and the precedence section in the README.
4. Infix operator can be used as usual constant by surrounding then
with left and right parenthesis, so that t SYM u = (SYM) t u
+ Removed the dependency to BOLT (replaced by Logs) and dypgen (replaced by menhir)
* Version 1.4.0
......
......@@ -5,6 +5,7 @@
1. Prefix operators have the highest priority
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).
4. Infix operator can be used as usual constant by surrounding then with left and right parenthesis, so that `t SYM u` = `(SYM) t u`
* Removed the dependency to BOLT (replaced by Logs) and dypgen (replaced by menhir)
# Version 1.4.0
......
......@@ -255,10 +255,15 @@ for linear abstraction
for non-linear abstraction
t u v
for application (eauql to (t u) v)
for application (equal to (t u) v)
t SYM u
if SYM is a infix symbol (lowest priority)
if SYM is a infix symbol (lowest priority). It is equal to
((SYM) t) u
where SYM is used as a usual constant, with the priority of application.
SYM t
if SYM is a prefic symbol (highest priority)
......@@ -300,6 +305,11 @@ A specification is non-empty comma-separated list of:
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.
It is possible to use an infix symbol as a normal constant by
surrounding it with left and right parenthesis, so that
t SYM u = (SYM) t u
***********************
* Syntax of lexicons *
***********************
......
......@@ -182,8 +182,8 @@ end
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 `(equivalent to to `(t u) v`)
* `t SYM u` if `SYM` is a infix symbol (lowest priority)
* `t u v` for application (equivalent to to `(t u) v`)
* `t SYM u` if `SYM` is a infix symbol (lowest priority). It is equal to `((SYM) t) u` where `SYM` is used as usual constant, with the priority of application
* `SYM t` if `SYM` is a prefix symbol (highest priority)
* `BINDER x y z.t` if `BINDER` is a binder
......@@ -209,6 +209,7 @@ end
+ 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`.
It is possible to use an infix symbol as a normal constant by surrounding it with left and right parenthesis, so that `t SYM u = (SYM) t u`
### Lexicons
......
......@@ -142,7 +142,7 @@ lexicon tag_strings (derived_trees) : strings =
claims := claims;
loves := loves;
to_love := to + love;
to_love := (+) to love;
who := who;
said := said;
liked := liked;
......
ACGC=acgc
#ACGC=acgc
BUILD_PATH=../../../_build/default/src/
#ACGC=$(BUILD_PATH)/grammars/acgc.exe
ACGC=$(BUILD_PATH)/grammars/acgc.exe
#ACG=$(BUILD_PATH)/scripting/acg.exe
.PHONY: default clean all archive
......
signature derived_trees =
(* It uses ony one type : the type of trees *)
tree : type;
(* Here are the non-terminal symbols we find in the trees, with
an index indicating their arity *)
WH1, N1, VP1 : tree -> tree;
N2, S2, VP2 : tree -> tree -> tree;
(* Here are the terminal symbols *)
every, dog, chases, a, cat, sleeps, slowly, new, big, black, seems,
john, mary, bill, paul, claims, loves, to_love, who, said, liked,
does, think : tree;
(* We define a few constants that will make the lexicon definitions
easier. *)
det = lambda d. lambda n. N2 d n
: tree -> (tree -> tree);
adv = lambda adv . lambda a v. a (VP2 v adv)
: tree -> (tree -> tree) -> (tree -> tree);
l_adj = lambda adj. lambda a n. a (N2 adj n)
: tree -> (tree -> tree) -> (tree -> tree);
r_adj = lambda adj. lambda a n. a (N2 n adj)
: tree -> (tree -> tree) -> (tree -> tree);
ctrl_v = lambda v. lambda v_root v_foot. v_root (VP2 v v_foot)
: tree -> (tree -> tree) -> (tree -> tree);
np = lambda proper_name. N1 proper_name
: tree -> tree;
inf_tv = lambda v. lambda s a np0 np1. S2 np1 (s (S2 np0 (a (VP1 v))))
: tree -> (tree -> tree) -> (tree -> tree) -> tree -> tree -> tree;
wh_extract_tv = lambda v. lambda s adv wh subj. S2 wh (s (S2 subj (adv (VP1 v))))
: tree -> (tree -> tree) -> (tree -> tree) -> tree -> tree -> tree;
end
\ No newline at end of file
load o test-fix.acgo;
select Integer;
check a + b + c + a + | b + d : int;
#In Integer:
# a + (b + (c + (a + ((| b) + d)))) : int
check a + b + c + a + ! | b + d : int;
#In Integer:
# a + (b + (c + (a + ((! (| b)) + d)))) : int
check a + b * c : int;
#In Integer:
# a + (b * c) : int
check a - b - b + c : int;
#In Integer:
# (a - b) - (b + c) : int
check a / b / c : int;
#check a / b / c : int;
#
#[ERROR]a / b / c : int
#[ERROR]File "stdin", line 1, characters 2-3
#Syntax error: Operator "/" is not associative but is used without parenthesis
%on_error_reduce bound_term_ending(EOI)
%on_error_reduce bound_term_ending(COLON)
%on_error_reduce bound_term_ending(SEMICOLON)
%%
%public bound_term(phantom) :
| binder = LAMBDA vars_and_term = bound_term_ending(phantom)
{ fun _ ->
let vars,(term_builder,t_loc) = vars_and_term in
let n_loc = new_loc binder t_loc in
let term_builder type_env sg warnings =
let type_env = List.fold_left
(fun acc (var,_) -> Typing_env.add var acc)
type_env
vars in
let t,ws = term_builder type_env sg warnings in
(fst
(List.fold_left
(fun (acc,first_var) (var,loc) ->
if first_var then
(fun t -> acc (abs (var,n_loc,t) Abstract_syntax.Non_linear)),false
else
(fun t -> acc (abs (var,loc,t) Abstract_syntax.Non_linear)),false)
((fun x -> x),true)
vars)) t,
ws in
Term (term_builder,n_loc)
}
| binder = LAMBDA0 vars_and_term = bound_term_ending(phantom)
{ fun _ ->
let vars,(term_builder,t_loc) = vars_and_term in
let n_loc = new_loc binder t_loc in
let term_builder type_env sg warnings =
let type_env = List.fold_left
(fun acc (var,_) -> Typing_env.add var acc)
type_env
vars in
let t,ws = term_builder type_env sg warnings in
(fst
(List.fold_left
(fun (acc,first_var) (var,loc) ->
if first_var then
(fun t -> acc (abs (var,n_loc,t) Abstract_syntax.Linear)),false
else
(fun t -> acc (abs (var,loc,t) Abstract_syntax.Linear)),false)
((fun x -> x),true)
vars)) t,
ws in
Term (term_builder,n_loc) }
| binder = IDENT vars_and_term = bound_term_ending(phantom)
{fun _ ->
let binder,loc = binder in
let vars,(term_builder,t_loc) = vars_and_term in
let n_loc = new_loc loc t_loc in
let term_builder type_env sg warnings =
let linearity =
match Environment.Signature1.is_constant binder sg with
| true,Some Abstract_syntax.Binder ->
(match Environment.Signature1.get_binder_argument_functional_type binder sg with
| None -> failwith "Bug: Binder of non functional type"
| Some k -> k)
| _ -> emit_parse_error (Error.Binder_expected binder) loc in
let type_env = List.fold_left
(fun acc (var,_) -> Typing_env.add var acc)
type_env
vars in
let t,ws = term_builder type_env sg warnings in
Abstract_syntax.App
(Const (binder,loc),
(fst (List.fold_left
(fun (acc,first_var) (var,loc) ->
if first_var then
(fun t -> acc (abs (var,n_loc,t) linearity )),false
else
(fun t -> acc (abs (var,loc,t) linearity )),false)
((fun x -> x),true)
vars)) t,
n_loc),
ws in
Term (term_builder,n_loc) }
bound_term_ending(phantom) :
| var = IDENT DOT t=type_or_term(phantom) {[var],
match t false with
| Type_or_term_or_ident (_,term_builder,_,loc)
| Term_or_ident (term_builder,_,loc)
| Type_or_term (_,term_builder,loc)
| Term (term_builder,loc) -> term_builder,loc
| Type (_,loc) ->
emit_parse_error (Error.Syntax_error "A term is expected (not a type).") loc
}
| var = IDENT vars_and_term = bound_term_ending(phantom) {let vars,t = vars_and_term in var::vars,t}
This diff is collapsed.
......@@ -11,7 +11,7 @@
(menhir
(merge_into data_parser)
(flags (--explain --table --strict))
(modules file_parser sig_parser lex_parser term_type_parser))
(modules file_parser sig_parser lex_parser term_type_parser bound_term_parser))
;; Rule to generate the messages ml file
......@@ -22,7 +22,7 @@
(alias update)
(alias check)
(:message_file data_parser.messages.new)
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly)
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly bound_term_parser.mly)
)
(action
(with-stdout-to messages.ml (run %{bin:menhir} --base data_parser --explain --table --compile-errors %{message_file} %{parsers})))
......@@ -31,7 +31,7 @@
;; Rule to generate the automatic message file
(rule
(targets data_parser.messages.automatic)
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly))
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly bound_term_parser.mly))
(action
(with-stdout-to data_parser.messages.automatic (run %{bin:menhir} --base data_parser --explain --table --list-errors %{parsers})))
)
......@@ -39,7 +39,7 @@
;; Rule to generate the message file
(rule
(targets data_parser.messages.new)
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly))
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly bound_term_parser.mly))
(action (with-stdout-to data_parser.messages.new (run %{bin:menhir} --base data_parser --explain --table --update-errors data_parser.messages %{parsers}))
)
)
......@@ -54,7 +54,7 @@
(deps
data_parser.messages.automatic
data_parser.messages
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly)
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly bound_term_parser.mly)
)
(action (run %{bin:menhir} --base data_parser --explain --table --compare-errors data_parser.messages.automatic --compare-errors data_parser.messages %{parsers}))
)
......
%{
open Parser_types
let add_cst_interpretations term abs_sig lex (id,l) =
match Environment.Signature1.is_constant id abs with
match Environment.Signature1.is_constant id abs_sig with
| true,_ -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) lex
| false,_ -> emit_parse_error (Error.Unknown_constant id) l
let add_type_interpretation stype abs_sig lex (id,l) =
match Environment.Signature1.is_type id abs with
| true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,term)) acc
match Environment.Signature1.is_type id abs_sig with
| true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) lex
| false -> emit_parse_error (Error.Unknown_type id) l
%}
......@@ -28,20 +28,28 @@
%public lex_entry :
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=type_or_term
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=type_or_term(SEMICOLON)
{
fun lex e ->
let abs,obj = Environment.Lexicon.get_sig lex in
match t with
| t,Term_k ->
let term = get_term t Typing_env.empty obj [] in
List.fold_left (add_cst_interpretations term abs) lex cst
| t,Type_k ->
let stype = get_type t obj [] in
List.fold_left (add_type_interpretation stype abs) lex cst
| t,Both ->
let term = get_term t Typing_env.empty obj [] in
let stype = get_type t obj [] in
let are_types,are_terms =
List.fold_left
(fun (are_types,are_terms) (id,loc) ->
match Environment.Signature1.is_type id abs,Environment.Signature1.is_constant id abs with
| false,(false, _) -> emit_parse_error (Error.Unknown_constant_nor_type id) loc
| false,(true, _) when not are_terms -> emit_parse_error (Error.Unknown_type id) loc
| false,(true, _) -> false,true
| true,(false, _) when not are_types -> emit_parse_error (Error.Unknown_constant id) loc
| true,(false, _) -> true,false
| true,(true,_) -> true && are_types,true && are_terms)
(true,true)
cst in
match t false,are_types,are_terms with
| _,false,false -> failwith "Bug: Should not happen"
| Type_or_term_or_ident (type_builder, term_builder,_,_),true,true
| Type_or_term (type_builder, term_builder,_),true,true ->
let term,_ = term_builder Typing_env.empty obj [] in
let stype,_ = type_builder obj [] in
List.fold_left
(fun acc cst ->
add_type_interpretation
......@@ -49,59 +57,20 @@
abs
(add_cst_interpretations term abs acc cst)
cst)
}
(*
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=type_or_term
{
fun lex e ->
let abs,obj = Environment.Lexicon.get_sig lex in
let id,loc = t in
match fst (Environment.Signature1.is_constant id obj), Environment.Signature1.is_type id obj with
| true,false ->
let term = Abstract_syntax.Const t in
List.fold_left
(fun acc (id,l) ->
match Environment.Signature1.is_constant id abs with
| true,_ -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc
| false,_ -> emit_parse_error (Error.Unknown_constant id) l)
lex
cst
| false,true ->
let stype = Abstract_syntax.Type_atom (id,loc,[]) in
List.fold_left
(fun acc (id,l) ->
match Environment.Signature1.is_type id abs with
| true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc
| false -> emit_parse_error (Error.Unknown_type id) l)
lex
cst
| true,true ->
let term = Abstract_syntax.Const t in
let stype = Abstract_syntax.Type_atom (id,loc,[]) in
let kind =
List.fold_left
(fun acc (id,l) ->
match acc,(fst (Environment.Signature1.is_constant id abs)),Environment.Signature1.is_type id abs with
| Both,false,true -> Type
| Both,true,false -> Term
| Both,true,true -> Both
| Type,_,true -> Type
| Type,_,false -> emit_parse_error (Error.Unknown_type id) l
| Term,true,_ -> Term
| Term,false,_ -> emit_parse_error (Error.Unknown_constant id) l
| _,false,false -> raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),l)))))
Both
cst in
List.fold_left
(fun acc (id,l) ->
match kind with
| Type -> Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc
| Term -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc
| Both ->
let acc' = Environment.Lexicon.insert (Abstract_syntax.Constant (id,l,term)) acc in
Environment.Lexicon.insert (Abstract_syntax.Type (id,l,stype)) acc')
lex
cst
| false,false -> raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),loc))))
}
*)
lex
cst
| Type_or_term_or_ident (_, term_builder,_,_),_,true
| Type_or_term (_, term_builder,_),_,true
| Term_or_ident (term_builder,_,_),_,true
| Term (term_builder,_),_,true ->
let term,_ = term_builder Typing_env.empty obj [] in
List.fold_left (fun acc cst -> add_cst_interpretations term abs acc cst) lex cst
| Type_or_term_or_ident (type_builder, _,_,_),true,_
| Type_or_term (type_builder, _,_),true,_
| Type (type_builder,_),true,_ ->
let stype,_ = type_builder obj [] in
List.fold_left (add_type_interpretation stype abs) lex cst
| Type (_,l),false,_ -> emit_parse_error (Error.Syntax_error "A type \"<type>\" is expected.") l
| Term_or_ident (_,_,l),_,false
| Term (_,l),_,false-> emit_parse_error (Error.Syntax_error "A term \"<term>\" is expected.") l
}
......@@ -6,147 +6,137 @@
let message =
fun s ->
match s with
| 0 ->
"A term is expected.\n"
| 27 | 25 ->
| 132 | 205 | 207 ->
"A term, an arrow ('->' or '=>'), a left parenthesis '(', or a colon ':' are expected."
| 100 | 108 | 125 ->
"A term, a left parenthesis '(', or a colon ':' are expected.\n"
| 69 | 83 ->
"A term, a left parenthesis '(', or a semi-colon ';' are expected.\n"
| 68 | 81 ->
"A term, an arrow ('->' or '=>'), a left parenthesis '(', or a semi-colon ';' are expected.\n"
| 14 | 17 ->
"A type \"<type>\" is expected.\n"
| 0 | 65 ->
"A term \"<term>\" is expected.\n"
| 23 | 26 ->
"A term or a colon ':' are expected.\n"
| 1 ->
"A term is expected.\n"
| 32 | 37 | 17 | 18 | 21 | 22 ->
| 21 | 22 ->
"A term or a right parenthesis ')' are expected.\n"
| 3 ->
| 4 | 64 | 66 ->
"An identifier (the name of a bound variable) or a dot '.' are expected.\n"
| 5 | 2 ->
| 6 | 3 | 63 ->
"An identifier (the name of a bound variable) is expected.\n"
| 40 | 7 | 19 | 38 ->
"A term or a colon ':' are expected.\n"
| 4 ->
| 5 ->
"A term is expected.\n"
| 60 ->
| 56 ->
"An identifier (i.e., a type or a term) or a symbol are expected.\n"
| 72 ->
| 90 ->
"A comma ',' or an interpretation symbol ':=' are expected.\n"
| 73 ->
| 91 ->
"An identifier (i.e., a type or a term) or a symbol are expected.\n"
| 65 | 64 | 42 | 41 ->
| 62 | 60 | 27 ->
"A term or a type are expected.\n"
| 56 ->
"An arrow ('->' or '=>'), a right parenthesis, a term, or a semi-colon are expected.\n"
| 43 ->
"An arrow ('->' or '=>'), a right parenthesis, or a semi-colon are expected.\n"
| 45 ->
| 82 ->
"An arrow ('->' or '=>'), or a semi-colon are expected.\n"
| 70 | 57 ->
"An end of input is expected (no more keyword or semi-colon or colon).\n"
| 68 ->
| 41 | 44 ->
"A type or an end of input are expected (no more keyword or semi-colon or colon).\n"
| 48 ->
"An arrow ('->' or '=>'), a right parenthesis ')', or an end of input are expected (no more keyword or semi-colon or colon).\n"
| 29 | 30 | 31 | 32 | 33 | 36 | 49 | 50 | 53 ->
"An arrow ('->' or '=>'), a left parenthesis '(', or an end of input are expected (no more keyword or semi-colon or colon).\n"
| 88 | 61 ->
"An arrow ('->' or '=>'), a term, or a semi-colon are expected.\n"
| 52 | 50 | 54 | 46 ->
| 77 | 74 ->
"A type expression is expected.\n"
| 77 ->
| 95 ->
"An equality symbol '=' is expected.\n"
| 141 | 78 ->
| 152 | 96 | 151 ->
"A signature entry (type declaration, type definition, term declaration, or term definition) is expected.\n"
| 75 ->
| 93 ->
"A declaration of a signature (keyword 'signature') or of a lexicon (keyword 'lexicon' or 'nl_lexicon') is expected.\n"
| 150 ->
| 161 ->
"An identifier (the name of a new lexicon) is expected.\n"
| 151 ->
| 162 ->
"A left parenthesis '(' is expected.\n"
| 153 ->
| 164 ->
"A right parenthesis ')' is expected.\n"
| 154 ->
| 165 | 9 ->
"A colon ':' is expected.\n"
| 155 ->
| 166 ->
"An identifier (the name of a signature) is expected.\n"
| 156 ->
| 167 ->
"An equality symbol '=' is expected.\n"
| 158 ->
| 169 ->
"A semi-colon ';' or the 'end' keyword are expected.\n"
| 164 ->
| 175 ->
"An identifier (the name of a new lexicon) is expected\n"
| 165 ->
| 176 ->
"A left parenthesis '(' is expected.\n"
| 166 ->
| 177 ->
"An identifier (the name of a signature) is expected.\n"
| 167 ->
| 178 ->
"A right parenthesis ')' is expected.\n"
| 168 ->
| 179 ->
"A expression in the form of \": <identifier> =\" where the identifier is the name of a signature is expected.\n"
| 169 | 152 | 76 ->
| 180 | 163 | 94 ->
"An identifier (the name of a signature) is expected.\n"
| 170 ->
| 181 ->
"An equality symbold '=' is expected.\n"
| 171 | 159 | 157 ->
| 182 | 170 | 168 ->
"A lexicon entry of the form \"<term> := <term>;\" or \"<type> := <type>\" is expected.\n"
| 174 | 173 ->
| 185 | 184 ->
"An expression representing the composition of lexicons is expected.\n"
| 179 ->
| 190 ->
"The composition operator '<<' or a right parenthesis ')' is expected.\n"
| 176 | 183 ->
| 187 | 194 ->
"The composition operator '<<' is expected.\n"
| 177 ->
| 188 ->
"An identifier (the name of a lexicon), or an expression representing the composition of lexicons is expected.\n"
| 189 ->
| 200 ->
"An identifier or a keyword ('infix', 'prefix', or 'binder') is expected.\n"
| 79 ->
| 97 ->
"A symbol is expected.\n"
| 95 ->
| 113 ->
"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 ->
| 117 ->
"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 ->
| 116 ->
"An associativity specification (one of the keywords 'Left', 'Right', or 'NonAssoc') is expected.\n"
| 100 ->
| 118 ->
"A precedence specification in the form of \"< <sym>\" where \"<sym>\" is an other infix symbol is expected.\n"
| 97 ->
| 115 ->
"A right square bracket ']' or a comma ',' followed by an associativity specification (one of the keywords 'Left', 'Right', or 'NonAssoc') are expected.\n"
| 96 ->
| 114 ->
"An identifier is expected.\n"
| 87 | 104 ->
| 105 | 122 ->
"A symbol or a declaration of associativity an precedence property are expected.\n"
| 88 | 80 | 105 ->
| 106 | 98 | 123 ->
"A typing judgement in the form of \": <type>;\" or a defintion in the form of \"= <term>: <type>;\" is expected.\n"
| 89 | 81 | 106 ->
| 107 | 99 | 124 ->
"A typing judgment in the form \"<term> : <type>;\" is expected.\n"
| 90 | 82 | 107 ->
| 1 ->
"A typing judgment in the form \": <type>;\" is expected.\n"
| 93 | 91 | 85 | 83 | 108 | 110 ->
| 111 | 109 | 103 | 101 | 126 | 128 ->
"A type is expected after the colon ':'.\n"
| 112 ->
| 130 ->
"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"
| 113 ->
| 131 ->
"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"
| 117 ->
"A typing judgement in the form of \": <type>\" is expected in a term definition.\n"
| 118 ->
"A type is expected in a term definition.\n"
| 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"
| 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"
| 114 ->
"In a type definition, a colon ':' is expeced before the keyword 'type'.\n"
| 115 ->
"In a type definition, the keyword 'type' is expected after the colon ':'.\n"
| 123 | 122 ->
| 137 | 136 | 154 | 202 ->
"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"
| 143 ->
"After a term declaration of the form \"<term>: \", a type expression and a semicolon \"<type> ;\" are expected.\n"
| 191 ->
"After a term declaration of the form \"<term>: <type>\", a semicolon ';' is expected.\n"
| 125 ->
| 139 ->
"An identidier (the name of the binder) is expected after the keyword 'binder'.\n"
| 126 ->
| 140 ->
"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"
| 127 ->
| 141 ->
"A term is expected as right hand side of a term definition.\n"
| 128 ->
"A typing judgment in the form of \": <type>\" is expected after defining a binder.\n"
| 193 | 8 ->
| 142 ->
"A term, a left parenthesis '(', or a colon ':' for a typing judgment in the form of \": <type>\" is expected after defining a binder.\n"
| 204 | 2 ->
"A typing judgment in the form of \"<term> : <type>\" is expected.\n"
| 195 ->
"A typing judgement in the form of \": <type>\" is expected after a term.\n"
| 197 | 196 | 131 | 129 | 140 ->
| 8 ->
"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"
| 35 | 206 | 145 | 143 | 133 | 28 ->
"A type expression is expected after ':'.\n"
| _ ->
raise Not_found
type kind =
| Type_k
| Term_k
| Both
type kind_parameter =
| Type
| Term
......
......@@ -66,27 +66,27 @@ sig_entry_eoi :
type_definition :
| id = IDENT EQUAL type_or_cst = type_or_term COLON TYPE
| id = IDENT EQUAL type_or_cst = type_or_term(COLON) COLON TYPE
{
fun sg _ ->
let id_name,id_loc = id in
let type_expr,type_expr_loc,_ = get_type type_or_cst sg [] in
let type_expr,_ = get_type (type_or_cst false) sg [] in
try
Environment.Signature1.add_entry (Abstract_syntax.Type_def (id_name,id_loc,type_expr,Abstract_syntax.K [])) s
Environment.Signature1.add_entry (Abstract_syntax.Type_def (id_name,id_loc,type_expr,Abstract_syntax.K [])) sg
with
| Environment.Signature1.Duplicate_type_definition ->
emit_parse_error (Error.Duplicated_type id_name) id_loc
}
term_declaration :
| dec = term_dec_start COLON type_exp = type_or_term
| dec = term_dec_start COLON type_exp = type_or_term (SEMICOLON)
{
fun s e ->
let dec',s' = dec s in
List.fold_left
(fun acc ((id,loc),kind) ->
try
let ty = get_type type_exp acc [] in
let ty,_ = get_type (type_exp false) acc [] in
Environment.Signature1.add_entry (Abstract_syntax.Term_decl (id,kind,loc,ty)) acc
with
| Environment.Signature1.Duplicate_term_definition ->
......@@ -111,27 +111,27 @@ term_declaration :
| BINDER id = IDENT { fun sg -> [id,Abstract_syntax.Binder],sg }
term_definition :
| id = IDENT EQUAL t = type_or_term COLON ty = type_or_term
| id = IDENT EQUAL t = type_or_term(COLON) COLON ty = type_or_term(SEMICOLON)
{
fun s _ ->
let id',l = id in
try
(* Attention, BUG : pas de gestion des warnings !!! *)
let term,_,_ = get_term t Typing_env.empty s [] in
let ty',_ = get_type ty s [] in
let term,_ = get_term (t false) Typing_env.empty s [] in
let ty',_ = get_type (ty false) s [] in
Environment.Signature1.add_entry (Abstract_syntax.Term_def (id',Abstract_syntax.Default,l,term,ty')) s
with
| Environment.Signature1.Duplicate_term_definition ->
emit_parse_error (Error.Duplicated_term id') l}
| def = term_def_start EQUAL t = type_or_term COLON ty = type_or_term