diff --git a/src/interpretation.ml b/src/interpretation.ml
index 6fa6794b7ead8ad19acd46b03cb7ae0db3eb6375..605e68de649d01d92abb0d2ef3d3753c20361f34 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-module CRE = Reduction_engine (* Caisar Reduction Engine *)
+module CRE = Reduction_engine (* CAISAR Reduction Engine *)
open Why3
open Base
@@ -43,7 +43,6 @@ type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
[@@deriving show]
type data = D_csv of string list [@@deriving show]
-type index = I_csv of int [@@deriving show]
type vector =
(Language.vector
@@ -56,9 +55,7 @@ type caisar_op =
| Classifier of classifier
| Dataset of dataset
| Data of data
- | Index of index
| Vector of vector
- | Tensor of int
[@@deriving show]
type caisar_env = {
@@ -163,7 +160,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
let n = Option.value_exn (Language.lookup_vector v) in
assert (List.length tl1 = n && i <= n);
term (List.nth_exn tl1 i)
- | Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
+ | Data _ | Classifier _ -> assert false)
| [ Term t1; Term t2 ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t1; t2 ])
@@ -181,14 +178,14 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| Vector v ->
int (BigInt.of_int (Option.value_exn (Language.lookup_vector v)))
| Data (D_csv data) -> int (BigInt.of_int (List.length data))
- | Classifier _ | Tensor _ | Index _ -> assert false)
+ | Classifier _ -> assert false)
| [ Term { t_node = Tapp (ls, tl); _ } ] -> (
match caisar_op_of_ls engine ls with
| Vector v ->
let n = Option.value_exn (Language.lookup_vector v) in
assert (List.length tl = n);
int (BigInt.of_int n)
- | Dataset _ | Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
+ | Dataset _ | Data _ | Classifier _ -> assert false)
| [ Term t ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t ])
@@ -264,71 +261,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
in
Eval (term_of_caisar_op ~args engine caisar_op ty)
| Dataset (DS_csv csv) -> int (BigInt.of_int (Csv.lines csv))
- | Data _ | Classifier _ | Tensor _ | Index _ -> assert false)
- | [ Term t1; Term t2 ] ->
- (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
- term (Term.t_app_infer ls [ t1; t2 ])
- | _ -> invalid_arg (error_message ls)
- in
-
- (* Tensor *)
- let tget : _ CRE.builtin =
- fun engine ls vl _ty ->
- (* Fmt.pr "--@.tget: ls:%a , ty:%a@." Pretty.print_ls ls *)
- (* Fmt.(option ~none:nop Pretty.print_ty) *)
- (* ty; *)
- match vl with
- | [
- Term ({ t_node = Tapp (ls1, tl1); _ } as _t1);
- Term ({ t_node = Tapp (ls2, _); _ } as _t2);
- ] -> (
- (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
- match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
- | Tensor n, Index (I_csv i) ->
- assert (i <= n);
- term (List.nth_exn tl1 i)
- | _ -> assert false)
- | [ Term t1; Term t2 ] ->
- (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
- term (Term.t_app_infer ls [ t1; t2 ])
- | _ -> invalid_arg (error_message ls)
- in
- let tminus : _ CRE.builtin =
- fun engine ls vl ty ->
- (* Fmt.pr "--@.tminus: ls:%a , ty:%a@." Pretty.print_ls ls *)
- (* Fmt.(option ~none:nop Pretty.print_ty) *)
- (* ty; *)
- match vl with
- | [
- Term ({ t_node = Tapp (ls1, tl1); _ } as _t1);
- Term ({ t_node = Tapp (ls2, _); _ } as _t2);
- ] -> (
- (* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
- match (caisar_op_of_ls engine ls1, caisar_op_of_ls engine ls2) with
- | Tensor n, Data (D_csv data) ->
- assert (n = List.length data);
- let ty_cst =
- match ty with
- | Some { ty_node = Tyapp (_, [ ty ]); _ } -> ty
- | _ -> assert false
- in
- let csts =
- List.map data ~f:(fun d ->
- let cst = const_real_of_float (Float.of_string d) in
- Term.t_const cst ty_cst)
- in
- let minus =
- (* TODO: generalize wrt the type of constants [csts]. *)
- let { env; _ } = CRE.user_env engine in
- let th = Env.read_theory env [ "ieee_float" ] "Float64" in
- Theory.(ns_find_ls th.th_export [ Ident.op_infix ".-" ])
- in
- let args =
- List.map2_exn tl1 csts ~f:(fun tl c ->
- (Term.t_app_infer minus [ tl; c ], ty_cst))
- in
- term (term_of_caisar_op ~args engine (Tensor n) ty)
- | _ -> assert false)
+ | Data _ | Classifier _ -> assert false)
| [ Term t1; Term t2 ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t1; t2 ])
@@ -402,19 +335,11 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
([ "length" ], None, length);
([ "L"; "mapi" ], None, mapi);
] );
- ( [ "interpretation" ],
- "Tensor",
- [],
- [
- ([ Ident.op_infix "#" ], None, tget);
- ([ Ident.op_infix "-" ], None, tminus);
- ] );
( [ "interpretation" ],
"Classifier",
[],
[
([ "read_classifier" ], None, read_classifier);
- ([ Ident.op_infix "@@" ], None, apply_classifier);
([ Ident.op_infix "%%" ], None, apply_classifier);
] );
( [ "interpretation" ],
@@ -425,37 +350,6 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
match cond.Term.t_node with
- | Tapp
- ( { ls_name = { id_string = "equal_shape"; _ }; _ },
- [
- ({ t_node = Tapp (ls, _); _ } as _t1);
- ({ t_node = Tvar vs2; _ } as _t2);
- ] ) ->
- (* Fmt.pr "--@.equal_shape: %a %a@." Pretty.print_term t1 Pretty.print_term
- t2; *)
- if not (Term.vs_equal vs vs2)
- then None
- else
- let n =
- match caisar_op_of_ls engine ls with
- | Data (D_csv d) -> List.length d
- | _ -> assert false
- in
- let ty =
- match vs.vs_ty with
- | { ty_node = Tyapp (_, ty :: _); _ } -> ty
- | _ -> assert false
- in
- let new_quant =
- List.init n ~f:(fun _ ->
- let preid = Ident.id_fresh "caisar_t" in
- Term.create_vsymbol preid ty)
- in
- let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
- let substitutions =
- [ term_of_caisar_op ~args engine (Tensor n) (Some vs.vs_ty) ]
- in
- Some { new_quant; substitutions }
| Tapp
( { ls_name = { id_string = "has_length"; _ }; _ },
[
@@ -487,25 +381,6 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
[ term_of_caisar_op ~args engine caisar_op (Some vs.vs_ty) ]
in
Some { new_quant; substitutions }
- | Tapp
- ( { ls_name = { id_string = "valid_index"; _ }; _ },
- [
- ({ t_node = Tapp (ls, _); _ } as _t1);
- ({ t_node = Tvar vs2; _ } as _t2);
- ] ) -> (
- if not (Term.vs_equal vs vs2)
- then None
- else
- match caisar_op_of_ls engine ls with
- | Tensor n ->
- let new_quant = [] in
- let substitutions =
- List.init n ~f:(fun i ->
- term_of_caisar_op engine (Index (I_csv i)) (Some vs.vs_ty))
- in
- Some { new_quant; substitutions }
- | _ -> assert false
- | exception _ -> None)
| _ -> None
let interpret_task ~cwd env task =
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index ab3b2779686f518d50f8e11ab549bc9d6f8dafec..f5c850372124c3f764130401cef47b64b081c654 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -52,35 +52,18 @@ theory Vector
end
end
-theory Tensor
- use int.Int
- use Vector
-
- type tensor 'a
- type index = vector int
-
- function (#) (t: tensor 'a) (v: vector int) : 'a
- function (-) (t1: tensor 'a) (t2: tensor 'a) : tensor 'a
-
- predicate equal_shape (t1: tensor 'a) (t2: tensor 'b)
- predicate valid_index (t: tensor 'a) (v: index)
-end
-
theory Classifier
use Vector
- use Tensor
type classifier
type kind = ONNX | NNet | OVO
function read_classifier (f: string) (k: kind) : classifier
- function (@@) (c: classifier) (t: tensor 'a) : vector 'a
function (%%) (c: classifier) (v: vector 'a) : vector 'a
end
theory Dataset
use Vector
- use Tensor
type dataset 'a 'b = vector ('a, 'b)
type format = CSV