From f4848c3d97ac5c049edae30f96ea0c905204d9a0 Mon Sep 17 00:00:00 2001
From: Colin Eles <elesc@mcmaster.ca>
Date: Tue, 8 Mar 2011 17:42:58 +0000
Subject: [PATCH] latest update copies over files from pvs_theories

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@7026 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
---
 @GUI/pvs_ext_call_sim.m              |  2 +-
 @PVS_checker/generate_pvs_file.m     | 12 +++++++++++-
 @PVS_checker/pvs_check.m             | 10 ++++++++++
 @PVS_checker/pvs_check_for_imports.m |  2 +-
 4 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/@GUI/pvs_ext_call_sim.m b/@GUI/pvs_ext_call_sim.m
index e43d8ba..801a9e7 100644
--- a/@GUI/pvs_ext_call_sim.m
+++ b/@GUI/pvs_ext_call_sim.m
@@ -20,7 +20,7 @@ object.PVS.type_mode = 1;
 
 
 % copy pvs theory to pwd
-copyfile(fullfile(fileparts(which('TTdiag')),'PVS_theories','matlab_types.pvs'),pwd);
+copyfile(fullfile(fileparts(which('TTdiag')),'PVS_theories','*'),pwd);
 
 % inputs = regexp(object.Data.function_inputs,',','split');
 % for i=1:size(inputs,2)
diff --git a/@PVS_checker/generate_pvs_file.m b/@PVS_checker/generate_pvs_file.m
index ddfbba5..600d486 100644
--- a/@PVS_checker/generate_pvs_file.m
+++ b/@PVS_checker/generate_pvs_file.m
@@ -87,7 +87,17 @@ fileid = fopen([filename '.pvs'],'w');
 code = [];
 code = sprintf('%s:THEORY\nBEGIN\n',function_name);
 %code = [code sprintf('IMPORTING Funcs\n')];
-code = [code object.pvs_check_for_imports];
+imports = object.pvs_check_for_imports;
+if ~isempty(imports)
+    
+    if ~isempty(regexp(imports,'double|single', 'once'))
+        % flag to copy files
+        error = 2;
+    end
+end
+code = [code imports];
+
+
 
 code = [code object.user_imports];
 if object.type_mode
diff --git a/@PVS_checker/pvs_check.m b/@PVS_checker/pvs_check.m
index 7852872..f835410 100644
--- a/@PVS_checker/pvs_check.m
+++ b/@PVS_checker/pvs_check.m
@@ -16,11 +16,21 @@ output = [];
 
 function_names = EMLGenerator.parse_inputs(object.data.function_name);
 function_name = char(function_names{1}(1));
+
+
+
+
 error = object.generate_pvs_file(function_name);
 if error == 1
     return;
+elseif error == 2
+    % copy pvs files over.
+    copyfile(fullfile(fileparts(which('TTdiag')),'PVS_theories','*.*'),pwd);
+
 end
 
+
+
 object.pvs_version = PVS_checker.get_pvs_version;
 
 
diff --git a/@PVS_checker/pvs_check_for_imports.m b/@PVS_checker/pvs_check_for_imports.m
index 1d60f92..4320da3 100644
--- a/@PVS_checker/pvs_check_for_imports.m
+++ b/@PVS_checker/pvs_check_for_imports.m
@@ -24,7 +24,7 @@ function string = pvs_check_for_imports(object)
 
 
 
-hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}};
+hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'} {'double', 'double'} {'double_finite', 'double'} {'single' 'single'} {'single_finite' 'single'}} ;
 
 % check for imports in the results grid.
 for i=1:size(object.data.Grid0.Cells,2)
-- 
GitLab