Commit c4f73c2c authored by POTTIER Francois's avatar POTTIER Francois

Introduced [Lr1.fold_entry].

Used it in three places in the table back-end and the code back-end.
parent c4af203f
......@@ -260,12 +260,9 @@ module Run (T: sig end) = struct
let write_start_nt f =
fprintf f "Definition start_nt (init:initstate) : nonterminal :=\n";
fprintf f " match init with\n";
ProductionMap.iter (fun prod node ->
match Production.rhs prod with
| [| Symbol.N startnt |] ->
fprintf f " | %s => %s\n" (print_init node) (print_nterm startnt)
| _ -> assert false
) Lr1.entry;
Lr1.fold_entry (fun _prod node startnt _t () ->
fprintf f " | %s => %s\n" (print_init node) (print_nterm startnt)
) ();
fprintf f " end.\n\n"
let write_actions f =
......@@ -435,9 +432,7 @@ module Run (T: sig end) = struct
fprintf f "Proof eq_refl true<:Parser.complete_validator () = true.\n\n";
end;
ProductionMap.iter (fun prod node ->
match Production.rhs prod with
| [| Symbol.N startnt |] ->
Lr1.fold_entry (fun _prod node startnt _t () ->
let funName = Nonterminal.print true startnt in
fprintf f "Definition %s := Parser.parse safe Aut.%s.\n\n"
funName (print_init node);
......@@ -466,7 +461,7 @@ module Run (T: sig end) = struct
fprintf f " end.\n";
fprintf f "Proof. apply Parser.parse_complete with (init:=Aut.%s); exact complete. Qed.\n\n" (print_init node);
end
| _ -> assert false) Lr1.entry
) ()
let write_all f =
if not Settings.coq_no_actions then
......
......@@ -1089,3 +1089,25 @@ let default_conflict_resolution () =
else if !ambiguities > 1 then
Error.grammar_warning [] (Printf.sprintf "%d states have an end-of-stream conflict." !ambiguities)
(* ------------------------------------------------------------------------ *)
(* Define [fold_entry], which in some cases facilitates the use of [entry]. *)
let fold_entry f accu =
ProductionMap.fold (fun prod state accu ->
let nt : Nonterminal.t =
match Production.classify prod with
| Some nt ->
nt
| None ->
assert false (* this is a start production *)
in
let t : Stretch.ocamltype =
match Nonterminal.ocamltype nt with
| Some t ->
t
| None ->
assert false (* every start symbol should carry a type *)
in
f prod state nt t accu
) entry accu
......@@ -31,6 +31,14 @@ module ImperativeNodeMap : Fix.IMPERATIVE_MAPS with type key = node
val entry: node ProductionMap.t
(* [fold_entry] folds over [entry]. For convenience, it gives access not only
to the start production and start state, but also to the nonterminal
symbol and to the OCaml type associated with this production. *)
val fold_entry:
(Production.index -> node -> Nonterminal.t -> Stretch.ocamltype -> 'a -> 'a) ->
'a -> 'a
(* Nodes are numbered sequentially from [0] to [n-1]. *)
val n: int
......
......@@ -698,24 +698,7 @@ let api : IL.valdef list =
let lexer = "lexer"
and lexbuf = "lexbuf" in
ProductionMap.fold (fun prod state api ->
let nt : Nonterminal.t =
match Production.classify prod with
| Some nt ->
nt
| None ->
assert false (* this is a start production *)
in
let t : typ =
match Nonterminal.ocamltype nt with
| Some t ->
TypTextual t
| None ->
assert false (* every start symbol should carry a type *)
in
Lr1.fold_entry (fun _prod state nt t api ->
define (
Nonterminal.print true nt,
EFun (
......@@ -730,13 +713,12 @@ let api : IL.valdef list =
]
)
),
type2scheme t
type2scheme (TypTextual t)
)
)
) ::
api
) Lr1.entry []
) []
(* ------------------------------------------------------------------------ *)
......
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