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

remove old commented and debug code

parent 6767b472
......@@ -571,205 +571,111 @@ struct
super_replace f (ExprVar(v)) e ;;
*)
(** Simplification d'une formule selon certains paramètres *)
(*
(* TODO : À optimiser ! *)
(* Supprimer l'évaluation (la fusionner à et la simplification) pour ne pas répéter le parcours de l'arbre *)
type evaluated_prop =
| T | F | U ;;
type evaluated_expr =
| Evaluated of int
| Unknown ;;
let evaluated_of_bool = function
| true -> T
| false -> F ;;
*)
(*
(* Ancienne façon de faire : évaluations partout *)
let eval_propop0 op =
match op with
| True -> T
| False -> F ;;
let eval_propop1 op f =
(** Simplification d'une formule selon la valeur de certaines variables et certains paramètres *)
type assoc_option =
| Found of int
| Not_found ;;
(* Simplification d'une expression *)
let rec simpl_expr e lv lk =
let rec assoc_find eq k1 l =
match l with
| [] -> Not_found
| (k2, v) :: t -> match eq k1 k2 with
| true -> Found v
| false -> assoc_find eq k1 t in
(* xFIXME? : Revoir la notion d'égalité : la fonction (=) propre à OCaml est-elle suffisante ? *)
(* TODO : à déplacer dans BRN (ou BRNinfo ?) *)
let paramequals = (=) in
let evalfun_of_exprop2 = function
| Plus -> (+)
| Minus -> (-) in
match e with
| ExprBin(op, e1, e2) -> (match simpl_expr e1 lv lk, simpl_expr e2 lv lk with
| ExprConst(i1), ExprConst(i2) -> ExprConst(evalfun_of_exprop2 op i1 i2)
| es1, es2 -> ExprBin(op, es1, es2))
| ExprVar(v) -> (match assoc_find BRN.varequals v lv with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprParam(v, l) -> (match assoc_find paramequals (v, l) lk with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprConst(i) -> ExprConst(i) ;;
let rec simpl_formula f lv lk =
let evalfun_of_relop2 = function
| LE -> (<=)
| LT -> (<)
| GE -> (>=)
| GT -> (>)
| Eq -> (=)
| NEq -> (!=) in
let simpl_exprop2 op e1 e2 lv lk =
match (simpl_expr e1 lv lk), (simpl_expr e2 lv lk) with
| ExprConst(i1), ExprConst(i2) -> (match (evalfun_of_relop2 op) i1 i2 with
| true -> PropConst(True)
| false -> PropConst(False))
| es1, es2 -> Rel(op, es1, es2) in
(* Simplification d'une formule *)
match f with
| PropConst(op) -> PropConst(op)
| PropUn(op, f) -> simpl_propop1 op f lv lk
| PropBin(op, f1, f2) -> simpl_propop2 op f1 f2 lv lk
| Rel(op, e1, e2) -> simpl_exprop2 op e1 e2 lv lk
| FreshState(f) -> FreshState(f) and (* TODO: Réfléchir à la simplification de FreshState : simplification des paramètres ? *)
(* Simplifications atomiques pour chaque forme de proposition *)
(* Opérateur unaire *)
simpl_propop1 op f lv lk =
match op with
| Neg -> match eval_formula f with
| T -> F
| F -> T
| U -> U ;;
let eval_propop2_And f1 f2 =
match eval_formula f1 with
| T -> eval_formula f2
| F -> F
| U -> match eval_formula f2 with
| T -> U
| F -> F
| U -> U ;;
let eval_propop2_Or f1 f2 =
match eval_formula f1 with
| T -> T
| F -> eval_formula f2
| U -> match eval_formula f2 with
| T -> T
| F -> U
| U -> U ;;
let eval_propop2_Impl f1 f2 =
match eval_formula f1 with
| T -> match eval_formula f2 with
| T -> T
| F -> F
| U -> U
| F -> T
| U -> U ;;
let eval_propop2 op f1 f2 =
| Neg -> match simpl_formula f lv lk with
| PropConst True -> PropConst False
| PropConst False -> PropConst True
| fs -> PropUn(Neg, fs) and
(* Opérateurs binaires *)
simpl_propop2 op f1 f2 lv lk =
match op with
| And -> eval_propop2_And f1 f2
| Or -> eval_propop2_Or f1 f2
| Impl -> eval_propop2_Impl f1 f2 ;;
let evalfun_of_relop2 = function
| LE -> (<=)
| LT -> (<)
| GE -> (>=)
| GT -> (>)
| Eq -> (=)
| NEq -> (!=) ;;
let eval_relop2 op e1 e2 =
match (eval_expr e1), (eval_expr e2) with
| Evaluated val1, Evaluated val2 -> evaluated_of_bool ((evalfun_of_relop2 op) val1 val2)
| _, _ -> U ;;
let evalfun_of_exprop2 = function
| Plus -> (+)
| Minus -> (-) ;;
let eval_exprop2 op e1 e2 =
match (eval_expr e1), (eval_expr e2) with
| Evaluated val1, Evaluated val2 -> (evalfun_of_exprop2 op) val1 val2
| _, _ -> U ;;
let eval_expr e lv lk =
match e with
| ExprBin(op, e1, e2) -> eval_exprop2 op e1 e2
| ExprVar(v) -> match assoc_find varequals lv v with
| Found val -> Evaluated val
| Not_found -> Unknown
| ExprParam(v, l) -> match assoc_find paramequals lk (v, l) with
| Found val -> Evaluated val
| Not_found -> Unknown
| ExprConst(i) -> Evaluated i ;;
let eval_prop e lv lk =
match e with
| PropConst(op) -> eval_propop0 op
| PropUn(op, f) -> eval_propop1 op f
| PropBin(op, f1, f2) -> eval_propop2 op f1 f2
| Rel(op, e1, e2) -> eval_relop1 op e1 e2
| FreshState(f) -> U ;; (* TODO: Réfléchir à l'évaluation de FreshState *)
*)
type assoc_option =
| Found of int
| Not_found ;;
(* Simplification d'une expression *)
let rec simpl_expr e lv lk =
let rec assoc_find eq k1 l =
match l with
| [] -> Not_found
| (k2, v) :: t -> match eq k1 k2 with
| true -> Found v
| false -> assoc_find eq k1 t in
(* xFIXME? : Revoir la notion d'égalité : la fonction (=) propre à OCaml est-elle suffisante ? *)
let paramequals = (=) in
let evalfun_of_exprop2 = function
| Plus -> (+)
| Minus -> (-) in
match e with
| ExprBin(op, e1, e2) -> (match simpl_expr e1 lv lk, simpl_expr e2 lv lk with
| ExprConst(i1), ExprConst(i2) -> ExprConst(evalfun_of_exprop2 op i1 i2)
| es1, es2 -> ExprBin(op, es1, es2))
| ExprVar(v) -> (match assoc_find BRN.varequals v lv with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprParam(v, l) -> (match assoc_find paramequals (v, l) lk with
| Found i -> ExprConst(i)
| Not_found -> e)
| ExprConst(i) -> ExprConst(i) ;;
let rec simpl_formula f lv lk =
let evalfun_of_relop2 = function
| LE -> (<=)
| LT -> (<)
| GE -> (>=)
| GT -> (>)
| Eq -> (=)
| NEq -> (!=) in
let simpl_exprop2 op e1 e2 lv lk =
match (simpl_expr e1 lv lk), (simpl_expr e2 lv lk) with
| ExprConst(i1), ExprConst(i2) -> (match (evalfun_of_relop2 op) i1 i2 with
| true -> PropConst(True)
| false -> PropConst(False))
| es1, es2 -> Rel(op, es1, es2) in
(* Simplification d'une formule *)
match f with
| PropConst(op) -> PropConst(op)
| PropUn(op, f) -> (* DEBUG print_endline (" === PropUn ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_propop1 op f lv lk))) ; *) simpl_propop1 op f lv lk
| PropBin(op, f1, f2) -> (* DEBUG print_endline (" === PropBin ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_propop2 op f1 f2 lv lk))) ; *) simpl_propop2 op f1 f2 lv lk
| Rel(op, e1, e2) -> (* DEBUG print_endline (" === Rel ===\n" ^ (string_of_formula f) ^ "\n" ^ (string_of_formula (simpl_exprop2 op e1 e2 lv lk))) ; *) simpl_exprop2 op e1 e2 lv lk
| FreshState(f) -> FreshState(f) and (* TODO: Réfléchir à la simplification de FreshState : simplification des paramètres ? *)
(* Simplifications atomiques pour chaque forme de proposition *)
(* Opérateur unaire *)
simpl_propop1 op f lv lk =
match op with
| Neg -> match simpl_formula f lv lk with
| PropConst True -> PropConst False
| PropConst False -> PropConst True
| fs -> PropUn(Neg, fs) and
(* Opérateurs binaires *)
simpl_propop2 op f1 f2 lv lk =
match op with
| And -> simpl_propop2_And f1 f2 lv lk
| Or -> simpl_propop2_Or f1 f2 lv lk
| Impl -> simpl_propop2_Impl f1 f2 lv lk and
simpl_propop2_And f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(False)
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> fs1
| PropConst(False) -> PropConst(False)
| fs2 -> PropBin(And, fs1, fs2)) and
simpl_propop2_Or f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> simpl_formula f2 lv lk
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> fs1
| fs2 -> PropBin(Or, fs1, fs2)) and
simpl_propop2_Impl f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(True)
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> PropUn(Neg, fs1)
| fs2 -> PropBin(Impl, fs1, fs2)) ;;
let simplify f lv lk =
let rec iter_lv l =
match l with
| [] -> PropConst(True)
| (v, i) :: [] -> Rel(Eq, ExprVar(v), ExprConst(i))
| (v, i) :: t -> PropBin(And, Rel(Eq, ExprVar(v), ExprConst(i)), iter_lv t) in
let rec iter_lk l =
match l with
| [] -> PropConst(True)
| ((v, lm), i) :: [] -> Rel(Eq, ExprParam(v, lm), ExprConst(i))
| ((v, lm), i) :: t -> PropBin(And, Rel(Eq, ExprParam(v, lm), ExprConst(i)), iter_lk t) in
(simpl_formula (PropBin(And, iter_lv lv, iter_lk lk)) [] [], simpl_formula f lv lk) ;;
| And -> simpl_propop2_And f1 f2 lv lk
| Or -> simpl_propop2_Or f1 f2 lv lk
| Impl -> simpl_propop2_Impl f1 f2 lv lk and
simpl_propop2_And f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(False)
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> fs1
| PropConst(False) -> PropConst(False)
| fs2 -> PropBin(And, fs1, fs2)) and
simpl_propop2_Or f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> simpl_formula f2 lv lk
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> fs1
| fs2 -> PropBin(Or, fs1, fs2)) and
simpl_propop2_Impl f1 f2 lv lk =
match simpl_formula f1 lv lk with
| PropConst(True) -> simpl_formula f2 lv lk
| PropConst(False) -> PropConst(True)
| fs1 -> (match simpl_formula f2 lv lk with
| PropConst(True) -> PropConst(True)
| PropConst(False) -> PropUn(Neg, fs1)
| fs2 -> PropBin(Impl, fs1, fs2)) ;;
(** Retourne la formule simplifiée et les hypothèses de simplification *)
(* TODO: Traduire à l'aide d'une fonction xx_of_list (fold_left ?) instpirée de string_of_list *)
let simplify f lv lk =
let rec iter_lv l =
match l with
| [] -> PropConst(True)
| (v, i) :: [] -> Rel(Eq, ExprVar(v), ExprConst(i))
| (v, i) :: t -> PropBin(And, Rel(Eq, ExprVar(v), ExprConst(i)), iter_lv t) in
let rec iter_lk l =
match l with
| [] -> PropConst(True)
| ((v, lm), i) :: [] -> Rel(Eq, ExprParam(v, lm), ExprConst(i))
| ((v, lm), i) :: t -> PropBin(And, Rel(Eq, ExprParam(v, lm), ExprConst(i)), iter_lk t) in
(simpl_formula (PropBin(And, iter_lv lv, iter_lk lk)) [] [], simpl_formula f lv lk) ;;
end ;;
......@@ -1015,6 +921,10 @@ open WP ;;
open ASP ;;
let and_simplify f lv lk =
let (a, b) = simplify f lv lk in
PropBin(And, a, b) ;;
(***********************************)
......@@ -1075,10 +985,6 @@ write_example pre3 "toyex-complex.lp" ;;
(** Exemple du papier *)
let and_simplify f lv lk =
let (a, b) = simplify f lv lk in
PropBin(And, a, b) ;;
let prog1 = Seq(Seq(Incr B, Incr C), Decr B) ;;
let post1 = Rel(Eq, ExprVar B, ExprConst 0) ;;
(* let pre1_nr = wp prog1 post1 ;; (* Sans raffinage *) *)
......
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