THF parser received some care

[helm.git] / helm / software / components / tptp_grafite / parserTHF.mly

diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly
index 35bc870ccb5cad5b9164d8b4f2d5204168a889dd..195b79f8de924c1f62ef96892190330de57503fe 100644 (file)
--- a/helm/software/components/tptp_grafite/parserTHF.mly
+++ b/helm/software/components/tptp_grafite/parserTHF.mly
@@ -7,6 +7,17 @@
   
   let parse_error s = Printf.eprintf "%s: " s ;;
   let rm_q s = String.sub s 1 (String.length s - 2) ;;
+
+let reserved = [
+  "in","In";
+  "to","To";
+  "theorem","Theorem";
+];;
+
+let unreserve k =
+  try List.assoc k reserved with Not_found -> k
+;;
+
   
 %}
   %token <string> TYPE
@@ -78,10 +89,19 @@
   ;
 
   annot_formula: 
-    | THF LPAREN 
-            name COMMA formula_type COMMA term formula_source_and_infos 
-          RPAREN DOT {
-            Formula($3,$5,$7)  
+    | THF LPAREN name COMMA formula_type COMMA 
+      term formula_source_and_infos RPAREN DOT {
+         match $5 with
+         | Definition ->
+             (match $7 with
+             | T.Appl [T.Symbol("Eq",_);T.Ident(name,_);body] -> 
+                   ThfDefinition($3,unreserve name,body)
+             | _ -> prerr_endline ("near " ^ $3); assert false)
+         | Type -> 
+             (match $7 with
+             | T.Cast (T.Ident(name,_),ty) -> ThfType($3,unreserve name,ty)
+             | _ -> assert false)
+         | _ -> ThfFormula($3,$5,$7)  
       }
   ;
   
@@ -109,8 +129,8 @@
     | LAMBDA {`Lambda}
 
   vardecl : 
-    | UNAME { T.Implicit `JustOne,Some (T.Ident($1,None)) }
-    | UNAME COLON term { $3,Some (T.Ident($1,None)) }
+    | UNAME { T.Ident($1,None), None }
+    | UNAME COLON term { T.Ident($1,None),Some $3 }
    
   varlist : 
     | vardecl { [$1] } 
@@ -120,30 +140,26 @@
     | quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
         List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
         }
-    | term IMPLY term { 
-        match $1 with 
-        | T.Appl l -> T.Appl (l @ [$3])
-        | x -> T.Appl ([$1; $3]) 
-    }
     | term APPLY term { 
         match $1 with 
         | T.Appl l -> T.Appl (l @ [$3])
         | x -> T.Appl ([$1; $3]) 
     }
     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
-    | term TO term { T.Binder (`Pi,($1,None),$3) }
-    | term IEQ term { T.Appl [T.Symbol("'eq",0);$1;$3] }
-    | term IAND term { T.Appl [T.Symbol("'and",0);$1;$3] }
-    | term IOR term { T.Appl [T.Symbol("'or",0);$1;$3] }
-    | NOT term { T.Appl [T.Symbol("'not",0);$2] }
+    | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+    | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+    | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+    | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
+    | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
+    | NOT term { T.Appl [T.Symbol("Not",0);$2] }
     | LPAREN term RPAREN {$2}
-    | LNAME { T.Ident($1,None) }
+    | LNAME { T.Ident(unreserve $1,None) }
     | UNAME { T.Ident($1,None) }
-    | TYPE_I { T.Symbol("'i",0) }
-    | TYPE_O { T.Symbol("'o",0) }
-    | TYPE_U { T.Sort `Set }
-    | FALSE { T.Symbol("'false",0)}
-    | TRUE { T.Symbol("'true",0)}
+    | TYPE_I { T.Symbol("i",0) }
+    | TYPE_O { T.Symbol("o",0) }
+    | TYPE_U { T.Sort (`NType "0") }
+    | FALSE { T.Symbol("False",0)}
+    | TRUE { T.Symbol("True",0)}
   ;
 
   include_: