Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / components / binaries / transcript / v8Parser.mly

diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly
index ff70df7138011031cbdbd5d74bf7db8ab1689712..969524d22e1b903c41b58f3f51c1c40d7104a6bc 100644 (file)
--- 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]                       }