Commit dd4ed2a6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs (en cours)

parent 2e8cce67
...@@ -24,6 +24,14 @@ type error = ...@@ -24,6 +24,14 @@ type error =
exception Error of error exception Error of error
(** parsing entry points *)
val parse_list0_decl : Lexing.lexbuf -> Ptree.decl list
val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
(** other functions to be re-used in other lexers/parsers *)
val newline : Lexing.lexbuf -> unit val newline : Lexing.lexbuf -> unit
val comment : Lexing.lexbuf -> unit val comment : Lexing.lexbuf -> unit
...@@ -32,8 +40,6 @@ val string : Lexing.lexbuf -> string ...@@ -32,8 +40,6 @@ val string : Lexing.lexbuf -> string
val report : Format.formatter -> error -> unit val report : Format.formatter -> error -> unit
val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
val remove_leading_plus : string -> string val remove_leading_plus : string -> string
val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a
...@@ -236,9 +236,9 @@ and string = parse ...@@ -236,9 +236,9 @@ and string = parse
| e -> raise (Loc.Located (loc lb, e)) | e -> raise (Loc.Located (loc lb, e))
let parse_lexpr = with_location (lexpr token) let parse_lexpr = with_location (lexpr token)
let parse_list0_decl = with_location (list0_decl token)
let parse_logic_file = with_location (logic_file token) let parse_logic_file = with_location (logic_file token)
let lexpr_of_string s = parse_lexpr (from_string s)
} }
(* (*
......
...@@ -110,6 +110,8 @@ ...@@ -110,6 +110,8 @@
%type <Ptree.lexpr> lexpr %type <Ptree.lexpr> lexpr
%start lexpr %start lexpr
%type <Ptree.decl list> list0_decl
%start list0_decl
%type <Ptree.logic_file> logic_file %type <Ptree.logic_file> logic_file
%start logic_file %start logic_file
%% %%
......
...@@ -170,7 +170,9 @@ rule token = parse ...@@ -170,7 +170,9 @@ rule token = parse
| "]" | "]"
{ RIGHTSQ } { RIGHTSQ }
| "{" | "{"
{ logic_start_loc := loc lexbuf; LOGIC (logic lexbuf) } { logic_start_loc := loc lexbuf;
let s = logic lexbuf in
LOGIC (snd !logic_start_loc, s) }
| "{{" | "{{"
{ LEFTBLEFTB } { LEFTBLEFTB }
| "}}" | "}}"
......
...@@ -76,6 +76,13 @@ ...@@ -76,6 +76,13 @@
in in
{ e with pdesc = Spost (e, (q, []), Transparent) } { e with pdesc = Spost (e, (q, []), Transparent) }
***) ***)
let parse_string f loc s =
let lb = Lexing.from_string s in
f lb
let logic_list0_decl = parse_string Lexer.parse_list0_decl
%} %}
/* Tokens */ /* Tokens */
...@@ -85,7 +92,7 @@ ...@@ -85,7 +92,7 @@
%token <string> OP0 OP1 OP2 OP3 %token <string> OP0 OP1 OP2 OP3
%token <Ptree.real_constant> FLOAT %token <Ptree.real_constant> FLOAT
%token <string> STRING %token <string> STRING
%token <string> LOGIC %token <Lexing.position * string> LOGIC
/* keywords */ /* keywords */
...@@ -160,8 +167,9 @@ list1_decl: ...@@ -160,8 +167,9 @@ list1_decl:
; ;
decl: decl:
| LIDENT | LOGIC
{ LogicDecl [] } { let l, s = $1 in
LogicDecl (logic_list0_decl l s) }
; ;
/***** /*****
......
...@@ -3,6 +3,8 @@ ...@@ -3,6 +3,8 @@
{ } { }
{ tagada }
(* (*
Local Variables: Local Variables:
compile-command: "unset LANG; make -C ../.. testl" compile-command: "unset LANG; make -C ../.. testl"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment