begin adding simplification

main.ml

@@ -139,7 +139,6 @@ struct
 end ;;
 *)
 
-(*
 (** Exemple du papier *)
 module SimpleExample =
 struct
@@ -175,7 +174,6 @@ struct
   let multcompare m1 m2 =
     compare (asp_of_mult m1) (asp_of_mult m2) ;;
 end ;;
-*)
 
 (*
 (** Phage lambda (depuis la thèse d'Adrien Richard) *)
@@ -228,6 +226,7 @@ struct
 end ;;
 *)
 
+(*
 (** Cycle circadien (depuis projet Circlock)  *)
 module Circlock =
 struct
@@ -299,14 +298,15 @@ struct
   let multcompare m1 m2 =
     compare (asp_of_mult m1) (asp_of_mult m2) ;;
 end ;;
+*)
 
 
 
 (** Sélection du BRN à considérer *)
 (* module BRN = ToyExample ;; *)
-(* module BRN = SimpleExample ;; *)
+module BRN = SimpleExample ;;
 (* module BRN = PhageLambda ;; *)
-module BRN = Circlock ;;
+(* module BRN = Circlock ;; *)
 
 
 
@@ -380,7 +380,6 @@ struct
 end ;;
 *)
 
-(*
 (** Exemple du papier *)
 module SimpleExampleInfo =
 struct
@@ -401,7 +400,6 @@ struct
     | B -> [Lambda ; Sigma]
     | C -> [L] ;;
 end ;;
-*)
 
 (*
 (** Phage lambda (depuis la thèse d'Adrien Richard) *)
@@ -433,6 +431,7 @@ struct
 end ;;
 *)
 
+(*
 (** Cycle circadien (depuis projet Circlock)  *)
 module CirclockInfo =
 struct
@@ -467,14 +466,15 @@ struct
     | BMAL1N -> [Inhib]
     | BMAL1C -> [Acetylation] ;;
 end ;;
+*)
 
 
 
 (** Sélection des informations du BRN à considérer *)
 (* module BRNinfo = ToyExampleInfo ;; *)
-(* module BRNinfo = SimpleExampleInfo ;; *)
+module BRNinfo = SimpleExampleInfo ;;
 (* module BRNinfo = PhageLambdaInfo ;; *)
-module BRNinfo = CirclockInfo ;;
+(* module BRNinfo = CirclockInfo ;; *)
 
 
 
@@ -514,23 +514,6 @@ struct
     | MAtom(v, i) -> formula_of_matom v i
     | MMult(m) -> formula_of_multformula (BRNinfo.getformula m) ;;
 
-(** Substitution d'une expression à une variable *)
-  let replace f v e =
-    let rec replace_expr ex v' e' =
-      match ex with
-        | ExprBin(op, e1, e2) -> ExprBin(op, replace_expr e1 v' e', replace_expr e2 v' e')
-        | ExprVar(v) -> if (BRN.varequals v v') then e' else ExprVar(v)
-        | ExprParam(v, l) -> ExprParam(v, l)
-        | ExprConst(i) -> ExprConst(i) in
-    let rec replace_formula tree v' e' =
-      match tree with
-        | PropConst(op) -> PropConst(op)
-        | 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')
-        | FreshState(f) -> FreshState(f) in
-    replace_formula f v e ;;
-
 (** Conversion d'une expression en chaîne de caractères pour ASP *)
   let rec asp_of_state_expr s =
     let paramlist = List.fold_right (fun v l -> (powerset_sort (BRNinfo.getpredec v) BRN.multcompare) :: l) BRN.varlist [] in
@@ -541,7 +524,7 @@ struct
     | ExprConst(i) -> string_of_int i ;;
   let asp_of_expr = asp_of_state_expr 0 ;;
 
-(** Conversion en chaîne de caractères pour affichage *)
+(** Conversion d'une expression en chaîne de caractères pour affichage *)
   let rec string_of_expr = function
     | ExprBin(op, e1, e2) -> ("(" ^ (string_of_expr e1) ^ (string_of_exprop2 op) ^ (string_of_expr e2) ^ ")")
     | ExprVar(v) -> BRN.string_of_var v
@@ -553,6 +536,195 @@ struct
     | 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) ^ ")")
     | FreshState(f) -> ("∀ state σ, " ^ (string_of_formula f)) ;;
+
+(** Substitution d'une expression à une variable *)
+(* (* Insuffisant : ne déconstruit pas une expression pour vérifier qu'elle contient l'expression à rechercher *)
+  let super_replace f e1 e2 =
+    let rec replace_expr ex re1 re2 =
+      if ex = re1 then re2 else ex in
+    let rec replace_formula tree re1 re2 =
+      match tree with
+        | PropConst(op) -> PropConst(op)
+        | PropUn(op, f) -> PropUn(op, replace_formula f re1 re2)
+        | PropBin(op, f1, f2) -> PropBin(op, replace_formula f1 re1 re2, replace_formula f2 re1 re2)
+        | Rel(op, e1, e2) -> Rel(op, replace_expr e1 re1 re2, replace_expr e2 re1 re2)
+        | FreshState(f) -> FreshState(f) in
+    replace_formula f e1 e2 ;;
+*)
+
+  let replace f v e =
+    let rec replace_expr ex v' e' =
+      match ex with
+        | ExprBin(op, e1, e2) -> ExprBin(op, replace_expr e1 v' e', replace_expr e2 v' e')
+        | ExprVar(v) -> if (BRN.varequals v v') then e' else ExprVar(v)
+        | ExprParam(v, l) -> ExprParam(v, l)
+        | ExprConst(i) -> ExprConst(i) in
+    let rec replace_formula tree v' e' =
+      match tree with
+        | PropConst(op) -> PropConst(op)
+        | 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')
+        | FreshState(f) -> FreshState(f) in
+    replace_formula f v e ;;
+(*
+    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
+    | T -> true
+    | F -> false ;;
+
+(*
+  let eval_propop0 op =
+    match op with
+      | True -> T
+      | False -> F ;;
+  let eval_propop1 op f =
+    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 =
+    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 ;;
+*)
+
+(* TODO *)
+(* assoc_find *)
+
+(* TODO *)
+(* paramequals pour égaliser deux paramètres *)
+
+  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 *)
+
+(* TODO *)
+(* TODO: Optimiser à grands coups de let ... in pour éviter les évaluations répétées *)
+  let 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)
+      | _ -> match simpl_formula f2 lv lk with
+               | PropConst(True) -> simpl_formula f1 lv lk
+               | PropConst(False) -> PropConst(False)
+               | _ -> PropBin(And, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
+  let 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
+      | _ -> match simpl_formula f2 lv lk with
+               | PropConst(True) -> PropConst(True)
+               | PropConst(False) -> simpl_formula f1 lv lk
+               | _ -> PropBin(Or, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
+  let simpl_propop2_Impl f1 f2 lv lk =
+    match simpl_formula f1 lv lk with
+      | PropConst(True) -> match simpl_formula f2 lv lk with
+               | PropConst(True) -> PropConst(True)
+               | PropConst(False) -> PropConst(False)
+               | _ -> simpl_formula f2 lv lk
+      | PropConst(False) -> PropConst(True)
+      | _ -> PropBin(Impl, simpl_formula f1 lv lk, simpl_formula f2 lv lk) ;;
+  let 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 ;;
+
+(* TODO: Transformer pour virer un maximum d'évaluations et les transformer en simplifications + simplifier si un seul membre peut être évalué *)
+  let evalfun_of_exprop2 = function
+    | Plus -> (+)
+    | Minus -> (-) ;;
+  let simpl_exprop2 op e1 e2 =
+    match (eval_expr e1), (eval_expr e2) with
+      | Evaluated val1, Evaluated val2 -> (evalfun_of_exprop2 op) val1 val2
+      | Evaluated val1, _ -> ...
+      | _, Evaluated val2 -> ...
+      | _, _ -> U ;;
+
+  let rec simpl_formula e lv lk =
+    match e with
+      | PropConst(op) -> PropConst(op)
+      | PropUn(op, f) -> match simplify f lv lk with
+                           | PropConst True -> PropConst False
+                           | PropConst False -> PropConst True
+      | PropBin(op, f1, f2) -> simpl_propop2 op f1 f2 lv lk
+      | Rel(op, e1, e2) -> match eval_exprop2 op e1 e2 with
+                             | T -> ExprConst True
+                             | F -> ExprConst False
+                             | U -> e
+      | FreshState(f) -> FreshState(f) ;;  (* TODO: Réfléchir à la simplification de FreshState *)
 end ;;
 
 
@@ -798,6 +970,19 @@ open WP ;;
 
 open ASP ;;
 
+
+
+(** Tests sur super_replace *)
+
+
+
+
+
+
+(***********************************)
+(*** Traitement sur les exemples ***)
+(***********************************)
+
 (** Exemple jouet *)
 (*
 let prog1 = Seq(Incr A, Decr A) ;;
@@ -851,7 +1036,7 @@ write_example pre3 "toyex-complex.lp" ;;
 
 
 (** Exemple du papier *)
-(*
+
 let prog1 = Seq(Seq(Incr B, Incr C), Decr B) ;;
 let post1 = Rel(Eq, ExprVar B, ExprConst 0) ;;
 (* let pre1 = wp prog1 post1 ;; (* Sans raffinage *) *)
@@ -869,6 +1054,7 @@ write_example pre1 "simpleex1.lp" ;;
 (* OK : 16 solutions (avec raffinage) *)
 (* Contraintes trouvées : a = 1, b = 0, c = 0, k_b,{σ} = 0, k_b,{λ;σ} = 1, k_c,{l} = 1 *)
 
+(*
 let prog2 = Seq(Incr B, Decr B) ;;
 let post2 = post1 ;;
 let pre2 = wp prog2 post2 ;;
@@ -934,9 +1120,13 @@ print_endline "*** Plus faible pré-condition calculée ***" ;;
 print_endline (string_of_formula pre4b) ;;
 write_example pre4b "simpleex4b.lp" ;;
 (* OK : Aucune solution (avec raffinage) *)
+
+(* Essai : résolution sur la post-condition VRAI *)
+write_example (PropConst True) "simpleex5.lp" ;;
 *)
 
 
+
 (** Phage lambda (depuis la thèse d'Adrien Richard) *)
 (*
 (*Qa = N+; CII+; CI+; CI+; N−; CII−
@@ -960,9 +1150,8 @@ write_example prepl1 "phagelex1.lp" ;;
 *)
 
 
-
 (** Cycle circadien (d'après projet Circlock) *)
-
+(*
 let prog1 = Skip ;;
 let post1 = PropConst(True) ;;
 let pre1 = wp prog1 post1 ;;
@@ -977,9 +1166,21 @@ print_endline (string_of_formula pre1) ;;
 print_endline "***************************" ;;
 
 write_example pre1 "circlock1.lp" ;;
+*)
 
 
 
+(** Affichage des correspondances variable ASP / paramètre *)
+(*
 print_endline "   *****" ;;
 asp_params () ;;
+*)
+(*
+let te1 = PropBin(And, Rel(LE, ExprVar(A), ExprConst(5)), Rel(Eq, ExprParam(B, [Lambda]), ExprConst(0))) ;;
+print_endline (string_of_formula te1) ;;
+print_endline (string_of_formula (super_replace te1 (ExprVar(A)) (ExprBin(Plus, ExprVar(A), ExprConst(2))))) ;;
 
+print_endline "";;
+
+print_endline (string_of_bool (ExprConst(2) = ExprConst(1+1))) ;;
+*)