ArithmeticExpressionParser

Pierre Letouzey edited this page Oct 26, 2017 · 7 revisions

This implements a certified parser on a simple grammar of arithmetic expressions. It assumes the input has already been tokenized.

Require Import Program.
Require Import ZArith.
Require Import List.
Inductive token : Set :=
| NUM (n:Z)
| PLUS | MINUS | TIMES | OPEN_PAREN | CLOSE_PAREN.
(* The target grammar, formalized below, is informally:
expr <- summand => $1
      | expr PLUS summand => $1 + $3
      | expr MINUS summand => $1 - $3
summand <- factor => $1
         | summand TIMES factor => $1 * $3
factor <- NUM => $1
        | PLUS factor => $2
        | MINUS factor => - $2
        | OPEN_PAREN expr CLOSE_PAREN => $2
*)
Inductive expr_value : list token -> Z -> Prop :=
| expr_rule_1 : forall (l1 : list token) (val1 : Z),
  summand_value l1 val1 -> expr_value l1 val1
| expr_rule_2 : forall (l1 : list token) (val1 : Z)
  (l3 : list token) (val3 : Z),
  expr_value l1 val1 -> summand_value l3 val3 ->
  expr_value (l1 ++ PLUS :: l3) (val1 + val3)
| expr_rule_3 : forall (l1 : list token) (val1 : Z)
  (l3 : list token) (val3 : Z),
  expr_value l1 val1 -> summand_value l3 val3 ->
  expr_value (l1 ++ MINUS :: l3) (val1 - val3)
with
summand_value : list token -> Z -> Prop :=
| summand_rule_1 : forall (l1 : list token) (val1 : Z),
  factor_value l1 val1 -> summand_value l1 val1
| summand_rule_2 : forall (l1 : list token) (val1 : Z)
  (l3 : list token) (val3 : Z),
  summand_value l1 val1 -> factor_value l3 val3 ->
  summand_value (l1 ++ TIMES :: l3) (val1 * val3)
with
factor_value : list token -> Z -> Prop :=
| factor_rule_1 : forall (n : Z),
  factor_value [NUM n] n
| factor_rule_2 : forall (l2 : list token) (val2 : Z),
  factor_value l2 val2 -> factor_value (PLUS :: l2) val2
| factor_rule_3 : forall (l2 : list token) (val2 : Z),
  factor_value l2 val2 -> factor_value (MINUS :: l2) (- val2)
| factor_rule_4 : forall (l2 : list token) (val2 : Z),
  expr_value l2 val2 -> factor_value (OPEN_PAREN :: l2 ++ [CLOSE_PAREN]) val2.
Lemma expr_nonempty : forall (l : list token) (n : Z), expr_value l n ->
  length l > 0 with
summand_nonempty : forall (l : list token) (n : Z), summand_value l n ->
  length l > 0 with
factor_nonempty : forall (l : list token) (n : Z), factor_value l n ->
  length l > 0.
Proof.
destruct 1; (repeat rewrite app_length; simpl; omega) || eauto.
destruct 1; (repeat rewrite app_length; simpl; omega) || eauto.
destruct 1; (repeat rewrite app_length; simpl; omega) || eauto.
Qed.
(* A few trivial results to recognize a string expression involving l
   as being equal to ? ++ l. *)
Lemma app_nil_start : forall l : list token, l = nil ++ l.
Proof.
reflexivity.
Qed.
Lemma app_cons_start : forall (t : token) (l' hd l : list token),
  l' = hd ++ l -> t :: l' = (t :: hd) ++ l.
Proof.
intros.
rewrite H.
reflexivity.
Qed.
Lemma app_app_start : forall (hd1 hd2 l l' : list token),
  l' = hd2 ++ l -> hd1 ++ l' = (hd1 ++ hd2) ++ l.
Proof.
intros.
rewrite H.
apply app_assoc.
Qed.
Local Ltac recog_tail :=
  eauto using app_nil_start, app_cons_start, app_app_start.
Inductive parse_ret (l : list token) (cond : list token -> Z -> Prop) : Set :=
| parse_success : forall (tl : list token) (n : Z),
  (exists hd : list token, l = hd ++ tl /\ cond hd n) ->
  parse_ret l cond
| parse_failure : parse_ret l cond.
Definition expr_sub_value (n : Z) : list token -> Z -> Prop :=
fun l m => forall (n_str : list token), expr_value n_str n ->
  expr_value (n_str ++ l) m.
(* Reduction rules for the fake "expr_sub n" symbol:
  expr_sub n <- empty => n
              | PLUS summand (expr_sub (n+$2)) => $3
              | MINUS summand (expr_sub (n-$2)) => $3 *)
Lemma expr_sub_rule1 : forall n : Z,
  expr_sub_value n nil n.
Proof.
intros n ? ?; rewrite <- app_nil_end; trivial.
Qed.
Lemma expr_sub_rule2 : forall (n : Z)
  (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z),
  summand_value l2 val2 ->
  expr_sub_value (n + val2) l3 val3 ->
  expr_sub_value n (PLUS :: l2 ++ l3) val3.
Proof.
intros.
intros ? ?.
evar (hd : list token); match goal with |- expr_value ?l _ =>
            replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd
                        end.
eauto using expr_value.
Qed.
Lemma expr_sub_rule3 : forall (n : Z)
  (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z),
  summand_value l2 val2 ->
  expr_sub_value (n - val2) l3 val3 ->
  expr_sub_value n (MINUS :: l2 ++ l3) val3.
Proof.
intros.
intros ? ?.
evar (hd : list token); match goal with |- expr_value ?l _ =>
            replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd
                        end.
eauto using expr_value.
Qed.
Definition summand_sub_value (n : Z) : list token -> Z -> Prop :=
fun l m => forall (n_str : list token),
  summand_value n_str n -> summand_value (n_str ++ l) m.
(* Reduction rules for the fake "summand_sub n" symbol:
  summand_sub n <- empty => n
                 | TIMES factor (summand_sub (n*$2)) => $3 *)
Lemma summand_sub_rule1 : forall n : Z,
  summand_sub_value n nil n.
Proof.
intros; intros ? ?; rewrite <- app_nil_end; trivial.
Qed.
Lemma summand_sub_rule2 : forall (n : Z)
  (l2 : list token) (val2 : Z) (l3 : list token) (val3 : Z),
  factor_value l2 val2 ->
  summand_sub_value (n * val2) l3 val3 ->
  summand_sub_value n (TIMES :: l2 ++ l3) val3.
Proof.
intros.
intros ? ?.
evar (hd : list token); match goal with |- summand_value ?l _ =>
            replace l with (hd ++ l3) by (symmetry; recog_tail); subst hd
                        end.
eauto using summand_value.
Qed.
(* Notations to allow us to act as if our parser functions were
   instances of StateT (list token) Maybe Z -- which they are if one
   ignores the proof content. *)
(* First, a couple utility functions which are literally instances of
   StateT (list token) Maybe (option token), and
   StateT (list token) Maybe token, respectively. *)
(* Peek at the next token, without removing it from the parser stream;
   if at end of stream, return None, but don't signal an error *)
Definition peek_token (l : list token) : option (list token * option token) :=
match l with
| nil => Some (l, None)
| t :: _ => Some (l, Some t)
end.
(* Get the next token and remove it from the parser stream;
   if at end of stream, signal an error *)
Definition get_token (l : list token) : option (list token * token) :=
match l with
| nil => None
| t :: l' => Some (l', t)
end.
(* Our actual intermediate terms that we build as part of the notation
   will be of this form: *)
Definition parse_monad_type (P : list token -> list token -> Prop)
  (cond : list token -> Z -> Prop) : Set :=
  forall l l0, P l l0 -> parse_ret l0 cond.
(* Here, l0 represents the "initial state", needed to specify the
   return type, and l represents the "current state".
   P will represent enough "context" from the monad invocations
   so far to continue.  For example, in the first return_ statement
   in parse_expr_sub below, P might look like:
   fun l l0 =>
   exists hd, expr_sub_value (n + m) hd result /\
   exists hd0, summand_value hd0 m /\
   exists l', get_token l' = Some (hd0 ++ hd ++ l, Anonymous) /\
   exists l'', peek_token l'' = Some (l', t) /\
   l'' = l0.
   For the outer structure, we will build an instance of
   parse_monad_type eq cond, and then pass arguments
   l l eq_refl *)
Program Definition parse_monad_bind {X P cond}
  (x : list token -> option (list token * X))
  (g : forall x0:X, parse_monad_type
                   (fun l l0 => exists l', x l' = Some (l, x0) /\
                                P l' l0)
                   cond) :
  parse_monad_type P cond :=
fun l l0 H =>
match x l as o return (x l = o -> _) with
| Some (l', x0) => fun _ => g x0 l' l0 _
| None => fun _ => parse_failure _ _
end eq_refl.
Next Obligation.
eexists; split; [ reflexivity | eassumption ].
Defined.
Program Definition parse_monad_bind_rec {P sz sz' cond cond'}
  (subparse : forall (l : list token), sz' l < sz ->
                parse_ret l cond')
  (g : forall n:Z, parse_monad_type
                   (fun l l0 => exists hd, cond' hd n /\ P (hd ++ l) l0)
                   cond) :
  (forall l l0:list token, P l l0 -> sz' l < sz) ->
  parse_monad_type P cond :=
fun Hlt l l0 H =>
match subparse l _ return _ with
| parse_success tl n _ => g n tl l0 _
| parse_failure => parse_failure _ _
end.
Next Obligation.
eexists; split; eassumption.
Defined.
Notation "'do' x0 <- x ; y" :=
  (parse_monad_bind x (fun x0 => y))
(at level 70, right associativity, x0 ident).
Notation "'do_rec' n <- x ; y" :=
  (parse_monad_bind_rec x (fun n => y) _)
(at level 70, right associativity, x0 ident).
Notation "'return_' n" := (fun l l0 _ => parse_success _ _ l n _)
(at level 71).
Notation "'error'" := (fun l l0 _ => parse_failure _ _)
(at level 71).
(* Notation "'subparser' p Hacc" :=
  (fun l Hlt => p l (Acc_inv Hacc Hlt)) (at level 90). *)
Definition subparser {P sz} (p : forall l, Acc lt (sz l) -> P l)
  {n} (Hacc : Acc lt n) :=
  fun (l:list token) (Hlt : sz l < n) => p l (Acc_inv Hacc Hlt).
Definition parse_expr_sz (l : list token) := 5 * length l + 4.
Definition parse_expr_sub_sz (l : list token) := 5 * length l + 3.
Definition parse_summand_sz (l : list token) := 5 * length l + 2.
Definition parse_summand_sub_sz (l : list token) := 5 * length l + 1.
Definition parse_factor_sz (l : list token) := 5 * length l.
Program Definition run_with_initial_state (l : list token) {cond}
  (m : parse_monad_type (fun l0 l1 => l0 = l /\ l1 = l) cond) :
  parse_ret l cond :=
m l l _.
Obligation Tactic := program_simpl; simpl; simpl in *;
  eauto using expr_value, summand_value, factor_value;
  try (repeat split; discriminate);
  repeat match goal with
  | H : ?f ?l = _ |- _ =>
    match f with
    | peek_token => idtac
    | get_token => idtac
    | _ => fail
    end;
    (is_var l; destruct l; (discriminate H || (injection H; intros; subst));
     clear H) ||
    (simpl f in H; injection H; intros; subst; clear H)
  end;
  try (unfold parse_expr_sz, parse_expr_sub_sz, parse_summand_sz,
              parse_summand_sub_sz, parse_factor_sz;
       simpl length; repeat rewrite app_length;
       repeat match goal with
       H : _ |- _ => apply expr_nonempty in H ||
                  apply summand_nonempty in H ||
                  apply factor_nonempty in H
       end; omega);
  try (eexists; split; [ recog_tail |
                         eauto using expr_value, summand_value, factor_value,
                         expr_sub_rule1, expr_sub_rule2, expr_sub_rule3,
                         summand_sub_rule1, summand_sub_rule2 ]).
Program Definition parse_expr_builder (l : list token)
  (parse_summand : forall l', parse_summand_sz l' < parse_expr_sz l ->
     parse_ret l' summand_value)
  (parse_expr_sub : forall n l', parse_expr_sub_sz l' < parse_expr_sz l ->
     parse_ret l' (expr_sub_value n)) :
  parse_ret l expr_value :=
run_with_initial_state l (
do_rec n <- parse_summand;
do_rec m <- parse_expr_sub n;
return_ m
).
Program Definition parse_expr_sub_builder (n : Z) (l : list token)
  (parse_summand : forall l', parse_summand_sz l' < parse_expr_sub_sz l ->
     parse_ret l' summand_value)
  (parse_expr_sub : forall n l', parse_expr_sub_sz l' < parse_expr_sub_sz l ->
     parse_ret l' (expr_sub_value n)) :
  parse_ret l (expr_sub_value n) :=
run_with_initial_state l (
do t <- peek_token;
match t with
| Some PLUS => do _ <- get_token;
               do_rec m <- parse_summand;
               do_rec result <- parse_expr_sub (n + m)%Z;
               return_ result
| Some MINUS => do _ <- get_token;
                do_rec m <- parse_summand;
                do_rec result <- parse_expr_sub (n - m)%Z;
                return_ result
| _ => return_ n
end
).
Program Definition parse_summand_builder (l : list token)
  (parse_summand_sub : forall n l',
     parse_summand_sub_sz l' < parse_summand_sz l ->
     parse_ret l' (summand_sub_value n))
  (parse_factor : forall l',
     parse_factor_sz l' < parse_summand_sz l ->
     parse_ret l' factor_value) :
  parse_ret l summand_value :=
run_with_initial_state l (
do_rec n <- parse_factor;
do_rec m <- parse_summand_sub n;
return_ m
).
Program Definition parse_summand_sub_builder (n : Z) (l : list token)
  (parse_summand_sub : forall n l',
     parse_summand_sub_sz l' < parse_summand_sub_sz l ->
     parse_ret l' (summand_sub_value n))
  (parse_factor : forall l',
     parse_factor_sz l' < parse_summand_sub_sz l ->
     parse_ret l' factor_value) :
  parse_ret l (summand_sub_value n) :=
run_with_initial_state l (
do t <- peek_token;
match t with
| Some TIMES => do _ <- get_token;
                do_rec m <- parse_factor;
                do_rec result <- parse_summand_sub (n * m)%Z;
                return_ result
| _ => return_ n
end
).
Program Definition parse_factor_builder (l : list token)
  (parse_expr : forall l',
     parse_expr_sz l' < parse_factor_sz l ->
     parse_ret l' expr_value)
  (parse_factor : forall l',
     parse_factor_sz l' < parse_factor_sz l ->
     parse_ret l' factor_value) :
  parse_ret l factor_value :=
run_with_initial_state l (
do t <- get_token;
match t with
| NUM n => return_ n
| PLUS => do_rec n <- parse_factor;
          return_ n
| MINUS => do_rec n <- parse_factor;
           return_ (-n)
| OPEN_PAREN => do_rec n <- parse_expr;
                do t <- get_token;
                match t with
                | CLOSE_PAREN => return_ n
                | _ => error
                end
| _ => error
end
).
Fixpoint
parse_expr (l : list token) (H : Acc lt (parse_expr_sz l)) {struct H} :
  parse_ret l expr_value :=
parse_expr_builder l
  (fun l' Hlt => parse_summand l' (Acc_inv H Hlt))
  (fun n l' Hlt => parse_expr_sub n l' (Acc_inv H Hlt))
with
parse_expr_sub (n : Z) (l : list token) (H : Acc lt (parse_expr_sub_sz l))
  {struct H} : parse_ret l (expr_sub_value n) :=
parse_expr_sub_builder n l
  (fun l' Hlt => parse_summand l' (Acc_inv H Hlt))
  (fun n l' Hlt => parse_expr_sub n l' (Acc_inv H Hlt))
with
parse_summand (l : list token) (H : Acc lt (parse_summand_sz l)) {struct H} :
  parse_ret l summand_value :=
parse_summand_builder l
  (fun n l' Hlt => parse_summand_sub n l' (Acc_inv H Hlt))
  (fun l' Hlt => parse_factor l' (Acc_inv H Hlt))
with
parse_summand_sub (n : Z) (l : list token) (H : Acc lt (parse_summand_sub_sz l))
  {struct H} : parse_ret l (summand_sub_value n) :=
parse_summand_sub_builder n l
  (fun n l' Hlt => parse_summand_sub n l' (Acc_inv H Hlt))
  (fun l' Hlt => parse_factor l' (Acc_inv H Hlt))
with
parse_factor (l : list token) (H : Acc lt (parse_factor_sz l)) {struct H} :
  parse_ret l factor_value :=
parse_factor_builder l
  (fun l' Hlt => parse_expr l' (Acc_inv H Hlt))
  (fun l' Hlt => parse_factor l' (Acc_inv H Hlt)).
Obligation Tactic := program_simpl.
Definition parse_ret_data {l cond} (ret : parse_ret l cond) :
  option (list token * Z) :=
match ret with
| parse_success l' n _ => Some (l', n)
| parse_failure => None
end.
Inductive starts_with {A:Type} : list A -> A -> Prop :=
| starts_with_intro :
  forall (tl : list A) (hd : A), starts_with (hd :: tl) hd.
Definition parse_expr_completeness_stmt hd n :=
  forall tl, ~ starts_with tl TIMES -> forall H, exists H',
  parse_ret_data (parse_expr (hd ++ tl) H) =
  parse_ret_data (parse_expr_sub n tl H').
Definition parse_summand_completeness_stmt hd n :=
  forall tl, forall H, exists H',
  parse_ret_data (parse_summand (hd ++ tl) H) =
  parse_ret_data (parse_summand_sub n tl H').
Definition parse_factor_completeness_stmt hd n :=
  forall tl, forall H,
  parse_ret_data (parse_factor (hd ++ tl) H) = Some (tl, n).
Lemma parse_expr_completeness' {hd n} :
  parse_expr_completeness_stmt hd n ->
  forall tl, ~ starts_with tl PLUS -> ~ starts_with tl MINUS ->
  ~ starts_with tl TIMES -> forall H,
  parse_ret_data (parse_expr (hd ++ tl) H) = Some (tl, n).
Proof.
intros.
destruct (H tl H2 H3) as [H' e]; rewrite e.
destruct H'; simpl parse_expr_sub.
destruct tl; simpl.
reflexivity.
destruct t; (match goal with
             | Hs : ~ starts_with (?t :: _) ?t |- _ =>
               contradict Hs; constructor
             end || reflexivity).
Qed.
Lemma parse_summand_completeness' {hd n} :
  parse_summand_completeness_stmt hd n ->
  forall tl, ~ starts_with tl TIMES -> forall H,
  parse_ret_data (parse_summand (hd ++ tl) H) = Some (tl, n).
Proof.
intros.
destruct (H tl H1) as [H' e]; rewrite e.
destruct H'; simpl parse_summand_sub.
destruct tl; simpl.
reflexivity.
destruct t; (match goal with
             | Hs : ~ starts_with (?t :: _) ?t |- _ =>
               contradict Hs; constructor
             end || reflexivity).
Qed.
Lemma parse_expr_completeness : forall hd n, expr_value hd n ->
  parse_expr_completeness_stmt hd n
with
parse_summand_completeness : forall hd n, summand_value hd n ->
  parse_summand_completeness_stmt hd n
with
parse_factor_completeness : forall hd n, factor_value hd n ->
  parse_factor_completeness_stmt hd n.
Proof.
Local Ltac inst_sub_cases parse_expr_completeness
  parse_summand_completeness parse_factor_completeness :=
destruct 1; repeat match goal with
| e : expr_value ?hd ?n |- _ =>
  progress match goal with
  | _ : parse_expr_completeness_stmt hd n |- _ => idtac
  | |- _ => let H := fresh in pose proof
         (parse_expr_completeness _ _ e) as H;
         pose proof (parse_expr_completeness' H)
  end
| s : summand_value ?hd ?n |- _ =>
  progress match goal with
  | _ : parse_summand_completeness_stmt hd n |- _ => idtac
  | |- _ => let H := fresh in pose proof
         (parse_summand_completeness _ _ s) as H;
         pose proof (parse_summand_completeness' H)
  end
| f : factor_value ?hd ?n |- _ =>
  progress match goal with
  | _ : parse_factor_completeness_stmt hd n |- _ => idtac
  | |- _ => pose proof (parse_factor_completeness _ _ f)
  end
end; clear parse_expr_completeness parse_summand_completeness
  parse_factor_completeness.
3: inst_sub_cases parse_expr_completeness parse_summand_completeness
  parse_factor_completeness.
2: inst_sub_cases parse_expr_completeness parse_summand_completeness
  parse_factor_completeness.
inst_sub_cases parse_expr_completeness parse_summand_completeness
  parse_factor_completeness.
Guarded.
Local Ltac subcase_intros :=
intro tl; repeat (simpl app; rewrite <- app_assoc; simpl app); intros.
Local Ltac expand_parser :=
match goal with
| H : Acc _ _ |- _ => destruct H; simpl
end;
unfold parse_expr_builder, parse_expr_sub_builder,
  parse_summand_builder, parse_summand_sub_builder, parse_factor_builder,
  run_with_initial_state, parse_monad_bind_rec, parse_monad_bind; simpl.
Local Ltac red_expr_completeness :=
match goal with
| H : parse_expr_completeness_stmt ?l ?val |-
  appcontext [parse_expr (?l ++ ?tl) ?Hacc] =>
  let H0 := fresh in
  assert (~ starts_with tl TIMES) as H0 by (red; inversion 1);
  destruct (H _ H0 Hacc) as [? e]; rewrite e
end.
Local Ltac red_parse_expr :=
match goal with
| |- appcontext [parse_expr (?l ++ ?tl) ?H] =>
   let a := fresh "a" in generalize H as a; intro a;
   remember (parse_expr (l ++ tl) a) as pe_val;
   try (match goal with
               | H0 : forall tl, ~ starts_with tl PLUS ->
                    ~ starts_with tl MINUS -> ~ starts_with tl TIMES ->
                 forall H, parse_ret_data (parse_expr (l ++ tl) H) =
                   Some (tl, ?val),
                 Heq : pe_val = _ |- _ =>
                 let Hplus := fresh in
                 assert (~ starts_with tl PLUS) as Hplus by
                   (red; inversion 1);
                 let Hminus := fresh in
                 assert (~ starts_with tl MINUS) as Hminus by
                   (red; inversion 1);
                 let Htimes := fresh in
                 assert (~ starts_with tl TIMES) as Htimes by
                   (red; inversion 1);
                 let Heqdata := fresh in
                 assert (parse_ret_data pe_val = Some (tl, val)) as Heqdata by
                   (rewrite Heq; apply (H0 _ Hplus Hminus Htimes));
                 destruct pe_val; discriminate Heqdata ||
                                  (injection Heqdata; intros; subst)
                 end)
end.
Local Ltac red_summand_completeness :=
match goal with
| H : parse_summand_completeness_stmt ?l ?val |-
  appcontext [parse_summand (?l ++ ?tl) ?Hacc] =>
  destruct (H _ Hacc) as [? e]; rewrite e
end.
Local Ltac red_parse_summand :=
match goal with
| |- appcontext [parse_summand (?l ++ ?tl) ?H] =>
   let a := fresh "a" in generalize H as a; intro a;
   remember (parse_summand (l ++ tl) a) as ps_val;
   try (match goal with
               | H0 : forall tl, ~ starts_with tl TIMES ->
                 forall H, parse_ret_data (parse_summand (l ++ tl) H) =
                   Some (tl, ?val),
                 H1 : ~ starts_with tl TIMES,
                 Heq : ps_val = _  |- _ =>
                 let Heqdata := fresh in
                 assert (parse_ret_data ps_val = Some (tl, val)) as Heqdata by
                   (rewrite Heq; apply (H0 _ H1));
               destruct ps_val; discriminate Heqdata ||
                                (injection Heqdata; intros; subst)
               end)
end.
Local Ltac red_parse_factor :=
match goal with
| |- appcontext [parse_factor (?l ++ ?tl) ?H] =>
   let a := fresh "a" in generalize H as a; intro a;
   remember (parse_factor (l ++ tl) a) as pf_val;
   try (match goal with
        | H0 : parse_factor_completeness_stmt l ?val,
          Heq : pf_val = _ |- _ =>
          let Heqdata := fresh in
            assert (parse_ret_data pf_val = Some (tl, val)) as Heqdata by
               (rewrite Heq; apply H0);
            destruct pf_val; discriminate Heqdata ||
                             (injection Heqdata; intros; subst)
        end)
end.
Local Ltac end_state p :=
match goal with
| |- appcontext [p ?tl ?H] =>
   let a := fresh "a" in generalize H as a; intro a; exists a;
   destruct (p tl a); reflexivity
end.
abstract (subcase_intros; expand_parser; red_parse_summand;
          end_state (parse_expr_sub val1)).
abstract (subcase_intros; red_expr_completeness; expand_parser;
  red_parse_summand; end_state (parse_expr_sub (val1 + val3))).
abstract (subcase_intros; red_expr_completeness; expand_parser;
  red_parse_summand; end_state (parse_expr_sub (val1 - val3))).
abstract (subcase_intros; expand_parser; red_parse_factor;
  end_state (parse_summand_sub val1)).
abstract (subcase_intros; red_summand_completeness; expand_parser;
  red_parse_factor; end_state (parse_summand_sub (val1 * val3))).
abstract (subcase_intros; expand_parser; reflexivity).
abstract (subcase_intros; expand_parser; red_parse_factor; reflexivity).
abstract (subcase_intros; expand_parser; red_parse_factor; reflexivity).
abstract (subcase_intros; expand_parser; red_parse_expr;
  simpl; reflexivity).
Qed.
Corollary parse_expr_completeness'' :
  forall {hd n}, expr_value hd n -> forall tl,
  ~ starts_with tl PLUS -> ~ starts_with tl MINUS ->
  ~ starts_with tl TIMES -> forall H,
  parse_ret_data (parse_expr (hd ++ tl) H) = Some (tl, n).
Proof.
intros hd n Hexpr.
apply parse_expr_completeness'.
apply parse_expr_completeness; trivial.
Qed.
Corollary parse_expr_completeness_no_tail :
  forall (l : list token) (n : Z), expr_value l n -> forall H,
  parse_ret_data (parse_expr l H) = Some (nil, n).
Proof.
intros l n ?; rewrite (app_nil_end l); intros.
apply parse_expr_completeness''; trivial; red; inversion 1.
Qed.
Program Definition parse_expr_wrapper (l : list token) :
  { n:Z | unique (expr_value l) n } +
  { forall n:Z, ~ expr_value l n } :=
match parse_expr l (lt_wf _) with
| parse_success nil n _ => inleft _ n
| _ => inright _ _
end.
Next Obligation.
clear Heq_anonymous.
red; split.
rewrite <- app_nil_end; trivial.
intros m ?.
rewrite <- app_nil_end in H.
pose proof (parse_expr_completeness_no_tail _ _ H (lt_wf _)).
rewrite (parse_expr_completeness_no_tail _ _ e0) in H0.
injection H0; auto.
Defined.
Next Obligation.
change (forall n wildcard',
  parse_success l expr_value [] n wildcard' <>
  parse_expr l (lt_wf _)) in H.
intro.
remember (parse_expr l (lt_wf _)) as pe_val.
assert (parse_ret_data pe_val = Some (nil, n)) by
  (rewrite Heqpe_val; apply parse_expr_completeness_no_tail; trivial).
destruct pe_val; simpl in H1; try discriminate H1.
injection H1; intros; subst.
contradiction (H n e); reflexivity.
Defined.
(* For extraction, use:
Require Import ExtrOcamlBasic.
Extraction Inline parse_expr_builder parse_expr_sub_builder
  parse_summand_builder parse_summand_sub_builder parse_factor_builder
  parse_monad_bind parse_monad_bind_rec run_with_initial_state.
Recursive Extraction parse_expr_wrapper.
*)
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.