X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Parser.mly;fp=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=969524d22e1b903c41b58f3f51c1c40d7104a6bc;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=ff70df7138011031cbdbd5d74bf7db8ab1689712;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly
index ff70df713..969524d22 100644
--- a/helm/software/components/binaries/transcript/v8Parser.mly
+++ b/helm/software/components/binaries/transcript/v8Parser.mly
@@ -35,7 +35,7 @@
    let cat x = String.concat " " x
 
    let mk_vars local idents =
-      let map ident = T.Inline (local, T.Var, trim ident, "") in
+      let map ident = T.Inline (local, T.Var, trim ident, "", None) in
       List.map map idents
 
    let strip2 s =
@@ -49,6 +49,16 @@
 
    let notation str =
       [T.Notation (false, str); T.Notation (true, str)]
+
+   let mk_flavour str =
+      match trim str with
+        | "Remark"     -> Some `Remark 
+        | "Lemma"      -> Some `Lemma
+        | "Theorem"    -> Some `Theorem
+        | "Definition" -> Some `Definition
+        | "Fixpoint"   -> Some `Definition
+        | "Let"        -> Some `Definition
+        | _            -> assert false
 %}
    %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
    %token <string> ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX REQ XP IP SET NOT LOAD ID COERC
@@ -277,59 +287,81 @@
    
    macro_step:
       | th ident restricts fs proof FS steps qed FS 
-         { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")]     }
+         { out "TH" $2;
+	   $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | th ident restricts fs proof restricts FS
-         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
+         { out "TH" $2; 
+	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | th ident restricts fs steps qed FS 
-         { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")]     }
+         { out "TH" $2;
+	   $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | th ident restricts def restricts FS
-         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
+         { out "TH" $2;
+	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | th ident def restricts FS
-         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
+         { out "TH" $2;
+	   [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | xlet ident restricts fs proof FS steps qed FS 
-         { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")]     }
+         { out "LET" $2;
+	   $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | xlet ident restricts fs proof restricts FS
-         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
+         { out "LET" $2;
+	   [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | xlet ident restricts fs steps qed FS 
-         { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")]     }
+         { out "LET" $2;
+	   $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | xlet ident restricts def restricts FS
-         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
+         { out "LET" $2;
+	   [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | xlet ident def restricts FS
-         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
+         { out "LET" $2;
+	   [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
+	 }
       | var idents xres FS
-         { out "VAR" (cat $2); mk_vars true $2                          }
+         { out "VAR" (cat $2); mk_vars true $2                      }
       | ax idents xres FS
-         { out "AX" (cat $2); mk_vars false $2                          }
+         { out "AX" (cat $2); mk_vars false $2                      }
       | ind ident unexports FS
-         { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 }
+         { out "IND" $2;
+	   T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
+	 }
       | sec ident FS
-         { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]           }
+         { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
       | xend ident FS
-         { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]          }
+         { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]      }
       | unx unexports FS 
-         { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)]     }
+         { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
       | req xp ident FS
-         { out "REQ" $3; [T.Include (trim $3)]                          }
+         { out "REQ" $3; [T.Include (trim $3)]                      }
       | req ip ident FS
-         { out "REQ" $3; [T.Include (trim $3)]                          }
+         { out "REQ" $3; [T.Include (trim $3)]                      }
       | req ident FS
-         { out "REQ" $2; [T.Include (trim $2)]                          } 
+         { out "REQ" $2; [T.Include (trim $2)]                      } 
       | load str FS
-         { out "REQ" $2; [T.Include (strip2 (trim $2))]                 }
+         { out "REQ" $2; [T.Include (strip2 (trim $2))]             }
       | coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $2); coercion (hd $2)                       }
+         { out "COERCE" (hd $2); coercion (hd $2)                   }
       | id coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $3); coercion (hd $3)                       }
+         { out "COERCE" (hd $3); coercion (hd $3)                   }
       | th ident error 
-         { out "ERROR" $2; failwith ("macro_step " ^ $2)                }
+         { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
       | ind ident error 
-         { out "ERROR" $2; failwith ("macro_step " ^ $2)                }
+         { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
       | var idents error 
          { let vs = cat $2 in
-	   out "ERROR" vs; failwith ("macro_step " ^ vs)                }
+	   out "ERROR" vs; failwith ("macro_step " ^ vs)            }
       | ax idents error 
          { let vs = cat $2 in
-	   out "ERROR" vs; failwith ("macro_step " ^ vs)                }
+	   out "ERROR" vs; failwith ("macro_step " ^ vs)            }
    ;
    item:
       | OQ verbatims CQ       { [T.Comment $2]                       }