diff --git a/@GUI/pvs_ext_call_sim.m b/@GUI/pvs_ext_call_sim.m index e43d8bac92c9a8c582e2d0a192b776fddb339780..801a9e7812a2c2fccc05730fa3192bbcedf18929 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 ddfbba5ef9c9d2f2f7851e322e6233d62b0e4815..600d486f1e690e14a349ca19fafa5bb1736cdc7c 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 7852872e26422b6c145842eb3f70cf80a2140273..f835410c267335b268998e53d31859845fe6845a 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 1d60f9270b04311841feb9d5978d5969d1e552d5..4320da3a5db2e3d87a122ec0b0d68089fbc51cfe 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)