Commit 579ec4a7 authored by Colin Eles's avatar Colin Eles
Browse files

latest update to table tool 


git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6058 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 372b2cae

@GUI/pvs_ext_call.m

+2 −1
Original line number Diff line number Diff line
@@ -9,7 +9,8 @@ 
        function [] = pvs_ext_call(object,src,event)

            object.save_data;

            error = object.check_call;

            

            object.PVS.output_type = object.output_data_type;

            object.PVS.input_type = object.input_data_type;

            if (~error)

                [check,result] = object.PVS.pvs_check;

                if (check == 1)

@PVS_checker/PVS_checker.m

+4 −2
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ classdef PVS_checker < handle 
        

        default_type = 'real';

        pvs_version = [];

        

        output_type = [];

        input_type = [];

        data = [];

        mode = []; % 0 - graphical, 1 - command

    end
@@ -25,6 +26,7 @@ classdef PVS_checker < handle 
        

        [paren_string, new_pos] = parse_paren(string,pos)

        

        matlab_type = matlab_type_to_pvs_type( pvs_type )



        

        version = get_pvs_version

@PVS_checker/generate_pvs_file.m

+21 −3
Original line number Diff line number Diff line
@@ -9,15 +9,18 @@ 
        % outputs;

        %   none

        function [] = generate_pvs_file(object,filename)

        type_mode = 1;

            fileid = fopen([filename '.pvs'],'w');

            code = [];

            code = sprintf('%s:THEORY\nBEGIN\n',object.data.function_name);

             

            code = [code sprintf('IMPORTING Funcs\n')];

            code = [code object.pvs_check_for_imports];

            

            code = [code object.user_imports];

            % declare variables for each input

            

            

            if type_mode == 0

            %inputs = get(object.gui.function_inputs_control,'String');

           %inputs = regexp(inputs,',','split');

                       parsed_inputs = EMLGenerator.parse_inputs(object.data.function_inputs);
@@ -38,8 +41,23 @@ 
                    inputs_new = [inputs_new ','];

                end

           end

              code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];



            else

                inputs_new = [];

           for i=1:size(object.input_type,2)

               

        

                   inputs_new = [inputs_new char(object.input_type(i,1)) ':' PVS_checker.matlab_type_to_pvs_type(char(object.input_type(i,2)))];

                

                if(i~=(size(object.input_type,2)))

                    inputs_new = [inputs_new ','];

                end

           end

              code = [code sprintf('%s(%s):real = \n',object.data.function_name,inputs_new)];



                

            end

            code = [code object.generate_pvs(object.data.Grid1,object.data.Grid2,0)];

            code = [code sprintf('\nEND %s',object.data.function_name)];

            fprintf(fileid,code);

@PVS_checker/matlab_type_to_pvs_type.m

0 → 100644
+23 −0
Original line number Diff line number Diff line 
function matlab_type = matlab_type_to_pvs_type( pvs_type )

    if(strcmp(pvs_type,'logical'))

        matlab_type = 'bool';

    elseif (strncmp(pvs_type, 'int',3))

        matlab_type = pvs_type;

    elseif (strncmp(pvs_type, 'uint', 4))

        matlab_type = pvs_type;

    elseif (strcmp(pvs_type,'single') || strcmp(pvs_type,'double'))

        matlab_type = 'real';

    elseif (strncmp(pvs_type,'Inherit',7))

        matlab_type = 'real';

    elseif (strncmp(pvs_type,'fixdt',5))

        params = regexp(pvs_type,'(?<=\().*(?=\))','match');

        split_params = regexp(params,',','split');

        matlab_type = sprintf('fp[%d,%d,%d]',eval(char(split_params{1}(2))),eval(char(split_params{1}(2)))-eval(char(split_params{1}(3)))-eval(char(split_params{1}(1))),eval(char(split_params{1}(1))));

    else

        matlab_type = 'error';

    end   







end