Benjamin_Loison/Synchronous_reactive_systems
1
0
Fork 0
Code Issues 7 Pull Requests Packages Projects Releases Wiki Activity

[parser] (wip) explicitely typing the language

Browse Source
This commit is contained in:
Arnaud DABY-SEESARAM 2022-12-09 16:33:07 +01:00
parent f84279c5d8
commit 428b0a75e2
4 changed files with 92 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

105
src/ast.ml
View File

@ -35,18 +35,23 @@ type t_var =
| IVar of ident | IVar of ident
| RVar of ident | RVar of ident
type t_expression = type full_ty =
| EVar of t_var | FTArr of full_ty * full_ty
| EMonOp of monop * t_expression | FTList of full_ty list
| EBinOp of binop * t_expression * t_expression | FTBase of base_ty
| ETriOp of triop * t_expression * t_expression * t_expression
| EComp of compop * t_expression * t_expression
| EWhen of t_expression * t_expression
| EConst of const
| ETuple of t_expression list
| EApp of t_node * t_expression
and t_varlist = t_var list type t_expression =
| EVar of full_ty * t_var
| EMonOp of full_ty * monop * t_expression
| EBinOp of full_ty * binop * t_expression * t_expression
| ETriOp of full_ty * triop * t_expression * t_expression * t_expression
| EComp of full_ty * compop * t_expression * t_expression
| EWhen of full_ty * t_expression * t_expression
| EConst of full_ty * const
| ETuple of full_ty * (t_expression list)
| EApp of full_ty * t_node * t_expression
and t_varlist = full_ty * (t_var list)
and t_equation = t_varlist * t_expression and t_equation = t_varlist * t_expression
@ -59,84 +64,8 @@ and t_node =
n_outputs: t_varlist; n_outputs: t_varlist;
n_local_vars: t_varlist; n_local_vars: t_varlist;
n_equations: t_eqlist; n_equations: t_eqlist;
n_type : full_ty;
} }
type t_nodelist = t_node list type t_nodelist = t_node list
type full_ty =
| FTArr of full_ty * full_ty
| FTList of full_ty list
| FTBase of base_ty
let varlist_get_type (vl: t_varlist): full_ty =
FTList
(List.map (function
| BVar _ -> FTBase TBool
| IVar _ -> FTBase TInt
| RVar _ -> FTBase TReal) vl)
let rec expression_get_type : t_expression -> full_ty = function
| EVar (BVar s) -> FTBase TBool
| EVar (IVar s) -> FTBase TInt
| EVar (RVar s) -> FTBase TReal
| EMonOp (_, e) -> expression_get_type e
| EBinOp (_, e1, e2) | EComp (_, e1, e2) ->
begin
let t1 = expression_get_type e1 in
let t2 = expression_get_type e2 in
if t1 = t2
then t1
else raise (MyTypeError "A binary operator only works on pairs of \
expressions of the same type.")
end
| ETriOp (_, e1, e2, e3) ->
begin
let t1 = expression_get_type e1 in
let t2 = expression_get_type e2 in
let t3 = expression_get_type e3 in
if t1 = FTBase TBool && t2 = t3
then t2
else raise (MyTypeError "A tertiary operator only works when its \
first argument is a boolean expressions, and its other expressions \
have the same type.")
end
| EWhen (e1, e2) ->
begin
let t1 = expression_get_type e1 in
let t2 = expression_get_type e2 in
if t2 = FTBase TBool
then t1
else raise (MyTypeError "The [when] keywork can only be used if its \
second argument is a boolean expression")
end
| EConst (CInt _) -> FTBase TInt
| EConst (CReal _) -> FTBase TReal
| EConst (CBool _) -> FTBase TBool
| ETuple l ->
begin
FTList (
List.fold_left (fun acc (expr: t_expression) ->
let t = expression_get_type expr in
match t with
| FTList lt -> lt @ acc
| _ -> t :: acc) [] l)
end
| EApp (n, e) ->
begin
let tn = node_get_type n in
let te = expression_get_type e in
match tn with
| FTArr (targs, tout) ->
if te = targs
then tout
else raise (MyTypeError "When applying another node [n], the \
the type of your arguments should match the type of the inputs \
of [n].")
| _ -> raise (MyTypeError "You cannot apply something that is not a \
node, it does not make sense.")
end
and node_get_type n =
FTArr (varlist_get_type n.n_inputs, varlist_get_type n.n_outputs)

54
src/parser.mly
View File

@ -14,13 +14,32 @@
("The node "^n^" does not exist.")) ("The node "^n^" does not exist."))
| Some node -> node | Some node -> node
let fetch_var (n: Ast.ident) = let fetch_var (n: Ast.ident) : Ast.t_var =
match Hashtbl.find_opt defined_vars n with match Hashtbl.find_opt defined_vars n with
| None -> | None ->
raise (MyParsingError raise (MyParsingError
("The var "^n^" does not exist.")) ("The var "^n^" does not exist."))
| Some var -> var | Some var -> var
let concat_varlist (t1, e1) (t2, e2) =
Ast.(
match t1, t2 with
| FTList lt1, FTList lt2 -> (FTList (lt1 @ lt2), e1@e2)
| _ ->
raise (MyParsingError "This exception should not have been raised."))
let make_ident (v : Ast.t_var) : Ast.t_varlist =
match v with
| IVar _ -> Ast.(FTList [FTBase TInt ], [v])
| BVar _ -> Ast.(FTList [FTBase TBool], [v])
| RVar _ -> Ast.(FTList [FTBase TReal], [v])
let add_ident (v : Ast.t_var) (l: Ast.t_varlist) : Ast.t_varlist =
match v, l with
| IVar _, (FTList tl, l) -> Ast.(FTList (FTBase TInt :: tl), v :: l)
| BVar _, (FTList tl, l) -> Ast.(FTList (FTBase TBool :: tl), v :: l)
| RVar _, (FTList tl, l) -> Ast.(FTList (FTBase TReal :: tl), v :: l)
| _ -> raise (MyParsingError "This exception should not have been raised.")
%} %}
%token EOF %token EOF
@ -88,34 +107,37 @@ node_content:
local_params local_params
LET equations TEL LET equations TEL
{ let node_name = $1 in { let node_name = $1 in
let (t_in, e_in) = $3 in
let (t_out, e_out) = $7 in
let n: Ast.t_node = let n: Ast.t_node =
{ n_name = node_name; { n_name = node_name;
n_inputs = $3; n_inputs = (t_in, e_in);
n_outputs = $7; n_outputs = (t_out, e_out);
n_local_vars = $10; n_local_vars = $10;
n_equations = $12; } in n_equations = $12;
n_type = FTArr (t_in, t_out); } in
Hashtbl.add defined_nodes node_name n; n Hashtbl.add defined_nodes node_name n; n
} ; } ;
in_params: in_params:
| /* empty */ { [] } | /* empty */ { (FTList [], []) }
| param_list { $1 } | param_list { $1 }
; ;
out_params: param_list { $1 } ; out_params: param_list { $1 } ;
local_params: local_params:
| /* empty */ { [] } | /* empty */ { (FTList [], []) }
| VAR param_list_semicol { $2 } | VAR param_list_semicol { $2 }
; ;
param_list_semicol: param_list_semicol:
| param SEMICOL { $1 } | param SEMICOL { $1 }
| param SEMICOL param_list_semicol { $1 @ $3 } | param SEMICOL param_list_semicol { concat_varlist $1 $3 }
param_list: param_list:
| param { $1 } | param { $1 }
| param SEMICOL param_list { $1 @ $3 } | param SEMICOL param_list { concat_varlist $1 $3 }
; ;
param: param:
@ -123,13 +145,16 @@ param:
{ let typ = $3 in { let typ = $3 in
let idents = $1 in let idents = $1 in
Ast.( Ast.(
(FTList
(List.map
(fun t -> FTBase t) (Utils.list_repeat (List.length idents) typ)),
match typ with match typ with
| TBool -> | TBool ->
List.map (fun s -> Hashtbl.add defined_vars s (BVar s); BVar s) idents List.map (fun s -> Hashtbl.add defined_vars s (BVar s); BVar s) idents
| TReal -> | TReal ->
List.map (fun s -> Hashtbl.add defined_vars s (RVar s); RVar s) idents List.map (fun s -> Hashtbl.add defined_vars s (RVar s); RVar s) idents
| TInt -> | TInt ->
List.map (fun s -> Hashtbl.add defined_vars s (IVar s); IVar s) idents) } List.map (fun s -> Hashtbl.add defined_vars s (IVar s); IVar s) idents)) }
; ;
ident_comma_list: ident_comma_list:
@ -148,12 +173,17 @@ equation:
; ;
pattern: pattern:
| IDENT { [fetch_var $1] } | IDENT
{ let v = fetch_var $1 in
match v with
| IVar _ -> Ast.(FTList [FTBase TInt ], [v])
| BVar _ -> Ast.(FTList [FTBase TBool], [v])
| RVar _ -> Ast.(FTList [FTBase TReal], [v]) }
| LPAREN ident_comma_list_patt RPAREN { $2 }; | LPAREN ident_comma_list_patt RPAREN { $2 };
ident_comma_list_patt: ident_comma_list_patt:
| IDENT { [fetch_var $1] } | IDENT { make_ident (fetch_var $1) }
| IDENT COMMA ident_comma_list_patt { (fetch_var $1) :: $3 } | IDENT COMMA ident_comma_list_patt { add_ident (fetch_var $1) $3 }
expr: expr:
/* Note: EQUAL does not follow the nomenclature CMP_, ... */ /* Note: EQUAL does not follow the nomenclature CMP_, ... */

66
src/pp.ml
View File

@ -8,45 +8,49 @@ let pp_loc fmt (start, stop) =
stop.pos_lnum stop.pos_cnum) stop.pos_lnum stop.pos_cnum)
let rec pp_varlist fmt : t_varlist -> unit = function let rec pp_varlist fmt : t_varlist -> unit = function
| [] -> () | (FTList [], []) -> ()
| IVar h :: [] -> Format.fprintf fmt "%s" h | (FTList (FTBase TInt :: _), IVar h :: []) -> Format.fprintf fmt "%s" h
| RVar h :: [] -> Format.fprintf fmt "%s" h | (FTList (FTBase TReal :: _), RVar h :: []) -> Format.fprintf fmt "%s" h
| BVar h :: [] -> Format.fprintf fmt "%s" h | (FTList (FTBase TBool :: _), BVar h :: []) -> Format.fprintf fmt "%s" h
| (IVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) | (FTList (FTBase TInt :: tl), (IVar h) :: h' :: l) ->
| (BVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) Format.fprintf fmt "%s, %a" h pp_varlist (FTList tl, (h' :: l))
| (RVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) | (FTList (FTBase TBool :: tl), (BVar h) :: h' :: l) ->
Format.fprintf fmt "%s, %a" h pp_varlist (FTList tl, (h' :: l))
| (FTList (FTBase TReal :: tl), (RVar h) :: h' :: l) ->
Format.fprintf fmt "%s, %a" h pp_varlist (FTList tl, (h' :: l))
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
let pp_expression = let pp_expression =
let upd_prefix s = s ^ " | " in let upd_prefix s = s ^ " | " in
let rec pp_expression_aux prefix fmt expression = let rec pp_expression_aux prefix fmt expression =
let rec pp_expression_list prefix fmt exprs = let rec pp_expression_list prefix fmt exprs =
match exprs with match exprs with
| ETuple([]) -> () | ETuple(FTList [], []) -> ()
| ETuple (expr :: exprs) -> | ETuple (FTList (_ :: tt), expr :: exprs) ->
Format.fprintf fmt "%a%a" Format.fprintf fmt "%a%a"
(pp_expression_aux (prefix^" |> ")) expr (pp_expression_aux (prefix^" |> ")) expr
(pp_expression_list prefix) (ETuple exprs) (pp_expression_list prefix) (ETuple (FTList tt, exprs))
| _ -> raise (MyTypeError "This exception should not have been raised.") | _ -> raise (MyTypeError "This exception should not have been raised.")
in in
match expression with match expression with
| EWhen (e1, e2) -> | EWhen (_, e1, e2) ->
begin begin
Format.fprintf fmt "\t\t\t%sWHEN\n%a\t\t\tWHEN\n%a" Format.fprintf fmt "\t\t\t%sWHEN\n%a\t\t\tWHEN\n%a"
prefix prefix
(pp_expression_aux (upd_prefix prefix)) e1 (pp_expression_aux (upd_prefix prefix)) e1
(pp_expression_aux (upd_prefix prefix)) e2 (pp_expression_aux (upd_prefix prefix)) e2
end end
| EConst c -> | EConst (_, c) ->
begin match c with begin match c with
| CBool true -> Format.fprintf fmt "\t\t\t%s<true : bool>\n" prefix | CBool true -> Format.fprintf fmt "\t\t\t%s<true : bool>\n" prefix
| CBool false -> Format.fprintf fmt "\t\t\t%s<false : bool>\n" prefix | CBool false -> Format.fprintf fmt "\t\t\t%s<false : bool>\n" prefix
| CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i | CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r
end end
| EVar (IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v | EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v
| EVar (BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v | EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v
| EVar (RVar v) -> Format.fprintf fmt "\t\t\t%s<real var %s>\n" prefix v | EVar (_, RVar v) -> Format.fprintf fmt "\t\t\t%s<real var %s>\n" prefix v
| EMonOp (mop, arg) -> | EMonOp (_, mop, arg) ->
begin match mop with begin match mop with
| MOp_not -> | MOp_not ->
Format.fprintf fmt "\t\t\t%s ¬ \n%a" prefix Format.fprintf fmt "\t\t\t%s ¬ \n%a" prefix
@ -58,7 +62,7 @@ let pp_expression =
Format.fprintf fmt "\t\t\t%spre\n%a" prefix Format.fprintf fmt "\t\t\t%spre\n%a" prefix
(pp_expression_aux (upd_prefix prefix)) arg (pp_expression_aux (upd_prefix prefix)) arg
end end
| EBinOp (bop, arg, arg') -> | EBinOp (_, bop, arg, arg') ->
begin begin
let s = match bop with let s = match bop with
| BOp_add -> " + " | BOp_sub -> " - " | BOp_add -> " + " | BOp_sub -> " - "
@ -68,7 +72,7 @@ let pp_expression =
(pp_expression_aux (upd_prefix prefix)) arg (pp_expression_aux (upd_prefix prefix)) arg
(pp_expression_aux (upd_prefix prefix)) arg' (pp_expression_aux (upd_prefix prefix)) arg'
end end
| EComp (cop, arg, arg') -> | EComp (_, cop, arg, arg') ->
begin begin
let s = match cop with let s = match cop with
| COp_eq -> "== " | COp_eq -> "== "
@ -79,7 +83,7 @@ let pp_expression =
(pp_expression_aux (upd_prefix prefix)) arg (pp_expression_aux (upd_prefix prefix)) arg
(pp_expression_aux (upd_prefix prefix)) arg' (pp_expression_aux (upd_prefix prefix)) arg'
end end
| ETriOp (top, arg, arg', arg'') -> | ETriOp (_, top, arg, arg', arg'') ->
begin match top with begin match top with
| TOp_if -> | TOp_if ->
Format.fprintf fmt "\t\t\t%sIF\n%a\t\t\tTHEN\n%a\t\t\tELSE\n%a" Format.fprintf fmt "\t\t\t%sIF\n%a\t\t\tTHEN\n%a\t\t\tELSE\n%a"
@ -94,13 +98,13 @@ let pp_expression =
(pp_expression_aux (upd_prefix prefix)) arg' (pp_expression_aux (upd_prefix prefix)) arg'
(pp_expression_aux (upd_prefix prefix)) arg'' (pp_expression_aux (upd_prefix prefix)) arg''
end end
| EApp (f, args) -> | EApp (_, f, args) ->
Format.fprintf fmt "\t\t\t%sApp %s\n%a" Format.fprintf fmt "\t\t\t%sApp %s\n%a"
prefix f.n_name prefix f.n_name
(pp_expression_list prefix) args (pp_expression_list prefix) args
| ETuple args -> | ETuple _ ->
Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix
(pp_expression_list prefix) (ETuple args); (pp_expression_list prefix) expression;
in in
pp_expression_aux "" pp_expression_aux ""
@ -112,25 +116,13 @@ let rec pp_equations fmt: t_eqlist -> unit = function
pp_expression expr pp_expression expr
pp_equations eqs pp_equations eqs
let rec pp_node_vars fmt = function
| [] -> ()
| BVar n :: vars ->
Format.fprintf fmt "\t\tVariable <name: %10s,\ttype: bool>\n%a"
n pp_node_vars vars
| IVar n :: vars ->
Format.fprintf fmt "\t\tVariable <name: %10s,\ttype: int>\n%a"
n pp_node_vars vars
| RVar n :: vars ->
Format.fprintf fmt "\t\tVariable <name: %10s,\ttype: real>\n%a"
n pp_node_vars vars
let pp_node fmt node = let pp_node fmt node =
Format.fprintf fmt "\t∗ Nom du nœud : %s\n\t Inputs:\n%a\n\t Outputs:\n%a\n\t\ Format.fprintf fmt "\t∗ Nom du nœud : %s\n\t Inputs:\n%a\n\t Outputs:\n%a\n\t\
\ \ Local variables:\n%a\n\t Equations:\n%a\n" \ \ Local variables:\n%a\n\t Equations:\n%a\n"
node.n_name node.n_name
pp_node_vars node.n_inputs pp_varlist node.n_inputs
pp_node_vars node.n_outputs pp_varlist node.n_outputs
pp_node_vars node.n_local_vars pp_varlist node.n_local_vars
pp_equations node.n_equations pp_equations node.n_equations
let rec pp_nodes fmt nodes = let rec pp_nodes fmt nodes =

2
src/utils.ml Normal file
View File

@ -0,0 +1,2 @@
let rec list_repeat n elt =
if n = 0 then [] else elt :: (list_repeat (n-1) elt)