[pre linearization] done, not tested

This commit is contained in:
Arnaud DABY-SEESARAM 2022-12-16 08:52:48 +01:00
parent 9987922e0f
commit d7f0f148e9

View File

@ -157,46 +157,65 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option
let pass_linearization verbose debug main_fn = let pass_linearization verbose debug main_fn =
let node_lin (node: t_node): t_node option = let node_lin (node: t_node): t_node option =
let pre_aux_expression b vars expr: t_eqlist * t_varlist * t_expression = let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
match expr with match expr with
| EVar _ -> [], vars, expr | EVar _ -> [], vars, expr
| EMonOp of full_ty * monop * t_expression -> (** TODO! *) | EMonOp (t, op, e) ->
begin
match op with
| MOp_pre ->
let eqs, vars, e = pre_aux_expression vars e in
let nvar: string = fresh_var_name vars 6 in
let nvar = match t with
| [TInt] -> IVar nvar
| [TBool] -> BVar nvar
| [TReal] -> RVar nvar
| _ -> failwith "Should not happened." in
let neq_patt: t_varlist = (t, [nvar]) in
let neq_expr: t_expression = EMonOp (t, MOp_pre, e) in
let vars = varlist_concat (t, [nvar]) vars in
(neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar)
| _ ->
let eqs, vars, e = pre_aux_expression vars e in
eqs, vars, EMonOp (t, op, e)
end
| EBinOp (t, op, e, e') -> | EBinOp (t, op, e, e') ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
let eqs', vars, e' = pre_aux_expression false vars e' in let eqs', vars, e' = pre_aux_expression vars e' in
eqs @ eqs', vars, EBinOp (t, op, e, e') eqs @ eqs', vars, EBinOp (t, op, e, e')
| ETriOp (t, op, e, e', e'') -> | ETriOp (t, op, e, e', e'') ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
let eqs', vars, e' = pre_aux_expression false vars e' in let eqs', vars, e' = pre_aux_expression vars e' in
let eqs'', vars, e'' = pre_aux_expression false vars e'' in let eqs'', vars, e'' = pre_aux_expression vars e'' in
eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
| EComp (t, op, e, e') -> | EComp (t, op, e, e') ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
let eqs', vars, e' = pre_aux_expression false vars e' in let eqs', vars, e' = pre_aux_expression vars e' in
eqs @ eqs', vars, EComp (t, op, e, e') eqs @ eqs', vars, EComp (t, op, e, e')
| EWhen (t, e, e') -> | EWhen (t, e, e') ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
let eqs', vars, e' = pre_aux_expression false vars e' in let eqs', vars, e' = pre_aux_expression vars e' in
eqs @ eqs', vars, EWhen (t, e, e') eqs @ eqs', vars, EWhen (t, e, e')
| EReset (t, e, e') -> | EReset (t, e, e') ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
let eqs', vars, e' = pre_aux_expression false vars e' in let eqs', vars, e' = pre_aux_expression vars e' in
eqs @ eqs', vars, EReset (t, e, e') eqs @ eqs', vars, EReset (t, e, e')
| EConst _ -> [], vars, expr | EConst _ -> [], vars, expr
(** TODO!*)
| ETuple (t, l) -> | ETuple (t, l) ->
let eqs, vars, l = List.fold_right let eqs, vars, l = List.fold_right
(fun e (eqs, vars, l) -> (fun e (eqs, vars, l) ->
let eqs', vars, e = pre_aux_expression false vars e in let eqs', vars, e = pre_aux_expression vars e in
eqs' @ eqs, vars, (e :: l)) eqs' @ eqs, vars, (e :: l))
l ([], vars, []) in l ([], vars, []) in
eqs, vars, ETuple (t, l) eqs, vars, ETuple (t, l)
| EApp (t, n, e) -> | EApp (t, n, e) ->
let eqs, vars, e = pre_aux_expression false vars e in let eqs, vars, e = pre_aux_expression vars e in
eqs, vars, EApp (t, n, e) eqs, vars, EApp (t, n, e)
in in
let rec pre_aux_equation (vars: t_varlist) (eq: t_equation) = let rec pre_aux_equation (vars: t_varlist) (eq: t_equation) =
[], ([], []) let (patt, expr) = eq in
let eqs, vars, expr = pre_aux_expression vars expr in
(patt, expr)::eqs, vars
in in
let rec tpl ((pat, exp): t_equation) = let rec tpl ((pat, exp): t_equation) =
match exp with match exp with