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
%token IOR
%token NIEQ
%token IEQ
+ %token XOR
%token IMPLY
+ %token IMPLYLR
+ %token COIMPLY
%token PEQ
%token DOT
%token EOF
;
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)
}
;
| 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] }
| 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 IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
+ | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
+ | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
+ | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+ | term NIEQ term { T.Appl [T.Symbol("NotEq",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_: