classdef PVS_checker < handle
    % class contains all the functionality specific to the PVS theorem
    % prover
    
    properties
        gui = [];
        counter_examples = 10000;
        counter_size = 100;
    end
    
    methods
        
        %% constructor
        function obj = PVS_checker(gui_new)
            obj.gui = gui_new;
        end
        
        %% pvs_ext_call
        function [] = pvs_check(obj)
            % file name will be expression_name.m
            fileid = fopen([get(obj.gui.function_name_control,'String') '.pvs'],'w');
            code = [];
            code = sprintf('%s:THEORY\nBEGIN\n',get(obj.gui.function_name_control,'String'));
             
            code = [code obj.pvs_check_for_imports];
            
            % declare variables for each input
            
            %inputs = get(obj.gui.function_inputs_control,'String');
           %inputs = regexp(inputs,',','split');
                       parsed_inputs = obj.gui.parse_inputs(get(obj.gui.function_inputs_control,'string'))
                       
           % initialize inputs to zero
           % functions are assumed to be total, so 0 is just for 
           % convienence
           inputs_new = [];
           for i=1:size(parsed_inputs,2)
                % set to zero
                if(size(parsed_inputs{i},2) == 2)
                    code = [code sprintf('%s:VAR %s\n',char(parsed_inputs{i}(1)), char(parsed_inputs{i}(2)))];
                else
                    code = [code sprintf('%s:VAR real\n',char(parsed_inputs{i}(1)))];
                end
                
                inputs_new = [inputs_new char(parsed_inputs{i}(1))];
                if(i~=(size(parsed_inputs,2)))
                    inputs_new = [inputs_new ',']
                end
           end
           
           code = [code sprintf('%s(%s):real = \n',get(obj.gui.function_name_control,'String'),inputs_new)];
            code = [code obj.generate_pvs(obj.gui.Grid1,obj.gui.Grid2,0)];
            code = [code sprintf('\nEND %s',get(obj.gui.function_name_control,'String'))];
            fprintf(fileid,code);

            fclose(fileid);
            
            % generate the proof script
            obj.generate_pvs_script(get(obj.gui.function_name_control,'String'))
            
            % call pvs in batch mode with script
            % ADD check that pvs actually exists in system
            [status, result] = system(['pvs -batch -v 3 -l ' get(obj.gui.function_name_control,'String') '.el'])
            %object.msgbox_scroll(result);
            parsed = obj.parse_pvs_result(result);
            if (isempty(parsed))
                msgbox('table is valid')
            else
                Valid_Report = ValidationReport(obj.gui);
                Valid_Report.set_results(parsed);
                Valid_Report.init();
            end
        end
        
        %% parse_pvs_result
        function output = parse_pvs_result(obj,result)
            found = regexp(result,'\w+(?=[\.]{4,})|(?<=[\.]{4,})\w+','match')
            char(found)
            seqs = [];
            for i = 1:2:size(found,2)-1
                if(~strcmp(char(found(i+1)),'proved'))
                    found2 = []
                    found3 = []
                    found4 = []
                    
                    % find the TCC that was unprovable
                    search_str = sprintf('(?<=Proving formula %s[\\n]*)%s.*?(?=[ \\n]*Rerunning step)',char(found(i)),char(found(i)))
                    found2 = regexp(result,char(search_str),'match','once')
                    
                    
                    % find the counter examples
                    search_str = sprintf('(?<=%s.*?substitutions:).*?(?=This will undo the proof to: \\n%s)|(?<=%s.*?)No counter-examples(?=.*?%s)',char(found(i)),char(found(i)),char(found(i)),char(found(i)))
                    found3 = regexp(result,char(search_str),'match','once')
                    if (~strcmp(found3,'No counter-examples'))
                        found4 = regexp(found3,'[^\n]*(?===>)|(?<===>)[^\n]*','match')
                    end
                    seqs = [seqs struct('id', '1234a', 'TCC', found(i), 'seq', found2, 'ce', {found4})]
                end
              
            end
            output = seqs;
        end
        
              %% matlab_to_pvs_syntax_translation
        function pvs_string = matlab_to_pvs_syntax_translation(obj,matlab_string)
            pvs_string = regexprep(matlab_string,'&&',' AND ')
            pvs_string = regexprep(pvs_string,'~(?!=)',' NOT ')
            pvs_string = regexprep(pvs_string,'~=',' /= ')
            pvs_string = regexprep(pvs_string,'==',' = ')
            pvs_string = regexprep(pvs_string,'\|\|',' OR ')
            pvs_string = regexprep(pvs_string,'ceil','ceiling')
        end
        
        
        %% generate_pvs_horizontal
        function code = generate_pvs_horizontal(obj,g1,g2_cell,depth)

        code = [];

            code = [code sprintf('COND\n')];
            elsecell = [];
            for i=1:size(g1.cells,2)
                g1cond = get(g1.cells(i).cond,'String');
                % condition string of otherwise corresponds to an else
                % statement, we allow this statement to be in any order
                % in the cells of the grid, so we need to find where it
                % is, if it exists.
                if (strcmp(g1cond,'otherwise'))
                    elsecell = g1.cells(i);
                    found = 1;
                    continue
                end
                code = [code sprintf('%s->',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(g1.cells(i).cond,'String')))))];
                resultcell = obj.gui.Grid0.search_return(g1.cells(i),g2_cell);
                if(~isempty(resultcell))
                    code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]
                    
                    if(isempty(elsecell))
                        if(i~= size(g1.cells,2))
                            code = [code sprintf(',\n')];
                        else
                            code = [code sprintf('\n')];
                        end
                    else
                        code = [code sprintf(',\n')];
                    end
                else
                end
            end
            if(~isempty(elsecell))
                 resultcell = obj.gui.Grid0.search_return(elsecell,g2_cell);
                code = [code sprintf('ELSE->%s\n',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))))];

            end
            code = [code sprintf('ENDCOND')];

       
            
     
        end
        
        %% genereate_pvs
        function code = generate_pvs(obj,g1,g2,depth)
          g1cond1 = get(g1.cells(1).cond,'String');
          g2cond1 = get(g2.cells(1).cond,'String');
          code = [];
          %1D horizontal
          if(~isempty(g1cond1) && isempty(g2cond1))
            code = [code obj.generate_pvs_horizontal(g1,g2.cells(1),depth)];
          % something in vertical column
          else

            code = [code sprintf('COND\n')];
            elsecell = [];
            for i=1:size(g2.cells,2)
                g2cond = get(g2.cells(i).cond,'String');
                % condition string of otherwise corresponds to an else
                % statement, we allow this statement to be in any order
                % in the cells of the grid, so we need to find where it
                % is, if it exists.
                if (strcmp(g2cond,'otherwise'))
                    elsecell = g2.cells(i);
                    found = 1;
                    continue
                end
                code = [code sprintf('%s->',obj.matlab_to_pvs_syntax_translation(strtrim(char(get(g2.cells(i).cond,'String')))))];
                
                if(~isempty(g2.cells(i).subgrid))
                    code = [code obj.generate_pvs(g1,g2.cells(i).subgrid,depth)];
                else
                    if (~isempty(g1cond1))
                         code = [code obj.generate_pvs_horizontal(g1,g2.cells(i),depth)];
                    else    
                
                        resultcell = obj.gui.Grid0.search_return(g1.cells(1),g2.cells(i));
                        if(~isempty(resultcell))
                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String'))))]

                            
                        else
                        end
                    end
                end
                if(isempty(elsecell))
                    if(i~= size(g2.cells,2))
                        code = [code sprintf(',\n')];
                    else
                        code = [code sprintf('\n')];
                    end
                else
                    code = [code sprintf(',\n')];
                end

            
              
            end
           if(~isempty(elsecell))
                 %resultcell = obj.Grid0.search_return(elsecell,elsecell);
                code = [code sprintf('ELSE->')];

                if(~isempty(elsecell.subgrid))
                    code = [code obj.generate_pvs(g1,elsecell.subgrid,depth) sprintf('\n')];
                else
                    if (~isempty(g1cond1))
                         code = [code obj.generate_pvs_horizontal(g1,elsecell,depth) sprintf('\n')];
                    else    
                
                        resultcell = obj.gui.Grid0.search_return(g1.cells(1),elsecell);
                        if(~isempty(resultcell))
                            code = [code obj.matlab_to_pvs_syntax_translation(strtrim(char(get(resultcell.result,'String')))) sprintf('\n')]

                            
                             
                     
                        end
                    end
                end
                
           end

         code = [code sprintf('ENDCOND')];
         
            
            
            
          end
          code
        end
        
        %% pvs_check_for_imports
        function string = pvs_check_for_imports(obj)
            [string,found] = obj.pvs_check_for_imports_g(obj.gui.Grid2,{});
            [string2,found2] = obj.pvs_check_for_imports_g(obj.gui.Grid1,found)
            string = [string string2];
        end
        
        %% pvs_check_for_imports
        function [string,found] = pvs_check_for_imports_g(obj,grid,found)
            string = [];
            for i=1:size(grid.cells,2)
                % recurse through
                if (~isempty(grid.cells(i).subgrid))
                    string = [string obj.pvs_check_for_imports_g(grid.cells(i).subgrid)];
                end
                text = char(get(grid.cells(i).cond,'String'));
                
                vars = regexp(text,'([a-zA-Z][a-zA-Z0-9_]*)','match')
                
                for j=1:size(vars,2)
                   if(exist(vars{j},'file')==2 && ~strcmp(vars{j},'otherwise'))
                       %check if already imported file
                       if (~any(ismember(found,vars{j})))
                            string = [string 'IMPORTING ' vars{j} sprintf('\n')];
                            found = [found vars{j}]
                       end
                   end
                end
            end
        end
        
        %% pvs_check_for_imports
        function [] = pvs_check_for_imports_rg(obj)
      
        end
        
        %% generate_pvs_script
        function [] = generate_pvs_script(obj,filename)
            fileid = fopen([filename '.el'],'w');
            code = ['(prove-tccs-pvs-file "' filename '" "(try (try (tcc) (try (assert) (skip) (fail) ) (fail))(skip) (random-test :count ' sprintf('%ld',obj.counter_examples) ' :size ' sprintf('%d',obj.counter_size) '))"  )' sprintf('\n')]

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