From cce563dd658091dfcd246278d7b29bd1c4c2f521 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 20 Sep 2022 16:40:37 +0200
Subject: [PATCH] Interp: Prettier code
---
colibri2/core/interp.ml | 25 +++++++++++++++----------
1 file changed, 15 insertions(+), 10 deletions(-)
diff --git a/colibri2/core/interp.ml b/colibri2/core/interp.ml
index a59f0c524..42450ac2c 100644
--- a/colibri2/core/interp.ml
+++ b/colibri2/core/interp.ml
@@ -158,14 +158,14 @@ let print_value_smt d fmt v =
let pr = Data.PrintValue.get Data.print_value k in
pr d fmt v
-let spy_sequence msg s i =
- if false then
+let spy_sequence msg s =
+ if false then fun i ->
Sequence.mapi
~f:(fun i x ->
Fmt.epr "@.%s %i: %a@." msg i Value.pp x;
x)
(s i)
- else s i
+ else s
let get_registered (type a) exn db call d x =
let exception Found of a in
@@ -288,13 +288,13 @@ let check_args d g =
raise (ArgOfGroundTermWithoutValueAfterModelFixing (g, n)))
let check_ground_terms d =
- Datastructure.Push.fold Data.reg_ground d ~init:false ~f:(fun acc g ->
+ Datastructure.Push.fold Data.reg_ground d ~init:`Right ~f:(fun acc g ->
if Option.is_none (Egraph.get_value d (Ground.node g)) then
raise (GroundTermWithoutValueAfterModelFixing (`Ground g));
check_args d g;
match check Data.check d g with
| Right -> acc
- | Unknown -> true
+ | Unknown -> `Unknown
| NA -> raise (CantCheckGround (`Ground g))
| Wrong ->
Debug.dprintf2 Egraph.print_contradiction
@@ -302,13 +302,13 @@ let check_ground_terms d =
Egraph.contradiction d)
let check_closed_quantifier d =
- Datastructure.Push.fold Data.reg_closed_quantifiers d ~init:false
+ Datastructure.Push.fold Data.reg_closed_quantifiers d ~init:`Right
~f:(fun acc g ->
if Option.is_none (Egraph.get_value d (Ground.ClosedQuantifier.node g))
then raise (GroundTermWithoutValueAfterModelFixing (`ClosedQuantifier g));
match check Data.check_closed_quantifier d g with
| Right -> acc
- | Unknown -> true
+ | Unknown -> `Unknown
| NA -> raise (CantCheckGround (`ClosedQuantifier g))
| Wrong ->
Debug.dprintf2 Egraph.print_contradiction
@@ -316,13 +316,13 @@ let check_closed_quantifier d =
Egraph.contradiction d)
let check_not_totally_applied d =
- Datastructure.Push.fold Data.reg_not_totally_applied d ~init:false
+ Datastructure.Push.fold Data.reg_not_totally_applied d ~init:`Right
~f:(fun acc g ->
if Option.is_none (Egraph.get_value d (Ground.NotTotallyApplied.node g))
then raise (GroundTermWithoutValueAfterModelFixing (`NotTotallyApplied g));
match check Data.check_not_totally_applied d g with
| Right -> acc
- | Unknown -> true
+ | Unknown -> `Unknown
| NA -> raise (CantCheckGround (`NotTotallyApplied g))
| Wrong ->
Debug.dprintf2 Egraph.print_contradiction
@@ -453,7 +453,12 @@ module Fix_model = struct
let unknown1 = check_ground_terms (Egraph.ro d) in
let unknown2 = check_closed_quantifier (Egraph.ro d) in
let unknown3 = check_not_totally_applied (Egraph.ro d) in
- let unknown = unknown1 || unknown2 || unknown3 in
+ let unknown =
+ match (unknown1, unknown2, unknown3) with
+ | `Right, `Right, `Right -> false
+ | _ -> true
+ in
+ Debug.dprintf1 debug "unknown:%b" unknown;
Egraph.set_unknown d unknown;
Egraph.set_env d Data.env Before;
Sequence.empty
--
GitLab