From 2a409542c7f75277adcdc3337bd37700998ee90e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 21 Sep 2022 17:17:24 +0200
Subject: [PATCH] [interpretation] Remove caisar specific code from reduction
engine.
---
src/interpretation.ml | 77 +++++++++++++++++++++++++++++++-
src/reduction_engine.ml | 96 +++++++---------------------------------
src/reduction_engine.mli | 30 ++++++++++---
tests/interpretation.t | 8 ++--
4 files changed, 120 insertions(+), 91 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index c1c96e4..5074aa2 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -24,8 +24,81 @@ module Caisar_reduction_engine = Reduction_engine
open Why3
open Base
+type dataset = { dataset : string } [@@deriving show]
+type caisar_op = Dataset of dataset | Size of dataset [@@deriving show]
+
+type caisar_env = {
+ dataset_ty : Ty.ty;
+ caisar_op_of_ls : caisar_op Term.Hls.t;
+ ls_of_caisar_op : (caisar_op, Term.lsymbol) Hashtbl.t;
+}
+
+type engine = caisar_env Caisar_reduction_engine.engine
+
+let ls_of_caisar_op (env : engine) op =
+ let caisar_env = Caisar_reduction_engine.user_env env in
+ if Hashtbl.mem caisar_env.ls_of_caisar_op op
+ then Hashtbl.find_exn caisar_env.ls_of_caisar_op op
+ else
+ let id = Ident.id_fresh "caisar_op" in
+ let ty =
+ match op with Dataset _ -> caisar_env.dataset_ty | Size _ -> Ty.ty_int
+ in
+ let ls = Term.create_fsymbol id [] ty in
+ Hashtbl.Poly.add_exn caisar_env.ls_of_caisar_op ~key:op ~data:ls;
+ Term.Hls.add caisar_env.caisar_op_of_ls ls op;
+ ls
+
+let caisar_op_of_ls env ls =
+ let caisar_env = Caisar_reduction_engine.user_env env in
+ Term.Hls.find caisar_env.caisar_op_of_ls ls
+
+let term_of_caisar_op env op = Term.t_app_infer (ls_of_caisar_op env op) []
+
+let read_caisar_env env =
+ let th = Env.read_theory env [ "caisar" ] "Interpret" in
+ let dataset_ts = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
+ {
+ dataset_ty = Ty.ty_app dataset_ts [];
+ ls_of_caisar_op = Hashtbl.Poly.create ();
+ caisar_op_of_ls = Term.Hls.create 10;
+ }
+
+let print_caisar_op fmt caisar_env =
+ Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
+ fmt caisar_env.caisar_op_of_ls
+
+let built_in_caisar : caisar_env Caisar_reduction_engine.built_in_theories list
+ =
+ let open_dataset : _ Caisar_reduction_engine.builtin =
+ fun engine _ l _ ->
+ match l with
+ | [ Term { t_node = Tconst (ConstStr dataset); _ } ] ->
+ Term (term_of_caisar_op engine (Dataset { dataset }))
+ | _ -> invalid_arg "We want a string! ;)"
+ in
+ let size : _ Caisar_reduction_engine.builtin =
+ fun engine _ l _ ->
+ match l with
+ | [ Term { t_node = Tapp (ls, []); _ } ] -> (
+ match caisar_op_of_ls engine ls with
+ | Dataset dataset -> Term (term_of_caisar_op engine (Size dataset))
+ | Size _ -> invalid_arg "We want a dataset! ;)")
+ | _ -> invalid_arg "We want a string! ;)"
+ in
+
+ [
+ (* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
+ eval_false ; ] ; *)
+ ( [ "caisar" ],
+ "Interpret",
+ [],
+ [ ("open_dataset", None, open_dataset); ("size", None, size) ] );
+ ]
+
let interpret_task env task =
let f = Task.task_goal_fmla task in
+ let caisar_env = read_caisar_env env in
let engine =
Caisar_reduction_engine.create
{
@@ -34,13 +107,13 @@ let interpret_task env task =
compute_def_set = Term.Sls.empty;
compute_max_quantifier_domain = 0;
}
- env Ident.Mid.empty
+ env Ident.Mid.empty caisar_env built_in_caisar
in
let f =
Caisar_reduction_engine.normalize ~limit:1000 engine Term.Mvs.empty f
in
Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term
- f Caisar_reduction_engine.print_caisar_op engine
+ f print_caisar_op caisar_env
let interpret ?debug ?format ~loadpath s =
let env, _config, mstr_theory =
diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index e0c5c12..5b89f9f 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -16,9 +16,6 @@ open Term
(* {2 Values} *)
-type dataset = { dataset : string } [@@deriving show]
-type caisar_op = Dataset of dataset | Size of dataset [@@deriving show]
-
type value =
| Term of term (* invariant: is in normal form *)
| Int of BigInt.t
@@ -26,12 +23,6 @@ type value =
(** {2 Environment} *)
-type caisar_env = {
- dataset_ty : Ty.ty;
- caisar_op_of_ls : caisar_op Term.Hls.t;
- ls_of_caisar_op : (caisar_op, Term.lsymbol) Hashtbl.t;
-}
-
type rule = Svs.t * term list * term
type params = {
@@ -41,48 +32,19 @@ type params = {
compute_max_quantifier_domain : int;
}
-type builtin = engine -> lsymbol -> value list -> Ty.ty option -> value
+type 'a builtin = 'a engine -> lsymbol -> value list -> Ty.ty option -> value
-and engine = {
+and 'a engine = {
env : Env.env;
known_map : Decl.decl Ident.Mid.t;
rules : rule list Mls.t;
params : params;
ls_lt : lsymbol; (* The lsymbol for [int.Int.(<)] *)
- caisar_env : caisar_env;
- builtins : builtin Hls.t;
+ user_env : 'a;
+ builtins : 'a builtin Hls.t;
}
-let ls_of_caisar_op env op =
- if Hashtbl.mem env.caisar_env.ls_of_caisar_op op
- then Hashtbl.find env.caisar_env.ls_of_caisar_op op
- else
- let id = Ident.id_fresh "caisar_op" in
- let ty =
- match op with
- | Dataset _ -> env.caisar_env.dataset_ty
- | Size _ -> Ty.ty_int
- in
- let ls = Term.create_fsymbol id [] ty in
- Hashtbl.add env.caisar_env.ls_of_caisar_op op ls;
- Term.Hls.add env.caisar_env.caisar_op_of_ls ls op;
- ls
-
-let caisar_op_of_ls env ls = Term.Hls.find env.caisar_env.caisar_op_of_ls ls
-let term_of_caisar_op env op = Term.t_app_infer (ls_of_caisar_op env op) []
-
-let read_caisar_env env =
- let th = Env.read_theory env [ "caisar" ] "Interpret" in
- let dataset_ts = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
- {
- dataset_ty = Ty.ty_app dataset_ts [];
- ls_of_caisar_op = Hashtbl.create 10;
- caisar_op_of_ls = Term.Hls.create 10;
- }
-
-let print_caisar_op fmt engine =
- Pp.print_iter2 Term.Hls.iter Pp.newline Pp.comma Pretty.print_ls pp_caisar_op
- fmt engine.caisar_env.caisar_op_of_ls
+let user_env x = x.user_env
let v_attr_copy orig v =
match v with Int _ -> v | Real _ -> v | Term t -> Term (t_attr_copy orig t)
@@ -356,13 +318,14 @@ let real_from_int _ _ls l _ty =
with NotNum -> raise Undetermined)
| _ -> assert false
-type built_in_theories =
+type 'a built_in_theories =
Env.pathname
* string
* (string * (Ty.tysymbol -> unit)) list
- * (string * lsymbol ref option * builtin) list
+ * (string * lsymbol ref option * 'a builtin) list
-let built_in_theories : built_in_theories list =
+let built_in_theories : unit -> 'a built_in_theories list =
+ fun () ->
[
(* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
eval_false ; ] ; *)
@@ -423,7 +386,7 @@ let built_in_theories : built_in_theories list =
ls_map_set, eval_map_set; ] ; *)
]
-let add_builtin_th env ((l, n, t, d) : built_in_theories) =
+let add_builtin_th env ((l, n, t, d) : 'a built_in_theories) =
let th = Env.read_theory env.env l n in
List.iter
(fun (id, r) ->
@@ -437,37 +400,10 @@ let add_builtin_th env ((l, n, t, d) : built_in_theories) =
match r with None -> () | Some r -> r := ls)
d
-let built_in_caisar : built_in_theories list =
- let open_dataset : builtin =
- fun engine _ l _ ->
- match l with
- | [ Term { t_node = Tconst (ConstStr dataset) } ] ->
- Term (term_of_caisar_op engine (Dataset { dataset }))
- | _ -> invalid_arg "We want a string! ;)"
- in
- let size : builtin =
- fun engine _ l _ ->
- match l with
- | [ Term { t_node = Tapp (ls, []) } ] -> (
- match caisar_op_of_ls engine ls with
- | Dataset dataset -> Term (term_of_caisar_op engine (Size dataset))
- | Size _ -> invalid_arg "We want a dataset! ;)")
- | _ -> invalid_arg "We want a string! ;)"
- in
-
- [
- (* ["bool"],"Bool", [], [ "True", None, eval_true ; "False", None,
- eval_false ; ] ; *)
- ( [ "caisar" ],
- "Interpret",
- [],
- [ ("open_dataset", None, open_dataset); ("size", None, size) ] );
- ]
-
-let get_builtins env =
+let get_builtins env built_in_user =
Hls.clear env.builtins;
- List.iter (add_builtin_th env) built_in_theories;
- List.iter (add_builtin_th env) built_in_caisar
+ List.iter (add_builtin_th env) (built_in_theories ());
+ List.iter (add_builtin_th env) built_in_user
(* {2 the reduction machine} *)
@@ -1387,7 +1323,7 @@ let normalize ?step_limit ~limit engine sigma t0 =
(* the rewrite engine *)
-let create p env km =
+let create p env km user_env built_in_user =
let th = Env.read_theory env [ "int" ] "Int" in
let ls_lt = Theory.ns_find_ls th.Theory.th_export [ Ident.op_infix "<" ] in
let env =
@@ -1398,10 +1334,10 @@ let create p env km =
params = p;
ls_lt;
builtins = Hls.create 17;
- caisar_env = read_caisar_env env;
+ user_env;
}
in
- if p.compute_builtin then get_builtins env;
+ if p.compute_builtin then get_builtins env built_in_user;
env
exception NotARewriteRule of string
diff --git a/src/reduction_engine.mli b/src/reduction_engine.mli
index da1f53c..53407b2 100644
--- a/src/reduction_engine.mli
+++ b/src/reduction_engine.mli
@@ -68,10 +68,10 @@
rewriting is done from left to right *)
open Why3
-type engine
+type 'a engine
(** abstract type for reduction engines *)
-val print_caisar_op : engine Fmt.t
+val user_env : 'a engine -> 'a
type params = {
compute_defs : bool;
@@ -85,14 +85,34 @@ type params = {
compute builtin functions. . [compute_max_quantifier_domain]: maximum domain
size for the reduction of bounded quantifications *)
-val create : params -> Env.env -> Decl.decl Ident.Mid.t -> engine
+type value =
+ | Term of Why3.Term.term (* invariant: is in normal form *)
+ | Int of BigInt.t
+ | Real of Number.real_value
+
+type 'a builtin =
+ 'a engine -> Why3.Term.lsymbol -> value list -> Ty.ty option -> value
+
+type 'a built_in_theories =
+ Env.pathname
+ * string
+ * (string * (Ty.tysymbol -> unit)) list
+ * (string * Why3.Term.lsymbol ref option * 'a builtin) list
+
+val create :
+ params ->
+ Env.env ->
+ Decl.decl Ident.Mid.t ->
+ 'a ->
+ 'a built_in_theories list ->
+ 'a engine
(** [create env known_map] creates a reduction engine with . builtins theories
(int.Int, etc.) extracted from [env] . known declarations from [known_map] .
empty set of rewrite rules *)
exception NotARewriteRule of string
-val add_rule : Term.term -> engine -> engine
+val add_rule : Term.term -> 'a engine -> 'a engine
(** [add_rule t e] turns [t] into a new rewrite rule and returns the new engine.
raise NotARewriteRule if [t] cannot be seen as a rewrite rule according to
@@ -101,7 +121,7 @@ val add_rule : Term.term -> engine -> engine
val normalize :
?step_limit:int ->
limit:int ->
- engine ->
+ 'a engine ->
Term.term Term.Mvs.t ->
Term.term ->
Term.term
diff --git a/tests/interpretation.t b/tests/interpretation.t
index 133dd62..ce2d416 100644
--- a/tests/interpretation.t
+++ b/tests/interpretation.t
@@ -24,12 +24,12 @@ Test verify
Reduction engine, ident not found: infix =
G3 : caisar_op = 2
caisar_op1,
- (Reduction_engine.Dataset { Reduction_engine.dataset = "datasets/a" })
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
caisar_op,
- (Reduction_engine.Size { Reduction_engine.dataset = "datasets/a" })
+ (Interpretation.Size { Interpretation.dataset = "datasets/a" })
Reduction engine, ident not found: infix =
G4 : caisar_op2 = 2
caisar_op3,
- (Reduction_engine.Dataset { Reduction_engine.dataset = "datasets/a" })
+ (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
caisar_op2,
- (Reduction_engine.Size { Reduction_engine.dataset = "datasets/a" })
+ (Interpretation.Size { Interpretation.dataset = "datasets/a" })
--
GitLab