#!/usr/local/bin/perl -T package SystemIDemo; $false = 0; $true = 1; #use warnings; #use strict; use Sys::Hostname; use POSIX ":signal_h"; use CGI qw(:standard); $CGI::POST_MAX=32768; # max 32K posts $query = new CGI; $| = 1; $valid_rank = $true; $valid_term = $true; $valid_impl = $true; $valid_epath = $true; ############################################################################## $error_report_address = "compositional-web-bugs\@types.bu.edu"; # Web page style our $background_color = "#fffff9"; our $figure_color = "#eeeeee"; our $figure2_color = "#dddddd"; our $header_color = "#cccccc"; $done = "(Done)"; $processing = "(Processing)"; $error = "(Error)"; $javadir = "church/java"; $lambda2xml = "church/src/lambda2xml-haskell.old-but-still-used/lambda2xml"; $java_inference="systemi.DriverXML"; $haskell_inference="church/src/Carlier-implementation-I/infer"; $sml_inference="church/src/Kfoury-Wells-implementation/bin/infer"; $lambda_schema = "church/compositional-analysis/lambda-xml/lambda.xsd"; $systemi_schema = "church/compositional-analysis/system-i/system-i.xsd"; $style_dir = "church/compositional-analysis/system-i"; $xml_stylesheet = $style_dir."/system-i.xml.xsl"; $postscript_stylesheet = $style_dir."/system-i.latex.xsl"; $text_stylesheet = $style_dir."/system-i.txt.xsl"; $xhtml_stylesheet = $style_dir."/system-i.xhtml.xsl"; if (hostname eq "buddha") { $ENV{PATH}="/usr/local/bin:/bin:/usr/bin:/usr/X11R6/bin"; $sml = "/usr/bin/sml"; # 110.0.7 $gzip = "/bin/gzip"; $ps2pdf = "/u1/pg/sebc/opt/i686-pc-linux-gnu/ghostscript-7.05/bin/ps2pdf"; $java = "/usr/bin/java"; # 1.4.0 $saxon = "com.icl.saxon.StyleSheet"; $msv = "com.sun.msv.driver.textui.Driver"; $dvips = "/usr/bin/dvips -z -Ppdf -G0 -D600"; $latex = "/usr/bin/latex"; $ENV{CLASSPATH}="./:/usr/java/j2sdk1.4.0/jre/lib/rt.jar"; } else { $ENV{PATH}="/usr/local/bin:/bin:/usr/bin:/usr/ucb:/usr/bin/X11"; $ENV{LD_LIBRARY_PATH}="/usr/local/lib"; $sml = "/usr/local/bin/sml"; $gzip = "/usr/local/bin/gzip"; $ps2pdf = "ps2pdf14"; $java = "/bin/java"; $saxon = "com.icl.saxon.StyleSheet"; $msv = "com.sun.msv.driver.textui.Driver"; $dvips = "/usr/local/bin/dvips -z -Ppdf -G0 -D600"; $latex = "/usr/local/bin/latex"; $ENV{CLASSPATH}="./:/usr/java/jre/lib/rt.jar"; } $ENV{CLASSPATH}=$ENV{CLASSPATH}.":$javadir/saxon/saxon-fop.jar:$javadir/saxon/saxon-jdom.jar:$javadir/saxon/saxon.jar:$javadir/jaxp-1.1/crimson.jar:$javadir/jaxp-1.1/jaxp.jar:$javadir/jaxp-1.1/xalan.jar:$javadir/msv-20010910/isorelax.jar:$javadir/msv-20010910/relaxngdatatype.jar:$javadir/msv-20010910/xsdlib.jar:$javadir/msv-20010910/msv.jar:./church/src/Ori-Implementation/systemi.jar:$javadir"; $convert_message = "Parsing and converting your term into XML."; # Status messages $inference_message = "Performing System I principal typing inference on your term."; $validate1_message = "Validating XML output from parsing against the Lambda schema."; $validate2_message = "Validating XML output from typing inference against the System I schema."; $style_message = "Applying the selected XML Stylesheet on the output from inference."; $max_rank = 8; # Assign a session code $session = unpack("H*", pack("Nn", time, $$)); $general_style_params = ['Initial Typing Judgement', 'Initial Skeleton', 'Unification Information', 'Final Typing Judgement', 'Final Skeleton or Derivation']; $standard_style_params = ['Initial Generated Constraint Set', 'Constraint Set at Failure', 'Final Substitution']; $tracing_style_params = ['Constraint Sets', 'Selected Substitutions', 'Substitutions', 'Incremental Skeletons']; $xml_tracing_style_params = ['Selected Substitutions', 'Incremental Skeletons']; ############################################################################## if($query->param("Action") eq "Generate") { $new_url = $query->self_url(); $new_url =~ s/Action=Generate\;//; print $query->redirect($new_url); } elsif(!$query->param("Action")) { display_form($valid_rank, $valid_term, $valid_impl, $valid_epath); } else { ############################################################################## ############################################################################## # The code that performs the inference and creates the status/progress page ############################################################################## # Code to make sure the inputs we were given are sane $upload_file = $query->param('Upload'); if(!($query->param("Rank") =~ /\d/) || ($query->param("Rank") =~ /\D/) || $query->param("Rank") > $max_rank) { $valid_rank = $false; } if(($query->param("Term") =~ /^\s*$/) && ($query->param("Examples") =~ /^\s*$/) && !$upload_file) { $valid_term = $false; } if(!($query->param("Examples") =~ /^\s*$/) && (!$upload_file) && ($query->param("Term") =~ /^\s*$/) && !($query->param("TermLanguage") eq "SML")) { $valid_impl = $false; } if(($query->param("Implementation") eq "Java") && ($query->param("EPathEnvironment") eq "on")) { $valid_epath = $false; } # If we got bad inputs notify the user by redisplaying the original form if(!$valid_rank || !$valid_term || !$valid_impl || !$valid_epath) { display_form($valid_rank, $valid_term, $valid_impl, $valid_epath); exit } ############################################################################## # Initially the status is empty @status = (); ############################################################################## # Write out our first progress message push @status, "$convert_message $processing"; write_status_page(-status=>[@status]); # Fork a child to handle the remainder of the session after redirecting $childpid = fork; if($childpid != 0) { $new_url = $query->self_url(); $new_url =~ s/^(.*)\/(.*)$/$1\//; print $query->redirect($new_url."$session.html"); #waitpid($childpid, 0); exit; } open STDIN, "/dev/null"; # Figure out where we are getting our term from. if($upload_file) { @text = <$upload_file>; $term = "@text"; } elsif (!($query->param("Term") =~ /^\s*$/)) { $term = $query->param("Term"); } else { $term = $query->param("Examples"); } if($query->param("TermLanguage") eq "SML") { $syntax = "s"; } elsif($query->param("TermLanguage") eq "Haskell") { $syntax = "c"; } elsif($query->param("TermLanguage") eq "Scheme") { $syntax = "l"; } else { pop @status; push @status, "$convert_message $error"; write_report_page(-status => [@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "You somehow managed to send us an invalid syntax selection, perhaps even intentionally. Naughty Naughty. Try again.", br;}); } # Parse the term, converting to XML $errors = parse_term(-term=>$term, -language=>$syntax, -output=>"/tmp/input-xml.$$"); # If there were errors, report them to the user if($errors) { pop @status; push @status, "$convert_message $error"; write_report_page(-status => [@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "Unable to parse your term:", br, "
", $errors, "
"; }); #delete_files("/tmp/input-xml.$$"); exit; } pop @status; push @status, "$convert_message $done"; ############################################################################## push @status, "$validate1_message $processing"; write_status_page(-status=>[@status]); # Validate the XML generated by the parser as a sanity check $errors = validate_xml(-input=>"/tmp/input-xml.$$", -schema=>$lambda_schema); # If there were errors, tell the user and maintainers if($errors) { pop @status; push @status, "$validate1_message $error"; send_error_report($errors); write_report_page(-status=>[@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "Internal Consistency Error:", br, "
\n", $errors,
                          "
", br, "The maintainers have been notified."; }); delete_files("/tmp/input-xml.$$"); exit; } pop @status; push @status, "$validate1_message $done"; ############################################################################## push @status, "$inference_message $processing"; write_status_page(-status=>[@status]); if($query->param("Rank") =~ /\d/) { $untainted_rank = $&; } else { pop @status; push @status, "$inference_message $error"; write_report_page(-status => [@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "You somehow managed to send us an invalid rank, perhaps even intentionally. Naughty Naughty. Try again.", br;}); # Do something better here } # Peform the actual typing inference $errors = infer_typing(-input=>"/tmp/input-xml.$$", -output=>"/tmp/output-xml.$$", -rank=>$untainted_rank, -implementation=>$query->param("Implementation")); # Two possible types of errors: inference failed or inference timed out. # If the inference engine chokes for other reasons # we have no way of knowing about it at present pop @status; if($errors == 1) { $inference_result = "(Done - inference failed)"; } elsif($errors == 2) { push @status, "$inference_message $error"; write_report_page(-status=>[@status], -reportsub => sub { my $FILE = shift(@_); print $FILE br, "", "Type inference timed out. This may mean that the term you requested requires more time to process than we allow.", ""; }); delete_files("/tmp/input-xml.$$"); exit; } else { $inference_result = "(Done - inference succeed)"; } push @status, "$inference_message $inference_result"; delete_files("/tmp/input-xml.$$"); ############################################################################## push @status, "$validate2_message $processing"; write_status_page(-status=>[@status]); # Validate the XML output from typing inference as a sanity check $errors = validate_xml(-input=>"/tmp/output-xml.$$", -schema=>$systemi_schema); # If there were errors, tell the user and maintainers if($errors) { pop @status; push @status, "$validate2_message $error"; send_error_report($errors); write_report_page(-status=>[@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "Internal Consistency Error:", br, "
\n", $errors,
                          "
", br, "The maintainers have been notified."; }); delete_files("/tmp/output-xml.$$"); exit; } pop @status; push @status, "$validate2_message $done"; ############################################################################## push @status, "$style_message $processing"; write_status_page(-status=>[@status]); # Figure out what options apply if($query->param("UnifyOptions") eq "Tracing") { $options = [$query->param("GeneralStyleOptions"), $query->param("TracingStyleOptions")]; } else { $options = [$query->param("GeneralStyleOptions"), $query->param("StandardStyleOptions")]; } if($query->param("EPathEnvironment") eq "on") { $options = [@{$options}, 'E-path Environment']; } if($query->param("IncludeLegend") eq "on") { $options = [@{$options}, 'Legend']; } # Apply a stylesheet to the output from typing inference %output = style_xml(-input=>"/tmp/output-xml.$$", -output_prefix=>$session, -style=>$query->param("OutputStyle"), -options=>$options); delete_files("/tmp/output-xml.$$"); if($output{'errors'}) { pop @status; push @status, "$style_message $error"; send_error_report($output{'errors'}); write_report_page(-status=>[@status], -reportsub => sub { my $FILE = shift(@_); print $FILE "Internal Consistency Error:", br, "
\n", $output{'errors'},
                          "
", br, "The maintainers have been notified."; }); delete_files($output{'file'}); exit; } pop @status; push @status, "$style_message $done"; ############################################################################## # Done, redirect the user to the output file write_report_page(-status=>[@status], -refresh=>$output{'file'}, -reportsub=> sub { my $FILE = shift(@_); print $FILE br, "
(This URL will become invalid in two minutes.)
"; }); sleep(120); delete_files($output{'file'}, "$session.html"); } ############################################################################## ############################################################################## # The code that displays the actual HTML that handles input ############################################################################## sub display_form { my $valid_rank = shift(@_); my $valid_term = shift(@_); my $valid_impl = shift(@_); my $valid_epath = shift(@_); print $query->header; print $query->start_html(-title=>'System I Experimentation Tool', -BGCOLOR=>$background_color, -head=>["" ,""]); print "
"; print "

System I Experimentation Tool

"; print "

Welcome user@".$query->remote_host()."!

"; print < This web application provides a friendly tool for experimenting with System I. System I allows inferring principal typings for pure terms of the lambda-calculus with intersection types for arbitrary finite ranks. It is particularly interesting because it can infer types for terms that cannot be typed in other commonly studied systems, as well as the fact that due to the principal typing property, type inference is compositional. System I was first described in Kfoury and Wells's POPL'99 paper, . We are currently in the process of extending System I beyond the pure lambda-calculus in order to smoothly handle important programming language constructs like variants, conditionals, and recursive definitions.

Unfortunately, this tool does not presently work with web browsers, such as , which do not support the use of <meta http-equiv="refresh">.

Direct bug reports and questions to:
(fn [user, host] => user ^ "@" ^ host) ["compositional-web-bugs", "types.bu.edu"];

Participants
Geoffrey Washburn Software Engineering
Assaf Kfoury Theory Consulting
Joe Wells Theory and Technical Consulting
Sebastien Carlier Software Engineering
Bradley Alan Original Unification Code
Bennett Yates Implementation
Ori Schwartz Implementation
END if(!$valid_impl || !$valid_rank || !$valid_term || !$valid_epath) { print "There is an error in your choice of input and options, see below for details."; } print $query->start_multipart_form(); $body = <When performing type inference you have three choices. One can choose to select a term out of the following examples (in syntax) that produce interesting output:

END @radio = $query->radio_group(-name=>'Examples', -nolabels=>1, -values=>['(fn x => x) (fn y => y y)', '(fn x => fn y => x y) (fn y => y y)', '(fn x => z (x (fn f => fn u => f u)) (x (fn v => fn g => g v))) (fn y => y y y)', '(fn x => x x) (fn x => x x)'], -default=>"-"); @examples = (< (* typable at rank 3 *)
$radio[0] (fn x => x) (fn y => y y)
END , < (* typable at rank 3 *)
$radio[1] (fn x => fn y => x y) (fn y => y y)
END , < (* typable at rank 3, untypable in System Fw *)
$radio[2] (fn x => z (x (fn f => fn u => f u)) (x (fn v => fn g => g v))) (fn y => y y y)
END , < (* untypable for all ranks *)
$radio[3] (fn x => x x) (fn x => x x)
END ); $body = $body.gen_altfigure(@examples).br; $body = $body.<Or one may enter a lambda-calculus term for which to infer a principal typing in the text-area below:
END $body = $body.$query->textarea(-name=>'Term', -rows=>4, -cols=>50); $body = $body.<
Or finally, one may select a local file containing a lambda-calculus term to upload:
END $body = $body."File: ".$query->filefield(-name=>'Upload',-size=>40,-maxlength=>32768); $body = $body.<
END if(!$valid_term) { $body = $body.br."(you must select a term for inference via one of the above methods)"; } $body = $body."
".$query->submit('Action','Infer')."
"; print gen_box("Term", $body), br; $body = <There are presently three implementations of variations of the System I principal typing inference algorithm.
  • The Alan-Washburn implementation closely matches the algorithm for System I presented in the and the presently unpublished corresponding extended technical report.
  • The Yates-Schwartz implementation also closely matches the algorithm for System I presented in the .
  • The Carlier implementation follows an inference algorithm suitable for System Iω, an extension of System I with the type constant ω. This system and the algorithm used in this implementation are presented in this . Note that this implementation solves constraints lazily, and as such is able to assign types to both strong and weakly normalizable terms.
Which implementation would you like to use?   END ($sml, $java, $haskell) = $query->radio_group(-name=>'Implementation', -values=>[ 'SML', 'Java', 'Haskell' ], -nolabels=>1, -default=>'SML'); $body = $body.< END print gen_box("Implementation", $body), br; $body = < If a term has a principal typing in System I, the inference engine will find it. However, if a term does not have a typing, the unification algorithm will not terminate. The unification algorithm can be made terminating by restricting the highest rank intersection type that it will attempt to unify. Presently, this is only supported by the Alan-Washburn implementation. If this restriction is set too low, some typable terms may not have a typing inferred for them. However, in the interest of preventing this CGI from using too much of the available system resources, the maximum rank we allow is $max_rank. Regardless, many interesting programs are typable at low ranks. Restrict to rank:  END $body = $body.$query->textfield(-name=>'Rank', -size=>1, -default=>'3'); if(!$valid_rank) { $body = $body."(invalid rank)"; } $body = $body."

"; print gen_box("Unification Options", $body), br; $body = < Our lambda-calculus parser is capable of accepting input in several different styles of syntax:

END $syntax = < (Standard ML) e::=x | fn x => e | e1 e2 | ( e ) (Haskell) e::=x | \\x1…xi -> e | e1 e2 | ( e ) (Scheme) e::=x | (lambda (x) e) | (e1 e2) END $body = $body.gen_figure($syntax).br; $body = $body.<radio_group(-name=>'TermLanguage', -values=>['SML','Haskell', 'Scheme'], -default=>'SML'); if(!$valid_impl) { $body = $body." (if using one of the SML examples above, you must selection SML as your syntax)"; } print gen_box("Input Format", $body), br; $body = < By default the output includes a fairly lengthy and verbose legend. More advanced users may wish for their output to omit the legend. END $body = $body.$query->checkbox(-name=>'IncludeLegend', -checked=>'on', -label=>'Include Legend'); $body = $body.< There are two modes of output, standard which includes only the initial constraints and the final substitution, and tracing provides a trace of the unification process. END $body = $body.$query->radio_group(-name=>'UnifyOptions', -values=>['Standard', 'Tracing'], -default=>"Standard"); $body = $body.<

In some examples the types may become very large making the skeletons and derivation difficult to read. One may opt to only apply expansion variable substitutions to the skeletons and derivations displayed in the output, which may make those examples easier to read. END $body = $body.$query->checkbox(-name=>'ExpandOnly', -checked=>'on', -label=>'Apply Expansions Only'); $body = $body.<

The Alan-Washburn implementation computes composed substitutions using safe composition, while the Yates-Schwartz implementation computes chains of small substitutions. The Carlier implementation works with chains internally, but has an option to compose them (using an algorithm different from safe composition). END $body = $body.$query->checkbox(-name=>'ComposeSubstitutions', -checked=>'on', -label=>'Compose Substitutions'); $body = $body.<

In the Alan-Washburn implementation, E-path Environments are generated and may optionally be included in the output. END $body = $body.$query->checkbox(-name=>'EPathEnvironment', -value=>'on', -label=>'Include E-path Environment'); if(!$valid_epath) { $body = $body." (cannot include E-Path Environment when using the Java implementation)"; } $body = $body.<

The output from our inference engines can be rendered using into several different file formats, which would you like?
END @radio = $query->radio_group( -name=>'OutputStyle', -values=>['Raw XML', 'PDF', 'Gzipped PostScript', 'PostScript','XHTML', 'ASCII Text'], -default=>'PDF'); $xml_radio = shift @radio; $body = $body."

    "; $body = $body."
  • @radio
  • "; $body = $body.<

    For these formats, you can choose among the following items to be included in your output: END $body = $body.$query->checkbox_group(-name=>"GeneralStyleOptions", -values=>$general_style_params, -defaults=>$general_style_params, -rows=>2); $body = $body."

    "; $body = $body.<

    Additional options relevant for standard unification output: END $body = $body.$query->checkbox_group(-name=>"StandardStyleOptions", -values=>$standard_style_params, -defaults=>$standard_style_params, -rows=>2); $body = $body.<

    Additional options relevant for tracing unification output: END $body = $body.$query->checkbox_group(-name=>"TracingStyleOptions", -values=>$tracing_style_params, -defaults=>$tracing_style_params, -rows=>2); $body = $body."

  • ".$xml_radio; $body = $body.<

    For XML output, the following options are relevant for tracing unification output: END $body = $body.$query->checkbox_group(-name=>"XMLTracingStyleOptions", -values=>$xml_tracing_style_params, -defaults=>$xml_tracing_style_params, -rows=>1); $body = $body."

"; print gen_box("Output Format", $body), br; $bookmark_url = $query->self_url(); $body = < As this tool provides quite a number of configuration options, and it becomes tiresome to readjust your settings on every visit, we provide the option for you to generate a bookmark-able URL that will preserve the options as they are presently set on this page. END $body = $body."
".$query->submit('Action','Generate')."

"; print gen_box("Generate URL", $body), br; print $query->endform; print $query->end_html; } ############################################################################## ############################################################################## # Utility functions ############################################################################## sub write_status_page { my %params = @_; my @status = @{$params{-status}}; my $refresh_current = ""; open(INFO, ">$session.html"); print INFO $query->start_html(-title=> "System I Experimentation Tool ($$)", -BGCOLOR=>$background_color, -head=>[$refresh_current]); print INFO "

System I Experimentation Tool

"; print INFO gen_altfigure(@status); print INFO $query->end_html; close(INFO); } ############################################################################## sub write_report_page { my %params = @_; my @status = @{$params{-status}}; my $reportsub = $params{-reportsub}; my $refresh = $params{-refresh} ||= "" ; open(INFO, ">$session.html"); if($refresh) { print INFO $query->start_html(-title=>"System I Experimentation Tool", -BGCOLOR=>$background_color, -head=>[refresh_to_file(-file=>$refresh)]); } else { print INFO $query->start_html(-title=>"System I Web Experimentation Tool", -BGCOLOR=>$background_color); } print INFO "

System I Experimentation Tool

"; print INFO gen_altfigure(@status), br; &{$reportsub}(INFO); print INFO $query->end_html; close(INFO); } ############################################################################## sub refresh_to_file { my %params = @_; my $file = $params{-file}; return ""; } ############################################################################## # A function to delete a list of files. Mainly to abstract away some, rather # than calling system everywhere, and it proves a central location to turn # of file deletion for debugging purposes sub delete_files { system("rm @_"); } ############################################################################## sub create_param_string { my @args = @_; $params = ""; for(@$general_style_params,@$standard_style_params,@$tracing_style_params, ('Legend')) { $option = $_; $option =~ tr/[A-Z\ ]/[a-z_]/; $opt = $_; $flag = 0; for(@args) { if($_ eq $opt) { $params = $params." ".$option."=1"; $flag = 1; break; } } if($flag == 0) { $params = $params." ".$option."=0"; } } return $params; } ############################################################################## # Code to take a title and content and generated HTML for a titled box sub gen_box { my $title = shift; my $content = shift; my $box_html = <
$title
$content
END return $box_html; } ############################################################################## # Code to take a list of elements and generate a figure with alternating # colors sub gen_altfigure { my $box_html = < END my $index = 0; for(@_) { my $color = undef; if(($index % 2) == 0) { $color = $figure_color; } else { $color = $figure2_color; } $box_html = $box_html.<$_ END $index++; } $box_html = $box_html.< END return $box_html; } ############################################################################## # Code to take content and produce a figure box sub gen_figure { my $figure_html = <
@_
END return $figure_html; } ############################################################################## sub parse_term { my %params = @_; my $term = $params{-term}; my $language = $params{-language}; my $output = $params{-output}; my $errors = "/tmp/errors.$$"; $language =~ tr/[A-Z]/[a-z]/; open(PARSER, "| $lambda2xml -$language > $output 2> $errors"); print PARSER $term; close(PARSER); open(ERRORS, $errors); @output = ; close(ERRORS); delete_files($errors); return "@output"; } ############################################################################## sub validate_xml { my %params = @_; my $input = $params{-input}; my $schema = $params{-schema}; my $output = "/tmp/xml-errors.$$"; system("$java $msv $schema $input > $output"); open(XML_ERRORS, $output); @output = ; close(XML_ERRORS); delete_files($output); if(grep /Error|NOT valid|failed/i, @output) { return "@output"; } else { return ""; } } ############################################################################## sub infer_typing { my %params = @_; my $input = $params{-input}; my $output = $params{-output}; my $rank = $params{-rank}; my $implementation = $params{-implementation}; my $timeout = $false; my $other = $false; my $opts = ""; if($query->param("ExpandOnly") eq "on") { $opts = $opts." --expand-only"; } if($query->param("UnifyOptions") eq "Tracing") { $opts = $opts." --trace"; if($query->param("OutputStyle") eq "Raw XML") { if(grep /Selected Substitutions/i, $query->param("XMLTracingStyleOptions")) { $opts = $opts." --trace-selected"; } if(grep /Incremental Skeletons/i, $query->param("XMLTracingStyleOptions")) { $opts = $opts." --trace-skeleton"; } } else { if(grep /Selected Substitutions/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-selected"; } if(grep /Incremental Skeletons/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-skeleton"; } } } my $childpid = fork; if($childpid == 0) { if($implementation eq "SML") { $cmd = "$sml_inference"; if($query->param("UnifyOptions") eq "Tracing") { if($query->param("EPathEnvironment") eq "on") { $opts = $opts." --epathenv"; } } else { if($query->param("EPathEnvironment") eq "on") { $opts = $opts." --epathenv"; } } $cmd = $cmd." ".$opts." --rank $rank $input > $output"; exec($cmd); } elsif($implementation eq "Haskell") { # FIXME $opts = ""; # Apply Expansions Only if ($query->param("ExpandOnly") eq "on") { $opts = $opts." --expand-only"; } # Compose Substitutions if ($query->param("ComposeSubstitutions") eq "on") { $opts = $opts." --compose-substitutions"; } # General Style Options if (grep /Initial Typing Judgement/i, $query->param("GeneralStyleOptions") || grep /Initial Skeleton/i, $query->param("GeneralStyleOptions")) { # Initial typing judgement is extracted from the initial skeleton $opts = $opts." --initial-skeleton"; } if (grep /Unification Information/i, $query->param("GeneralStyleOptions")) { # Unification Information option is not supported. } if (grep /Final Skeleton or Derivation/i, $query->param("GeneralStyleOptions")) { $opts = $opts." --derivation"; } if (grep /Final Typing Judgement/i, $query->param("GeneralStyleOptions")) { $opts = $opts." --judgement"; } if ($query->param("UnifyOptions") eq "Tracing") { # Tracing unification output $opts = $opts." --trace"; if($query->param("OutputStyle") eq "Raw XML") { # FIXME: always --trace-constraints and --trace-composed ? if(grep /Selected Substitutions/i, $query->param("XMLTracingStyleOptions")) { $opts = $opts." --trace-selected"; } if(grep /Incremental Skeletons/i, $query->param("XMLTracingStyleOptions")) { $opts = $opts." --trace-skeleton"; } } else { if (grep /Constraint Sets/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-constraints"; } if (grep /Substitutions/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-composed"; } if(grep /Selected Substitutions/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-selected"; } if(grep /Incremental Skeletons/i, $query->param("TracingStyleOptions")) { $opts = $opts." --trace-skeleton"; } } } else { # Standard unification output if (grep /Initial Generated Constraint Set/i, $query->param("StandardStyleOptions")) { $opts = $opts." --initial-constraints"; } if (grep /Final Substitution/i, $query->param("StandardStyleOptions")) { $opts = $opts." --final-substitution"; } # Constraint Set at Failure is not supported (inference never fails) } open(INFER, "| $haskell_inference $opts > $output"); open(XML, $input); print INFER ; close(XML); close(INFER); } elsif($implementation eq "Java") { open(INFER, "| $java $java_inference $opts > $output"); open(XML, $input); print INFER ; close(XML); close(INFER); } exit; } else { eval { local $SIG{ALRM} = sub { die("timedout"); }; alarm(120); waitpid($childpid, 0); alarm(0); }; if ($@ and $@ =~ /timedout/) { $timeout = $true; kill 9, $childpid; } } if($timeout) { return 2; } open(XML, $output); @output = ; close(XML); if(grep /inference-failure/i, @output) { return 1; } else { return 0; } } ############################################################################## sub style_xml { my %params = @_; my $input = $params{-input}; my $output_prefix = $params{-output_prefix}; my $style = $params{-style}; my @options= @{$params{-options}}; my $style_error = "/tmp/xslt-error.$$"; $params = create_param_string(@options); if($style eq "Raw XML") { $output_file = "$output_prefix.xml"; system("cp $input $output_file > $style_error"); } elsif ($style eq "ASCII Text") { $output_file = "$output_prefix.txt"; system("$java $saxon $input $text_stylesheet $params > $output_file 2> $style_error"); } elsif ($style eq "XHTML") { $output_file = "$output_prefix.xhtml"; system("$java $saxon $input $xhtml_stylesheet $params > $output_file 2> $style_error"); } elsif ($style eq "PostScript") { my $tmp_output = "/tmp/output.$$"; my $tex_output = "$tmp_output.tex"; $output_file = "$output_prefix.ps"; system("$java $saxon $input $postscript_stylesheet $params > $tex_output 2> $style_error"); system("cd /tmp; $latex $tex_output > /dev/null 2> /dev/null"); system("$dvips -q $tmp_output -o $output_file"); delete_files("$tmp_output*"); } elsif ($style eq "PDF") { my $tmp_output = "/tmp/output.$$"; my $tex_output = "$tmp_output.tex"; my $ps_output = "$tmp_output.ps"; my $pdf_output = "$tmp_output.pdf"; $output_file = "$output_prefix.pdf"; system("$java $saxon $input $postscript_stylesheet $params > $tex_output 2> $style_error"); system("cd /tmp; $latex $tex_output > /dev/null 2> /dev/null"); system("$dvips -q $tmp_output -o $ps_output"); system("$ps2pdf $ps_output $pdf_output"); system("cp $pdf_output $output_file"); delete_files("$tmp_output*"); } elsif ($style eq "Gzipped PostScript") { my $tmp_output = "/tmp/output.$$"; my $tex_output = "$tmp_output.tex"; my $ps_output = "$tmp_output.ps"; $output_file = "$output_prefix.ps.gz"; system("$java $saxon $input $postscript_stylesheet $params > $tex_output 2> $style_error"); system("cd /tmp; $latex $tex_output > /dev/null 2> /dev/null"); system("$dvips -q $tmp_output -o $ps_output"); system("$gzip -c $ps_output > $output_file"); delete_files("$tmp_output*"); } else { # do something appropriate } open(STYLE_ERRORS, $style_error); @errors = ; close(STYLE_ERRORS); delete_files($style_error); return ( file => $output_file, errors => "@errors" ); } ############################################################################## # Code to send a report to the the maintainers, along with data about the # input to the CGI that caused the error sub send_error_report { open(MAIL, "| mail -t $error_report_address"); print MAIL "Subject: Internal Consistency Error in System I CGI\n\n"; print MAIL "Message:\n"; print MAIL "\n @_"; print MAIL "CGI called with:\n"; for($query->param) { print MAIL $_, " := ", (join(" ", $query->param("$_"))), "\n\n"; } print MAIL "Remote host := ", $query->remote_host(), "\n\n"; print MAIL "Remote addr := ", $query->remote_addr(), "\n\n"; print MAIL "Remote ident := ", $query->remote_ident(), "\n\n"; print MAIL "Remote user agent := ", $query->user_agent(), "\n\n"; close(MAIL); } ##############################################################################