From 33e944d4a1b0336e30a7652018f88fa67087122a Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 26 Sep 2022 16:10:37 +0200
Subject: [PATCH] [stdlib] Rename theory to more precise name
DataSetClassification.
---
src/saver.ml | 4 +++-
stdlib/caisar.mlw | 2 +-
tests/simple_ovo.t | 3 +--
3 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/saver.ml b/src/saver.ml
index 2c563a4..243f156 100644
--- a/src/saver.ml
+++ b/src/saver.ml
@@ -32,7 +32,9 @@ type interpreted_task = {
}
let find_predicate_ls env p =
- let dataset_th = Pmodule.read_module env [ "caisar" ] "DataSet" in
+ let dataset_th =
+ Pmodule.read_module env [ "caisar" ] "DataSetClassification"
+ in
Theory.ns_find_ls dataset_th.mod_theory.th_export [ p ]
let interpret_predicate env ls =
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 7d02870..302a893 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -38,7 +38,7 @@ theory Model
function predict: model -> array t -> int
end
-theory DataSet
+theory DataSetClassification
use ieee_float.Float64
use int.Int
use array.Array
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index cd85182..df79cd4 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -30,8 +30,7 @@ Test verify
> use TestSVM.SVMasArray
> use ieee_float.Float64
> use int.Int
- > use array.Array
- > use caisar.DataSet
+ > use caisar.DataSetClassification
>
> goal G: robust svm_apply dataset (8.0:t)
> goal H: correct svm_apply dataset (8.0:t)
--
GitLab