Resolve plclub#158.

examples/containers/Makefile

@@ -69,7 +69,7 @@ vfiles: $(OUT)/edits  $(HS_SPEC)/README.md $(OUT)/README.md $(OUT)/_CoqProject $
 $(OUT)/_CoqProject : Makefile $(OUT)/README.md
 	> $@
 	echo '-Q . ""' >> $@
-	echo '-R ../../../base ""' >> $@
+	echo '-Q ../../../base ""' >> $@
 	echo $(addsuffix .v,$(HANDMOD)) >> $@
 	echo $(addsuffix .v,$(MODULES)) >> $@
 	echo $(addsuffix .v,$(SPECIAL_MODULES)) >> $@

examples/containers/lib/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 Utils/Containers/Internal/PtrEquality.v CTZ.v BitTerminationProofs.v Test/QuickCheck/Property.v Test/QuickCheck/Arbitrary.v Test/QuickCheck/Gen.v IntWord.v
 Data/Set/Internal.v Utils/Containers/Internal/BitUtil.v Data/IntSet/Internal.v Data/IntSet/InternalWord.v Data/IntMap/Internal.v Data/Map/Internal.v IntSetValidity.v
 

examples/containers/theories/_CoqProject

@@ -1,6 +1,6 @@
 -Q . ""
 -Q ../hs-spec ""
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../containers/lib ""
 CustomTactics.v

examples/core-semantics/Makefile

@@ -33,7 +33,7 @@ vfiles: $(OUT)/edits  $(OUT)/README.md $(OUT)/_CoqProject $(VFILES)
 $(OUT)/_CoqProject : $(OUT)/README.md Makefile
 	> $@
 	echo '-Q . ""' >> $@
-	echo '-R ../../../base ""' >> $@
+	echo '-Q ../../../base ""' >> $@
 	echo '-Q ../../../base-thy  Proofs' >> $@
 	echo '-Q ../../containers/lib   ""' >> $@
 	echo '-Q ../../containers/theories   ""' >> $@

examples/core-semantics/lib/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../containers/lib   ""
 -Q ../../containers/theories   ""

examples/ghc/Makefile

@@ -272,7 +272,7 @@ $(OUT)/edits:
 $(OUT)/_CoqProject: $(OUT)/README.md Makefile
 	> $@
 	echo '-Q . ""' >> $@
-	echo '-R ../../../base ""' >> $@
+	echo '-Q ../../../base ""' >> $@
 	echo '-Q ../../../base-thy  Proofs' >> $@
 	echo '-Q ../../containers/lib   ""' >> $@
 	echo '-Q ../../containers/theories  ""' >> $@

examples/ghc/lib/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../containers/lib   ""
 -Q ../../containers/theories  ""

examples/ghc/theories/StateLogic.v

@@ -1,6 +1,6 @@
 Require Import GHC.Base.
 Require State.
-Require Traversable.
+Require Data.Traversable.
 
 Set Bullet Behavior "Strict Subproofs".
 

examples/ghc/theories/_CoqProject

@@ -1,5 +1,5 @@
 -Q . Proofs
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../ghc/lib ""
 -Q ../../transformers/lib ""

examples/graph/Makefile

@@ -68,7 +68,7 @@ vfiles: $(OUT)/edits  $(HS_SPEC)/README.md $(OUT)/README.md $(OUT)/_CoqProject $
 $(OUT)/_CoqProject : Makefile $(OUT)/README.md
 	> $@
 	echo '-Q . ""' >> $@
-	echo '-R ../../../base ""' >> $@
+	echo '-Q ../../../base ""' >> $@
 	echo '-Q ../../containers/lib ""' >> $@
 	echo $(addsuffix .v,$(HANDMOD)) >> $@
 	echo $(addsuffix .v,$(MODULES)) >> $@

examples/graph/lib/Data/Graph/Inductive/Graph.v

@@ -28,7 +28,6 @@ Require Data.IntSet.Internal.
 Require Data.Maybe.
 Require Data.OldList.
 Require Data.Tuple.
-Require Err.
 Require GHC.Base.
 Require GHC.Err.
 Require GHC.List.
@@ -396,7 +395,7 @@ Definition insNode {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph
    : LNode a -> gr a b -> gr a b :=
   fun '(pair v l) => (fun arg_1__ => pair (pair (pair nil v) l) nil & arg_1__).
 
-Definition insEdge {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}
+Definition insEdge {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}
    : LEdge b -> gr a b -> gr a b :=
   fun arg_0__ arg_1__ =>
     match arg_0__, arg_1__ with
@@ -471,7 +470,7 @@ Definition insNodes {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph
    : list (LNode a) -> gr a b -> gr a b :=
   fun vs g => Data.Foldable.foldl' (GHC.Base.flip insNode) g vs.
 
-Definition insEdges {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}
+Definition insEdges {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}
    : list (LEdge b) -> gr a b -> gr a b :=
   fun es g => Data.Foldable.foldl' (GHC.Base.flip insEdge) g es.
 
@@ -520,7 +519,7 @@ Definition subgraph {gr : Type -> Type -> Type} {a : Type} {b : Type} `{DynGraph
     let vs' := Data.IntSet.Internal.fromList vs in
     nfilter (fun arg_1__ => Data.IntSet.Internal.member arg_1__ vs').
 
-Definition context {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}
+Definition context {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}
    : gr a b -> Node -> Context a b :=
   fun g v =>
     Data.Maybe.fromMaybe (GHC.Err.error (Coq.Init.Datatypes.app
@@ -609,7 +608,7 @@ Definition deg' {a : Type} {b : Type} : Context a b -> GHC.Num.Int :=
   fun '(pair (pair (pair p _) _) s) =>
     GHC.List.length p GHC.Num.+ GHC.List.length s.
 
-Definition deg {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}
+Definition deg {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}
    : gr a b -> Node -> GHC.Num.Int :=
   deg' .: context.
 
@@ -709,9 +708,8 @@ End Notations.
      Data.Function.on Data.IntSet.Internal.fromList Data.IntSet.Internal.member
      Data.Maybe.fromMaybe Data.Maybe.isJust Data.Maybe.maybe Data.OldList.delete
      Data.OldList.op_zrzr__ Data.OldList.sortBy Data.Tuple.fst Data.Tuple.snd
-     Err.Default GHC.Base.Eq_ GHC.Base.compare GHC.Base.flip GHC.Base.fmap
-     GHC.Base.hs_string__ GHC.Base.id GHC.Base.map GHC.Base.op_z2218U__
-     GHC.Base.op_zeze__ GHC.Base.op_zsze__ GHC.Err.error GHC.List.elem
-     GHC.List.filter GHC.List.length GHC.Num.Int GHC.Num.op_zp__ GHC.Tuple.pair2
-     String.EmptyString
+     GHC.Base.Eq_ GHC.Base.compare GHC.Base.flip GHC.Base.fmap GHC.Base.hs_string__
+     GHC.Base.id GHC.Base.map GHC.Base.op_z2218U__ GHC.Base.op_zeze__
+     GHC.Base.op_zsze__ GHC.Err.Default GHC.Err.error GHC.List.elem GHC.List.filter
+     GHC.List.length GHC.Num.Int GHC.Num.op_zp__ GHC.Tuple.pair2 String.EmptyString
 *)

examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v

@@ -20,7 +20,6 @@ Require Import Wellfounded.
 
 Require Data.Foldable.
 Require Data.Tuple.
-Require Err.
 Require GHC.Base.
 Require GHC.Err.
 Require List.
@@ -87,7 +86,7 @@ Fixpoint mergeAll {a : Type} {b : Type} `{GHC.Base.Ord a} (arg_0__
 Definition isEmpty {a : Type} {b : Type} : Heap a b -> bool :=
   fun arg_0__ => match arg_0__ with | Empty => true | _ => false end.
 
-Definition findMin {a} {b} `{Err.Default (a * b)} : Heap a b -> a * b :=
+Definition findMin {a} {b} `{GHC.Err.Default (a * b)} : Heap a b -> a * b :=
   fun arg_0__ =>
     match arg_0__ with
     | Empty => GHC.Err.error (GHC.Base.hs_string__ "Heap.findMin: empty heap")
@@ -102,7 +101,8 @@ Definition deleteMin {a : Type} {b : Type} `{GHC.Base.Ord a}
     | Node _ _ hs => mergeAll hs
     end.
 
-Definition splitMin {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b * Heap a b)}
+Definition splitMin {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b *
+                                                                 Heap a b)}
    : Heap a b -> a * b * Heap a b :=
   fun arg_0__ =>
     match arg_0__ with
@@ -158,22 +158,22 @@ Proof.
   intros. assert (A: h <> Empty) by auto; apply deleteMin_size in A; omega.
 Qed.
 
-Program Fixpoint toList {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b)}
+Program Fixpoint toList {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b)}
                         (arg_0__ : Heap a b) {measure (size arg_0__)} : list (a * b)
   := match arg_0__ with
      | Empty => nil
      | h => let 'pair x r := pair (findMin h) (deleteMin h) in cons x (toList r)
      end.
 Solve Obligations with ((Tactics.program_simpl; apply toList_termination; auto)).
 
-Definition heapsort {a} `{GHC.Base.Ord a} `{Err.Default (a * a)}
+Definition heapsort {a} `{GHC.Base.Ord a} `{GHC.Err.Default (a * a)}
    : list a -> list a :=
   GHC.Base.map Data.Tuple.fst GHC.Base.∘
   (toList GHC.Base.∘ (build GHC.Base.∘ GHC.Base.map (fun x => pair x x))).
 
 (* External variables:
      Type bool cons false list nil op_ze__ op_zl__ op_zlzg__ op_zp__ op_zt__ pair
-     plus true Data.Foldable.foldr Data.Tuple.fst Err.Default GHC.Base.Ord
-     GHC.Base.map GHC.Base.op_z2218U__ GHC.Base.op_zl__ GHC.Err.error List.fold_right
-     List.map Nat.add
+     plus true Data.Foldable.foldr Data.Tuple.fst GHC.Base.Ord GHC.Base.map
+     GHC.Base.op_z2218U__ GHC.Base.op_zl__ GHC.Err.Default GHC.Err.error
+     List.fold_right List.map Nat.add
 *)

examples/graph/lib/Data/Graph/Inductive/Internal/Queue.v

@@ -13,9 +13,9 @@ Require Coq.Program.Wf.
 (* Converted imports: *)
 
 Require Data.Foldable.
-Require Err.
 Require GHC.Base.
 Require GHC.DeferredFix.
+Require GHC.Err.
 Require GHC.List.
 
 (* Converted type declarations: *)
@@ -38,7 +38,8 @@ Definition queuePut {a : Type} : a -> Queue a -> Queue a :=
 Definition queuePutList {a : Type} : list a -> Queue a -> Queue a :=
   fun xs q => Data.Foldable.foldl' (GHC.Base.flip queuePut) q xs.
 
-Definition queueGet {a} `{Err.Default (a * Queue a)} : Queue a -> a * Queue a :=
+Definition queueGet {a} `{GHC.Err.Default (a * Queue a)}
+   : Queue a -> a * Queue a :=
   GHC.DeferredFix.deferredFix1 (fun queueGet (arg_0__ : Queue a) =>
                                   match arg_0__ with
                                   | MkQueue ins (cons item rest) => pair item (MkQueue ins rest)
@@ -51,6 +52,6 @@ Definition queueEmpty {a : Type} : Queue a -> bool :=
 
 (* External variables:
      Type andb bool cons list nil op_zt__ pair Data.Foldable.foldl'
-     Data.Foldable.null Err.Default GHC.Base.flip GHC.DeferredFix.deferredFix1
+     Data.Foldable.null GHC.Base.flip GHC.DeferredFix.deferredFix1 GHC.Err.Default
      GHC.List.reverse
 *)

examples/graph/lib/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../containers/lib ""
 
 Data/Graph/Inductive/Graph.v Data/Graph/Inductive/Internal/Queue.v Data/Graph/Inductive/Internal/RootPath.v Data/Graph/Inductive/Internal/Heap.v Data/Graph/Inductive/Query/BFS.v Data/Graph/Inductive/Query/SP.v

examples/graph/module-edits/Data/Graph/Inductive/Graph/edits

@@ -29,10 +29,10 @@ in Data.Graph.Inductive.Graph.lab rewrite forall, GHC.Base.fmap = (@GHC.Base.fma
 rewrite forall s, (GHC.Show.show s) = (GHC.Base.hs_string__ String.EmptyString)
 
 #need some Default constraints
-set type Data.Graph.Inductive.Graph.insEdge : forall {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}, (LEdge b) -> ((gr a b) -> (gr a b))
-set type Data.Graph.Inductive.Graph.insEdges : forall {gr} {b} {a} `{DynGraph gr} `{Err.Default (Context a b)}, list (LEdge b) -> ((gr a b) -> (gr a b))
-set type Data.Graph.Inductive.Graph.context: forall {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}, (gr a b) -> (Node -> (Context a b))
-set type Data.Graph.Inductive.Graph.deg: forall {gr} {a} {b} `{Graph gr} `{Err.Default (Context a b)}, (gr a b) -> (Node -> GHC.Num.Int)
+set type Data.Graph.Inductive.Graph.insEdge : forall {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}, (LEdge b) -> ((gr a b) -> (gr a b))
+set type Data.Graph.Inductive.Graph.insEdges : forall {gr} {b} {a} `{DynGraph gr} `{GHC.Err.Default (Context a b)}, list (LEdge b) -> ((gr a b) -> (gr a b))
+set type Data.Graph.Inductive.Graph.context: forall {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}, (gr a b) -> (Node -> (Context a b))
+set type Data.Graph.Inductive.Graph.deg: forall {gr} {a} {b} `{Graph gr} `{GHC.Err.Default (Context a b)}, (gr a b) -> (Node -> GHC.Num.Int)
 
 #Coq gets confused about some polymorphic definitions
 in Data.Graph.Inductive.Graph.hasNeighborAdj rewrite forall, Data.Foldable.elem = GHC.List.elem

examples/graph/module-edits/Data/Graph/Inductive/Internal/Heap/edits

@@ -2,8 +2,8 @@ skip Data.Graph.Inductive.Internal.Heap.prettyHeap
 skip Data.Graph.Inductive.Internal.Heap.printPrettyHeap
 
 #needs default as well for some reason
-set type Data.Graph.Inductive.Internal.Heap.splitMin: forall {a} {b} `{GHC.Base.Ord a} `{Err.Default ((a * b) * (Heap a b))}, (Heap a b) -> ((a * b) * (Heap a b))
-set type Data.Graph.Inductive.Internal.Heap.findMin: forall {a} {b} `{Err.Default (a * b)}, (Heap a b) -> (a * b)
+set type Data.Graph.Inductive.Internal.Heap.splitMin: forall {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default ((a * b) * (Heap a b))}, (Heap a b) -> ((a * b) * (Heap a b))
+set type Data.Graph.Inductive.Internal.Heap.findMin: forall {a} {b} `{GHC.Err.Default (a * b)}, (Heap a b) -> (a * b)
 
 #need to prove that toList terminates - we need a function for the size of a heap
 add Data.Graph.Inductive.Internal.Heap Fixpoint Data.Graph.Inductive.Internal.Heap.size {a} {b} (h: Heap a b) :=
@@ -56,8 +56,8 @@ termination Data.Graph.Inductive.Internal.Heap.toList        {measure (Data.Grap
 obligations Data.Graph.Inductive.Internal.Heap.toList       (Tactics.program_simpl; apply toList_termination; auto)
 
 #more defaut constrants 
-set type Data.Graph.Inductive.Internal.Heap.toList: forall {a} {b} `{GHC.Base.Ord a} `{Err.Default (a * b)}, (Heap a b) -> list (a * b)
-set type Data.Graph.Inductive.Internal.Heap.heapsort: forall {a} `{GHC.Base.Ord a} `{Err.Default (a * a)}, list a -> list a
+set type Data.Graph.Inductive.Internal.Heap.toList: forall {a} {b} `{GHC.Base.Ord a} `{GHC.Err.Default (a * b)}, (Heap a b) -> list (a * b)
+set type Data.Graph.Inductive.Internal.Heap.heapsort: forall {a} `{GHC.Base.Ord a} `{GHC.Err.Default (a * a)}, list a -> list a
 
 #recursive definition that is difficult to translate
 skip class GHC.Base.Ord

examples/graph/module-edits/Data/Graph/Inductive/Internal/Queue/edits

@@ -1,3 +1,3 @@
 #does not terminate on empty queue
-set type Data.Graph.Inductive.Internal.Queue.queueGet: forall {a} `{Err.Default (a * Queue a)}, Queue a -> (a * Queue a)
+set type Data.Graph.Inductive.Internal.Queue.queueGet: forall {a} `{GHC.Err.Default (a * Queue a)}, Queue a -> (a * Queue a)
 termination Data.Graph.Inductive.Internal.Queue.queueGet  deferred

examples/graph/theories/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 -Q ../../../base-thy  Proofs
 -Q ../../graph/lib ""
 -Q ../../containers/lib ""

examples/shuffle/Makefile

@@ -22,7 +22,7 @@ coq: $(OUT)/Makefile
 $(OUT)/_CoqProject: $(OUT) Makefile
 	mkdir -p $(OUT)
 	echo '-Q .                      ""' >  $@
-	echo '-R ../../../base          ""' >> $@
+	echo '-Q ../../../base          ""' >> $@
 	echo '-Q ../../containers/lib   ""' >> $@
 	echo '-Q ../../transformers/lib ""' >> $@
 	(cd $(OUT) && find . -name '*.v')   >> $@

examples/shuffle/theories/_CoqProject

@@ -1,6 +1,6 @@
 -Q . Proofs
 
--R ../../../base     ""
+-Q ../../../base     ""
 -Q ../../../base-thy Proofs
 
 -Q ../../transformers/lib    ""

examples/transformers/Makefile

@@ -72,7 +72,7 @@ $(OUT)/_CoqProject : Makefile
 	mkdir -p $(OUT)
 	> $@
 	echo '-Q . ""' >> $@
-	echo '-R ../../../base ""' >> $@
+	echo '-Q ../../../base ""' >> $@
 	echo $(addsuffix .v,$(HANDMOD)) >> $@
 	echo $(addsuffix .v,$(MODULES)) >> $@
 	echo $(addsuffix .v,$(SPECIAL_MODULES)) >> $@

examples/transformers/lib/_CoqProject

@@ -1,5 +1,5 @@
 -Q . ""
--R ../../../base ""
+-Q ../../../base ""
 
 Data/Functor/Constant.v Data/Functor/Reverse.v Control/Applicative/Backwards.v Control/Applicative/Lift.v Control/Monad/Trans/Class.v Control/Monad/Signatures.v Control/Monad/Trans/Identity.v Control/Monad/Trans/Reader.v Control/Monad/Trans/Writer/Lazy.v Control/Monad/Trans/State/Lazy.v Control/Monad/Trans/Cont.v Control/Monad/Trans/Except.v Control/Monad/Trans/Maybe.v Control/Monad/Trans/RWS/Lazy.v