From 428b0a75e2b11c7269bb5391049ff582cdf4e236 Mon Sep 17 00:00:00 2001 From: Arnaud DABY-SEESARAM Date: Fri, 9 Dec 2022 16:33:07 +0100 Subject: [PATCH] [parser] (wip) explicitely typing the language --- src/ast.ml | 105 ++++++++----------------------------------------- src/parser.mly | 58 ++++++++++++++++++++------- src/pp.ml | 66 ++++++++++++++----------------- src/utils.ml | 2 + 4 files changed, 92 insertions(+), 139 deletions(-) create mode 100644 src/utils.ml diff --git a/src/ast.ml b/src/ast.ml index 5a31f22..2179b24 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -35,18 +35,23 @@ type t_var = | IVar of ident | RVar of ident -type t_expression = - | EVar of t_var - | EMonOp of monop * t_expression - | EBinOp of binop * t_expression * t_expression - | 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 +type full_ty = + | FTArr of full_ty * full_ty + | FTList of full_ty list + | FTBase of base_ty -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 @@ -59,84 +64,8 @@ and t_node = n_outputs: t_varlist; n_local_vars: t_varlist; n_equations: t_eqlist; + n_type : full_ty; } 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) - diff --git a/src/parser.mly b/src/parser.mly index 74dc112..bac8f42 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -14,13 +14,32 @@ ("The node "^n^" does not exist.")) | 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 | None -> raise (MyParsingError ("The var "^n^" does not exist.")) | 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 @@ -88,34 +107,37 @@ node_content: local_params LET equations TEL { let node_name = $1 in + let (t_in, e_in) = $3 in + let (t_out, e_out) = $7 in let n: Ast.t_node = { n_name = node_name; - n_inputs = $3; - n_outputs = $7; + n_inputs = (t_in, e_in); + n_outputs = (t_out, e_out); 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 } ; in_params: - | /* empty */ { [] } + | /* empty */ { (FTList [], []) } | param_list { $1 } ; out_params: param_list { $1 } ; local_params: - | /* empty */ { [] } + | /* empty */ { (FTList [], []) } | VAR param_list_semicol { $2 } ; param_list_semicol: | param SEMICOL { $1 } - | param SEMICOL param_list_semicol { $1 @ $3 } + | param SEMICOL param_list_semicol { concat_varlist $1 $3 } param_list: | param { $1 } - | param SEMICOL param_list { $1 @ $3 } + | param SEMICOL param_list { concat_varlist $1 $3 } ; param: @@ -123,13 +145,16 @@ param: { let typ = $3 in let idents = $1 in Ast.( + (FTList + (List.map + (fun t -> FTBase t) (Utils.list_repeat (List.length idents) typ)), match typ with | 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 -> - 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 -> - 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: @@ -148,12 +173,17 @@ equation: ; 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 }; ident_comma_list_patt: - | IDENT { [fetch_var $1] } - | IDENT COMMA ident_comma_list_patt { (fetch_var $1) :: $3 } + | IDENT { make_ident (fetch_var $1) } + | IDENT COMMA ident_comma_list_patt { add_ident (fetch_var $1) $3 } expr: /* Note: EQUAL does not follow the nomenclature CMP_, ... */ diff --git a/src/pp.ml b/src/pp.ml index 4c6ef37..fa537f1 100644 --- a/src/pp.ml +++ b/src/pp.ml @@ -8,45 +8,49 @@ let pp_loc fmt (start, stop) = stop.pos_lnum stop.pos_cnum) let rec pp_varlist fmt : t_varlist -> unit = function - | [] -> () - | IVar h :: [] -> Format.fprintf fmt "%s" h - | RVar h :: [] -> Format.fprintf fmt "%s" h - | BVar h :: [] -> Format.fprintf fmt "%s" h - | (IVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) - | (BVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) - | (RVar h) :: h' :: l -> Format.fprintf fmt "%s, %a" h pp_varlist (h' :: l) + | (FTList [], []) -> () + | (FTList (FTBase TInt :: _), IVar h :: []) -> Format.fprintf fmt "%s" h + | (FTList (FTBase TReal :: _), RVar h :: []) -> Format.fprintf fmt "%s" h + | (FTList (FTBase TBool :: _), BVar h :: []) -> Format.fprintf fmt "%s" h + | (FTList (FTBase TInt :: tl), (IVar h) :: h' :: l) -> + Format.fprintf fmt "%s, %a" h pp_varlist (FTList tl, (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 upd_prefix s = s ^ " | " in let rec pp_expression_aux prefix fmt expression = let rec pp_expression_list prefix fmt exprs = match exprs with - | ETuple([]) -> () - | ETuple (expr :: exprs) -> + | ETuple(FTList [], []) -> () + | ETuple (FTList (_ :: tt), expr :: exprs) -> Format.fprintf fmt "%a%a" (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.") in match expression with - | EWhen (e1, e2) -> + | EWhen (_, e1, e2) -> begin Format.fprintf fmt "\t\t\t%sWHEN\n%a\t\t\tWHEN\n%a" prefix (pp_expression_aux (upd_prefix prefix)) e1 (pp_expression_aux (upd_prefix prefix)) e2 end - | EConst c -> + | EConst (_, c) -> begin match c with | CBool true -> Format.fprintf fmt "\t\t\t%s\n" prefix | CBool false -> Format.fprintf fmt "\t\t\t%s\n" prefix | 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 end - | EVar (IVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v - | EVar (BVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v - | EVar (RVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v - | EMonOp (mop, arg) -> + | EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v + | EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v + | EVar (_, RVar v) -> Format.fprintf fmt "\t\t\t%s\n" prefix v + | EMonOp (_, mop, arg) -> begin match mop with | MOp_not -> 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 (pp_expression_aux (upd_prefix prefix)) arg end - | EBinOp (bop, arg, arg') -> + | EBinOp (_, bop, arg, arg') -> begin let s = match bop with | 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' end - | EComp (cop, arg, arg') -> + | EComp (_, cop, arg, arg') -> begin let s = match cop with | COp_eq -> "== " @@ -79,7 +83,7 @@ let pp_expression = (pp_expression_aux (upd_prefix prefix)) arg (pp_expression_aux (upd_prefix prefix)) arg' end - | ETriOp (top, arg, arg', arg'') -> + | ETriOp (_, top, arg, arg', arg'') -> begin match top with | TOp_if -> 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'' end - | EApp (f, args) -> + | EApp (_, f, args) -> Format.fprintf fmt "\t\t\t%sApp %s\n%a" prefix f.n_name (pp_expression_list prefix) args - | ETuple args -> + | ETuple _ -> Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix - (pp_expression_list prefix) (ETuple args); + (pp_expression_list prefix) expression; in pp_expression_aux "" @@ -112,25 +116,13 @@ let rec pp_equations fmt: t_eqlist -> unit = function pp_expression expr pp_equations eqs -let rec pp_node_vars fmt = function - | [] -> () - | BVar n :: vars -> - Format.fprintf fmt "\t\tVariable \n%a" - n pp_node_vars vars - | IVar n :: vars -> - Format.fprintf fmt "\t\tVariable \n%a" - n pp_node_vars vars - | RVar n :: vars -> - Format.fprintf fmt "\t\tVariable \n%a" - n pp_node_vars vars - 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\ \ \ Local variables:\n%a\n\t Equations:\n%a\n" node.n_name - pp_node_vars node.n_inputs - pp_node_vars node.n_outputs - pp_node_vars node.n_local_vars + pp_varlist node.n_inputs + pp_varlist node.n_outputs + pp_varlist node.n_local_vars pp_equations node.n_equations let rec pp_nodes fmt nodes = diff --git a/src/utils.ml b/src/utils.ml new file mode 100644 index 0000000..f032a51 --- /dev/null +++ b/src/utils.ml @@ -0,0 +1,2 @@ +let rec list_repeat n elt = + if n = 0 then [] else elt :: (list_repeat (n-1) elt)