diff options
Diffstat (limited to 'MenhirLib/Interpreter.v')
-rw-r--r-- | MenhirLib/Interpreter.v | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v index 07aeae5a..158bba9f 100644 --- a/MenhirLib/Interpreter.v +++ b/MenhirLib/Interpreter.v @@ -27,7 +27,7 @@ Class Decidable (P : Prop) := decide : {P} + {~P}. Arguments decide _ {_}. (** A [Comparable] type has decidable equality. *) -Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) : +Global Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) : Decidable (x = y). Proof. unfold Decidable. @@ -35,7 +35,7 @@ Proof. right; intros ->; by rewrite compare_refl in EQ. Defined. -Instance list_decidable_eq T : +Global Instance list_decidable_eq T : (forall x y : T, Decidable (x = y)) -> (forall l1 l2 : list T, Decidable (l1 = l2)). Proof. unfold Decidable. decide equality. Defined. @@ -83,6 +83,9 @@ Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed. CoInductive buffer : Type := Buf_cons { buf_head : token; buf_tail : buffer }. +(* Note: Coq 8.12.0 wants a Declare Scope command, + but this breaks compatibility with Coq < 8.10. + Declare Scope buffer_scope. *) Delimit Scope buffer_scope with buf. Bind Scope buffer_scope with buffer. @@ -274,10 +277,11 @@ Qed. different to [Err] (from the error monad), which mean that the automaton is bogus and has perfomed a forbidden action. **) Inductive step_result := - | Fail_sr: step_result + | Fail_sr_full: state -> token -> step_result | Accept_sr: symbol_semantic_type (NT (start_nt init)) -> buffer -> step_result | Progress_sr: stack -> buffer -> step_result. + (** [reduce_step] does a reduce action : - pops some elements from the stack - execute the action of the production @@ -367,7 +371,7 @@ Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result := | Reduce_act prod => fun Hv => reduce_step stk prod buffer Hv Hi | Fail_act => fun _ => - Fail_sr + Fail_sr_full (state_of_stack stk) tok end (fun _ => Hv I (token_term tok)) end end (fun _ => reduce_ok _). @@ -425,7 +429,7 @@ Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant result type, so that this inductive is extracted without the use of Obj.t in OCaml. **) Inductive parse_result {A : Type} := - | Fail_pr: parse_result + | Fail_pr_full: state -> token -> parse_result | Timeout_pr: parse_result | Parsed_pr: A -> buffer -> parse_result. Global Arguments parse_result _ : clear implicits. @@ -433,7 +437,7 @@ Global Arguments parse_result _ : clear implicits. Definition parse (buffer : buffer) (log_n_steps : nat): parse_result (symbol_semantic_type (NT (start_nt init))). refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with - | Fail_sr => Fail_pr + | Fail_sr_full st tok => Fail_pr_full st tok | Accept_sr sem buffer' => Parsed_pr sem buffer' | Progress_sr _ _ => Timeout_pr end). @@ -443,10 +447,17 @@ Defined. End Interpreter. -Arguments Fail_sr {init}. +Arguments Fail_sr_full {init} _ _. Arguments Accept_sr {init} _ _. Arguments Progress_sr {init} _ _. +(* These notations are provided for backwards compatibility with Coq code + * from before the addition of the return information. They are used in the + * theorem statements. + *) +Notation Fail_sr := (Fail_sr_full _ _) (only parsing). +Notation Fail_pr := (Fail_pr_full _ _) (only parsing). + End Make. Module Type T(A:Automaton.T). |