Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_4456.v Sprache: Coq

Original von: Coq^©

(* -*- mode: coq; coq-prog-args: ("-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *)
(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *)
(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0
   coqtop version 8.5beta3 (November 2015) *)
(* Variable P : forall n m : nat, n = m -> Prop. *)
(* Axiom Prefl : forall n : nat, P n n eq_refl. *)
Axiom proof_admitted : False.

Tactic Notation "admit" := case proof_admitted.

Require Coq.Program.Program.
Require Coq.Strings.String.
Require Coq.omega.Omega.
Module Export Fiat_DOT_Common.
Module Export Fiat.
Module Common.
Import Coq.Lists.List.
Export Coq.Program.Program.

Global Set Implicit Arguments.

Global Coercion is_true : bool >-> Sortclass.
Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false.

Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type
  := match ls return Type with
     | nil => True
     | x::xs => (P x * ForallT P xs)%type
     end.
Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type
  := match ls with
     | nil => P nil
     | x::xs => (P (x::xs) * Forall_tails P xs)%type
     end.

End Common.

End Fiat.

End Fiat_DOT_Common.
Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.
Module Export Fiat.
Module Export Parsers.
Module Export StringLike.
Module Export Core.
Import Coq.Relations.Relation_Definitions.
Import Coq.Classes.Morphisms.

Local Coercion is_true : bool >-> Sortclass.

Module Export StringLike.
  Class StringLike {Char : Type} :=
    {
      String :> Type;
      is_char : String -> Char -> bool;
      length : String -> nat;
      take : nat -> String -> String;
      drop : nat -> String -> String;
      get : nat -> String -> option Char;
      unsafe_get : nat -> String -> Char;
      bool_eq : String -> String -> bool;
      beq : relation String := fun x y => bool_eq x y
    }.

  Arguments StringLike : clear implicits.
  Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope.
  Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope.
  Local Open Scope string_like_scope.

  Class StringLikeProperties (Char : Type) `{StringLike Char} :=
    {
      singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch';
      singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ];
      get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch;
      get_S : forall n s, get (S n) s = get n (drop 1 s);
      unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch;
      length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
      bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
      is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
      length_Proper :> Proper (beq ==> eq) length;
      take_Proper :> Proper (eq ==> beq ==> beq) take;
      drop_Proper :> Proper (eq ==> beq ==> beq) drop;
      bool_eq_Equivalence :> Equivalence beq;
      bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
      take_short_length : forall str n, n <= length str -> length (take n str) = n;
      take_long : forall str n, length str <= n -> take n str =s str;
      take_take : forall str n m, take n (take m str) =s take (min n m) str;
      drop_length : forall str n, length (drop n str) = length str - n;
      drop_0 : forall str, drop 0 str =s str;
      drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str;
      drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str);
      take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str);
      bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str'
    }.
Global Arguments StringLikeProperties _ {_}.
End StringLike.

End Core.

End StringLike.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.

Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core.
Module Export Fiat.
Module Export Parsers.
Module Export ContextFreeGrammar.
Module Export Core.
Import Coq.Strings.String.
Import Coq.Lists.List.
Export Fiat.Parsers.StringLike.Core.

Section cfg.
  Context {Char : Type}.

  Section definitions.

    Inductive item :=
    | Terminal (_ : Char)
    | NonTerminal (_ : string).

    Definition production := list item.
    Definition productions := list production.

    Record grammar :=
      {
        Start_symbol :> string;
        Lookup :> string -> productions;
        Start_productions :> productions := Lookup Start_symbol;
        Valid_nonterminals : list string;
        Valid_productions : list productions := map Lookup Valid_nonterminals
      }.
  End definitions.

  End cfg.

Arguments item _ : clear implicits.
Arguments production _ : clear implicits.
Arguments productions _ : clear implicits.
Arguments grammar _ : clear implicits.

End Core.

End ContextFreeGrammar.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core.

Module Export Fiat_DOT_Parsers_DOT_BaseTypes.
Module Export Fiat.
Module Export Parsers.
Module Export BaseTypes.
Import Coq.Arith.Wf_nat.

Local Coercion is_true : bool >-> Sortclass.

Section recursive_descent_parser.
  Context {Char} {HSL : StringLike Char} {G : grammar Char}.

  Class parser_computational_predataT :=
    { nonterminals_listT : Type;
      nonterminal_carrierT : Type;
      of_nonterminal : String.string -> nonterminal_carrierT;
      to_nonterminal : nonterminal_carrierT -> String.string;
      initial_nonterminals_data : nonterminals_listT;
      nonterminals_length : nonterminals_listT -> nat;
      is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool;
      remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }.

  Class parser_removal_dataT' `{predata : parser_computational_predataT} :=
    { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop
      := ltof _ nonterminals_length;
      nonterminals_length_zero : forall ls,
                                   nonterminals_length ls = 0
                                   -> forall nt, is_valid_nonterminal ls nt = false;
      remove_nonterminal_dec : forall ls nonterminal,
                                 is_valid_nonterminal ls nonterminal
                                 -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls;
      remove_nonterminal_noninc : forall ls nonterminal,
                                    ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal);
      initial_nonterminals_correct : forall nonterminal,
                                       is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G);
      initial_nonterminals_correct' : forall nonterminal,
                                       is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G);
      to_of_nonterminal : forall nonterminal,
                            List.In nonterminal (Valid_nonterminals G)
                            -> to_nonterminal (of_nonterminal nonterminal) = nonterminal;
      of_to_nonterminal : forall nonterminal,
                            is_valid_nonterminal initial_nonterminals_data nonterminal
                            -> of_nonterminal (to_nonterminal nonterminal) = nonterminal;
      ntl_wf : well_founded nonterminals_listT_R
      := well_founded_ltof _ _;
      remove_nonterminal_1
      : forall ls ps ps',
          is_valid_nonterminal (remove_nonterminal ls ps) ps'
          -> is_valid_nonterminal ls ps';
      remove_nonterminal_2
      : forall ls ps ps',
          is_valid_nonterminal (remove_nonterminal ls ps) ps' = false
          <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }.

  Class split_dataT :=
    { split_string_for_production
      : item Char -> production Char -> String -> list nat }.

  Class boolean_parser_dataT :=
    { predata :> parser_computational_predataT;
      split_data :> split_dataT }.
End recursive_descent_parser.

End BaseTypes.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_BaseTypes.

Module Export Fiat_DOT_Common_DOT_List_DOT_Operations.
Module Export Fiat.
Module Export Common.
Module Export List.
Module Export Operations.

Import Coq.Lists.List.

Module Export List.
  Section InT.
    Context {A : Type} (a : A).

    Fixpoint InT (ls : list A) : Set
      := match ls return Set with
           | nil => False
           | b :: m => (b = a) + InT m
         end%type.
  End InT.

  End List.

End Operations.

End List.

End Common.

End Fiat.

End Fiat_DOT_Common_DOT_List_DOT_Operations.

Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties.
Module Export Fiat.
Module Export Parsers.
Module Export StringLike.
Module Export Properties.

Section String.
  Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.

  Lemma take_length {str n}
  : length (take n str) = min n (length str).
admit.
Defined.

  End String.

End Properties.

End StringLike.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties.

Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties.
Module Export Fiat.
Module Export Parsers.
Module Export ContextFreeGrammar.
Module Export Properties.

Local Open Scope list_scope.
Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char)
  := { nt : _
   & { prefix : _
     & List.In nt (Valid_nonterminals G)
       * List.InT
            (prefix ++ p)
            (Lookup G nt) } }%type.

End Properties.

End ContextFreeGrammar.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties.

Module Export Fiat_DOT_Parsers_DOT_MinimalParse.
Module Export Fiat.
Module Export Parsers.
Module Export MinimalParse.
Import Coq.Lists.List.
Import Fiat.Parsers.ContextFreeGrammar.Core.

Local Coercion is_true : bool >-> Sortclass.
Local Open Scope string_like_scope.

Section cfg.
  Context {Char} {HSL : StringLike Char} {G : grammar Char}.
  Context {predata : @parser_computational_predataT}
          {rdata' : @parser_removal_dataT' _ G predata}.

  Inductive minimal_parse_of
  : forall (len0 : nat) (valid : nonterminals_listT)
           (str : String),
      productions Char -> Type :=
  | MinParseHead : forall len0 valid str pat pats,
                     @minimal_parse_of_production len0 valid str pat
                     -> @minimal_parse_of len0 valid str (pat::pats)
  | MinParseTail : forall len0 valid str pat pats,
                     @minimal_parse_of len0 valid str pats
                     -> @minimal_parse_of len0 valid str (pat::pats)
  with minimal_parse_of_production
  : forall (len0 : nat) (valid : nonterminals_listT)
           (str : String),
      production Char -> Type :=
  | MinParseProductionNil : forall len0 valid str,
                              length str = 0
                              -> @minimal_parse_of_production len0 valid str nil
  | MinParseProductionCons : forall len0 valid str n pat pats,
                               length str <= len0
                               -> @minimal_parse_of_item len0 valid (take n str) pat
                               -> @minimal_parse_of_production len0 valid (drop n str) pats
                               -> @minimal_parse_of_production len0 valid str (pat::pats)
  with minimal_parse_of_item
  : forall (len0 : nat) (valid : nonterminals_listT)
           (str : String),
      item Char -> Type :=
  | MinParseTerminal : forall len0 valid str ch,
                         str ~= [ ch ]
                         -> @minimal_parse_of_item len0 valid str (Terminal ch)
  | MinParseNonTerminal
    : forall len0 valid str (nt : String.string),
        @minimal_parse_of_nonterminal len0 valid str nt
        -> @minimal_parse_of_item len0 valid str (NonTerminal nt)
  with minimal_parse_of_nonterminal
  : forall (len0 : nat) (valid : nonterminals_listT)
           (str : String),
      String.string -> Type :=
  | MinParseNonTerminalStrLt
    : forall len0 valid (nt : String.string) str,
        length str < len0
        -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)
        -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt)
        -> @minimal_parse_of_nonterminal len0 valid str nt
  | MinParseNonTerminalStrEq
    : forall len0 str valid nonterminal,
        length str = len0
        -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal)
        -> is_valid_nonterminal valid (of_nonterminal nonterminal)
        -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal)
        -> @minimal_parse_of_nonterminal len0 valid str nonterminal.

End cfg.

End MinimalParse.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_MinimalParse.

Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes.
Module Export Fiat.
Module Export Parsers.
Module Export CorrectnessBaseTypes.
Import Coq.Lists.List.
Import Fiat.Parsers.ContextFreeGrammar.Core.
Import Fiat_DOT_Common.Fiat.Common.
Section general.
  Context {Char} {HSL : StringLike Char} {G : grammar Char}.

  Definition split_list_completeT_for {data : @parser_computational_predataT}
             {len0 valid}
             (it : item Char) (its : production Char)
             (str : String)
             (pf : length str <= len0)
             (split_list : list nat)

    := ({ n : nat
              & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it)
                * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type)
       -> ({ n : nat
                 & (In (min (length str) n) (map (min (length str)) split_list))
                   * (minimal_parse_of_item (G := G) len0 valid (take n str) it)
                   * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type).

  Definition split_list_completeT {data : @parser_computational_predataT}
             (splits : item Char -> production Char -> String -> list nat)
    := forall len0 valid str (pf : length str <= len0) nt,
         is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)
         -> ForallT
              (Forall_tails
                 (fun prod
                  => match prod return Type with
                       | nil => True
                       | it::its
                         => @split_list_completeT_for data len0 valid it its str pf (splits it its str)
                     end))
              (Lookup G nt).

  Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} :=
    { split_string_for_production_complete
      : split_list_completeT split_string_for_production }.
End general.

End CorrectnessBaseTypes.

End Parsers.

End Fiat.

End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes.

Module Export Fiat.
Module Export Parsers.
Module Export ContextFreeGrammar.
Module Export Valid.
Export Fiat.Parsers.StringLike.Core.

Section cfg.
  Context {Char : Type} {HSL : StringLike Char} (G : grammar Char)
          {predata : parser_computational_predataT}.

  Definition item_valid (it : item Char)
    := match it with
         | Terminal _ => True
         | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt'))
       end.

  Definition production_valid pat
    := List.Forall item_valid pat.

  Definition productions_valid pats
    := List.Forall production_valid pats.

  Definition grammar_valid
    := forall nt,
         List.In nt (Valid_nonterminals G)
         -> productions_valid (Lookup G nt).
End cfg.

End Valid.
End ContextFreeGrammar.
End Parsers.
End Fiat.

Section app.
  Context {Char : Type} {HSL : StringLike Char} (G : grammar Char)
          {predata : parser_computational_predataT}.

  Lemma hd_production_valid
        (it : item Char)
        (its : production Char)
        (H : production_valid (it :: its))
  : item_valid it.
admit.
Defined.

  Lemma production_valid_cons
        (it : item Char)
        (its : production Char)
        (H : production_valid (it :: its))
  : production_valid its.
admit.
Defined.

  End app.

Import Coq.Lists.List.
Import Coq.omega.Omega.
Import Fiat_DOT_Common.Fiat.Common.
Import Fiat.Parsers.ContextFreeGrammar.Valid.
Local Open Scope string_like_scope.

Section recursive_descent_parser.
  Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char).
  Context {data : @boolean_parser_dataT Char _}
          {cdata : @boolean_parser_completeness_dataT' Char _ G data}
          {rdata : @parser_removal_dataT' _ G _}
          {gvalid : grammar_valid G}.

  Local Notation dec T := (T + (T -> False))%type (only parsing).

  Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing).

  Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B).
admit.
Defined.

  Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls
  : dec { a : _ & (In a ls * P a) }.
admit.
Defined.

      Section item.
        Context {len0 valid}
                (str : String)
                (str_matches_nonterminal'
                 : nonterminal_carrierT -> bool)
                (str_matches_nonterminal
                 : forall nt : nonterminal_carrierT,
                     dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))).

        Section valid.
          Context (Hmatches
                   : forall nt,
                       is_valid_nonterminal initial_nonterminals_data nt
                       -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool)
                  (it : item Char)
                  (Hvalid : item_valid it).

          Definition parse_item'
          : dec (minimal_parse_of_item (G := G) len0 valid str it).
          Proof.
            clear Hvalid.
            refine (match it return dec (minimal_parse_of_item len0 valid str it) with
                      | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ])
                                       then inl (MinParseTerminal _ _ _ _ _)
                                       else inr (fun _ => !)
                      | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt)
                                          then inl (MinParseNonTerminal _)
                                          else inr (fun _ => !)
                    end);
              clear str_matches_nonterminal Hmatches;
              admit.
          Defined.
        End valid.

        End item.
        Context {len0 valid}
                (parse_nonterminal
                 : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT),
                     dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))).

        Lemma dec_in_helper {ls it its str}
        : iffT {n0 : nat &
                     (In (min (length str) n0) (map (min (length str)) ls) *
                      minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
                      minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type}
               {n0 : nat &
                     (In n0 ls *
                      (minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
                       minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}.
admit.
Defined.

        Lemma parse_production'_helper {str it its} (pf : length str <= len0)
        : dec {n0 : nat &
                    (minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
                     minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type}
          -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)).
admit.
Defined.
        Local Ltac t_parse_production_for := repeat
                      match goal with
              | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H
              | _ => progress subst
              | _ => solve [ constructor; assumption ]
              | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H)
              | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H)
              | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H'
              | _ => progress simpl in *
              | _ => discriminate
              | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z))
              | _ => solve [ eauto with nocore ]
              | _ => solve [ apply Min.min_case_strong; omega ]
              | _ => omega
              | [ H : production_valid (_::_) |- _ ]
                => let H' := fresh in
                   pose proof H as H';
                     apply production_valid_cons in H;
                     apply hd_production_valid in H'
            end.

        Definition parse_production'_for
                 (splits : item Char -> production Char -> String -> list nat)
                 (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str))
                 (str : String)
                 (len : nat)
                 (Hlen : length str = len)
                 (pf : len <= len0)
                 (prod : production Char)
                 (Hreachable : production_is_reachableT G prod)
        : dec (minimal_parse_of_production (G := G) len0 valid str prod).
        Proof.
          revert prod Hreachable str len Hlen pf.
          refine
            ((fun pf_helper =>
               list_rect
                 (fun prod =>
                    forall (Hreachable : production_is_reachableT G prod)
                           (str : String)
                           (len : nat)
                           (Hlen : length str = len)
                           (pf : len <= len0),
                      dec (minimal_parse_of_production (G := G) len0 valid str prod))
                 (
                   fun Hreachable str len Hlen pf
                   => match Utils.dec (beq_nat len 0) with
                        | left H => inl _
                        | right H => inr (fun p => _)
                      end)
                 (fun it its parse_production' Hreachable str len Hlen pf
                  => parse_production'_helper
                       _
                       (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in
                        let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in
                        let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in
                        match dec_In
                                (fun n => dec_prod (parse_item n) (parse_production n))
                                (splits it its str)
                        with
                          | inl p => inl (existT _ (projT1 p) (snd (projT2 p)))
                          | inr p
                            => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in
                               let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in
                               inr (fun p' => p (fst dec_in_helper (H p')))
                        end)
              )) _);
            [ clear parse_nonterminal Hsplits splits rdata cdata
            | clear parse_nonterminal Hsplits splits rdata cdata
            | ..
            | admit ].
          abstract t_parse_production_for.
          abstract t_parse_production_for.
          abstract t_parse_production_for.
          abstract t_parse_production_for.
        Defined.
End recursive_descent_parser.

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.