Commit cf826654 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

Remove remaining commented Mult's

parent 7b1ad224
......@@ -498,7 +498,6 @@ struct
| PropUn of propop1 * formula
| PropBin of propop2 * formula * formula
| Rel of relop2 * expr * expr
(* | Mult of BRN.mult (* TODOx: À supprimer ? Conversion en amont *) *)
| FreshState of formula ;;
(** Conversion d'une formule de multiplexe en formule FOL générale *)
......@@ -513,7 +512,7 @@ struct
| MPropBin(op, f1, f2) -> PropBin(op, formula_of_multformula f1, formula_of_multformula f2)
| MRel(op, e1, e2) -> Rel(op, expr_of_multexpr e1, expr_of_multexpr e2)
| MAtom(v, i) -> formula_of_matom v i
| MMult(m) -> formula_of_multformula (BRNinfo.getformula m) ;; (* Mult m *)
| MMult(m) -> formula_of_multformula (BRNinfo.getformula m) ;;
(** Substitution d'une expression à une variable *)
let replace f v e =
......@@ -529,7 +528,6 @@ struct
| PropUn(op, f) -> PropUn(op, replace_formula f v' e')
| PropBin(op, f1, f2) -> PropBin(op, replace_formula f1 v' e', replace_formula f2 v' e')
| Rel(op, e1, e2) -> Rel(op, replace_expr e1 v' e', replace_expr e2 v' e')
(* | Mult(m) -> replace_formula (formula_of_multformula (BRNinfo.getformula m)) v' e' *)
| FreshState(f) -> FreshState(f) in
replace_formula f v e ;;
......@@ -561,7 +559,6 @@ struct
| PropUn(op, f) -> ((string_of_propop1 op) ^ (string_of_formula f))
| PropBin(op, f1, f2) -> ("(" ^ (string_of_formula f1) ^ " " ^ (string_of_propop2 op) ^ " " ^ (string_of_formula f2) ^ ")")
| Rel(op, e1, e2) -> ("(" ^ (string_of_expr e1) ^ (string_of_relop2 op) ^ (string_of_expr e2) ^ ")")
(* | Mult(m) -> BRN.string_of_mult m *)
| FreshState(f) -> ("∀ state σ, " ^ (string_of_formula f)) ;;
end ;;
......@@ -647,11 +644,11 @@ struct
match l with
| [] -> PropConst True (*raise (Invalid_argument "phi_eval: Empty l list for phi_eval")*)
| h :: [] -> if (mem h omega)
then formula_of_multformula (BRNinfo.getformula h) (* Mult h *)
else PropUn(Neg, formula_of_multformula (BRNinfo.getformula h)) (* Mult h *)
then formula_of_multformula (BRNinfo.getformula h)
else PropUn(Neg, formula_of_multformula (BRNinfo.getformula h))
| h :: t -> PropBin(And, (if (mem h omega)
then formula_of_multformula (BRNinfo.getformula h) (* Mult h *)
else PropUn(Neg, formula_of_multformula (BRNinfo.getformula h))), (* Mult h *)
then formula_of_multformula (BRNinfo.getformula h)
else PropUn(Neg, formula_of_multformula (BRNinfo.getformula h))),
phi_eval v t omega) in
phi_eval v (BRNinfo.getpredec v) omega ;;
let rec conj_phi_param v l comp =
......
Supports Markdown
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