Initial commit.
This commit is contained in:
parent
485e3c6f54
commit
e42f509f1d
100
Calc.thy
Normal file
100
Calc.thy
Normal file
@ -0,0 +1,100 @@
|
||||
theory
|
||||
Calc
|
||||
imports
|
||||
LexYacc
|
||||
begin
|
||||
|
||||
ml_lex_yacc
|
||||
with_lex\<open>
|
||||
structure Tokens = Tokens
|
||||
|
||||
type pos = int
|
||||
type svalue = Tokens.svalue
|
||||
type ('a,'b) token = ('a,'b) Tokens.token
|
||||
type lexresult= (svalue,pos) token
|
||||
|
||||
val pos = ref 0
|
||||
fun eof () = Tokens.EOF(!pos,!pos)
|
||||
fun error (e,l : int,_) = TextIO.output (TextIO.stdOut, String.concat[
|
||||
"line ", (Int.toString l), ": ", e, "\n"
|
||||
])
|
||||
|
||||
%%
|
||||
%header (functor CalcLexFun(structure Tokens: Calc_TOKENS));
|
||||
alpha=[A-Za-z];
|
||||
digit=[0-9];
|
||||
ws = [\ \t];
|
||||
%%
|
||||
\n => (pos := (!pos) + 1; lex());
|
||||
{ws}+ => (lex());
|
||||
{digit}+ => (Tokens.NUM (valOf (Int.fromString yytext), !pos, !pos));
|
||||
|
||||
"+" => (Tokens.PLUS(!pos,!pos));
|
||||
"*" => (Tokens.TIMES(!pos,!pos));
|
||||
";" => (Tokens.SEMI(!pos,!pos));
|
||||
{alpha}+ => (if yytext="print"
|
||||
then Tokens.PRINT(!pos,!pos)
|
||||
else Tokens.ID(yytext,!pos,!pos)
|
||||
);
|
||||
"-" => (Tokens.SUB(!pos,!pos));
|
||||
"^" => (Tokens.CARAT(!pos,!pos));
|
||||
"/" => (Tokens.DIV(!pos,!pos));
|
||||
"." => (error ("ignoring bad character "^yytext,!pos,!pos);
|
||||
lex());
|
||||
\<close>
|
||||
and_yacc\<open>
|
||||
(* Sample interactive calculator for ML-Yacc *)
|
||||
|
||||
fun lookup "bogus" = 10000
|
||||
| lookup s = 0
|
||||
|
||||
%%
|
||||
|
||||
%eop EOF SEMI
|
||||
|
||||
(* %pos declares the type of positions for terminals.
|
||||
Each symbol has an associated left and right position. *)
|
||||
|
||||
%pos int
|
||||
|
||||
%left SUB PLUS
|
||||
%left TIMES DIV
|
||||
%right CARAT
|
||||
|
||||
%term ID of string | NUM of int | PLUS | TIMES | PRINT |
|
||||
SEMI | EOF | CARAT | DIV | SUB
|
||||
%nonterm EXP of int | START of int option
|
||||
|
||||
%name Calc
|
||||
|
||||
%subst PRINT for ID
|
||||
%prefer PLUS TIMES DIV SUB
|
||||
%keyword PRINT SEMI
|
||||
|
||||
%noshift EOF
|
||||
%value ID ("bogus")
|
||||
%verbose
|
||||
%%
|
||||
|
||||
(* the parser returns the value associated with the expression *)
|
||||
|
||||
START : PRINT EXP (print (Int.toString EXP);
|
||||
print "\n";
|
||||
SOME EXP)
|
||||
| EXP (SOME EXP)
|
||||
| (NONE)
|
||||
EXP : NUM (NUM)
|
||||
| ID (lookup ID)
|
||||
| EXP PLUS EXP (EXP1+EXP2)
|
||||
| EXP TIMES EXP (EXP1*EXP2)
|
||||
| EXP DIV EXP (EXP1 div EXP2)
|
||||
| EXP SUB EXP (EXP1-EXP2)
|
||||
| EXP CARAT EXP (let fun e (m,0) = 1
|
||||
| e (m,l) = m*e(m,l-1)
|
||||
in e (EXP1,EXP2)
|
||||
end)
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
end
|
||||
91
LexYacc.thy
Normal file
91
LexYacc.thy
Normal file
@ -0,0 +1,91 @@
|
||||
theory LexYacc
|
||||
imports
|
||||
YaccLib
|
||||
keywords "ml_lex_yacc" :: thy_decl
|
||||
and "with_lex"::quasi_command
|
||||
and "and_yacc"::quasi_command
|
||||
|
||||
begin
|
||||
|
||||
section\<open>ML Lex\<close>
|
||||
SML_file \<open>mllex-polyml/LexGen.sml\<close>
|
||||
SML_export \<open>structure MlLexExe = struct val run = LexGen.lexGen end\<close>
|
||||
|
||||
section\<open>ML Yacc\<close>
|
||||
|
||||
SML_file\<open>mlyacc-polyml/src/utils.sig\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/utils.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/sigs.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/verbose.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/coreutils.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/grammar.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/graph.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/hdr.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/lalr.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/absyn.sig\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/absyn.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/core.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/look.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/mklrtable.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/shrink.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/yacc.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/mkprstruct.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/parse.sml\<close>
|
||||
|
||||
text\<open>Generated: \<close>
|
||||
SML_file\<open>mlyacc-polyml_bootstrapping/yacc.grm.sig\<close>
|
||||
|
||||
SML_file\<open>mlyacc-polyml_bootstrapping/yacc.grm.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml_bootstrapping/yacc.lex.sml\<close>
|
||||
text\<open>Final linking and export\<close>
|
||||
SML_file\<open>mlyacc-polyml/src/link.sml\<close>
|
||||
|
||||
SML_export \<open>structure MlYaccExe = struct val run = ParseGen.parseGen end\<close>
|
||||
|
||||
|
||||
section\<open>Glue Layer\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure MlLexYacc = struct
|
||||
|
||||
fun generate lex_input yacc_input thy =
|
||||
Isabelle_System.with_tmp_dir "lex_yacc" (fn input_path =>
|
||||
let
|
||||
val input_path = (Path.append input_path (Path.make ["input"]))
|
||||
val lex_file = Path.ext "lex" input_path
|
||||
val yacc_file = Path.ext "grm" input_path
|
||||
val _ = File.write lex_file lex_input
|
||||
val _ = File.write yacc_file yacc_input
|
||||
val _ = MlLexExe.run (File.platform_path lex_file)
|
||||
val _ = MlYaccExe.run (File.platform_path yacc_file)
|
||||
val lex_sml = File.read (Path.ext "lex.sml" input_path)
|
||||
val yacc_sig = File.read (Path.ext "grm.sig" input_path)
|
||||
val yacc_sml = File.read (Path.ext "grm.sml" input_path)
|
||||
val generated_code = yacc_sig^"\n\n"^lex_sml^"\n\n"^yacc_sml
|
||||
val toks =
|
||||
ML_Lex.read generated_code
|
||||
|> map (fn Antiquote.Text tok => tok
|
||||
| _ => error "Unexpected antiquote in generated code")
|
||||
val flags: ML_Compiler.flags =
|
||||
{environment = ML_Env.SML_export, redirect = false, verbose = true, catch_all = true,
|
||||
debug = NONE, writeln = writeln, warning = warning}
|
||||
val thy' = Context.theory_map (
|
||||
ML_Context.exec (fn () =>
|
||||
ML_Compiler.eval flags Position.none toks
|
||||
)
|
||||
) thy
|
||||
in
|
||||
thy'
|
||||
end);
|
||||
end
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val _ = Outer_Syntax.command @{command_keyword "ml_lex_yacc"}
|
||||
"Generate and load SML parser based on lex/yacc specifications."
|
||||
((\<^keyword>\<open>with_lex\<close> -- Parse.cartouche -- \<^keyword>\<open>and_yacc\<close> -- Parse.cartouche)
|
||||
>> (fn (((_,lex_spec), _), yacc_spec) =>
|
||||
Toplevel.theory (fn thy => MlLexYacc.generate lex_spec yacc_spec thy)))
|
||||
\<close>
|
||||
end
|
||||
11
YaccLib.thy
Normal file
11
YaccLib.thy
Normal file
@ -0,0 +1,11 @@
|
||||
theory
|
||||
YaccLib
|
||||
imports
|
||||
Main
|
||||
begin
|
||||
SML_file\<open>mlyacc-polyml/mlyacc-lib/base.sig\<close>
|
||||
SML_file\<open>mlyacc-polyml/mlyacc-lib/join.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/mlyacc-lib/lrtable.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/mlyacc-lib/stream.sml\<close>
|
||||
SML_file\<open>mlyacc-polyml/mlyacc-lib/parser2.sml\<close>
|
||||
end
|
||||
Loading…
Reference in New Issue
Block a user