Skip to content

GitLab

A
ACGtk
Commit b412c005 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files
Options

Fixed optional semi-colon for the last sig entry before the keyword "end"

parent d4ddbedd
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 528 additions and 291 deletions
src/grammars/data_parser.messages
View file @ b412c005
This diff is collapsed.
src/grammars/file_parser.mly
View file @ b412c005
......@@ -101,8 +101,34 @@
sig_or_lex:
| s=signature { fun e -> s e }
| l=lexicon { fun e -> l e }
signature :
signature :
| SIG_OPEN id=IDENT EQUAL entries = signature_end_of_dec
{
fun e ->
let s,loc = id in
if is_signature s e then
raise (Error.(Error (Env_error (Duplicated_signature s,loc))))
else
let new_sig =
List.fold_left
(fun acc entry -> entry acc e)
(Environment.Signature1.empty id)
entries in
Environment.(insert (Signature new_sig) false e)
}
signature_end_of_dec :
| entry = sig_entry SEMICOLON? END_OF_DEC
{
[entry]
}
| entry = sig_entry SEMICOLON entries = signature_end_of_dec
{ entry :: entries }
(*
| SIG_OPEN id=IDENT EQUAL entries=separated_list(SEMICOLON,sig_entry) END_OF_DEC
{
fun e ->
......@@ -117,7 +143,7 @@ sig_or_lex:
entries in
Environment.(insert (Signature new_sig) false e)
}
*)
lexicon :
| LEX_OPEN lex=lex_declaration
......@@ -131,11 +157,22 @@ lexicon :
%inline lex_declaration :
| lex=IDENT LPAREN abs=IDENT RPAREN COLON obj=IDENT EQUAL entries=separated_list(SEMICOLON,lex_entry) END_OF_DEC
| lex=IDENT LPAREN abs=IDENT RPAREN COLON obj=IDENT EQUAL END_OF_DEC
{
fun ~non_linear e ->
let lex_name,lex_loc = lex in
let abs',obj'= get_sig abs e,get_sig obj e in
if is_lexicon lex_name e then
raise (Error.(Error (Env_error (Duplicated_lexicon lex_name,lex_loc))))
else
let lex' = Environment.Lexicon.empty lex ~abs:abs' ~obj:obj' ~non_linear in
Environment.(insert (Lexicon lex') false e)
}
| lex=IDENT LPAREN abs=IDENT RPAREN COLON obj=IDENT EQUAL entries=separated_nonempty_list(SEMICOLON,lex_entry) END_OF_DEC
{fun ~non_linear e ->
let lex_name,lex_loc = lex in
(* let abs_name,abs_loc = abs in
let obj_name,obj_loc = obj in *)
let abs',obj'= get_sig abs e,get_sig obj e in
if is_lexicon lex_name e then
raise (Error.(Error (Env_error (Duplicated_lexicon lex_name,lex_loc))))
......@@ -144,6 +181,7 @@ lexicon :
(fun acc entry -> entry acc e)
(Environment.Lexicon.empty lex ~abs:abs' ~obj:obj' ~non_linear)
entries in
(* let lex' = entry lex' e in *)
let () = Environment.Lexicon.check lex' in
Environment.(insert (Lexicon lex') false e)
}
......
src/grammars/lex_parser.mly
View file @ b412c005
......@@ -10,7 +10,7 @@
lex_entry_eoi :
| e = lex_entry EOI { e }
%public lex_entry :
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=atomic_type_or_term
{
......
src/grammars/messages.ml
View file @ b412c005
......@@ -8,131 +8,131 @@ let message =
match s with
| 0 ->
"A term is expected.\n"
| 16 | 14 ->
| 27 | 25 ->
"A term or a colon \":\" are expected.\n"
| 2 ->
| 1 ->
"A term is expected.\n"
| 27 | 25 ->
| 35 | 39 | 17 | 18 | 21 | 22 ->
"A term or a right parenthesis \")\" are expected.\n"
| 4 ->
| 3 ->
"An identifier (the name of a bound variable) or a dot \".\" are expected.\n"
| 8 | 3 ->
| 7 | 2 ->
"An identifier (the name of a bound variable) is expected.\n"
| 22 | 29 | 11 ->
| 42 | 10 | 19 | 40 ->
"A term or a colon \":\" are expected.\n"
| 13 | 10 | 7 ->
| 9 | 6 ->
"A term is expected.\n"
| 49 ->
"An identifier (i.e., a type or a term) or a symbol are expected.\n"
| 62 ->
"An identifier (i.e., a type or a term) or a symbol are expected.\n"
| 74 ->
"A comma \",\" or an interpretation symbol \":=\" are expected.\n"
| 63 ->
| 75 ->
"An identifier (i.e., a type or a term) or a symbol are expected.\n"
| 54 | 53 | 31 | 30 ->
| 67 | 66 | 44 | 43 ->
"A term or a type are expected.\n"
| 55 | 45 ->
| 58 ->
"An arrow (\"->\" or \"=>\"), a right parenthesis, a term, or a semi-colon are expected.\n"
| 32 ->
| 45 ->
"An arrow (\"->\" or \"=>\"), a right parenthesis, or a semi-colon are expected.\n"
| 34 ->
| 47 ->
"An arrow (\"->\" or \"=>\"), or a semi-colon are expected.\n"
| 60 | 46 ->
| 72 | 59 ->
"An end of input is expected (no more keyword or semi-colon or colon).\n"
| 58 ->
| 70 ->
"An arrow (\"->\" or \"=>), a term, or a semi-colon are expected.\n"
| 41 | 39 | 43 | 35 ->
| 54 | 52 | 56 | 48 ->
"A type expression is expected.\n"
| 67 ->
| 79 ->
"An equality symbol \"=\" is expected.\n"
| 114 | 68 ->
| 127 | 80 ->
"A signature entry (type declaration, type definition, term declaration, or term definition) is expected.\n"
| 157 | 65 ->
| 77 ->
"A declaration of a signature (keyword \"signature\") or of a lexicon (keyword \"lexicon\" or \"nl_lexicon\") is expected.\n"
| 123 ->
| 135 ->
"An identifier (the name of a new lexicon) is expected.\n"
| 124 ->
| 136 ->
"A left parenthesis \"(\" is expected.\n"
| 126 ->
| 138 ->
"A right parenthesis \")\" is expected.\n"
| 127 ->
| 139 ->
"A colon \":\" is expected.\n"
| 128 ->
| 140 ->
"An identifier (the name of a signature) is expected.\n"
| 129 ->
| 141 ->
"An equality symbol \"=\" is expected.\n"
| 134 ->
| 146 ->
"A semi-colon \";\" or the \"end\" keyword are expected.\n"
| 137 ->
| 149 ->
"An identifier (the name of a new lexicon) is expected\n"
| 138 ->
| 150 ->
"A left parenthesis \"(\" is expected.\n"
| 139 ->
| 151 ->
"An identifier (the name of a signature) is expected.\n"
| 140 ->
| 152 ->
"A right parenthesis \")\" is expected.\n"
| 141 ->
| 153 ->
"A expression in the form of \": <identifier> =\" where the identifier is the name of a signature is expected.\n"
| 142 | 125 | 66 ->
| 154 | 137 | 78 ->
"An identifier (the name of a signature) is expected.\n"
| 143 ->
| 155 ->
"An equality symbold \"=\" is expected.\n"
| 144 | 135 | 130 ->
| 156 | 147 | 142 ->
"A lexicon entry of the form \"<term> := <term>;\" or \"<type> := <type>\" is expected.\n"
| 148 | 147 ->
| 161 | 160 ->
"An expression representing the composition of lexicons is expected.\n"
| 153 ->
| 166 ->
"The composition operator \"<<\" or a right parenthesis \")\" is expected.\n"
| 150 ->
| 163 | 170 ->
"The composition operator \"<<\" is expected.\n"
| 151 ->
| 164 ->
"An identifier (the name of a lexicon), or an expression representing the composition of lexicons is expected.\n"
| 163 ->
| 176 ->
"An identifier or a keyword (\"infix\", \"prefix, or \"binder\") is expected.\n"
| 77 | 69 ->
| 89 | 81 ->
"A symbol is expected.\n"
| 78 | 70 ->
| 90 | 82 ->
"A typing judgmenet in the form of \": <type>;\" or a defintion in the form of \"= <term>: <type>;\" is expected.\n"
| 79 | 71 ->
| 91 | 83 ->
"A typing judgment in the form \"term : <type>;\" is expected.\n"
| 80 | 72 ->
| 92 | 84 ->
"A typing judgment in the form \": <type>;\" is expected.\n"
| 83 | 81 | 75 | 73 ->
| 95 | 93 | 87 | 85 ->
"A type is expected after the colon \":\".\n"
| 85 ->
| 97 ->
"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"
| 86 ->
| 98 ->
"A definition in the form of \"<term> : <type>;\" or a type definition of the form \"<type> : type;\" is expected after a term or a type defintion, resp.\n"
| 90 ->
| 102 ->
"A typing judgement in the form of \": <type>\" is expected in a term definition.\n"
| 91 ->
| 103 ->
"A type is expected in a term definition.\n"
| 93 ->
| 105 ->
"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 expectedin a term or a type definition.\n"
| 106 ->
| 118 ->
"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"
| 87 ->
| 99 ->
"In a type definition, a colon \":\" is expeced before the keyword \"type\".\n"
| 88 ->
| 100 ->
"In a type definition, the keyword \"type\" is expected after the colon \":\".\n"
| 96 | 95 ->
| 108 | 107 ->
"After a term or type declaration of the form \"<ident1>, <ident2>\", a type declaration of the form \": type;\" (where type is a keyword) or a typing judgment of the form \": <type>;\" is expected.\n"
| 117 ->
| 130 ->
"After a term declaration of the form \"<term>: \", a type expression and a semicolon \"<type> ;\" are expected.\n"
| 165 ->
| 178 ->
"After a term declaration of the form \"<term>: <type>\", a semicolon \";\" is expected.\n"
| 98 ->
| 110 ->
"An identidier (the name of the binder) is expected after the keyword \"binder\".\n"
| 99 ->
| 111 ->
"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"
| 100 ->
| 112 ->
"A term is expected as right hand side of a term definition.\n"
| 101 ->
| 113 ->
"A typing judgment in the form of \": <type>\" is expected after defining a binder.\n"
| 167 ->
| 180 | 11 | 32 ->
"A typing judgment in the form of \"<term> : <type>\" is expected.\n"
| 169 ->
| 182 ->
"A typing judgement in the form of \": <type>\" is expected after a term.\n"
| 171 | 170 | 104 | 102 | 113 ->
| 184 | 183 | 116 | 114 | 126 ->
"A type expression is expected after \":\".\n"
| _ ->
raise Not_found
src/grammars/term2_parser.mly
View file @ b412c005
%{
let id_to_term (id,loc) typing_env sg warnings =
match Environment.Signature1.is_constant id sg,Typing_env.mem id typing_env with
| (true,_),false -> Abstract_syntax.Const (id,loc),loc,warnings
| (false,_),true -> Abstract_syntax.Var (id,loc),loc,warnings
| (true,_),true -> Abstract_syntax.Var (id,loc),loc,(Error.Variable_or_constant (id,loc))::warnings
| (false,_),false -> emit_parse_error (Error.Unknown_constant_nor_variable id) loc
%}
%token <Logic.Abstract_syntax.Abstract_syntax.location> LAMBDA
%token <Logic.Abstract_syntax.Abstract_syntax.location> LAMBDA0
%token <Logic.Abstract_syntax.Abstract_syntax.location> DOT
......@@ -28,21 +39,123 @@
%public term:
| t = atomic_type_or_term {
fun type_env sg warnings ->
let id,loc = t in
match Environment.Signature1.is_constant id sg,Typing_env.mem id type_env with
| (true,_),false -> Abstract_syntax.Const (id,loc),loc,warnings
| (false,_),true -> Abstract_syntax.Var (id,loc),loc,warnings
| (true,_),true -> Abstract_syntax.Var (id,loc),loc,(Error.Variable_or_constant (id,loc))::warnings
| (false,_),false -> emit_parse_error (Error.Unknown_constant_nor_variable id) loc
fun type_env sg warnings ->
id_to_term t type_env sg warnings
}
| t = not_atomic_term { t }
%public atomic_type_or_term:
| id = IDENT { id }
| LPAREN t = atomic_type_or_term RPAREN { t }
%public not_atomic_term:
ident_sequence:
| id0 = IDENT ids = IDENT+ { id0,ids }
%public not_atomic_term:
| id_seq = ident_sequence
{
fun type_env sg warnings ->
let id1,ids = id_seq in
let t,t_loc,ws = id_to_term id1 type_env sg warnings in
let res,res_loc,ws' =
List.fold_left
(fun (acc,loc,ws) id ->
let t',l',ws' = id_to_term id type_env sg ws in
let loc' = new_loc loc l' in
Abstract_syntax.App (acc,t',loc'),loc',ws')
(t,t_loc,ws)
ids in
res,res_loc,ws'
}
| id_seq = IDENT* sym = SYMBOL terms = term0*
{
fun type_env sg warnings ->
let sym_name,sym_loc = sym in
let sym_term =
match Environment.Signature1.is_constant sym_name sg with
| true,Some fix -> Term_sequence.Op (Abstract_syntax.Const (sym_name,sym_loc),fix,sym_loc)
| true,None -> failwith "Bug: Should no happen"
| false,_ -> emit_parse_error (Error.Unknown_constant sym_name) sym_loc in
let id_seq',ws =
List.fold_left
(fun (acc,ws) id ->
let t,l,ws' = (id_to_term id type_env sg ws) in
(Term_sequence.Term (t,l))::acc,ws')
([],warnings)
id_seq in
let terms,warnings' =
List.fold_left
(fun (lst,ws) t ->
let t',ws'= t type_env sg ws in
t'::lst,ws')
(sym_term::id_seq',ws)
terms in
let tok,stream = Term_sequence.next (List.rev terms) in
let result,result_loc = Term_sequence.parse_sequence [] tok stream sg in
result,result_loc, warnings'
}
| id_seq = IDENT+ LPAREN t = term RPAREN terms = term0*
{
fun type_env sg warnings ->
let term,loc,ws = t type_env sg warnings in
let term' = Term_sequence.Term (term,loc) in
let id_seq',ws' =
List.fold_left
(fun (acc,ws) id ->
let t,l,ws' = (id_to_term id type_env sg ws) in
(Term_sequence.Term (t,l))::acc,ws')
([],ws)
id_seq in
let terms,warnings =
List.fold_left
(fun (lst,ws) t ->
let t',ws'= t type_env sg ws in
t'::lst,ws')
(term'::id_seq',ws')
terms in
let tok,stream = Term_sequence.next (List.rev terms) in
let result,result_loc = Term_sequence.parse_sequence [] tok stream sg in
result,result_loc, warnings
}
| LPAREN t = not_atomic_term RPAREN terms = term0*
{
fun type_env sg warnings ->
let term,loc,ws = t type_env sg warnings in
let term' = Term_sequence.Term (term,loc) in
let terms,warnings =
List.fold_left
(fun (lst,ws) t ->
let t',ws'= t type_env sg ws in
t'::lst,ws')
([],ws)
terms in
let result,result_loc = Term_sequence.parse_sequence [] (Some term') (List.rev terms) sg in
result,result_loc, warnings
}
(*
| id_seq = IDENT* LPAREN t = not_atomic_term RPAREN terms = term0*
{
fun type_env sg warnings ->
let term,loc,ws = t type_env sg warnings in
let term' = Term_sequence.Term (term,loc) in
let id_seq' =
List.fold_left
(fun acc id -> (id_to_term id typing_env sg)::acc)
[]
id_seq in
let terms,warnings =
List.fold_left
(fun (lst,ws) t ->
let t',ws'= t type_env sg ws in
t'::lst,ws')
(term'::id_seq',ws)
terms in
let tok,stream = Term_sequence.next (List.rev terms) in
let result,result_loc = Term_sequence.parse_sequence [] tok stream sg in
result,result_loc, warnings
}
*)
(*
| t1 = term0 terms = term0+
{ fun type_env sg warning ->
let t1, ws = t1 type_env sg warning in
......@@ -55,6 +168,7 @@
terms in
let result,result_loc = Term_sequence.parse_sequence [] (Some t1) (List.rev terms) sg in
result,result_loc, warnings }
*)
| t = bound_term { t }
%inline bound_term :
......@@ -93,10 +207,10 @@
n_loc,
ws' }
| binder = IDENT vars = IDENT+ DOT t = term
| idents = ident_sequence DOT t = term
{
fun type_env sg warnings ->
let binder,loc = binder in
let (binder,loc),vars = idents in
let linearity =
match Environment.Signature1.is_constant binder sg with
| true,Some Abstract_syntax.Binder ->
......
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