From 51daaa182cdbb891b558cb3a5a576182cd415687 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 8 Mar 2023 17:04:22 +0100
Subject: [PATCH] [interpretation] Rename interpretation theory.
---
src/interpretation.ml | 4 ++--
stdlib/caisar.mlw | 2 +-
tests/interpretation.t | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index 80a0539..eb1cdc0 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -52,7 +52,7 @@ let term_of_caisar_op engine op =
Term.t_app_infer (ls_of_caisar_op engine op) []
let caisar_env env cwd =
- let th = Env.read_theory env [ "caisar" ] "Interpret" in
+ let th = Env.read_theory env [ "caisar" ] "Interpretation" in
let ts_dataset = Theory.ns_find_ts th.Theory.th_export [ "dataset" ] in
{
dataset_ty = Ty.ty_app ts_dataset [];
@@ -89,7 +89,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
in
[
( [ "caisar" ],
- "Interpret",
+ "Interpretation",
[],
[ ("open_dataset", None, open_dataset); ("size", None, size) ] );
]
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index e5c815a..13583bb 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -81,7 +81,7 @@ theory NN
function relu (a: t): t = if a .> (0.0:t) then a else (0.0:t)
end
-theory Interpret
+theory Interpretation
use bool.Bool
use int.Int
diff --git a/tests/interpretation.t b/tests/interpretation.t
index 364dbee..31dcd1a 100644
--- a/tests/interpretation.t
+++ b/tests/interpretation.t
@@ -1,7 +1,7 @@
Test interpret
$ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
- > use caisar.Interpret
+ > use caisar.Interpretation
> use int.Int
>
> goal G1: 1+1=2
--
GitLab