From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Dec 2010 22:58:13 +0000 (+0000)
Subject: Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable
X-Git-Tag: make_still_working~2652
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e7e01cd771c07b3605ba54d3853ac34a02cb86d;p=helm.git

Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable
in order to localize all Obj.magic --- related to use of Ulexing in Camlp5 ---
in GrafiteParser (as they used to be).
---

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 8c2cbf909..9b5ecfe7c 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -42,6 +42,12 @@ let exc_located_wrapper f =
       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))
diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli
index ea4d43a62..ec5cdbb21 100644
--- a/matita/components/grafite_parser/grafiteParser.mli
+++ b/matita/components/grafite_parser/grafiteParser.mli
@@ -47,4 +47,6 @@ val extend : #status as 'status ->
  (* 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
diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 4429f9636..185b0ed1f 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -249,10 +249,9 @@ and compile ~compiling ~include_paths fname =
         (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 _ _ -> ())
diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 856805db8..5bbac3e2b 100644
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -30,7 +30,7 @@ exception FailureCompiling of string * exn
 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
diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 3a73d6ce6..b84180037 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -193,9 +193,9 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff
     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
@@ -665,9 +665,9 @@ object (self)
   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
diff --git a/matita/matita/nlibrary/Plogic/connectives.ma b/matita/matita/nlibrary/Plogic/connectives.ma
index dd3b967cb..a58c06386 100644
--- a/matita/matita/nlibrary/Plogic/connectives.ma
+++ b/matita/matita/nlibrary/Plogic/connectives.ma
@@ -29,15 +29,15 @@ nmk: (A → False) → Not A.
 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.
@@ -45,11 +45,11 @@ inductive And (A,B:Prop) : Prop ≝
 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 ≝
diff --git a/matita/matita/nlibrary/Plogic/equality.ma b/matita/matita/nlibrary/Plogic/equality.ma
index 615151d14..4195c06f6 100644
--- a/matita/matita/nlibrary/Plogic/equality.ma
+++ b/matita/matita/nlibrary/Plogic/equality.ma
@@ -21,43 +21,43 @@ interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 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.
@@ -76,10 +76,10 @@ definition R2 :
   ∀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 :
@@ -99,10 +99,10 @@ 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 :
@@ -134,10 +134,10 @@ 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.