Merge branch 'v8.8'

Author: gmalecha

.gitignore

@@ -1,6 +1,12 @@
 *.vo
 *.glob
 *.v.d
+*.cmi
+*.cmx
+*.cmxs
+*.native
+*.o
+*.aux
 Makefile.coq
 Makefile.opam.coq
 *~

Makefile

@@ -1,28 +1,27 @@
-PROJECT_NAME=coq-ext-lib
-
 all: theories examples
 
-theories:
-	$(MAKE) -C theories
+theories: Makefile.coq
+	$(MAKE) -f Makefile.coq
+
+Makefile.coq:
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-install:
-	$(MAKE) -C theories install
+install: Makefile.coq
+	$(MAKE) -f Makefile.coq install
 
 examples: theories
 	$(MAKE) -C examples
 
 clean:
-	$(MAKE) -C theories clean
+	$(MAKE) -f Makefile.coq clean
 	$(MAKE) -C examples clean
+	@ rm Makefile.coq
 
 uninstall:
-	$(MAKE) -C theories uninstall
+	$(MAKE) -f Makefile.coq uninstall
 
 
 dist:
 	@ git archive --prefix coq-ext-lib/ HEAD -o $(PROJECT_NAME).tgz
 
-.dir-locals.el: tools/dir-locals.el
-	@ sed s,PWD,$(shell pwd -P),g tools/dir-locals.el > .dir-locals.el
-
 .PHONY: all clean dist theories examples

README.md

@@ -5,9 +5,10 @@ A collection of theories and plugins that may be useful in other Coq development
 
 Ideas
 -----
+- Embrace new features, e.g. universe polymorphism, primitive projections, etc.
 - Use modules for controlling namespaces.
-- Avoid functors in favor of type classes since type classes are more flexible
-  b/c they are first-class.
+- Use first-class abstractions where appropriate, e.g. type classes, canonical structures, etc.
+  - The library is mostly built around type clases
 - Notations should be hidden by modules that are explicitly opened.
   - This avoids clashes between precedence.
   - TB: Actually, this does not completely avoid clashes, if we have to open two modules at the same time (for instance, I often need to open Equality, to get dependent destruction, which conflicts with the rest of my development)
@@ -19,8 +20,6 @@ Ideas
 
 File Structure
 --------------
-* plugins/
-  - Base directory to the provided plugins
 * theories/
   - Base directory to the provided theories
 

_CoqProject

@@ -0,0 +1,132 @@
+-Q theories ExtLib
+
+theories/ExtLib.v
+theories/Tactics.v
+
+theories/Core/Any.v
+theories/Core/CmpDec.v
+theories/Core/EquivDec.v
+theories/Core/RelDec.v
+theories/Core/Type.v
+
+theories/Structures/Applicative.v
+theories/Structures/BinOps.v
+theories/Structures/CoFunctor.v
+theories/Structures/CoMonad.v
+theories/Structures/EqDep.v
+theories/Structures/Foldable.v
+theories/Structures/FunctorLaws.v
+theories/Structures/Functor.v
+theories/Structures/Identity.v
+theories/Structures/Maps.v
+theories/Structures/MonadCont.v
+theories/Structures/MonadExc.v
+theories/Structures/MonadFix.v
+theories/Structures/MonadLaws.v
+theories/Structures/MonadPlus.v
+theories/Structures/MonadReader.v
+theories/Structures/MonadState.v
+theories/Structures/Monads.v
+theories/Structures/MonadTrans.v
+theories/Structures/Monad.v
+theories/Structures/MonadWriter.v
+theories/Structures/MonadZero.v
+theories/Structures/Monoid.v
+theories/Structures/Proper.v
+theories/Structures/Reducible.v
+theories/Structures/Sets.v
+theories/Structures/Traversable.v
+
+theories/Data/Bool.v
+theories/Data/Char.v
+theories/Data/Checked.v
+theories/Data/Eq.v
+theories/Data/Eq/UIP_trans.v
+theories/Data/Fin.v
+theories/Data/Fun.v
+theories/Data/HList.v
+theories/Data/LazyList.v
+theories/Data/Lazy.v
+theories/Data/ListFirstnSkipn.v
+theories/Data/ListNth.v
+theories/Data/List.v
+theories/Data/Member.v
+theories/Data/Nat.v
+theories/Data/N.v
+theories/Data/Option.v
+theories/Data/Pair.v
+theories/Data/Positive.v
+theories/Data/PreFun.v
+theories/Data/Prop.v
+theories/Data/SigT.v
+theories/Data/Stream.v
+theories/Data/String.v
+theories/Data/SumN.v
+theories/Data/Sum.v
+theories/Data/Tuple.v
+theories/Data/Unit.v
+theories/Data/Vector.v
+theories/Data/Z.v
+
+theories/Data/POption.v
+theories/Data/PList.v
+theories/Data/PPair.v
+
+
+theories/Generic/Data.v
+theories/Generic/DerivingData.v
+theories/Generic/Func.v
+theories/Generic/Ind.v
+
+theories/Programming/Eqv.v
+theories/Programming/Extras.v
+theories/Programming/Injection.v
+theories/Programming/Le.v
+theories/Programming/Show.v
+theories/Programming/With.v
+
+theories/Recur/Facts.v
+theories/Recur/GenRec.v
+theories/Recur/Measure.v
+theories/Recur/Relation.v
+
+theories/Relations/Compose.v
+theories/Relations/TransitiveClosure.v
+
+theories/Tactics/BoolTac.v
+theories/Tactics/Cases.v
+theories/Tactics/Consider.v
+theories/Tactics/EqDep.v
+theories/Tactics/Equality.v
+theories/Tactics/Forward.v
+theories/Tactics/Injection.v
+theories/Tactics/MonadTac.v
+theories/Tactics/Parametric.v
+theories/Tactics/Reify.v
+theories/Tactics/TypeTac.v
+
+theories/Data/Graph/BuildGraph.v
+theories/Data/Graph/GraphAdjList.v
+theories/Data/Graph/GraphAlgos.v
+theories/Data/Graph/Graph.v
+
+theories/Data/Map/FMapAList.v
+theories/Data/Map/FMapPositive.v
+theories/Data/Map/FMapTwoThreeK.v
+
+theories/Data/Monads/ContMonad.v
+theories/Data/Monads/EitherMonad.v
+theories/Data/Monads/FuelMonadLaws.v
+theories/Data/Monads/FuelMonad.v
+theories/Data/Monads/IdentityMonadLaws.v
+theories/Data/Monads/IdentityMonad.v
+theories/Data/Monads/ListMonad.v
+theories/Data/Monads/OptionMonadLaws.v
+theories/Data/Monads/OptionMonad.v
+theories/Data/Monads/ReaderMonadLaws.v
+theories/Data/Monads/ReaderMonad.v
+theories/Data/Monads/StateMonad.v
+theories/Data/Monads/WriterMonad.v
+theories/Data/Set/ListSet.v
+theories/Data/Set/SetMap.v
+theories/Data/Set/TwoThreeTrees.v

examples/ConsiderDemo.v

@@ -1,14 +1,16 @@
+Require NPeano.
+Import NPeano.Nat.
 Require Import ExtLib.Tactics.Consider.
+Require Import Coq.Bool.Bool.
+Require Import ExtLib.Data.Nat.
+
+Require Import Coq.omega.Omega.
 
 Set Implicit Arguments.
 Set Strict Implicit.
 
 (**  Some tests *)
 Section test.
-  Require Import NPeano Coq.Bool.Bool.
-  Require Import ExtLib.Data.Nat.
-
-  Require Import Omega.
   Goal forall x y z,  (ltb x y && ltb y z) = true ->
                  ltb x z = true.
   intros x y z.

examples/EvalWithExc.v

@@ -1,9 +1,10 @@
+Require Import Coq.Strings.String.
 (** Require the monad definitions **)
 Require Import ExtLib.Structures.Monads.
 (** Use the instances for exceptions **)
 Require Import ExtLib.Data.Monads.EitherMonad.
 (** Strings will be used for error messages **)
-Require Import String.
+Require Import ExtLib.Data.String.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -27,16 +28,16 @@ Section monadic.
   Variable m : Type -> Type.
   Context {Monad_m : Monad m}.
   Context {MonadExc_m : MonadExc string m}.
-  
+
   (** Use the notation for monads **)
   Import MonadNotation.
   Local Open Scope monad_scope.
-  
+
   (** Functions that get [nat] or [bool] values from a [value] **)
   Definition asInt (v : value) : m nat :=
     match v with
-      | Int n => ret n 
-      | _ => 
+      | Int n => ret n
+      | _ =>
         (** if we don't have an integer, signal an error using
          ** [raise] from the MoandExc instance
          **)
@@ -54,7 +55,7 @@ Section monadic.
    **)
   Fixpoint eval' (e : exp) : m value :=
     match e with
-        (** when there is no error, we can just return (i.e. [ret]) 
+        (** when there is no error, we can just return (i.e. [ret])
          ** the answer
          **)
       | ConstI i => ret (Int i)
@@ -72,7 +73,7 @@ Section monadic.
         t <- eval' t ;;
         t <- asBool t ;;
         (** case split and perform the appropriate recursion **)
-        if t then
+        if (t : bool) then
           eval' tr
         else
           eval' fa
@@ -83,7 +84,7 @@ End monadic.
 (** Wrap the [eval] function up with the monad instance that we
  ** want to use
  **)
-Definition eval : exp -> string + value := 
+Definition eval : exp -> string + value :=
   eval' (m := sum string).
 
 (** Some tests **)

examples/Makefile

@@ -1,42 +1,9 @@
-MODULES    := $(patsubst %.v,%,$(wildcard *.v))
-TESTS      := 
-VS         := $(MODULES:%=%.v)
-TVS        := $(TESTS:%=%.v)
-
-ARGS :=-R ../theories ExtLib
-
-.PHONY: coq clean admit depgraph toplevel whitespace
-
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
-Makefile.coq: Makefile $(VS)
-	coq_makefile $(ARGS) $(VS) \
-          | sed -re 's/-R ([^ ]+) ExtLib/-I \1 -as ExtLib/g' \
-          > Makefile.coq
-
-Makefile.test.coq: Makefile $(TVS)
-	coq_makefile $(ARGS) $(TVS) \
-          | sed -re 's/-R ([^ ]+) ExtLib/-I \1 -as ExtLib/g' \
-          > Makefile.coq
-
-test: coq Makefile.test.coq
-	$(MAKE) -f Makefile.test.coq
-
-clean:: Makefile.coq
+clean: Makefile.coq
 	$(MAKE) -f Makefile.coq clean
-	rm -f Makefile.coq .depend
-
-whitespace:
-	@ ./../tools/whitespace.sh $(MODULES:%=%.v)
-
-admit:
-	@ grep -n -e 'admit' -e 'Admitted' ${VS}
-
-depgraph: Makefile.coq
-	@ echo Generating dependency graph to ../deps.pdf
-	@ ./../tools/deps.py $(MODULES:%=%.v.d) > ../deps.dot
-	@ ./../tools/deps.py $(MODULES:%=%.v.d) | dot -Tpdf -o ../deps.pdf
+	rm Makefile.coq
 
-toplevel: coq
-	coqtop.opt $(ARGS)
+Makefile.coq: Makefile _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq

examples/MonadReasoning.v

@@ -7,6 +7,9 @@ Require Import ExtLib.Data.Fun.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** Currently not ported due to universes *)
+
+(*
 Section with_m.
   Variable m : Type -> Type.
   Variable Monad_m : Monad m.
@@ -53,4 +56,5 @@ Section with_m.
       eapply equiv_prefl; eauto. }
   Qed.
 
-End with_m.
+End with_m.
+*)

examples/Printing.v

@@ -1,5 +1,6 @@
 Require Import Coq.Strings.String.
 Require Import ExtLib.Structures.MonadWriter.
+Require Import ExtLib.Data.PPair.
 Require Import ExtLib.Data.Monads.WriterMonad.
 Require Import ExtLib.Data.Monads.IdentityMonad.
 Require Import ExtLib.Programming.Show.
@@ -16,11 +17,14 @@ Definition printString (str : string) : PrinterMonad unit :=
                     (@show_exact str _ show_inj (@show_mon _ ShowScheme_string_compose)).
 
 Definition runPrinter {T : Type} (c : PrinterMonad T) : T * string :=
-  let '(val,str) := unIdent (runWriterT c) in
+  let '(ppair val str) := unIdent (runWriterT c) in
   (val, str ""%string).
 
 
-Eval compute in runPrinter (Monad.bind (print 1) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (print 1) (fun _ => print 2)).
 
-Eval compute in runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
-Eval compute in runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (print "hello "%string) (fun _ => print 2)).
+Eval compute in
+    runPrinter (Monad.bind (printString "hello "%string) (fun _ => print 2)).