New flag GDV + epsilon terms + annotations (#51)

* Parsing (and typing) of espilon-terms in TPTP input files

(TPTP syntax # [ X ] : ... )

* Producing an annotation term for TPTP input

* WIP finding the name of a Skolem symbol from annotations

* Add annotation.ml to Makefile

* New flag -gdv instead of flag -lp-package

Author: gburel

Makefile

@@ -22,7 +22,7 @@ VERSION = $(VERSION_MAJOR).$(VERSION_MINOR).$(VERSION_BUGFIX)
 # modules in linking order.
 
 SOURCES = log.ml version.ml config.dummy misc.ml heap.ml globals.ml error.ml \
-          progress.ml namespace.ml expr.ml \
+          progress.ml namespace.ml annotation.ml expr.ml \
           phrase.ml llproof.ml mlproof.ml index.ml print.ml \
 	  watch.ml eqrel.ml \
 	  rewrite.ml typer.ml \

annotation.ml

@@ -0,0 +1,5 @@
+type annotation =
+  Atom of string
+| Fun of string * annotation list
+| List of annotation list
+| Colon of annotation * annotation

annotation.mli

@@ -0,0 +1,6 @@
+type annotation =
+  Atom of string
+| Fun of string * annotation list
+| List of annotation list
+| Colon of annotation * annotation
+

globals.ml

@@ -31,7 +31,7 @@ let debug_rwrt = ref false;;
 
 let output_sig = ref false;;
 let signature_name = ref "";;
-let lp_package = ref "";;
+let gdv = ref false;;
 let conjecture = ref "";;
 let check_axiom = ref false;;
 let szs = ref false;;

globals.mli

@@ -31,7 +31,7 @@ val debug_rwrt : bool ref;;
 
 val output_sig : bool ref;;
 val signature_name : string ref;;
-val lp_package : string ref;;
+val gdv : bool ref;;
 val conjecture : string ref;;
 val check_axiom : bool ref;;
 val szs : bool ref;;

lextptp.mll

@@ -57,6 +57,7 @@ rule token = parse
   | "."              { DOT }
   | "?"              { EX }
   | "!"              { ALL }
+  | "#"              { HASH }
   | "~"              { NOT }
   | "|"              { OR }
   | "&"              { AND }

lltolp.ml

@@ -1061,13 +1061,10 @@ let output_term oc phrases _ llp =
   let dkproof = make_proof_term (List.hd goal) prooftree in
   fprintf oc "require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL \
               Logic.Zenon.Main;\n";
-  if !Globals.lp_package <> "" then begin
-    fprintf oc "require %s.Signature as S;\n" !Globals.lp_package;
-    fprintf oc "require %s.Formulae as F;\n" !Globals.lp_package;
+  if !Globals.gdv then
     fprintf oc "\nrule F.%s ↪ " goal_name
-  end
   else
-  fprintf oc "\nsymbol %s ≔ " goal_name;
+    fprintf oc "\nsymbol %s ≔ " goal_name;
   if !Globals.conjecture <> "" then
     fprintf oc "λ __negated_conjecture_proof__,";
   begin

lpprint.ml

@@ -112,7 +112,7 @@ and print_dk_cst typ o (t, var_context) =
     if Mltoll.is_meta s then fprintf o "select (%a)" print_dk_zentype_aux (typ, var_context)
     else
        begin
-         fprintf o (if !Globals.lp_package = "" then "%s"
+         fprintf o (if !Globals.gdv then "%s"
                     else if is_formula then "F.%s"
                     else "S.%s")
            (escape_name s);

main.ml

@@ -217,8 +217,8 @@ let argspec = [
         "               print the proof in Dk script format (force -rename)";
   "-sig", Arg.String (fun s -> Globals.signature_name := s),
               "<n>            set the module path of the signature";
-  "-lp-package", Arg.String (fun s -> Globals.lp_package := s),
-              "<n>            set the module path for lambdapi";
+  "-gdv", Arg.Set Globals.gdv,
+              " use the format expected by GDV for the lambdapi output";
   "-odkterm", Arg.Unit (fun () -> proof_level := Proof_dkterm;
 				  opt_level := 0;
 				  Globals.output_dk := true),

parsetptp.mly

@@ -4,6 +4,7 @@
 Version.add "$Id: parsetptp.mly,v 1.9 2012-04-24 17:32:04 doligez Exp $";;
 
 open Expr;;
+open Annotation
 
 let ns pre s = (if !Globals.namespace_flag then pre else "") ^ s;;
 (* Renaming is now done during typechecking *)
@@ -73,6 +74,7 @@ let cnf_to_formula l =
 %token XOR
 %token NOR
 %token NAND
+%token HASH
 %token <string> ANNOT
 
 %nonassoc OPEN
@@ -100,55 +102,53 @@ phrase:
   | INCLUDE OPEN LIDENT COMMA LBRACKET name_list RBRACKET CLOSE DOT
                                    { Phrase.Include ($3, Some ($6)) }
   | INPUT_FORMULA OPEN name COMMA LIDENT COMMA formula annotations CLOSE DOT
-                                   { Phrase.Formula (ns_hyp $3, $5, $7, None) }
+                                   { Phrase.Formula (ns_hyp $3, $5, $7, $8) }
   | INPUT_CLAUSE OPEN name COMMA LIDENT COMMA cnf_formula annotations CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, $5, cnf_to_formula $7, None) }
-  | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula COMMA LIDENT annotations CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, Some $9) }
+      { Phrase.Formula (ns_hyp $3, $5, cnf_to_formula $7, $8) }
   | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA formula annotations CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
+     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, $8) }
   | INPUT_TFF_FORMULA OPEN name COMMA LIDENT COMMA type_def annotations CLOSE DOT
-     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, None) }
+     { Phrase.Formula (ns_hyp $3, "tff_" ^ $5, $7, $8) }
   | ANNOT                          { Phrase.Annotation $1 }
 ;
 annotations:
-  | {}
-  | COMMA source optional_info {}
+  | {None}
+  | COMMA source optional_info {Some $2}
 ;
 
 source:
-general_term {}
+general_term {$1}
 ;
 
 general_term:
-general_data {}
-  | general_data COLON general_term {}
-  | general_list {}
+general_data {$1}
+  | general_data COLON general_term {Colon ($1, $3)}
+  | general_list {List $1}
 ;
 
 general_data:
-LIDENT {}
-  | general_function {}
-  | UIDENT {}
-  | INT {}
-  | RAT {}
-  | REAL {}
-  | STRING {}
+LIDENT {Atom $1}
+  | general_function {$1}
+  | UIDENT {Atom $1}
+  | INT {Atom $1}
+  | RAT {Atom $1}
+  | REAL {Atom $1}
+  | STRING {Atom $1}
 /* | formula_data {} unsupported */
 ;
 
 general_function:
-LIDENT OPEN general_terms CLOSE {}
+LIDENT OPEN general_terms CLOSE {Fun ($1, $3)}
 ;
 
 general_terms:
-general_term {}
-  | general_term COMMA general_terms {}
+general_term { [$1] }
+  | general_term COMMA general_terms {$1::$3}
 ;
 
 general_list:
-LBRACKET RBRACKET {}
-  | LBRACKET general_terms RBRACKET {}
+LBRACKET RBRACKET {[]}
+  | LBRACKET general_terms RBRACKET {$2}
 ;
 
 optional_info:
@@ -168,6 +168,7 @@ expr:
   | expr EQSYM expr                    { eeq $1 $3 }
   | expr NEQSYM expr                   { enot (eeq $1 $3) }
   | OPEN expr CLOSE                    { $2 }
+  | HASH LBRACKET var_list RBRACKET COLON unit_formula { etau (List.hd $3, $6) }
 ;
 arguments:
   | OPEN expr_list CLOSE         { $2 }