| 1 | % (c) 2016-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(latex_processor, [ process_latex_file/2 | |
| 6 | ]). | |
| 7 | ||
| 8 | ||
| 9 | :- use_module(probsrc(module_information)). | |
| 10 | :- module_info(group,visualization). | |
| 11 | :- module_info(description,'This module processes Latex Files for ProB commands.'). | |
| 12 | ||
| 13 | ||
| 14 | :- use_module(probsrc(debug)). | |
| 15 | :- use_module(probsrc(translate)). | |
| 16 | :- use_module(probsrc(error_manager)). | |
| 17 | :- use_module(probsrc(preferences)). | |
| 18 | :- use_module(probsrc(tools_io), [with_open_stream_to_codes/4]). | |
| 19 | :- use_module(library(lists)). | |
| 20 | ||
| 21 | :- set_prolog_flag(double_quotes, codes). | |
| 22 | ||
| 23 | process_latex_file(FileIn,FileOut) :- | |
| 24 | reset_latex_processor_errors, | |
| 25 | temporary_set_preference(repl_cache_parsing,true,CHNG), | |
| 26 | get_preference(latex_encoding,EncodingPref), | |
| 27 | (EncodingPref=auto | |
| 28 | -> open(FileIn,read,StreamIn), | |
| 29 | stream_property(StreamIn,encoding(Encoding)) | |
| 30 | ; open(FileIn,read,StreamIn,[encoding(EncodingPref)]), | |
| 31 | Encoding = EncodingPref | |
| 32 | ), | |
| 33 | %stream_property(StreamIn,encoding_signature(BOM)), | |
| 34 | debug_println(19,encoding(Encoding,FileIn)), | |
| 35 | open(FileOut,write,StreamOut,[encoding(Encoding)]), % use same encoding | |
| 36 | update_latex_output_file(FileOut), | |
| 37 | call_cleanup(process_lines_loop(1,StreamIn,StreamOut), | |
| 38 | (close_stream(StreamIn), | |
| 39 | close_stream(StreamOut), | |
| 40 | reset_temporary_preference(repl_cache_parsing,CHNG), | |
| 41 | latex_processor_errors(Errors), | |
| 42 | (Errors > 0 -> format(user_error,'~w error(s) occurred while processing ~w~n',[Errors,FileIn]), | |
| 43 | add_error(latex_processor,'Latex Processor Errors: ',Errors) | |
| 44 | ; true) | |
| 45 | )), | |
| 46 | !. | |
| 47 | process_latex_file(FileIn,_FileOut) :- add_error(process_latex_file,'Processing failed: ',FileIn). | |
| 48 | ||
| 49 | process_lines_loop(Nr,Stream,StreamOut) :- | |
| 50 | catch(read_line(Stream,Line), E, ( | |
| 51 | add_latex_processor_error('Exception reading line: ',Nr:E), | |
| 52 | Line=end_of_file | |
| 53 | )), | |
| 54 | (Line = end_of_file -> true | |
| 55 | ; %format("Read line ~w : ~s~n",[Nr,Line]), | |
| 56 | (process_line(StreamOut,Nr,Line,[]) -> true | |
| 57 | ; add_latex_processor_error('Processing of line failed: ',Nr), | |
| 58 | format(StreamOut,'ERROR\\marginpar{ProB Error on line ~w} ',[Nr]) | |
| 59 | ), | |
| 60 | nl(StreamOut), | |
| 61 | N1 is Nr+1, | |
| 62 | !, | |
| 63 | process_lines_loop(N1,Stream,StreamOut)). | |
| 64 | ||
| 65 | :- use_module(probsrc(eval_strings), | |
| 66 | [eval_codes/6, eval_expression_codes/7, set_eval_dot_file/1, unset_eval_dot_file/0]). | |
| 67 | :- use_module(probsrc(system_call),[system_call/5]). | |
| 68 | :- use_module(probsrc(bsyntaxtree),[is_set_type/2]). | |
| 69 | :- use_module(probsrc(translate),[translate_bexpression/2]). | |
| 70 | ||
| 71 | eval_codes_success(LineNr,Codes,OuterQuantifier,StringResult,EnumWarning,LocalState) :- | |
| 72 | eval_codes(Codes,OuterQuantifier,StringResult,EnumWarning,LocalState,TypeInfo), | |
| 73 | debug:debug_println(5,eval_codes_output(LineNr,StringResult,TypeInfo)), | |
| 74 | (error_code(TypeInfo) -> | |
| 75 | add_latex_processor_error('ProB Evaluation returned error code: ',TypeInfo), | |
| 76 | fail | |
| 77 | ; string_result_unknown(StringResult) -> | |
| 78 | add_latex_processor_error('ProB Evaluation result unknown on line: ',LineNr), | |
| 79 | fail | |
| 80 | ; true), | |
| 81 | !. | |
| 82 | eval_codes_success(LineNr,_Codes,_,StringResult,EnumWarning,LocalState) :- | |
| 83 | add_warning(process_latex_file,'ProB Evaluation failed on line: ',LineNr), | |
| 84 | StringResult = 'FAIL', LocalState = [], EnumWarning=false. | |
| 85 | ||
| 86 | eval_expression_codes_success(Codes,StringResult,EnumWarning,LocalState,Typed) :- | |
| 87 | eval_expression_codes(Codes,StringResult,EnumWarning,LocalState,Typed,TypeInfo,[]), | |
| 88 | debug:debug_println(4,output_expr(TypeInfo)), | |
| 89 | \+ error_code(TypeInfo). | |
| 90 | ||
| 91 | string_result_unknown('UNKNOWN'). | |
| 92 | string_result_unknown('NOT-WELL-DEFINED'). | |
| 93 | ||
| 94 | error_code(error). | |
| 95 | error_code(syntax_error). | |
| 96 | ||
| 97 | string_result_false_or_unknown('UNKNOWN'). | |
| 98 | string_result_false_or_unknown('NOT-WELL-DEFINED'). | |
| 99 | string_result_false_or_unknown('FALSE'). | |
| 100 | string_result_false_or_unknown('FAIL'). | |
| 101 | ||
| 102 | write_string_result(Stream,Args,StringResult) :- | |
| 103 | write_optional_leadsto(Stream,Args), | |
| 104 | write_stream(Stream,StringResult). | |
| 105 | ||
| 106 | write_optional_leadsto(Stream,Args) :- | |
| 107 | (member("print",Args) | |
| 108 | -> (member("ascii",Args) -> write(Stream,' == ') ; write(Stream,' \\leadsto ')) | |
| 109 | ; true). | |
| 110 | ||
| 111 | :- use_module(extrasrc(bvisual2), | |
| 112 | [set_bvisual2_translation_mode/1, bvisual2_translation_mode/1]). % in case external functions FORMULA_INFOS,... called | |
| 113 | ||
| 114 | % TO DO: maybe process other comments (\begin{comment}...\end{comment}); but then we need multi-line processing | |
| 115 | % TO DO: \probinclude{FILE} include file with processing; allows to reuse code multiple times; e.g, when drawing diagrams a la BMS in Latex | |
| 116 | % TO DO: \probprolog{Stream}{PrologCodeUsingStream} ?? very dangerous | |
| 117 | process_line(Stream,_) --> "%",!, ignore_rest(R), {format_stream(Stream,"%~s",[R])}. | |
| 118 | process_line(Stream,LineNr) --> prob_command(LineNr,CMD,Codes,Args),!, | |
| 119 | {filter_preferences(Args,TempPrefs,RealArgs,LineNr)}, | |
| 120 | process_command_with_catch(CMD,Codes,RealArgs,Stream,LineNr), | |
| 121 | !, | |
| 122 | {maplist(reset_preference,TempPrefs)}, % reset to old values | |
| 123 | process_line(Stream,LineNr). | |
| 124 | process_line(Stream,LineNr) --> [Code],!, {put_code(Stream,Code)}, process_line(Stream,LineNr). | |
| 125 | process_line(_Stream,_) --> []. % do not generate newline, processline also used for single lines in \probdot | |
| 126 | ||
| 127 | % detect set-pref commands: | |
| 128 | filter_preferences([],[],[],_). | |
| 129 | filter_preferences(["set-pref",P,Val|T],[pref(Pref,CHNG)|PT],Args,LineNr) :- | |
| 130 | atom_codes(PA,P), | |
| 131 | (preference_description(PA,_Desc) -> Pref=PA | |
| 132 | ; eclipse_preference(PA,Pref),preference_description(Pref,_Desc) | |
| 133 | ; tools:ajoin(['Unknown preference for set-pref argument on line ',LineNr,': '],Msg), | |
| 134 | add_latex_processor_error(Msg,PA), | |
| 135 | fail), | |
| 136 | atom_codes(NewValueAtom,Val), | |
| 137 | temporary_set_preference(Pref,NewValueAtom,CHNG),!, | |
| 138 | print(set_pref(Pref,NewValueAtom)),nl, | |
| 139 | filter_preferences(T,PT,Args,LineNr). | |
| 140 | filter_preferences([H|T],P,[H|AT],LineNr) :- filter_preferences(T,P,AT,LineNr). | |
| 141 | ||
| 142 | reset_preference(pref(PA,CHNG)) :- reset_temporary_preference(PA,CHNG). | |
| 143 | ||
| 144 | process_command_with_catch(CMD,Codes,Args,Stream,LineNr,In,Out) :- | |
| 145 | catch( | |
| 146 | process_command(CMD,Codes,Args,Stream,LineNr,In,Out), | |
| 147 | E, | |
| 148 | (tools:ajoin(['Exception for ProB command ',CMD,' on line ',LineNr,': '],Msg), | |
| 149 | add_latex_processor_error(Msg,E), | |
| 150 | format(Stream,' ProB Exception on line ~w ',[LineNr]), | |
| 151 | In=Out)), | |
| 152 | !. | |
| 153 | process_command_with_catch(CMD,_Codes,_Args,Stream,LineNr,In,Out) :- | |
| 154 | tools:ajoin(['Failed to execute ProB command on line ',LineNr,': '],Msg), | |
| 155 | add_latex_processor_error(Msg,CMD), | |
| 156 | format(Stream,' ProB Failure on line ~w ',[LineNr]), | |
| 157 | In=Out. | |
| 158 | ||
| 159 | :- dynamic latex_processor_errors/1. | |
| 160 | latex_processor_errors(0). | |
| 161 | reset_latex_processor_errors :- retractall(latex_processor_errors(_)), assertz(latex_processor_errors(0)). | |
| 162 | add_latex_processor_error(Msg,E) :- | |
| 163 | add_error(latex_processor,Msg,E), | |
| 164 | retract(latex_processor_errors(N)), N1 is N+1, % we need to count as eval_strings/REPL will reset error manager ! | |
| 165 | assertz(latex_processor_errors(N1)). | |
| 166 | ||
| 167 | :- use_module(probsrc(system_call), [system_call/5]). | |
| 168 | :- use_module(extrasrc(table_tools),[print_value_as_table/4]). | |
| 169 | ||
| 170 | % process commands: | |
| 171 | process_command(system,Codes,Args,Stream,LineNr) --> | |
| 172 | !, | |
| 173 | {atom_codes(Cmd,Codes), | |
| 174 | maplist(codes_to_arg,Args,CmdArgs), | |
| 175 | format_stream(Stream,'>>> ~w ~w~n',[Cmd,CmdArgs]), | |
| 176 | system_call(Cmd,CmdArgs,Text,ErrorTextAsCodeList,JExit), | |
| 177 | format_stream(Stream,'~s~n',[Text]), | |
| 178 | (ErrorTextAsCodeList=[] -> true ; | |
| 179 | add_latex_processor_error('Error executing command on line: ',LineNr)), | |
| 180 | (JExit=exit(0) -> true ; | |
| 181 | add_latex_processor_error('Error return code executing command on line: ',LineNr:JExit))}. | |
| 182 | process_command(let,Codes,[Expr|Args],Stream,LineNr) --> % \problet calls \probrepl with print option and prints let id = ... | |
| 183 | !, | |
| 184 | { atom_codes(ID,Codes), | |
| 185 | %(member("ascii",Args) -> set_bvisual2_translation_mode(ascii) ; set_latex_mode,set_bvisual2_translation_mode(latex)), | |
| 186 | translate:translate_bexpression(b(identifier(ID),any,[]),IDS), | |
| 187 | format_stream(Stream,'let\\ ~w = ',[IDS]), | |
| 188 | append(["let ",Codes," = ",Expr],NewCodes)}, | |
| 189 | process_command(repl,NewCodes,["print"|Args],Stream,LineNr). | |
| 190 | process_command(repl,Codes,Args,Stream,LineNr) --> % \probrepl | |
| 191 | { dformat(user_output,"executing ProB REPL command on line ~w: ~s (~w)~n",[LineNr,Codes,Args]), | |
| 192 | setup_prefs_for_command(Args,CHNG), | |
| 193 | call_cleanup((get_preference(expand_avl_upto,Max), | |
| 194 | set_preference(expand_avl_upto,-1), % means no limit | |
| 195 | eval_codes_success(LineNr,Codes,exists,StringResult,_EnumWarning,LocalState), | |
| 196 | (member("print",Args) -> | |
| 197 | eval_strings:last_expression(_,TypedExpr), | |
| 198 | print_expr(Stream,TypedExpr,Args) | |
| 199 | ; true), | |
| 200 | (member("silent",Args) -> true | |
| 201 | ; string_result_false_or_unknown(StringResult) -> write_string_result(Stream,Args,StringResult) | |
| 202 | ; member("solution",Args) -> write_solution(Stream,Args,LocalState) | |
| 203 | ; write_string_result(Stream,Args,StringResult))), | |
| 204 | reset_prefs_for_command(Args,CHNG)), | |
| 205 | set_preference(expand_avl_upto,Max), | |
| 206 | ((member("check-true",Args), StringResult \== 'TRUE') | |
| 207 | -> tools:ajoin(['Result not TRUE on line ',LineNr,': '],Msg), | |
| 208 | add_latex_processor_error(Msg,StringResult) | |
| 209 | ; true), | |
| 210 | (member("store",Args), | |
| 211 | (LocalState = [] -> add_latex_processor_error('No bindings to store on line: ',LineNr) ; true), | |
| 212 | member(bind(ID,IDValue),LocalState), | |
| 213 | (kernel_objects:infer_value_type(IDValue,IDType) -> true ; IDType=any), | |
| 214 | store_let_value(ID,IDType,IDValue),fail | |
| 215 | ; true), | |
| 216 | print_last_eval_time(Stream,Args) | |
| 217 | }. | |
| 218 | process_command(requires,Codes,_Args,_Stream,LineNr) --> % \probrequires | |
| 219 | !, | |
| 220 | { version:version_str(CurVersion), | |
| 221 | split_chars(Codes,".",VCNrs), | |
| 222 | maplist(codes_to_number,VCNrs,VNrs), | |
| 223 | dformat(user_output,"checking ProB version on line ~w: ~w (against ~w)~n",[LineNr,VNrs,CurVersion]), | |
| 224 | version:compare_against_current_version(VNrs,CompareResult), | |
| 225 | (CompareResult = current_older | |
| 226 | -> add_latex_processor_error('Version of probcli is older than requested: ',CurVersion) | |
| 227 | ; CompareResult = current_newer -> format(user_output,"~n*** ProB version newer than required on line ~w: ~s (against ~w)~n~n",[LineNr,Codes,CurVersion]) | |
| 228 | ; true)}. | |
| 229 | ||
| 230 | process_command(print,Codes,Args,Stream,LineNr) --> % \probprint | |
| 231 | !, | |
| 232 | { dformat(user_output,"pretty-printing ProB expression on line ~w: ~s (~w)~n",[LineNr,Codes,Args]), | |
| 233 | setup_prefs_for_command(Args,CHNG), | |
| 234 | call_cleanup(((member("pred",Args) ->eval_strings:repl_parse_predicate(Codes,exists,TypedExpr,_) | |
| 235 | ; member("expr",Args) -> eval_strings:repl_parse_expression(Codes,TypedExpr,_,_) | |
| 236 | ; member("subst",Args) -> eval_strings:repl_parse_substitution(Codes,TypedExpr) | |
| 237 | ; eval_strings:repl_parse_expression(Codes,TypedExpr,_,_) -> true | |
| 238 | ; eval_strings:repl_parse_predicate(Codes,exists,TypedExpr,_) | |
| 239 | ), | |
| 240 | print_expr(Stream,TypedExpr,Args) | |
| 241 | ), | |
| 242 | reset_prefs_for_command(Args,CHNG)) | |
| 243 | }. | |
| 244 | process_command(expr,Codes,Args,Stream,LineNr) --> | |
| 245 | !, | |
| 246 | { dformat(user_output,"evaluating ProB expression on line ~w: ~s (~w)~n",[LineNr,Codes,Args]), | |
| 247 | setup_prefs_for_command(Args,CHNG), | |
| 248 | call_cleanup((get_preference(expand_avl_upto,Max), | |
| 249 | set_preference(expand_avl_upto,-1), % means no limit | |
| 250 | eval_expression_codes_success(Codes,StringResult,_EnumWarning,_LocalState,Typed), | |
| 251 | translate_bexpression(Typed,PS), | |
| 252 | %tools:print_bt_message(trans(PS)), | |
| 253 | (member("value",Args) -> true % we only print value | |
| 254 | ; member("silent",Args) -> true % we only print value | |
| 255 | ; write_stream(Stream,PS), write_stream(Stream,' = ')), | |
| 256 | ((member("string",Args),eval_strings:get_last_result_value(_,string,string(Value))) | |
| 257 | -> write_stream(Stream,Value) % remove string quotes | |
| 258 | ; write_stream(Stream,StringResult)) | |
| 259 | ), | |
| 260 | reset_prefs_for_command(Args,CHNG)), | |
| 261 | print_last_eval_time(Stream,Args), | |
| 262 | set_preference(expand_avl_upto,Max)}. | |
| 263 | process_command(table,Codes,Args,Stream,LineNr) --> | |
| 264 | % options for \probtable : no-tabular, no-hline, no-headings, no-row-numbers, max-table-size=NR | |
| 265 | !, | |
| 266 | { dformat(user_output,"evaluating ProB expression as table on line ~w: ~s (~w)~n",[LineNr,Codes,Args]), | |
| 267 | set_latex_mode, | |
| 268 | call_cleanup( (eval_codes_success(LineNr,Codes,exists,_StringResult,_EnumWarning,_LocalState), | |
| 269 | eval_strings:get_last_result_value(Expr,_,Value), | |
| 270 | maplist(codes_to_arg,Args,Options), | |
| 271 | print_value_as_table(Stream,Expr,Value,[latex|Options])), | |
| 272 | unset_latex_mode) | |
| 273 | }. | |
| 274 | process_command(dotcmd,Codes,Args,_Stream,LineNr) --> % probdotcmd: call ProB Dot generation command such as state_space, signature_merge, dfa_merge, state_as_graph, invariant, properties, ... | |
| 275 | {atom_codes(Cmd,Codes), process_dot_command(Cmd,Args,LineNr)}. | |
| 276 | process_command(dot,Codes,Args,_Stream,LineNr) --> | |
| 277 | { dformat(user_output,"evaluating ProB expression or predicate as dot on line ~w: ~s (~w)~n",[LineNr,Codes,Args]), | |
| 278 | atom_codes(Atom,Codes), | |
| 279 | (Args = [FileCodes|T] | |
| 280 | -> % process Filename in case \probexpr used there; tell used to re-direct any normal print,... away from FCStream | |
| 281 | with_open_stream_to_codes(process_line(FCStream,LineNr,FileCodes,[]), | |
| 282 | FCStream,NewFileCodes,[]), | |
| 283 | atom_codes(File,NewFileCodes), %tcltk_interface:tcltk_show_expression_as_dot(Atom,File), | |
| 284 | expand_file_relativ_to_latex_file(File,EFile), | |
| 285 | set_eval_dot_file(EFile), | |
| 286 | call_cleanup(eval_codes_success(LineNr,Codes,exists,_StringResult,_EnumWarning,_LocalState), | |
| 287 | unset_eval_dot_file), | |
| 288 | % we could call dotsrc(state_as_dot_graph):print_cstate_graph(_LocalState,File) | |
| 289 | (T= [PDF_Codes|RestArgs] -> | |
| 290 | % also process PDF_Codes: in case \probexpr used | |
| 291 | with_open_stream_to_codes(process_line(FCStream2,LineNr,PDF_Codes,[]), | |
| 292 | FCStream2,NewPDF_Codes,[]), | |
| 293 | dformat(user_output,' ~s ==> ~s ~n',[PDF_Codes,NewPDF_Codes]), | |
| 294 | atom_codes(PDFFile,NewPDF_Codes), | |
| 295 | expand_file_relativ_to_latex_file(PDFFile,EPDFFile), | |
| 296 | gen_pdf(EFile,RestArgs,EPDFFile) | |
| 297 | ; true % user will have to generate PDF in Makefile | |
| 298 | ) | |
| 299 | ; add_latex_processor_error('No file provided for probdot and expression: ',Atom) | |
| 300 | ) | |
| 301 | }. | |
| 302 | process_command(if,TestC,Args,Stream,LineNr) --> | |
| 303 | { dformat(user_output,"evaluating ProB if-construct on line ~w: ~s (~w)~n",[LineNr,TestC,Args]), | |
| 304 | Args = [ LatexTRUE, LatexFALSE], | |
| 305 | eval_codes_success(LineNr,TestC,exists,StringResult,_EnumWarning,_LocalState), % TO DO: refactor eval_codes to return various number of results in list | |
| 306 | dformat(user_output,'Value for probif: ~w~n',[StringResult]), | |
| 307 | (StringResult = 'TRUE' -> process_line(Stream,LineNr,LatexTRUE,[]) | |
| 308 | ; StringResult = 'FALSE' -> process_line(Stream,LineNr,LatexFALSE,[]) | |
| 309 | ; StringResult = 'UNKNOWN' -> add_latex_processor_error('UNKNOWN predicate or BOOL expression result for probif: ',LineNr) | |
| 310 | ; add_latex_processor_error('Not a predicate or BOOL expression for probif: ',LineNr) | |
| 311 | ) | |
| 312 | }. | |
| 313 | process_command(for,VARC,Args,Stream,LineNr) --> | |
| 314 | { dformat(user_output,"evaluating ProB for-construct on line ~w: ~s (~w)~n",[LineNr,VARC,Args]), | |
| 315 | Args = [ EXPRC, LATEX], | |
| 316 | atom_codes(ID,VARC), % the iteration variable | |
| 317 | eval_expression_codes_success(EXPRC,_StringResult,_EnumWarning,_LocalState,_Typed), | |
| 318 | eval_strings:get_last_result_value(_,Type,Value), %print(value(Value,Type)),nl, | |
| 319 | is_set_type(Type,IDType), | |
| 320 | custom_explicit_sets:expand_custom_set_to_list(Value,ExpValue,_,probfor), | |
| 321 | prob_foreach(ExpValue,ID,IDType,LATEX,Stream,LineNr) | |
| 322 | }. | |
| 323 | % TO DO: add command to register latex pretty printing modifications | |
| 324 | % e.g., \probppid{epsilon}{\epsilon} | |
| 325 | ||
| 326 | :- use_module(probsrc(tools),[get_filename_extension/2]). | |
| 327 | :- use_module(extrasrc(meta_interface),[command_arguments/2, %command_optional_arguments/4, | |
| 328 | command_category/2, | |
| 329 | is_dot_command/1, is_dot_command_for_expr/1, | |
| 330 | call_command/5]). | |
| 331 | % this works for is_dot_command and is_dot_command_for_expr | |
| 332 | process_dot_command(Cmd,Args,LineNr) :- print(process(Cmd,LineNr)),nl, | |
| 333 | command_category(Cmd,dot), | |
| 334 | command_arguments(Cmd,FormalArgs), | |
| 335 | dformat(user_output,"evaluating DOT command ~w using ~w~n",[Cmd,FormalArgs]), | |
| 336 | !, | |
| 337 | same_length(FormalArgs,ActualArgsC), | |
| 338 | (append(ActualArgsC,OptionalArgsC,Args) | |
| 339 | -> maplist(codes_to_atom,ActualArgsC,ActualArgs0), | |
| 340 | include(latex_dot_arg,OptionalArgsC,LatexArgs), % arguments for latex_processor here | |
| 341 | exclude(latex_dot_arg,OptionalArgsC,OptionalArgsC2), | |
| 342 | maplist(codes_to_arg,OptionalArgsC2,OptionalArgsA), | |
| 343 | expand_relative_files(FormalArgs,ActualArgs0,ActualArgs), | |
| 344 | ((get_dot_file(FormalArgs,ActualArgs,DOTFILE), | |
| 345 | append([PDFFILE],OptionalArgs,OptionalArgsA), | |
| 346 | get_filename_extension(PDFFILE,'pdf') ) | |
| 347 | -> debug:debug_println(19,will_generate_pdf(PDFFILE,OptionalArgs)) % first argument is PDFFile | |
| 348 | ; OptionalArgs=OptionalArgsA | |
| 349 | ), | |
| 350 | debug:debug_println(19,call_command(Cmd,FormalArgs,ActualArgs,OptionalArgs)), | |
| 351 | (is_dot_command(Cmd) -> true | |
| 352 | ; is_dot_command_for_expr(Cmd) -> true | |
| 353 | ; add_latex_processor_error('Unknown dotcmd: ',Cmd)), | |
| 354 | setup_prefs_for_command(["ascii"|LatexArgs],CHNG), % DOT does not support Latex | |
| 355 | (call_command(dot,Cmd,FormalArgs,ActualArgs,OptionalArgs) | |
| 356 | -> reset_prefs_for_command(["ascii"|LatexArgs],CHNG), | |
| 357 | (var(PDFFILE) -> true ; expand_file_relativ_to_latex_file(PDFFILE,EPDFILE), | |
| 358 | gen_pdf(DOTFILE,LatexArgs,EPDFILE)) | |
| 359 | ; reset_prefs_for_command(["ascii"|LatexArgs],CHNG), | |
| 360 | add_latex_processor_error('Command failed: ',Cmd),fail) | |
| 361 | % TO DO: catch exception and reset_prefs, optionally generate PDF | |
| 362 | ; tools:ajoin(['Not enough arguments for dot command on line ',LineNr,': '],Msg), | |
| 363 | add_latex_processor_error(Msg,Cmd),fail | |
| 364 | ). | |
| 365 | process_dot_command(Cmd,_Args,LineNr) :- | |
| 366 | tools:ajoin(['Not a valid dot command on line ',LineNr,': '],Msg), | |
| 367 | add_latex_processor_error(Msg,Cmd),fail. | |
| 368 | ||
| 369 | :- use_module(probsrc(tools_commands),[get_dot_engine_options/2]). | |
| 370 | gen_pdf(DOTFILE,Args,PDFFILE) :- | |
| 371 | (member("sfdp",Args) -> get_dot_engine_options(sfdp,Opts) ; get_dot_engine_options(default,Opts)), | |
| 372 | get_preference(path_to_dot,DOTCMD), | |
| 373 | dformat(user_output,'Calling dot: ~w to generate ~w~n',[DOTCMD,PDFFILE]), | |
| 374 | append(Opts,['-Tpdf', '-o', PDFFILE, DOTFILE],CmdArgs), | |
| 375 | system_call(DOTCMD, CmdArgs,_TextOut,_ErrText,_JExit). | |
| 376 | % try and find the dotfile in the arguments | |
| 377 | get_dot_file([dotfile|_],[H|_],Res) :- !, Res=H. | |
| 378 | get_dot_file([_|FT],[_|T],Res) :- get_dot_file(FT,T,Res). | |
| 379 | ||
| 380 | expand_relative_files([],[],[]). | |
| 381 | expand_relative_files([dotfile|T],[A|AT], [EA|EAT]) :- !, | |
| 382 | expand_file_relativ_to_latex_file(A,EA), expand_relative_files(T,AT,EAT). | |
| 383 | expand_relative_files([_|FT],[AA|AT],[AA|EAT]) :- expand_relative_files(FT,AT,EAT). | |
| 384 | ||
| 385 | % list of arguments processed by latex | |
| 386 | latex_dot_arg(X) :- member(X,["nopt","prop-logic","sfdp","dot"]). % dot ist the default | |
| 387 | ||
| 388 | % used for maplist | |
| 389 | codes_to_atom(C,A) :- atom_codes(A,C). | |
| 390 | codes_to_number(C,A) :- number_codes(A,C). | |
| 391 | ||
| 392 | % printing expression or substitution: | |
| 393 | print_expr(Stream,TypedExpr,Args) :- | |
| 394 | (member("strip-exists",Args) | |
| 395 | -> strip_exists(TypedExpr,TE2) % sometimes we do not want to see the outer existential quantifiers | |
| 396 | ; TE2=TypedExpr), | |
| 397 | translate:translate_subst_or_bexpr(TE2,PS), | |
| 398 | %dformat(user_output,"pretty-printing :: ~w ~n",[PS]), | |
| 399 | format_stream(Stream,'~w ',[PS]). | |
| 400 | ||
| 401 | :- use_module(probsrc(tools),[split_chars/3, safe_number_codes/2,safe_atom_codes/2]). | |
| 402 | % used for table argument processing | |
| 403 | codes_to_arg(Codes,argument_value(L,R)) :- split_chars(Codes,"=",[Left,Right]), !, % detect Option=Value | |
| 404 | atom_codes(L,Left), | |
| 405 | (safe_number_codes(R,Right) -> true ; atom_codes(R,Right)). | |
| 406 | codes_to_arg(C,A) :- atom_codes(A,C). | |
| 407 | ||
| 408 | prob_command(LineNr,CMD,Codes,Args) --> "\\prob",cmd(CMD),"{", get_command(LineNr,0,Codes,Args), | |
| 409 | {check_for_invalid_args(CMD,Args,LineNr)}. | |
| 410 | ||
| 411 | check_for_invalid_args(CMD,Args,LineNr) :- invalid_arg(CMD,Args,IllegalArg), | |
| 412 | tools:ajoin(['Illegal argument for ProB Latex command on line ',LineNr,': '],Msg), | |
| 413 | safe_atom_codes(Arg,IllegalArg), | |
| 414 | add_latex_processor_error(Msg,CMD:Arg),fail. | |
| 415 | check_for_invalid_args(_,_,_). | |
| 416 | ||
| 417 | ||
| 418 | cmd(dot) --> "dot". | |
| 419 | cmd(dotcmd) --> "dotcmd". | |
| 420 | cmd(expr) --> "expr". | |
| 421 | cmd(for) --> "for". | |
| 422 | cmd(if) --> "if". | |
| 423 | cmd(let) --> "let". | |
| 424 | cmd(print) --> "print". | |
| 425 | cmd(repl) --> "repl". | |
| 426 | cmd(table) --> "table". | |
| 427 | cmd(requires) --> "requires". | |
| 428 | cmd(system) --> "system". | |
| 429 | ||
| 430 | argmember(Cmd,["set-pref",_,_|T]) :- !, argmember(Cmd,T). | |
| 431 | argmember(Cmd,[Cmd|_]). | |
| 432 | argmember(Cmd,[_|T]) :- argmember(Cmd,T). | |
| 433 | ||
| 434 | invalid_arg(let,[_|Args],IllegalArg) :- argmember(IllegalArg,Args), | |
| 435 | nonmember(IllegalArg,["ascii","silent","solution","store","time","nopt","prop-logic"]). | |
| 436 | invalid_arg(repl,Args,IllegalArg) :- argmember(IllegalArg,Args), | |
| 437 | nonmember(IllegalArg,["ascii","check-true","print","silent","solution","store","strip-exists", | |
| 438 | "time","nopt","prop-logic","check"]). | |
| 439 | invalid_arg(print,Args,IllegalArg) :- argmember(IllegalArg,Args), | |
| 440 | nonmember(IllegalArg,["ascii","pred","expr","nopt","prop-logic","strip-exists","subst"]). % expr is default | |
| 441 | invalid_arg(expr,Args,IllegalArg) :- argmember(IllegalArg,Args), | |
| 442 | nonmember(IllegalArg,["ascii","silent","string","time","value","nopt","prop-logic"]). | |
| 443 | %invalid_arg(table,Args,IllegalArg) :- member(IllegalArg,Args),nonmember(IllegalArg,["no-headings","no-hline",...]). | |
| 444 | invalid_arg(if,[_,_,IllegalArg|_],IllegalArg). % too many args | |
| 445 | invalid_arg(for,[_,_,IllegalArg|_],IllegalArg). | |
| 446 | ||
| 447 | get_command(LineNr,Nr,[123|T],Arg) --> "{", !, {N1 is Nr+1}, get_command(LineNr,N1,T,Arg). | |
| 448 | get_command(LineNr,0,[],Arg) --> "}",!, get_arguments(LineNr,Arg). | |
| 449 | get_command(LineNr,Nr,[125|T],Arg) --> "}", !, {N1 is Nr-1}, get_command(LineNr,N1,T,Arg). | |
| 450 | get_command(LineNr,Nr,[H|T],Arg) --> [H],!, get_command(LineNr,Nr,T,Arg). | |
| 451 | get_command(LineNr,_,[],[]) --> {add_error(get_command,'prob command not closed: ',LineNr)}. | |
| 452 | ||
| 453 | get_arguments(LineNr,[Arg|T]) --> "{", get_arg(Arg,0,LineNr),!, get_arguments(LineNr,T). | |
| 454 | get_arguments(_,[]) --> []. | |
| 455 | ||
| 456 | get_arg([],0,_) --> "}". | |
| 457 | get_arg([123|T],Level,LineNr) --> "{", !, {L1 is Level+1}, get_arg(T,L1,LineNr). | |
| 458 | get_arg([125|T],Level,LineNr) --> "}", {Level>0}, !, {L1 is Level-1}, get_arg(T,L1,LineNr). | |
| 459 | get_arg([H|T],Level,LineNr) --> [H],!,get_arg(T,Level,LineNr). | |
| 460 | get_arg([],_,LineNr) --> {add_error(get_arg,'prob argument not closed: ',LineNr)}. | |
| 461 | ||
| 462 | ||
| 463 | ignore_rest([H|T]) --> [H], !, ignore_rest(T). | |
| 464 | ignore_rest([]) --> []. | |
| 465 | ||
| 466 | ||
| 467 | setup_prefs_for_command(Args,(CHNG1,CHNG2,BV)) :- | |
| 468 | bvisual2_translation_mode(BV), | |
| 469 | (member("ascii",Args) | |
| 470 | -> (latex_mode -> unset_latex_mode ; true), | |
| 471 | set_bvisual2_translation_mode(ascii) % in bvisual | |
| 472 | ; set_latex_mode, | |
| 473 | set_bvisual2_translation_mode(latex)), | |
| 474 | (member("nopt",Args) -> temporary_set_preference(optimize_ast,false,CHNG1) ; true), | |
| 475 | (member("prop-logic",Args) -> temporary_set_preference(pp_propositional_logic_mode,true,CHNG2) ; true). | |
| 476 | reset_prefs_for_command(Args,(CHNG1,CHNG2,BV)) :- | |
| 477 | set_bvisual2_translation_mode(BV), | |
| 478 | (member("ascii",Args) -> true ; unset_latex_mode), % after each command we unset latex mode | |
| 479 | (member("nopt",Args) -> reset_temporary_preference(optimize_ast,CHNG1) ; true), | |
| 480 | (member("prop-logic",Args) -> reset_temporary_preference(pp_propositional_logic_mode,CHNG2) ; true). | |
| 481 | ||
| 482 | % ------------------------------ | |
| 483 | :- use_module(probsrc(debug),[debug_mode/1]). | |
| 484 | ||
| 485 | dformat(Stream,F,A) :- (debug_mode(on) -> format_stream(Stream,F,A) ; true). | |
| 486 | ||
| 487 | format_stream(Stream,F,A) :- | |
| 488 | catch(format(Stream,F,A), E, ( | |
| 489 | add_latex_processor_error('Exception while writing to stream with format: ',E), | |
| 490 | write(Stream,' *** EXCEPTION *** ') | |
| 491 | )). | |
| 492 | ||
| 493 | write_stream(Stream,T) :- | |
| 494 | catch(write(Stream,T), E, ( | |
| 495 | add_latex_processor_error('Exception while writing to stream: ',E), | |
| 496 | write(Stream,' *** EXCEPTION *** ') | |
| 497 | )). | |
| 498 | ||
| 499 | close_stream(Stream) :- | |
| 500 | catch(close(Stream), E, add_latex_processor_error('Exception while closing stream: ',E)). | |
| 501 | ||
| 502 | print_last_eval_time(Stream,Args) :- member("time",Args), | |
| 503 | eval_strings:last_eval_time(_Time,WTime),!, | |
| 504 | (member("ascii",Args) -> format_stream(Stream,'\\ (~w ms)',[WTime]) % includes parsing time | |
| 505 | ; format_stream(Stream,' \\mathit{\\ (~w ms)}',[WTime])). | |
| 506 | print_last_eval_time(Stream,Args) :- member("time",Args),!, write(Stream,' (?? ms) '). | |
| 507 | print_last_eval_time(_,_). | |
| 508 | ||
| 509 | :- use_module(probsrc(translate),[translate_bvalue/2]). | |
| 510 | write_solution(Stream,Args,LocalState) :- | |
| 511 | write_optional_leadsto(Stream,Args), | |
| 512 | (member("ascii",Args) -> FormatStr = ' ~w = ~w '; FormatStr = ' \\mathit{~w} = ~w '), | |
| 513 | write_sol_aux(LocalState, Stream, FormatStr). | |
| 514 | write_sol_aux([bind(ID,IDV)|T],Stream,FormatStr) :- | |
| 515 | translate_bvalue(IDV,VS), | |
| 516 | format_stream(Stream,FormatStr,[ID,VS]), | |
| 517 | (T=[] -> true ; write(Stream,' \\wedge'), write_sol_aux(T,Stream,FormatStr)). | |
| 518 | write_sol_aux([],Stream,_) :- write(Stream,'TRUE'). | |
| 519 | ||
| 520 | % ------------------------------ | |
| 521 | ||
| 522 | ||
| 523 | prob_foreach([],_ID,_IDT,_Ltx,_Stream,_). | |
| 524 | prob_foreach([Value|TVal], ID, IDType,LATEX, Stream,LineNr) :- | |
| 525 | %print(process_foreach(ID,Value)),nl, | |
| 526 | store_let_value(ID,IDType,Value), | |
| 527 | %print(process(LATEX)),nl, | |
| 528 | % now process line with ID = Value | |
| 529 | process_line(Stream,LineNr,LATEX,[]), %nl(Stream), | |
| 530 | %print(done),nl, | |
| 531 | prob_foreach(TVal,ID, IDType,LATEX,Stream,LineNr). | |
| 532 | ||
| 533 | ||
| 534 | ||
| 535 | store_let_value(ID,IDType,Value) :- | |
| 536 | retractall(eval_strings:stored_let_value(ID,_,_)), % TO DO: provide proper predicate in eval_strings for this | |
| 537 | assertz(eval_strings:stored_let_value(ID,IDType,Value)). | |
| 538 | ||
| 539 | strip_exists(b(exists(_,Body),pred,_),Res) :- !, strip_exists(Body,Res). | |
| 540 | strip_exists(B,B). | |
| 541 | ||
| 542 | % ---------------------- | |
| 543 | ||
| 544 | :- use_module(probsrc(tools_strings),[string_concatenate/3]). | |
| 545 | :- use_module(probsrc(tools),[get_parent_directory/2, is_absolute_path/1]). | |
| 546 | :- dynamic latex_output_file/2. | |
| 547 | update_latex_output_file(FileOut) :- | |
| 548 | retractall(latex_output_file(_,_)), | |
| 549 | get_parent_directory(FileOut,Dir), | |
| 550 | assertz(latex_output_file(FileOut,Dir)). | |
| 551 | ||
| 552 | expand_file_relativ_to_latex_file(File,ExpandedFile) :- \+ is_absolute_path(File), | |
| 553 | latex_output_file(_,Dir), | |
| 554 | !, | |
| 555 | string_concatenate(Dir,File,ExpandedFile). | |
| 556 | expand_file_relativ_to_latex_file(F,F). |