projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Add `Self direction in Formula + compute fixed point in Run.
[tatoo.git]
/
src
/
formula.ml
diff --git
a/src/formula.ml
b/src/formula.ml
index
8369571
..
2d9893c
100644
(file)
--- a/
src/formula.ml
+++ b/
src/formula.ml
@@
-15,7
+15,7
@@
INCLUDE "utils.ml"
open Format
INCLUDE "utils.ml"
open Format
-type move = [ `Left | `Right ]
+type move = [ `Left | `Right
| `Self
]
type 'hcons expr =
| False | True
| Or of 'hcons * 'hcons
type 'hcons expr =
| False | True
| Or of 'hcons * 'hcons
@@
-73,30
+73,30
@@
let prio f =
| Or _ -> 1
(* Begin Lucca Hirschi *)
| Or _ -> 1
(* Begin Lucca Hirschi *)
-let rec eval_form
ss
f = match expr f with
+let rec eval_form
(q,qf,qn)
f = match expr f with
| False -> false
| True -> true
| False -> false
| True -> true
- | And(f1,f2) -> eval_form
ss f1 && eval_form ss
f2
- | Or(f1,f2) -> eval_form
ss f1 || eval_form ss
f2
+ | And(f1,f2) -> eval_form
(q,qf,qn) f1 && eval_form (q,qf,qn)
f2
+ | Or(f1,f2) -> eval_form
(q,qf,qn) f1 || eval_form (q,qf,qn)
f2
| Atom(dir, b, s) ->
| Atom(dir, b, s) ->
- let set = match dir with |`Left -> fst ss | `Right -> snd ss in
+ let set = match dir with
+ |`Left -> qf | `Right -> qn | `Self -> q in
if b then StateSet.mem s set
else not (StateSet.mem s set)
if b then StateSet.mem s set
else not (StateSet.mem s set)
-let rec infer_form s
sq ssr
f = match expr f with
+let rec infer_form s
q sqf sqn
f = match expr f with
| False -> false
| True -> true
| False -> false
| True -> true
- | And(f1,f2) -> infer_form s
sq ssr f1 && infer_form ssq ssr
f2
- | Or(f1,f2) -> infer_form s
sq ssr f1 || infer_form ssq ssr
f2
+ | And(f1,f2) -> infer_form s
q sqf sqn f1 && infer_form sq sqf sqn
f2
+ | Or(f1,f2) -> infer_form s
q sqf sqn f1 || infer_form sq sqf sqn
f2
| Atom(dir, b, s) ->
let setq, setr = match dir with
| Atom(dir, b, s) ->
let setq, setr = match dir with
- |`Left -> fst ssq, fst ssr
- | `Right -> snd ssq, snd ssr in
+ | `Left -> sqf | `Right -> sqn | `Self -> sq in
(* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
let mem = StateSet.mem s setq || StateSet.mem s setr in
if b then mem else not mem
(* End *)
(* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *)
let mem = StateSet.mem s setq || StateSet.mem s setr in
if b then mem else not mem
(* End *)
-
+
let rec print ?(parent=false) ppf f =
if parent then fprintf ppf "(";
let _ = match expr f with
let rec print ?(parent=false) ppf f =
if parent then fprintf ppf "(";
let _ = match expr f with
@@
-117,6
+117,7
@@
let rec print ?(parent=false) ppf f =
match dir with
| `Left -> Pretty.down_arrow, Pretty.subscript 1
| `Right -> Pretty.down_arrow, Pretty.subscript 2
match dir with
| `Left -> Pretty.down_arrow, Pretty.subscript 1
| `Right -> Pretty.down_arrow, Pretty.subscript 2
+ | `Self -> Pretty.down_arrow, Pretty.subscript 0
in
fprintf fmt "%s%s" a_str d_str;
State.print fmt s;
in
fprintf fmt "%s%s" a_str d_str;
State.print fmt s;
@@
-147,6
+148,7
@@
let atom_ d p s =
let ss = match d with
| `Left -> si, StateSet.empty
| `Right -> StateSet.empty, si
let ss = match d with
| `Left -> si, StateSet.empty
| `Right -> StateSet.empty, si
+ | `Self -> si, StateSet.empty (* TODO WHAT? *)
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let not_ f = f.Node.node.neg
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let not_ f = f.Node.node.neg