| 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_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). |