[interpretation] Add specific caisar builtins.

src/interpretation.ml

@@ -20,13 +20,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module Caisar_reduction_engine = Reduction_engine
 open Why3
 open Base
 
 let interpret_task env task =
   let f = Task.task_goal_fmla task in
   let engine =
-    Reduction_engine.create
+    Caisar_reduction_engine.create
       {
         compute_defs = false;
         compute_builtin = true;
@@ -35,8 +36,11 @@ let interpret_task env task =
       }
       env Ident.Mid.empty
   in
-  let f = Reduction_engine.normalize ~limit:1000 engine Term.Mvs.empty f in
-  Fmt.pr "%a : %a@." Pretty.print_pr (Task.task_goal task) Pretty.print_term f
+  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
 
 let interpret ?debug ?format ~loadpath s =
   let env, _config, mstr_theory =

src/reduction_engine.mli

@@ -9,116 +9,109 @@
 (*                                                                  *)
 (********************************************************************)
 
-
 (** A reduction engine for Why3 terms *)
 
-(*
-terms are normalized with respect to
+(* terms are normalized with respect to
 
-1) built-in computation rules
+   1) built-in computation rules
 
- a) on propositional connectives, e.g.
+   a) on propositional connectives, e.g.
 
    f /\ true -> f
 
- b) on integers, e.g.
+   b) on integers, e.g.
 
    35 + 7 -> 42
 
- c) on projections of pairs and of other ADTs, e.g
-
-  fst (x,y) -> x
-
-  cdr (Cons x y) -> y
+   c) on projections of pairs and of other ADTs, e.g
 
- d) on defined function symbols, e.g.
+   fst (x,y) -> x
 
-  function sqr (x:int) = x * x
+   cdr (Cons x y) -> y
 
-  sqr 4 -> 4 * 4 -> 16
+   d) on defined function symbols, e.g.
 
-  sqr x -> x * x
+   function sqr (x:int) = x * x
 
- e) (TODO?) on booleans, e.g.
+   sqr 4 -> 4 * 4 -> 16
 
-  True xor False -> True
+   sqr x -> x * x
 
- f) (TODO?) on reals, e.g.
+   e) (TODO?) on booleans, e.g.
 
-  1.0 + 2.5 -> 3.5
+   True xor False -> True
 
-2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if
+   f) (TODO?) on reals, e.g.
 
-    function dot : t -> t -> t
-    axiom assoc: forall x y z, dot (dot x y) z = dot x (dot y z)
-    meta "rewrite" assoc
+   1.0 + 2.5 -> 3.5
 
-  then
+   2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if
 
-  dot (dot a b) (dot c d) -> dot a (dot b (dot c d))
+   function dot : t -> t -> t axiom assoc: forall x y z, dot (dot x y) z = dot x
+   (dot y z) meta "rewrite" assoc
 
-  axioms used as rewrite rules must be either of the form
+   then
 
-    forall ... t1 = t2
+   dot (dot a b) (dot c d) -> dot a (dot b (dot c d))
 
-  or
+   axioms used as rewrite rules must be either of the form
 
-    forall ... f1 <-> f2
+   forall ... t1 = t2
 
-   where the root symbol of t1 (resp. f1) is a non-interpreted function
-   symbol (resp. non-interpreted predicate symbol)
+   or
 
-  rewriting is done from left to right
+   forall ... f1 <-> f2
 
+   where the root symbol of t1 (resp. f1) is a non-interpreted function symbol
+   (resp. non-interpreted predicate symbol)
 
-*)
+   rewriting is done from left to right *)
 open Why3
 
 type engine
 (** abstract type for reduction engines *)
 
+val print_caisar_op : engine Fmt.t
+
 type params = {
   compute_defs : bool;
   compute_builtin : bool;
   compute_def_set : Term.Sls.t;
   compute_max_quantifier_domain : int;
 }
-(** Configuration of the engine.
-   . [compute_defs]: if set to true, automatically compute symbols using
-     known definitions. Otherwise, only symbols in [compute_def_set]
-     will be computed.
-   . [compute_builtin]: if set to true, compute builtin functions.
-   . [compute_max_quantifier_domain]: maximum domain size for the reduction of
-     bounded quantifications *)
+(** Configuration of the engine. . [compute_defs]: if set to true, automatically
+    compute symbols using known definitions. Otherwise, only symbols in
+    [compute_def_set] will be computed. . [compute_builtin]: if set to true,
+    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
-(** [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
-*)
+(** [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
-(** [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 the general rules given above.
-*)
-
-
-val normalize : ?step_limit:int -> limit:int -> engine -> Term.term Term.Mvs.t -> Term.term -> Term.term
-(** [normalize e sigma t] normalizes the term [t] with respect to the engine
-    [e] with an initial variable environment [sigma].
-
-    parameter [limit] provides a maximum number of steps for execution.
-    When limit is reached, the partially reduced term is returned.
-    parameter [step_limit] provides a maximum number of steps on reductions
-    that would change the term even after reconstruction.
-*)
-
+(** [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
+    the general rules given above. *)
+
+val normalize :
+  ?step_limit:int ->
+  limit:int ->
+  engine ->
+  Term.term Term.Mvs.t ->
+  Term.term ->
+  Term.term
+(** [normalize e sigma t] normalizes the term [t] with respect to the engine [e]
+    with an initial variable environment [sigma].
+
+    parameter [limit] provides a maximum number of steps for execution. When
+    limit is reached, the partially reduced term is returned. parameter
+    [step_limit] provides a maximum number of steps on reductions that would
+    change the term even after reconstruction. *)
 
 open Term
 
@@ -130,4 +123,5 @@ exception NoMatchpat of (pattern * pattern) option
 
 type substitution = term Mvs.t
 
-val first_order_matching: Svs.t -> term list -> term list -> Ty.ty Ty.Mtv.t * substitution
+val first_order_matching :
+  Svs.t -> term list -> term list -> Ty.ty Ty.Mtv.t * substitution

stdlib/caisar.mlw

@@ -80,3 +80,13 @@ theory NN
 
   function relu (a: t): t =  if a .> (0.0:t) then a else (0.0:t)
 end
+
+theory Interpret
+
+  type dataset
+
+  function open_dataset string: dataset
+
+  function size dataset: int
+
+end

tests/interpretation.t

 Test verify
   $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
+  >  use caisar.Interpret
   >  use int.Int
   > 
   >   goal G1: 1+1=2
   > 
   >   goal G2: 1+1=3
   > 
+  >   goal G3: size (open_dataset "datasets/a") = 2
+  > 
+  >   goal G4:
+  >       let dataset = open_dataset "datasets/a" in
+  >       size dataset = 2
+  > 
+  > 
   > end
   > EOF
   G1 : true
+  
   G2 : false
+  
+  Reduction engine, ident not found: infix =
+  G3 : caisar_op = 2
+  caisar_op1,
+  (Reduction_engine.Dataset { Reduction_engine.dataset = "datasets/a" })
+  caisar_op,
+  (Reduction_engine.Size { Reduction_engine.dataset = "datasets/a" })
+  Reduction engine, ident not found: infix =
+  G4 : caisar_op2 = 2
+  caisar_op3,
+  (Reduction_engine.Dataset { Reduction_engine.dataset = "datasets/a" })
+  caisar_op2,
+  (Reduction_engine.Size { Reduction_engine.dataset = "datasets/a" })