Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 8519b0ef authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

ACG data files parsers rewrinting is now completed.

parent 5f509c82
......@@ -310,6 +310,8 @@ surrounding it with left and right parenthesis, so that
t SYM u = (SYM) t u
See examples/infix-examples and examples/infix-examples-script for examples.
***********************
* Syntax of lexicons *
***********************
......
......@@ -210,6 +210,8 @@ 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`
See [examples/infix-examples](examples/infix-examples) and [examples/infix-examples-script](examples/infix-examples) for examples.
### Lexicons
......
load o test-fix.acgo;
select Integer;
check a + b + c + a + | b + d : int;
#In Integer:
# a + (b + (c + (a + ((| b) + d)))) : int
# Is interpreted as:
# a + (b + (c + (a + ((| b) + d)))) : int
check a + b + c + a + ! | b + d : int;
#In Integer:
# a + (b + (c + (a + ((! (| b)) + d)))) : int
# Is interpreted as:
# a + (b + (c + (a + ((! (| b)) + d)))) : int
check a + b * c : int;
#In Integer:
# a + (b * c) : int
#Is interpreted as:
# a + (b * c) : int
check a - b - b + c : int;
#In Integer:
# (a - b) - (b + c) : int
#Is interpreted as:
# (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
# Raises an error as "/" is defined as non-associative
......@@ -9,6 +9,11 @@ signature Integer =
prefix ! : int -> int ;
a, b, c, d : int;
x, y, z : int -> int;
(* The following line is a valid definition, *)
(* as the '+' operator is surrounded by parenthesis *)
(* that make it lose its infix nature.*)
new_op = (+) : int -> int -> int;
(* However, the following line is NOT a valid definition, as *)
(* the '+' operator is infix and should be used between 2 terms*)
(* new_op = + : int -> int -> int;*)
end
\ No newline at end of file
signature toto =
a,b,c : type;
a:b -> a -> b;
x:b ;
E = a lambda x :a -> b;
end
\ No newline at end of file
......@@ -8,37 +8,55 @@
%public bound_term(phantom) :
| binder = LAMBDA vars_and_term = bound_term_ending(phantom)
{ fun _ ->
let vars,(term_builder,t_loc) = vars_and_term in
{ fun kind _ ->
let vars,(bounded_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)
let type_builder _ _ =
emit_parse_error
(Error.Syntax_error "A type identifier is expected") binder in
if kind = Type_ctx then
type_builder () ()
else
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 =
match bounded_term_builder with
| Type_or_term (_,t_builder,_) ->
t_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
Type_or_term (type_builder,term_builder,n_loc)
}
| binder = LAMBDA0 vars_and_term = bound_term_ending(phantom)
{ fun _ ->
let vars,(term_builder,t_loc) = vars_and_term in
{ fun kind _ ->
let vars,(bounded_term_builder,t_loc) = vars_and_term in
let n_loc = new_loc binder t_loc in
let type_builder _ _ =
emit_parse_error
(Error.Syntax_error "A type identifier is expected") binder in
if kind = Type_ctx then
type_builder () ()
else
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
vars in
let t,ws =
match bounded_term_builder with
| Type_or_term (_,t_builder,_) ->
t_builder type_env sg warnings in
(fst
(List.fold_left
(fun (acc,first_var) (var,loc) ->
......@@ -49,25 +67,41 @@
((fun x -> x),true)
vars)) t,
ws in
Term (term_builder,n_loc) }
Type_or_term (type_builder,term_builder,n_loc) }
| binder = IDENT vars_and_term = bound_term_ending(phantom)
{fun _ ->
{fun kind _ ->
let binder,loc = binder in
let vars,(term_builder,t_loc) = vars_and_term in
let vars,(bounded_term_builder,t_loc) = vars_and_term in
let n_loc = new_loc loc t_loc in
let type_builder sg warnings =
match Environment.Signature1.is_type binder sg,vars_and_term with
| true,((_,var_loc)::_,_) ->
emit_parse_error
(Error.Syntax_error "An arrow ('->' or '=>') or a right parenthesis ')' are expected.") var_loc
| true,([],_) -> failwith "Bug: should not happen"
| false,_ -> emit_parse_error (Error.Unknown_type binder) loc in
let () =
match kind, vars_and_term with
| Type_ctx,((_,var_loc)::_,_) ->
emit_parse_error
(Error.Syntax_error "An arrow ('->' or '=>') or a right parenthesis ')' are expected.") var_loc
| Type_ctx,([],_) -> failwith "Bug: Should not happen"
| Term_ctx,_ -> () 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 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
let t,ws =
match bounded_term_builder with
| Type_or_term (_,t_builder,_) -> t_builder type_env sg warnings in
Abstract_syntax.App
(Const (binder,loc),
(fst (List.fold_left
......@@ -80,16 +114,15 @@
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
}
Type_or_term (type_builder,term_builder,n_loc) }
bound_term_ending(phantom) :
| var = IDENT d = DOT t=type_or_term(phantom) {[var],
let type_builder _ _ =
emit_parse_error
(Error.Syntax_error "An arrow ('->' or '=>') or a right parenthesis ')' are expected.") d in
match t Term_ctx false with
| Type_or_term (_,term_builder,loc) -> Type_or_term (type_builder,term_builder,loc),loc
}
| var = IDENT vars_and_term = bound_term_ending(phantom) {let vars,t = vars_and_term in var::vars,t}
......@@ -71,7 +71,7 @@ term_alone: IDENT SEMICOLON
## IDENT
##
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.
A typing judgement in the form of ": <type>;", or a type definition with a colon ':' and the 'type' keyword in the form of ": type;" are expected in a term or a type definition.
term_alone: TYPE
##
......
......@@ -44,33 +44,30 @@
| 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
stype
abs
(add_cst_interpretations term abs acc cst)
match are_types,are_terms with
| false,false -> failwith "Bug: Should not happen"
| true,true ->
(match t Type_ctx false with
| Type_or_term (type_builder, term_builder,_) ->
let term,_ = term_builder Typing_env.empty obj [] in
let stype,_ = type_builder obj [] in
List.fold_left
(fun acc cst ->
add_type_interpretation
stype
abs
(add_cst_interpretations term abs acc cst)
cst)
lex
cst)
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
| false,true ->
(match t Term_ctx false with
| Type_or_term (_, term_builder,_) ->
let term,_ = term_builder Typing_env.empty obj [] in
List.fold_left (fun acc cst -> add_cst_interpretations term abs acc cst) lex cst)
| true,false ->
(match t Type_ctx false with
| Type_or_term (type_builder, _,_) ->
let stype,_ = type_builder obj [] in
List.fold_left (add_type_interpretation stype abs) lex cst)
}
......@@ -19,7 +19,10 @@
| {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'
type context =
| Type_ctx
| Term_ctx
%}
......@@ -68,6 +71,7 @@ sig_entry_eoi :
type_definition :
| id = IDENT EQUAL type_or_cst = type_or_term(COLON) COLON TYPE
{
let type_or_cst = type_or_cst Type_ctx in
fun sg _ ->
let id_name,id_loc = id in
let type_expr,_ = get_type (type_or_cst false) sg [] in
......@@ -81,6 +85,7 @@ sig_entry_eoi :
term_declaration :
| dec = term_dec_start COLON type_exp = type_or_term (SEMICOLON)
{
let type_exp = type_exp Type_ctx in
fun s e ->
let dec',s' = dec s in
List.fold_left
......@@ -112,7 +117,9 @@ term_declaration :
term_definition :
| id = IDENT EQUAL t = type_or_term(COLON) COLON ty = type_or_term(SEMICOLON)
{
{
let t = t Term_ctx in
let ty = ty Type_ctx in
fun s _ ->
let id',l = id in
try
......@@ -126,6 +133,8 @@ term_declaration :
| def = term_def_start EQUAL t = type_or_term(COLON) COLON ty = type_or_term(SEMICOLON)
{
let t = t Term_ctx in
let ty = ty Type_ctx in
fun s _ ->
let (id,l),k,s' = def s in
try
......
This diff is collapsed.
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