Commit 1403e3d0 authored by jjourdan's avatar jjourdan

Coq backend : 1- Use ' instead of _ as separator in identifiers 2- correct a bug introduced in r319

git-svn-id: svn+ssh://scm.gforge.inria.fr/svnroot/menhir@356 0f8b5475-4b4e-0410-85a8-ee3154a6bfe7
parent aa4d346d
...@@ -5,10 +5,10 @@ module Run (T: sig end) = struct ...@@ -5,10 +5,10 @@ module Run (T: sig end) = struct
let print_term t = let print_term t =
assert (not (Terminal.pseudo t)); assert (not (Terminal.pseudo t));
sprintf "%s_t" (Terminal.print t) sprintf "%s't" (Terminal.print t)
let print_nterm nt = let print_nterm nt =
sprintf "%s_nt" (Nonterminal.print true nt) sprintf "%s'nt" (Nonterminal.print true nt)
let print_symbol = function let print_symbol = function
| Symbol.N nt -> sprintf "NT %s" (print_nterm nt) | Symbol.N nt -> sprintf "NT %s" (print_nterm nt)
...@@ -39,10 +39,10 @@ module Run (T: sig end) = struct ...@@ -39,10 +39,10 @@ module Run (T: sig end) = struct
Lr1.foldx (fun accu node -> if not (is_final_state node) then f accu node else accu) Lr1.foldx (fun accu node -> if not (is_final_state node) then f accu node else accu)
let print_nis nis = let print_nis nis =
sprintf "Nis_%d" (Lr1.number nis) sprintf "Nis'%d" (Lr1.number nis)
let print_init init = let print_init init =
sprintf "Init_%d" (Lr1.number init) sprintf "Init'%d" (Lr1.number init)
let print_st st = let print_st st =
match Lr1.incoming_symbol st with match Lr1.incoming_symbol st with
...@@ -57,7 +57,7 @@ module Run (T: sig end) = struct ...@@ -57,7 +57,7 @@ module Run (T: sig end) = struct
(ProductionMap.empty, SymbolMap.empty) (ProductionMap.empty, SymbolMap.empty)
let print_prod p = let print_prod p =
sprintf "Prod_%s_%d" (Nonterminal.print true (Production.nt p)) (ProductionMap.find p prod_ids) sprintf "Prod'%s'%d" (Nonterminal.print true (Production.nt p)) (ProductionMap.find p prod_ids)
let () = let () =
if not Settings.coq_no_actions then if not Settings.coq_no_actions then
...@@ -369,7 +369,7 @@ module Run (T: sig end) = struct ...@@ -369,7 +369,7 @@ module Run (T: sig end) = struct
let first = ref true in let first = ref true in
Item.Map.iter (fun item lookaheads -> Item.Map.iter (fun item lookaheads ->
let prod, pos = Item.export item in let prod, pos = Item.export item in
if Production.is_start prod then begin if not (Production.is_start prod) then begin
if !first then first := false if !first then first := false
else fprintf f ";\n "; else fprintf f ";\n ";
fprintf f "{| prod_item := %s;\n" (print_prod prod); fprintf f "{| prod_item := %s;\n" (print_prod prod);
......
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