Quelle Extraction_matchs_2413.v Sprache: Coq

(** Extraction : tests of optimizations of pattern matching *)

Require Corelib.extraction.Extraction.

(** First, a few basic tests *)

Definition test1 b :=
match b with
   | true => true
   | false => false
end.

Extraction test1. (** should be seen as the identity *)

Definition test2 b :=
match b with
   | true => false
   | false => false
end.

Extraction test2. (** should be seen a the always-false constant function *)

Inductive hole (A:Set) : Set := Hole | Hole2.

Definition wrong_id (A B : Set) (x:hole A) : hole B :=
match x with
  | Hole _ => @Hole _
  | Hole2 _ => @Hole2 _
end.

Extraction wrong_id. (** should _not_ be optimized as an identity *)

Definition test3 (A:Type)(o : option A) :=
match o with
   | Some x => Some x
   | None  => None
end.

Extraction test3.  (** Even with type parameters, should be seen as identity *)

Inductive indu : Type := A : nat -> indu | B | C.

Definition test4 n :=
match n with
   | A m => A (S m)
   | B => B
   | C => C
end.

Extraction test4. (** should merge branchs B C into a x->x *)

Definition test5 n :=
match n with
   | A m => A (S m)
   | B => B
   | C => B
end.

Extraction test5. (** should merge branches B C into _->B *)

Inductive indu' : Type := A' : nat -> indu' | B' | C' | D' | E' | F'.

Definition test6 n :=
match n with
   | A' m => A' (S m)
   | B' => C'
   | C' => C'
   | D' => C'
   | E' => B'
   | F' => B'
end.

Extraction test6. (** should merge some branches into a _->C' *)

(** NB : In Coq, "| a => a"  corresponds to n, hence some "| _ -> n" are
    extracted *)

Definition test7 n :=
  match n with
    | A m => Some m
    | B => None
    | C => None
  end.

Extraction test7. (** should merge branches B,C into a _->None *)

(** Script from bug #2413 *)

Set Implicit Arguments.

Section S.

Definition message := nat.
Definition word := nat.
Definition mode := nat.
Definition opcode := nat.

Variable condition : word -> option opcode.

Section decoder_result.

Variable inst : Type.

Inductive decoder_result : Type :=
| DecUndefined : decoder_result
| DecUnpredictable : decoder_result
| DecInst : inst -> decoder_result
| DecError : message -> decoder_result.

End decoder_result.

Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode)
  (w : word) (inst : Type) (g : mode -> opcode -> inst) :
  decoder_result inst :=
  match condition w with
    | Some oc =>
      match f w with
        | DecInst i => DecInst (g i oc)
        | DecError _ m => @DecError inst m
        | DecUndefined _ => @DecUndefined inst
        | DecUnpredictable _ => @DecUnpredictable inst
      end
    | None => @DecUndefined inst
  end.

End S.

Extraction decode_cond_mode.
(** inner match should not be factorized with a partial x->x (different type) *)

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.