KevinMidboe/linguist
1
0
Fork 0
mirror of https://github.com/KevinMidboe/linguist.git synced 2025-10-29 17:50:22 +00:00
Code Issues Packages Projects Releases Wiki Activity

Some comments are triggering charlock binary

Browse Source
This commit is contained in:
Joshua Peek
2012-09-24 10:48:22 -05:00
parent d96dd473b8
commit 2b36f73da6
4 changed files with 22 additions and 60 deletions
Download Patch File Download Diff File Expand all files Collapse all files

46
samples/Coq/Heap.v
View File

@@ -1,13 +1,3 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
(** A development of Treesort on Heap trees. It has an average (** A development of Treesort on Heap trees. It has an average
complexity of O(n.log n) but of O(n²) in the worst case (e.g. if complexity of O(n.log n) but of O(n²) in the worst case (e.g. if
the list is already sorted) *) the list is already sorted) *)
@@ -88,9 +78,9 @@ Section defs.
forall P:Tree -> Type, forall P:Tree -> Type,
P Tree_Leaf -> P Tree_Leaf ->
(forall (a:A) (T1 T2:Tree), (forall (a:A) (T1 T2:Tree),
leA_Tree a T1 -> leA_Tree a T1 ->
leA_Tree a T2 -> leA_Tree a T2 ->
is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) -> is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T:Tree, is_heap T -> P T. forall T:Tree, is_heap T -> P T.
Proof. Proof.
simple induction T; auto with datatypes. simple induction T; auto with datatypes.
@@ -105,9 +95,9 @@ Section defs.
forall P:Tree -> Set, forall P:Tree -> Set,
P Tree_Leaf -> P Tree_Leaf ->
(forall (a:A) (T1 T2:Tree), (forall (a:A) (T1 T2:Tree),
leA_Tree a T1 -> leA_Tree a T1 ->
leA_Tree a T2 -> leA_Tree a T2 ->
is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) -> is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T:Tree, is_heap T -> P T. forall T:Tree, is_heap T -> P T.
Proof. Proof.
simple induction T; auto with datatypes. simple induction T; auto with datatypes.
@@ -135,13 +125,13 @@ Section defs.
(forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
merge_lem l1 l2. merge_lem l1 l2.
Require Import Morphisms. Require Import Morphisms.
Instance: Equivalence (@meq A). Instance: Equivalence (@meq A).
Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A). Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
Proof. intros x y H x' y' H'. now apply meq_congr. Qed. Proof. intros x y H x' y' H'. now apply meq_congr. Qed.
Lemma merge : Lemma merge :
forall l1:list A, Sorted leA l1 -> forall l1:list A, Sorted leA l1 ->
forall l2:list A, Sorted leA l2 -> merge_lem l1 l2. forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.
@@ -150,8 +140,8 @@ Section defs.
apply merge_exist with l2; auto with datatypes. apply merge_exist with l2; auto with datatypes.
rename l1 into l. rename l1 into l.
revert l2 H0. fix 1. intros. revert l2 H0. fix 1. intros.
destruct l2 as [|a0 l0]. destruct l2 as [|a0 l0].
apply merge_exist with (a :: l); simpl; auto with datatypes. apply merge_exist with (a :: l); simpl; auto with datatypes.
elim (leA_dec a a0); intros. elim (leA_dec a a0); intros.
(* 1 (leA a a0) *) (* 1 (leA a a0) *)
@@ -159,18 +149,18 @@ Section defs.
destruct (merge l H (a0 :: l0) H0). destruct (merge l H (a0 :: l0) H0).
apply merge_exist with (a :: l1). clear merge merge0. apply merge_exist with (a :: l1). clear merge merge0.
auto using cons_sort, cons_leA with datatypes. auto using cons_sort, cons_leA with datatypes.
simpl. rewrite m. now rewrite munion_ass. simpl. rewrite m. now rewrite munion_ass.
intros. apply cons_leA. intros. apply cons_leA.
apply (@HdRel_inv _ leA) with l; trivial with datatypes. apply (@HdRel_inv _ leA) with l; trivial with datatypes.
(* 2 (leA a0 a) *) (* 2 (leA a0 a) *)
apply Sorted_inv in H0. destruct H0. apply Sorted_inv in H0. destruct H0.
destruct (merge0 l0 H0). clear merge merge0. destruct (merge0 l0 H0). clear merge merge0.
apply merge_exist with (a0 :: l1); apply merge_exist with (a0 :: l1);
auto using cons_sort, cons_leA with datatypes. auto using cons_sort, cons_leA with datatypes.
simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm. simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity. repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
intros. apply cons_leA. intros. apply cons_leA.
apply (@HdRel_inv _ leA) with l0; trivial with datatypes. apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
Qed. Qed.
@@ -186,7 +176,7 @@ Section defs.
match t with match t with
| Tree_Leaf => emptyBag | Tree_Leaf => emptyBag
| Tree_Node a t1 t2 => | Tree_Node a t1 t2 =>
munion (contents t1) (munion (contents t2) (singletonBag a)) munion (contents t1) (munion (contents t2) (singletonBag a))
end. end.
@@ -272,11 +262,11 @@ Section defs.
apply flat_exist with (a :: l); simpl; auto with datatypes. apply flat_exist with (a :: l); simpl; auto with datatypes.
apply meq_trans with apply meq_trans with
(munion (list_contents _ eqA_dec l1) (munion (list_contents _ eqA_dec l1)
(munion (list_contents _ eqA_dec l2) (singletonBag a))). (munion (list_contents _ eqA_dec l2) (singletonBag a))).
apply meq_congr; auto with datatypes. apply meq_congr; auto with datatypes.
apply meq_trans with apply meq_trans with
(munion (singletonBag a) (munion (singletonBag a)
(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))). (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
apply munion_rotate. apply munion_rotate.
apply meq_right; apply meq_sym; trivial with datatypes. apply meq_right; apply meq_sym; trivial with datatypes.
Qed. Qed.

14
samples/Coq/PermutSetoid.v
View File

@@ -1,11 +1,3 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import Omega Relations Multiset SetoidList. Require Import Omega Relations Multiset SetoidList.
(** This file is deprecated, use [Permutation.v] instead. (** This file is deprecated, use [Permutation.v] instead.
@@ -154,7 +146,7 @@ Lemma permut_add_cons_inside :
Proof. Proof.
intros; intros;
replace (a :: l) with ([] ++ a :: l); trivial; replace (a :: l) with ([] ++ a :: l); trivial;
apply permut_add_inside; trivial. apply permut_add_inside; trivial.
Qed. Qed.
Lemma permut_middle : Lemma permut_middle :
@@ -168,8 +160,8 @@ Lemma permut_sym_app :
Proof. Proof.
intros l1 l2; intros l1 l2;
unfold permutation, meq; unfold permutation, meq;
intro a; do 2 rewrite list_contents_app; simpl; intro a; do 2 rewrite list_contents_app; simpl;
auto with arith. auto with arith.
Qed. Qed.
Lemma permut_rev : Lemma permut_rev :

14
samples/Coq/Permutation.v
View File

@@ -1,17 +1,5 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*********************************************************************)
(** * List permutations as a composition of adjacent transpositions *)
(*********************************************************************)
(* Adapted in May 2006 by Jean-Marc Notin from initial contents by (* Adapted in May 2006 by Jean-Marc Notin from initial contents by
Laurent Théry (Huffmann contribution, October 2003) *) Laurent Thery (Huffmann contribution, October 2003) *)
Require Import List Setoid Compare_dec Morphisms. Require Import List Setoid Compare_dec Morphisms.
Import ListNotations. (* For notations [] and [a;b;c] *) Import ListNotations. (* For notations [] and [a;b;c] *)

8
samples/Coq/Sorting.v
View File

@@ -1,10 +1,2 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Export Sorted. Require Export Sorted.
Require Export Mergesort. Require Export Mergesort.