Commit f4848c3d authored by Colin Eles's avatar Colin Eles
Browse files

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
parent 5518b07d

@GUI/pvs_ext_call_sim.m

+1 −1
Original line number Diff line number Diff line
@@ -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)

@PVS_checker/generate_pvs_file.m

+11 −1
Original line number Diff line number Diff line
@@ -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

@PVS_checker/pvs_check.m

+10 −0
Original line number Diff line number Diff line
@@ -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;

@PVS_checker/pvs_check_for_imports.m

+1 −1
Original line number Diff line number Diff line
@@ -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)