vastly improved proof management in system, user can check an existing proof... (dd867073) · Commits · Abdulrahman elgendy / tet

GUI.m

+70 −2

Original line number	Diff line number	Diff line
		@@ -222,7 +222,7 @@ classdef GUI < handle
		uimenu(editmenu,'Label','Ports and Data Manager','Accelerator','p','Callback',@(src,event)input_call(obj,src,event));
		uimenu(pvsmenu,'Label','Typecheck','Accelerator','t','Callback',@(src,event)pvs_ext_call(obj,src,event));
		uimenu(pvsmenu,'Label','PVS Settings','Callback',@(src,event)settings_call(obj,src,event));

		uimenu(pvsmenu,'Label','Check Status','Callback',@(src,event)prf_file_call(obj,src,event))



		@@ -256,7 +256,7 @@ classdef GUI < handle




		%%
		function [] = update_Statusbar(object)

		warning off MATLAB:HandleGraphics:ObsoletedProperty:JavaFrame
		@@ -276,10 +276,78 @@ classdef GUI < handle
		end
		end

		%%
		function [] = new_call(object,src,event)
		TableToolMatlab
		end

		%%
		function [] = prf_file_call(object,src,event)
		object.save_data;
		% check if a pvs file exists
		if (~exist([object.Data.function_name '.pvs'],'file'))
		errordlg(['PVS theory file for this function does not exist' sprintf('\n') 'Nothing to check']);
		return;
		end
		% check if prf file exists
		if (~exist([object.Data.function_name '.prf'],'file'))
		errordlg(['PVS proof (.prf) file for this function does not exist' sprintf('\n') 'Nothing to check']);
		return;
		end
		% check if pvs file is different from current table
		temp_pvs = [object.Data.function_name '_temp'];
		object.PVS.generate_pvs_file(temp_pvs);

		% read pvs theory on file
		pvs1 = textread([object.Data.function_name '.pvs'], '%s', 'whitespace', '', 'bufsize', 268435456);
		pvs2 = textread([temp_pvs '.pvs'], '%s', 'whitespace', '', 'bufsize', 268435456);

		if(size(pvs1{1},2) ~= size(pvs2{1},2))
		errordlg(['pvs-theory file is different from the given graphical representation, ' sprintf('\n') ' you will need to reprove']);
		return;
		else

		if ~all(pvs1{1} == pvs2{1})
		errordlg(['pvs-theory file is different from the given graphical representation, ' sprintf('\n') ' you will need to reprove']);
		return;
		end


		end
		delete([temp_pvs '.pvs']);




		status = object.PVS.check_status;
		if (status ~= object.pvs_checked)

		object.pvs_checked = status;
		object.update_Statusbar;
		if (object.mode == 1)
		TableBlock.set_block_display(object.block_handle,object.pvs_checked)
		end

		end

		if (status == 1)
		msgbox('Table has been proven');
		else
		msgbox('Table has not been proven');
		end
		% [FileName, PathName, FilterIndex] = uigetfile('*.prf','Select prf file');
		% if ~isempty(FileName)
		% data = textread([PathName FileName], '%s', 'whitespace', '', 'bufsize', 268435456);
		% %data_one = regexprep(data,'\n','');
		% string = data{1};
		% [theory_name, decls] = PVS_checker.parse_prf_file(string);
		%
		%
		%
		% end
		end

		%%
		function [] = open_call(object,src,event)
		[FileName, PathName, FilterIndex] = uigetfile('*.table','Select pvs files');
		if ~isempty(FileName)

PVS_checker.m

+99 −29

Original line number	Diff line number	Diff line
		@@ -15,11 +15,9 @@ classdef PVS_checker < handle

		methods(Static)

		function [theory_id, decls] = parse_prf_file()
		function [theory_id, decls] = parse_prf_file(string)
		decls = [];
		data = textread('Held_For.prf', '%s', 'whitespace', '', 'bufsize', 100000000);
		%data_one = regexprep(data,'\n','');
		string = data{1};

		if string(1) ~= '('
		msgbox('error reading file')
		end
		@@ -255,12 +253,9 @@ classdef PVS_checker < handle
		obj.data = data;
		end

		%% pvs_ext_call
		function [check,output] = pvs_check(obj)
		check = 0;
		output = [];
		% file name will be expression_name.m
		fileid = fopen([obj.data.function_name '.pvs'],'w');

		function [] = generate_pvs_file(obj,filename)
		fileid = fopen([filename '.pvs'],'w');
		code = [];
		code = sprintf('%s:THEORY\nBEGIN\n',obj.data.function_name);

		@@ -300,21 +295,51 @@ classdef PVS_checker < handle

		fclose(fileid);

		% generate the proof script
		obj.generate_pvs_script(obj.data.function_name)
		end

		%% pvs_ext_call
		function [check,output] = pvs_check(obj)
		check = 0;
		output = [];
		% file name will be expression_name.m
		obj.generate_pvs_file(obj.data.function_name);




		% THIS SECTION NEEDS SOME WORK
		%-------------
		% delete the existing proof

		exists = 0;
		button = '';
		if (exist([obj.data.function_name '.prf'],'file'))
		exists = 1;
		button = questdlg(['A proof file already exists for this function ' sprintf('\n') ' What would you like to do' sprintf('\n') 'Note: Attempting to prove will delete existing prf file'],'prf exists','Attempt to prove','Open PVS','Cancel','Cancel')
		end

		if (exists == 1 && (isempty(button) \|\| strcmp(button,'Cancel')))
		% do nothing
		elseif (exists == 1 && (strcmp(button,'Open PVS')));
		[status, result] = system(['pvs ' obj.data.function_name '.pvs']);
		elseif (exists == 0 \|\| strcmp(button,'Attempt to prove'))
		box = waitbar(0,'Generating Proof Script')


		delete([obj.data.function_name '.prf'])


		% generate the proof script
		obj.generate_pvs_script(obj.data.function_name)
		waitbar(.10,box,'Running Proof')
		%---------
		% call pvs in batch mode with script
		% ADD check that pvs actually exists in system
		[status, result] = system(['pvs -batch -v 3 -l ' obj.data.function_name '.el'])
		%object.msgbox_scroll(result);
		waitbar(.70,box,'Parsing Results')
		[parsed error] = obj.parse_pvs_result(result);

		if (error == 1)
		msgbox(result);
		else
		@@ -329,6 +354,12 @@ classdef PVS_checker < handle
		%Valid_Report.init();
		end
		end
		waitbar(.100,box,'Deleting Proof Script')

		delete([obj.data.function_name '.el']);

		delete(box);
		end
		end


		@@ -566,6 +597,8 @@ classdef PVS_checker < handle





		%% pvs_check_for_imports
		function [] = pvs_check_for_imports_rg(obj)

		@@ -580,6 +613,43 @@ classdef PVS_checker < handle
		fclose(fileid);
		end

		%% generate_pvs_script
		function [script_name] = generate_pvs_status_script(obj,filename)
		script_name = [filename '_status' '.el'];
		fileid = fopen(script_name,'w');
		code = ['(status-proof-pvs-file "' filename '")'];

		fprintf(fileid,code);
		fclose(fileid);
		end

		%%
		function status = check_status(obj)
		script_name = obj.generate_pvs_status_script(obj.data.function_name);
		[status, result] = system(['pvs -batch -v 3 -l ' script_name])
		parsed = obj.parse_status(result);
		pass = 1;
		if (size(parsed,2) == 0)
		pass = 0;
		end
		for i=1:2:size(parsed,2)-1
		if ~strncmp(parsed(i+1),'proved',6)
		pass = 0;
		end
		end

		status = pass;
		delete(script_name);

		end

		%%
		function [parsed] = parse_status(obj,string)
		thrms_status = regexp(string,'\w+(?=[\.]{4,})\|(?<=[\.]{4,})\w+','match');
		parsed = thrms_status;

		end

		end

		end