[interpretation] Remove caisar specific code from reduction engine.

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 =

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

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

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" })