X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fv8Parser.mly;h=ff70df7138011031cbdbd5d74bf7db8ab1689712;hb=137a822662f81efbbeac7ddc833fc9ffe252a70e;hp=9529bfb62529024897bd2f71c668727e4d9b436c;hpb=c5e25191f05bb2662fc738bfb2742eb03b941510;p=helm.git

diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly
index 9529bfb62..ff70df713 100644
--- a/helm/software/components/binaries/transcript/v8Parser.mly
+++ b/helm/software/components/binaries/transcript/v8Parser.mly
@@ -28,10 +28,14 @@
    
    let out t s = () (* prerr_endline ("-- " ^ t ^ " " ^ s) *)
 
+   let trim = HExtlib.trim_blanks
+
+   let hd = List.hd
+
    let cat x = String.concat " " x
 
-   let mk_vars idents =
-      let map ident = T.Inline (T.Var, ident) in
+   let mk_vars local idents =
+      let map ident = T.Inline (local, T.Var, trim ident, "") in
       List.map map idents
 
    let strip2 s =
@@ -40,10 +44,14 @@
    let strip1 s = 
       String.sub s 1 (String.length s - 1)
 
-   let hd = List.hd
+   let coercion str = 
+      [T.Coercion (false, str); T.Coercion (true, str)]
+
+   let notation str =
+      [T.Notation (false, str); T.Notation (true, str)]
 %}
    %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
-   %token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
+   %token <string> ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX REQ XP IP SET NOT LOAD ID COERC
    %token EOF
    
    %start items
@@ -64,16 +72,38 @@
      |           { ""      }
      | SPC rspcs { $1 ^ $2 }
    ;
+   xident:
+      | IDENT { $1 }
+      | LET   { $1 }
+      | TH    { $1 }
+      | QED   { $1 }
+      | PROOF { $1 }
+      | VAR   { $1 }
+      | AX    { $1 }
+      | IND   { $1 }
+      | SEC   { $1 }
+      | END   { $1 }
+      | UNX   { $1 }
+      | REQ   { $1 }
+      | LOAD  { $1 }
+      | NOT   { $1 }
+      | ID    { $1 }
+      | COERC { $1 }
+   ;
    fs: FS spcs { $1 ^ $2 };
-   ident: IDENT spcs { $1 ^ $2 };
+   ident: xident spcs { $1 ^ $2 };
    th: TH spcs { $1 ^ $2 };
+   xlet: LET spcs { $1 ^ $2 };
    proof: PROOF spcs { $1 ^ $2 };
    qed: QED spcs { $1 ^ $2 };
    sec: SEC spcs { $1 ^ $2 };
+   xend: END spcs { $1 ^ $2 };
+   unx: UNX spcs { $1 ^ $2 };
    def: DEF spcs { $1 ^ $2 };
    op: OP spcs { $1 ^ $2 };
-   xlet: LET spcs { $1 ^ $2 };
+   abbr: ABBR spcs { $1 ^ $2 };
    var: VAR spcs { $1 ^ $2 };
+   ax: AX spcs { $1 ^ $2 };
    req: REQ spcs { $1 ^ $2 };
    load: LOAD spcs { $1 ^ $2 };
    xp: XP spcs { $1 ^ $2 };
@@ -89,7 +119,6 @@
    id: ID spcs { $1 ^ $2 };
    coerc: COERC spcs { $1 ^ $2 };
 
-
    idents:
       | ident        { [$1]     }
       | ident idents { $1 :: $2 }
@@ -114,7 +143,7 @@
       | CC               { $1           }
       | COE              { $1           }
       | STR              { $1           }   
-      | xlet extends0 IN { $1 ^ $2 ^ $3 }
+      | abbr extends0 IN { $1 ^ $2 ^ $3 }
       | op extends1 CP   { $1 ^ $2 ^ $3 }
       
    ;
@@ -168,7 +197,7 @@
       | COE   { $1 }
       | STR   { $1 }   
       | OP    { $1 }
-      | LET   { $1 }
+      | ABBR  { $1 }
       | IN    { $1 }
       | CP    { $1 }
       | DEF   { $1 }
@@ -187,8 +216,10 @@
       | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } 
    ;
    field: 
-      | ident cn unexports_r  { $1 ^ $2 ^ fst $3, snd $3                   }
-      | ident coe unexports_r { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion $1] }
+      | ident cn unexports_r  
+         { $1 ^ $2 ^ fst $3, snd $3                      }
+      | ident coe unexports_r 
+         { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
    ;  
    fields:
       | field           { $1                                      }
@@ -211,9 +242,13 @@
       | CC          { $1 }
       | SC          { $1 }
       | TH          { $1 }       
+      | LET         { $1 }       
       | VAR         { $1 }
+      | AX          { $1 }
       | IND         { $1 }
       | SEC         { $1 }
+      | END         { $1 }
+      | UNX         { $1 }
       | REQ         { $1 } 
       | XP          { $1 } 
       | IP          { $1 } 
@@ -236,53 +271,72 @@
    ;
    
    qid:
-      | IDENT  { [$1]            }
+      | xident { [$1]            }
       | qid AC { strip1 $2 :: $1 }
    ;
    
    macro_step:
       | th ident restricts fs proof FS steps qed FS 
-         { out "TH" $2; $7 @ [T.Inline (T.Con, $2)]            }
+         { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")]     }
       | th ident restricts fs proof restricts FS
-         { out "TH" $2; [T.Inline (T.Con, $2)]                 }
+         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
       | th ident restricts fs steps qed FS 
-         { out "TH" $2; $5 @ [T.Inline (T.Con, $2)]            }
+         { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")]     }
       | th ident restricts def restricts FS
-         { out "TH" $2; [T.Inline (T.Con, $2)]                 }
+         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
       | th ident def restricts FS
-         { out "TH" $2; [T.Inline (T.Con, $2)]                 }
+         { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
+      | xlet ident restricts fs proof FS steps qed FS 
+         { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")]     }
+      | xlet ident restricts fs proof restricts FS
+         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
+      | xlet ident restricts fs steps qed FS 
+         { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")]     }
+      | xlet ident restricts def restricts FS
+         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
+      | xlet ident def restricts FS
+         { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
       | var idents xres FS
-         { out "VAR" (cat $2); mk_vars $2                      }      
+         { out "VAR" (cat $2); mk_vars true $2                          }
+      | ax idents xres FS
+         { out "AX" (cat $2); mk_vars false $2                          }
       | ind ident unexports FS
-         { out "IND" $2; snd $3 @ [T.Inline (T.Ind, $2)]       }
-      | sec unexports FS 
-         { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ $3)] }
+         { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 }
+      | sec ident FS
+         { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]           }
+      | xend ident FS
+         { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]          }
+      | unx unexports FS 
+         { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)]     }
       | req xp ident FS
-         { out "REQ" $3; [T.Include $3]                        }
+         { out "REQ" $3; [T.Include (trim $3)]                          }
       | req ip ident FS
-         { out "REQ" $3; [T.Include $3]                        }
+         { out "REQ" $3; [T.Include (trim $3)]                          }
       | req ident FS
-         { out "REQ" $2; [T.Include $2]                        } 
+         { out "REQ" $2; [T.Include (trim $2)]                          } 
       | load str FS
-         { out "REQ" $2; [T.Include (strip2 $2)]               }
+         { out "REQ" $2; [T.Include (strip2 (trim $2))]                 }
       | coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $2); [T.Coercion (hd $2)]          }
+         { out "COERCE" (hd $2); coercion (hd $2)                       }
       | id coerc qid spcs cn unexports FS
-         { out "COERCE" (hd $3); [T.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)                }
    ;
    item:
-      | comment               { [T.Comment $1]                      }
-      | macro_step            { $1                                  }
-      | set unexports FS      { [T.Unexport ($1 ^ fst $2 ^ $3)]     }
-      | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ $3)]     }
-      | error                 { out "ERROR" "item"; failwith "item" }
+      | OQ verbatims CQ       { [T.Comment $2]                       }
+      | macro_step            { $1                                   }
+      | set unexports FS      { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
+      | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3)     }
+      | error                 { out "ERROR" "item"; failwith "item"  }
     ;
     items:
       | rspcs EOF        { []      }