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