raise (HExtlib.Localized
(floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
+type parsable = Grammar.parsable
+
+let parsable_statement status buf =
+ let grammar = CicNotationParser.level2_ast_grammar status in
+ Grammar.parsable grammar (Obj.magic buf)
+
let parse_statement grafite_parser parsable =
exc_located_wrapper
(fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) parsable))
(* never_include: do not call LexiconEngine to do includes,
* always raise NoInclusionPerformed *)
(** @raise End_of_file *)
-val parse_statement: #status -> Grammar.parsable -> GrafiteAst.statement
+type parsable
+val parsable_statement: #status -> Ulexing.lexbuf -> parsable
+val parse_statement: #status -> parsable -> GrafiteAst.statement
(Filename.dirname
(Http_getter.filename ~local:true ~writable:true (baseuri ^
"foo.con")));
- let grammar = CicNotationParser.level2_ast_grammar grafite_status in
let buf =
- Grammar.parsable grammar
- (Obj.magic (Ulexing.from_utf8_channel (open_in fname)))
+ GrafiteParser.parsable_statement grafite_status
+ (Ulexing.from_utf8_channel (open_in fname))
in
let print_cb =
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
exception CircularDependency of string
val get_ast:
- GrafiteTypes.status -> include_paths:string list -> Grammar.parsable ->
+ GrafiteTypes.status -> include_paths:string list -> GrafiteParser.parsable ->
GrafiteAst.statement
(* heavy checks slow down the compilation process but give you some interesting
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
- let grammar = CicNotationParser.level2_ast_grammar grafite_status in
let strm =
- Grammar.parsable grammar (Obj.magic(Ulexing.from_utf8_string text)) in
+ GrafiteParser.parsable_statement grafite_status
+ (Ulexing.from_utf8_string text) in
let ast = MatitaEngine.get_ast grafite_status include_paths strm in
ast, text
| `Ast (st, text) -> st, text
method eos =
let rec is_there_only_comments lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let grammar = CicNotationParser.level2_ast_grammar lexicon_status in
let strm =
- Grammar.parsable grammar (Obj.magic(Ulexing.from_utf8_string s)) in
+ GrafiteParser.parsable_statement lexicon_status
+ (Ulexing.from_utf8_string s)in
match GrafiteParser.parse_statement lexicon_status strm with
| GrafiteAst.Comment (loc,_) ->
let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
interpretation "logical not" 'not x = (Not x).
theorem absurd : ∀ A:Prop. A → ¬A → False.
-#A; #H; #Hn; elim Hn;/2/; qed.
+#A #H #Hn elim Hn /2/ qed.
(*
ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
-#A; #C; #H; #Hn; nelim (Hn H).
+#A #C #H #Hn nelim (Hn H).
nqed. *)
theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
-/4/; qed.
+/4/ qed.
inductive And (A,B:Prop) : Prop ≝
conj : A → B → And A B.
interpretation "logical and" 'and x y = (And x y).
theorem proj1: ∀A,B:Prop. A ∧ B → A.
-#A; #B; #AB; elim AB; //.
+#A #B #AB elim AB //.
qed.
theorem proj2: ∀ A,B:Prop. A ∧ B → B.
-#A; #B; #AB; elim AB; //.
+#A #B #AB elim AB //.
qed.
inductive Or (A,B:Prop) : Prop ≝
lemma eq_rect_r:
∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p.
- #A; #a; #x; #p; cases p; #P; #H; assumption.
+ #A #a #x #p cases p #P #H assumption.
qed.
lemma eq_ind_r :
∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; apply (eq_rect_r ? ? ? p0); assumption.
+ #A #a #P #p #x0 #p0 apply (eq_rect_r ? ? ? p0) assumption.
qed.
lemma eq_rect_Type2_r :
∀A:Type[0].∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
- #A;#a;#P;#H;#x;#p;generalize in match H;generalize in match P;
- cases p;//;
+ #A #a #P #H #x #p generalize in match H generalize in match P
+ cases p //
qed.
(*
nlemma eq_ind_r :
∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
- #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
-ncases p0; #Heq; nassumption.
+ #A #a #P #p #x0 #p0 ngeneralize in match p
+ncases p0 #Heq nassumption.
nqed.
*)
theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
-#A; #x; #P; #Hx; #y; #Heq;cases Heq;assumption.
+#A #x #P #Hx #y #Heq cases Heq assumption.
qed.
theorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
-#A; #x; #y; #Heq; apply (rewrite_l A x (λz.z=x));
+#A #x #y #Heq apply (rewrite_l A x (λz.z=x))
[ % | assumption ]
qed.
theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
-#A; #x; #P; #Hx; #y; #Heq; cases (sym_eq ? ? ?Heq); assumption.
+#A #x #P #Hx #y #Heq cases (sym_eq ? ? ?Heq) assumption.
qed.
theorem eq_coerc: ∀A,B:Type[1].A→(A=B)→B.
-#A; #B; #Ha; #Heq;elim Heq; assumption.
+#A #B #Ha #Heq elim Heq assumption.
qed.
definition R0 ≝ λT:Type[0].λt:T.t.
∀b1: T1 b0 e0.
∀e1:R1 ?? T1 a1 ? e0 = b1.
T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
-apply (eq_rect_Type0 ????? e1);
-apply (R1 ?? ? ?? e0);
-apply a2;
+#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
+apply (eq_rect_Type0 ????? e1)
+apply (R1 ?? ? ?? e0)
+apply a2
qed.
definition R3 :
∀b2: T2 b0 e0 b1 e1.
∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
-apply (eq_rect_Type0 ????? e2);
-apply (R2 ?? ? ???? e0 ? e1);
-apply a3;
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
+apply (eq_rect_Type0 ????? e2)
+apply (R2 ?? ? ???? e0 ? e1)
+apply a3
qed.
definition R4 :
∀b3: T3 b0 e0 b1 e1 b2 e2.
∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
T4 b0 e0 b1 e1 b2 e2 b3 e3.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
-apply (eq_rect_Type0 ????? e3);
-apply (R3 ????????? e0 ? e1 ? e2);
-apply a4;
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
+apply (eq_rect_Type0 ????? e3)
+apply (R3 ????????? e0 ? e1 ? e2)
+apply a4
qed.
-axiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
\ No newline at end of file
+axiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
projects / helm.git / commitdiff