Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 67d9d8f2 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Intermediate state...

parent cd876851
#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
......
This diff is collapsed.
......@@ -11,7 +11,7 @@
(menhir
(merge_into data_parser)
(flags (--explain --table --strict))
(modules file_parser sig_parser lex_parser type_parser term_parser))
(modules file_parser sig_parser lex_parser term_type_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_parser.mly type_parser.mly)
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_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_parser.mly type_parser.mly))
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_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_parser.mly type_parser.mly))
(deps (:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_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_parser.mly type_parser.mly)
(:parsers file_parser.mly lex_parser.mly sig_parser.mly term_type_parser.mly)
)
(action (run %{bin:menhir} --base data_parser --explain --table --compare-errors data_parser.messages.automatic --compare-errors data_parser.messages %{parsers}))
)
......
%{
type kind =
| Both
| Type
| Term
open Parser_types
let add_cst_interpretations term abs_sig lex (id,l) =
match Environment.Signature1.is_constant id abs 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
| false -> emit_parse_error (Error.Unknown_type id) l
%}
%token <Logic.Abstract_syntax.Abstract_syntax.location> COLON_EQUAL
......@@ -18,8 +26,32 @@
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
%public lex_entry :
| 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
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
List.fold_left
(fun acc cst ->
add_type_interpretation
stype
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
......@@ -72,32 +104,4 @@
cst
| false,false -> raise (Error.(Error (Parse_error ((Unknown_constant_nor_variable id),loc))))
}
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=not_atomic_term
{
fun lex e ->
let abs,obj = Environment.Lexicon.get_sig lex in
let term,loc,ws = t Typing_env.empty obj [] in
List.fold_left
(fun acc (id,l) ->
match Environment.Signature1.is_constant id abs,Environment.Signature1.is_type id abs with
| (true,_),false -> Environment.Lexicon.insert (Abstract_syntax.Constant (id,loc,term)) acc
| (false,_), _ -> emit_parse_error (Error.Unknown_constant id) l
| (true,_),true -> failwith (Printf.sprintf "Bug: should not happen. \"%s\" should not be both a type and a term" id))
lex
cst
}
| cst = separated_nonempty_list(COMMA,id_or_sym) COLON_EQUAL t=not_atomic_type_expression
{
fun lex e ->
let abs,obj = Environment.Lexicon.get_sig lex in
let term,loc = t obj in
List.fold_left
(fun acc (id,l) ->
match Environment.Signature1.is_constant id abs,Environment.Signature1.is_type id abs with
| (false,_),true -> Environment.Lexicon.insert (Abstract_syntax.Type (id,loc,term)) acc
| _,false -> emit_parse_error (Error.Unknown_type id) l
| (true,_),true -> failwith (Printf.sprintf "Bug: should not happen. \"%s\" should not be both a type and a term" id))
lex
cst
}
*)
type kind_parameter =
| Type
| Term
type type_or_term_value =
| Type_value of Logic.Abstract_syntax.Abstract_syntax.type_def
| Term_value of Logic.Abstract_syntax.Abstract_syntax.term
| Term_token of Term_sequence.token
type kind =
| Type_k
| Term_k
| Both
type kind_parameter =
| Type
| Term
type type_or_term_value =
| Type_value of Logic.Abstract_syntax.Abstract_syntax.type_def
| Term_value of Logic.Abstract_syntax.Abstract_syntax.term
| Term_token of Term_sequence.token
......@@ -64,48 +64,29 @@ sig_entry_eoi :
ids
}
type_or_term_definition_prefix :
| id = IDENT EQUAL type_or_cst = atomic_type_or_term COLON { id,type_or_cst }
type_definition :
| definition = type_or_term_definition_prefix TYPE
{
| id = IDENT EQUAL type_or_cst = type_or_term COLON TYPE
{
fun sg _ ->
let (id_name,id_loc),(type_expr,type_expr_loc) = definition in
if Environment.Signature1.is_type type_expr sg then
try
Environment.Signature1.add_entry (Abstract_syntax.(Type_def (id_name,id_loc,Type_atom(type_expr,type_expr_loc,[]),K []))) sg
with
| Environment.Signature1.Duplicate_type_definition ->
emit_parse_error (Error.Duplicated_type id_name) id_loc
else
emit_parse_error (Error.Unknown_type type_expr) type_expr_loc
}
| id = IDENT EQUAL type_expr = not_atomic_type_expression COLON TYPE
{
fun s _ ->
let id_name,id_loc = id in
let type_expr',_ = type_expr s in
try
Environment.Signature1.add_entry (Abstract_syntax.Type_def (id_name,id_loc,type_expr',Abstract_syntax.K [])) s
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_expression
let id_name,id_loc = id in
let type_expr,type_expr_loc,_ = get_type type_or_cst sg [] in
try
Environment.Signature1.add_entry (Abstract_syntax.Type_def (id_name,id_loc,type_expr,Abstract_syntax.K [])) s
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
{
fun s e ->
let dec',s' = dec s in
List.fold_left
(fun acc ((id,loc),kind) ->
try
let ty = fst (type_exp acc) in
let ty = get_type type_exp acc [] in
Environment.Signature1.add_entry (Abstract_syntax.Term_decl (id,kind,loc,ty)) acc
with
| Environment.Signature1.Duplicate_term_definition ->
......@@ -125,52 +106,32 @@ sig_entry_eoi :
| INFIX opt = infix_option sym = SYMBOL { fun sg ->
let sym,fix,sg' = build_infix opt sym sg in
[sym,fix],sg'
(* let sym_id,_ = sym in
let p,sg' = Environment.Signature1.new_precedence sym_id sg in
[sym,Abstract_syntax.Infix (Left,p)],sg *)
}
| BINDER id = IDENT { fun sg -> [id,Abstract_syntax.Binder],sg }
term_definition :
| definition = type_or_term_definition_prefix ty = type_expression
{
fun sg _ ->
let (id,l),(term,term_loc) = definition in
if fst (Environment.Signature1.is_constant term sg) then
try
let term = Abstract_syntax.Const (term,term_loc) in
let ty',_ = ty sg in
Environment.Signature1.add_entry (Abstract_syntax.Term_def (id,Abstract_syntax.Default,l,term,ty')) sg
with
| Environment.Signature1.Duplicate_term_definition ->
emit_parse_error (Error.Duplicated_term id) l
else
emit_parse_error (Error.Unknown_constant term) term_loc
}
| id = IDENT EQUAL t = not_atomic_term COLON ty = type_expression
| id = IDENT EQUAL t = type_or_term COLON ty = type_or_term
{
fun s _ ->
let id',l = id in
try
(* Attention, BUG : pas de gestion des warnings !!! *)
let term,_,_ = t Typing_env.empty s [] in
let ty',_ = ty s in
let term,_,_ = get_term t Typing_env.empty s [] in
let ty',_ = get_type ty 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 = term COLON ty = type_expression
{
| def = term_def_start EQUAL t = type_or_term COLON ty = type_or_term
{
fun s _ ->
let (id,l),k,s' = def s in
try
(* Attention, BUG : pas de gestion des warnings !!! *)
let term,_,_ = t Typing_env.empty s' [] in
let ty',_ = ty s' in
let term,_,_ = get_term t Typing_env.empty s' [] in
let ty',_ = get_type ty s' [] in
Environment.Signature1.add_entry (Abstract_syntax.Term_def (id,k,l,term,ty')) s'
with
| Environment.Signature1.Duplicate_term_definition ->
......@@ -185,23 +146,7 @@ sig_entry_eoi :
let sym_id,_ = sym in
let p,sg' = Environment.Signature1.new_precedence sym_id sg in
sym,Abstract_syntax.Infix (Abstract_syntax.Left,p),sg'}
| INFIX opt = infix_option sym = SYMBOL {fun sg -> 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'
*)
}
| INFIX opt = infix_option sym = SYMBOL {fun sg -> build_infix opt sym sg }
| BINDER id = IDENT {fun sg -> id,Abstract_syntax.Binder,sg}
......
......@@ -46,7 +46,7 @@
%public atomic_type_or_term:
| id = IDENT { id }
| LPAREN t = atomic_type_or_term RPAREN { t }
(*| LPAREN t = atomic_type_or_term RPAREN { t } *)
ident_sequence:
| id0 = IDENT ids = IDENT+ { id0,ids }
......
%{
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
let get_type t sg ws =
match t ~kind:Type Typing_Env.empty sg ws with
| Paser_types.Type_value (t,l,ws),_ -> t,l,ws
| _ -> failwith "Bug: Should not happen"
let get_term t ty_env sg ws =
match t ~kind:Term ty_env sg ws with
| Paser_types.term_value (t,l,ws),_ -> t,l,ws
| _ -> failwith "Bug: Should not happen"
let get_token t ty_env sg ws =
match t ~kind:Term ty_env sg ws with
| Paser_types.Term_token (t,l,ws),_ -> t,l,ws
| _ -> failwith "Bug: Should not happen"
type 'a result = 'a * Error.warning list
type build_type = Environment.Signature1.t -> Error.warning -> Abstract_syntax.type_def result
type build_term = Typing_env.t -> Environment.Signature1.t -> Error.warning -> Abstract_syntax.term result
type build_token = Typing_env.t -> Environment.Signature1.t -> Error.warning -> Term_sequence.token result
type ident = string * Abstract_syntax.location
type term0_result =
| All of (build_type * build_token * ident * Abstract_syntax.location)
| Type_or_token of (build_type * build_token * Abstract_syntax.location)
| Token of (build_token * Abstract_syntax.location)
type type_or_term_result =
| Type_or_term_or_ident (build_type * build_term * (ident * ident list) * Abstract_syntax.location)
| Term_or_ident (build_term * (ident * ident list) * Abstract_syntax.location)
| Type_or_term of (build_type * build_term * Abstract_syntax.location)
| Type of (build_type * Abstract_syntax.location)
| Term of (build_term * Abstract_syntax.location)
let token_to_term_builder token_builder =
fun type_env sg ws ->
match token_builder type_env sg ws with
| Term (t',l'),_,ws -> Term_value t',l', ws
| Op _,_,_ -> failwith "Bug: Should not happen" in
%}
%token <Logic.Abstract_syntax.Abstract_syntax.location> ARROW
%token <Logic.Abstract_syntax.Abstract_syntax.location> LIN_ARROW
(*%on_error_reduce type_expression *)
%token <Logic.Abstract_syntax.Abstract_syntax.location> LAMBDA
%token <Logic.Abstract_syntax.Abstract_syntax.location> LAMBDA0
%token <Logic.Abstract_syntax.Abstract_syntax.location> DOT
%start < AcgData.Environment.Environment.Signature1.t -> Logic.Lambda.Lambda.term * Logic.Lambda.Lambda.stype > term_alone
%start < AcgData.Environment.Environment.Signature1.t -> AcgData.Environment.Environment.Signature1.t -> Logic.Abstract_syntax.Abstract_syntax.term * Logic.Abstract_syntax.Abstract_syntax.type_def > heterogenous_term_and_type
%%
%public term_alone:
| t = type_or_term COLON ty = type_or_term EOI {
fun sg ->
let t,_,ws = get_term t Typin_env.empty sg [] in
let ty,_ = get_type ty sg [] in
Environment.Signature1.convert_term t ty sg
}
%public heterogenous_term_and_type:
| t = type_or_term COLON ty = type_or_term EOI
{
fun abs obj ->
let t,_,ws = get_term t Typing_env.empty obj [] in
let ty,_ = get_type ty abs [] in
t,ty
}
%public type_or_term :
| t = type_or_term0 {
match t with
| All (type_builder, token_builder, id, loc) ->
let term_builder = token_to_term_builder token_builder in
Type_or_term_or_ident (type_builder,term_builder,(id,[]),loc)
| Type_or_token (type_builder, token_builder,loc) ->
let term_builder = token_to_term_builder token_builder in
Type_or_term (type_builder,term_builder,loc)
| Token (token_builder,loc) ->
let term_builder = token_to_term_builder token_builder in
Term (term_builder,loc)
}
| t1 = type_or_term0 arrow = arrow t2 = type_or_term {
match t1,t2 with
| All (type_builder1,_,_,l1)
| Type_or_token (type_builder1,_,l1) ->
(match t2 with
| Type_or_term_or_ident (type_builder2,_,_,l2)
| Type_or_term (type_builder2,_,l2)
| Type (type_builder2,l2) ->
let new_loc = new_loc l1 l2 in
let type_builder sg ws =
let ty1',ws' = type_builder1 sg ws in
let ty2',ws'' = type_builder2 sg ws' in
let new_type =
match arrow with
| Abstract_syntax.Linear -> Abstract_syntax.Linear_arrow (ty1',ty2',new_loc)
| Abstract_syntax.Non_linear -> Abstract_syntax.Arrow (ty1',ty2',new_loc) in
new_type,ws'' in
Type (type_builder,new_loc)
| Term_or_ident (_,_,loc)
| Term (_,loc) ->
emit_parse_error (Error.Syntax_error "A type is expected.") loc)
| Token (_,loc) -> emit_parse_error (Error.Syntax_error "In front of an arrow, a type is expected.") loc
}
| t = type_or_term0 terms = type_or_term0+ {
match t with
| All (_,token_builder,id,loc) ->
let term_builders,id_lst,last_loc =
List.fold_left
(fun (builders,ids,_) =
function
| All (_,tok_b,i,l) -> (tok_b,l)::builders,(i,l)::ids,l
| Type_or_token (_, tok_b,l)
| Token (tok_b,l) -> (tok_b,l)::builders,ids,l)
([],[],loc)
terms in
let new_loc = new_loc loc last_loc in
let term_builder type_env sg warnings =
let term,ws = token_builder type_env sg warnings in
let terms,warnings=
List.fold_left
(fun (lst,ws) (builder,_) ->
let t,ws'= builder type_env sg ws in
t'::lst,ws')
([],ws)
terms_builders in
let result,_ = Term_sequence.parse_sequence (term::terms) sg in
result,warnings in
let binder_builder = id,List.rev id_lst in
Term_or_ident (term_builder, binder_builder,new_loc)
| Token (token_builder,loc) ->
let term_builders,last_loc =
List.fold_left
(fun (builders,_) =
function
| All (_,tok_b,_,l) -> (tok_b,l)::builders,l
| Type_or_token (_, tok_b,l)
| Token (tok_b,l) -> (tok_b,l)::builders,l)
([],loc)
terms in
let new_loc = new_loc loc last_loc in
let term_builder type_env sg warnings =
let term,ws = token_builder type_env sg warnings in
let terms,warnings=
List.fold_left
(fun (lst,ws) (builder,_) ->
let t,ws'= builder type_env sg ws in
t'::lst,ws')
([],ws)
terms_builders in
let result,_ = Term_sequence.parse_sequence (term::terms) sg in
result,warnings in
Term (term_builder, new_loc)
}
| t = bound_term { t }
type_or_term0:
| id = IDENT {
let id,loc = id in
let type_builder sg warnings =
match Environment.Signature1.is_type id sg with
| true -> Abstract_syntax.Type_atom (id,loc,[]),warnings
| false -> emit_parse_error (Error.Unknown_type id) loc in
let token_builder type_env sg warnings =
let t,ws =
match Environment.Signature1.is_constant id sg,Typing_env.mem id type_env with
| (true,_),false -> Abstract_syntax.Const (id,loc),warnings
| (false,_),true -> Abstract_syntax.Var (id,loc),warnings
| (true,_),true -> Abstract_syntax.Var (id,loc),(Error.Variable_or_constant (id,loc))::warnings
| (false,_),false -> emit_parse_error (Error.Unknown_constant_nor_variable id) loc in
Term_sequence.Term (t,loc),ws in
let binder_builder = id,loc in
All (typebuilder,token_builder,binder_builder,loc)
}
| LPAREN t = type_or_term RPAREN {
match t with
| Both (type_builder,term_builder) ->
let token_builder type_env sg ws =
let t,l,ws' = term_builder type_env sg ws in
Term_sequence.Term (t,l),ws' in
Type_or_token (type_builder,token_builder,l)
| Type _ -> t
| Term term_builder ->
let token_builder type_env sg ws =
let t,l,ws' = term_builder type_env sg ws in
Term_sequence.Term (t,l),ws' in
Token (token_builder,l)}
| id = SYMBOL {
let name,loc = id in
let token_builder type_env sg warnings =
match Environment.Signature1.is_constant name sg with
| true,Some fix -> Op (Abstract_syntax.Const (name,loc),fix,loc),warnings
| true,None -> failwith "Bug: Should no happen"
| false,_ -> emit_parse_error (Error.Unknown_constant name) loc in
Token (token_builder,loc)
}
%inline arrow :
| ARROW { Abstract_syntax.Non_linear }
| LIN_ARROW { Abstract_syntax.Linear }
%inline bound_term :
| binder = LAMBDA vars_and_term = bound_term_ending
{
let vars,(term_builder,t_loc) = vars_and_term 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
let n_loc = new_loc binder loc 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 in
Term (term_builder,n_loc)
}
| binder = LAMBDA0 vars_and_term = bound_term_ending
{
let vars,(term_builder,t_loc) = vars_and_term 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
let n_loc = new_loc binder loc 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 (