Commit ff242077 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Fix coq backend.

parent bdae60bc
......@@ -171,7 +171,7 @@ Class Numbered (A:Type) := {
surj : positive -> A;
surj_inj_compat : forall x, surj (inj x) = x;
inj_bound : positive;
inj_bound_spec : forall x, (inj x <= inj_bound)%positive
inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive
}.
Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
......@@ -192,6 +192,7 @@ Proof.
generalize (inj_bound_spec x). generalize (inj x). clear x. intros x.
match goal with |- ?Hx -> In ?s (fst ?p) =>
assert ((Hx -> In s (fst p)) /\ snd p = Pos.succ inj_bound); [|now intuition] end.
rewrite Pos.lt_succ_r.
induction inj_bound as [|y [IH1 IH2]] using Pos.peano_ind;
(split; [intros Hx|]); simpl.
+ rewrite (Pos.le_antisym _ _ Hx); auto using Pos.le_1_l.
......
......@@ -118,7 +118,7 @@ module Run (T: sig end) = struct
fprintf f "Definition %s := %s'.\n\n" name name;
if List.length constrs > 0 then
begin
let iteri f = ignore (List.fold_left (fun k x -> f k x; succ k) 0 constrs) in
let iteri f = ignore (List.fold_left (fun k x -> f k x; succ k) 1 constrs) in
fprintf f "Program Instance %sNum : %sAlphabet.Numbered %s :=\n" name menhirlib_path name;
fprintf f " { inj := fun x => match x return _ with ";
iteri (fun k constr -> fprintf f "\n | %s => %d%%positive" constr k);
......@@ -502,6 +502,7 @@ module Run (T: sig end) = struct
Front.grammar.BasicSyntax.preludes;
fprintf f "From Coq.Lists Require List.\n";
fprintf f "From Coq.Numbers Require Import BinNums.\n";
from_menhirlib f; fprintf f "Require Main.\n";
from_menhirlib f; fprintf f "Require Version.\n";
fprintf f "Import List.ListNotations.\n\n";
......
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