From b3894910d6cf4048914c2ffc6eabdfa122e87e09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit-Claudel?= <clement.pitclaudel@live.com>
Date: Sat, 16 Nov 2019 11:49:34 -0500
Subject: [PATCH] coq: Clean up imports

---
 coq/CircuitCorrectness.v  | 3 ---
 coq/CircuitProperties.v   | 1 -
 coq/Circuits.v            | 2 --
 coq/Common.v              | 5 +++--
 coq/Desugaring.v          | 2 --
 coq/Environments.v        | 2 --
 coq/IndexUtils.v          | 3 ---
 coq/Interop.v             | 4 +---
 coq/Member.v              | 3 ---
 coq/OneRuleAtATime.v      | 2 --
 coq/Parsing.v             | 6 +-----
 coq/PrimitiveProperties.v | 3 ---
 coq/SemanticProperties.v  | 3 +--
 coq/Semantics.v           | 2 --
 coq/SyntaxMacros.v        | 7 +------
 coq/TypeInference.v       | 2 --
 coq/TypedSyntax.v         | 1 -
 coq/TypedSyntaxTools.v    | 4 +---
 coq/Types.v               | 2 --
 coq/UntypedSyntaxTools.v  | 3 ---
 20 files changed, 8 insertions(+), 52 deletions(-)

diff --git a/coq/CircuitCorrectness.v b/coq/CircuitCorrectness.v
index 82aec826..ea939e40 100644
--- a/coq/CircuitCorrectness.v
+++ b/coq/CircuitCorrectness.v
@@ -1,7 +1,4 @@
 Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring Coq.setoid_ring.Ring.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
-Import ListNotations.
 
 Require Import
         Koika.Common Koika.Environments Koika.Syntax
diff --git a/coq/CircuitProperties.v b/coq/CircuitProperties.v
index a9f04988..1a14ff5c 100644
--- a/coq/CircuitProperties.v
+++ b/coq/CircuitProperties.v
@@ -1,4 +1,3 @@
-Require Export Coq.Bool.Bool Coq.Lists.List.
 Require Export Koika.Circuits.
 Require Import Koika.Common Koika.Environments Koika.Types.
 
diff --git a/coq/Circuits.v b/coq/Circuits.v
index 8e2cf177..247a56ba 100644
--- a/coq/Circuits.v
+++ b/coq/Circuits.v
@@ -1,7 +1,5 @@
 Require Export Koika.Common Koika.Environments.
 Require Import Koika.Syntax Koika.TypedSyntax Koika.TypedSyntaxTools.
-Require Import Coq.Strings.String.
-Open Scope string_scope.
 
 Import PrimTyped CircuitSignatures.
 
diff --git a/coq/Common.v b/coq/Common.v
index 1b438bcc..1d59292e 100644
--- a/coq/Common.v
+++ b/coq/Common.v
@@ -1,8 +1,9 @@
-Require Import Coq.Lists.List Coq.Bool.Bool Coq.Strings.String.
 Require Export Coq.omega.Omega.
+Require Export Coq.Lists.List Coq.Bool.Bool Coq.Strings.String.
 Require Export Koika.EqDec Koika.Vect Koika.FiniteType Koika.Show.
 
-Import ListNotations.
+Export ListNotations.
+Global Open Scope string_scope.
 Global Open Scope list_scope.
 
 (* https://coq-club.inria.narkive.com/HeWqgvKm/boolean-simplification *)
diff --git a/coq/Desugaring.v b/coq/Desugaring.v
index db557d13..1cb9671d 100644
--- a/coq/Desugaring.v
+++ b/coq/Desugaring.v
@@ -1,6 +1,4 @@
 Require Import Koika.Common Koika.Environments Koika.Syntax Koika.TypedSyntax Koika.ErrorReporting Koika.SyntaxMacros.
-Require Import Coq.Lists.List.
-Import ListNotations.
 
 Section Desugaring.
   (* The desugaring phase can produce larger terms than its inputs, and so
diff --git a/coq/Environments.v b/coq/Environments.v
index ef773902..99e9fe18 100644
--- a/coq/Environments.v
+++ b/coq/Environments.v
@@ -1,7 +1,5 @@
-Require Import Coq.Strings.String Coq.Lists.List.
 Require Import Koika.Common.
 Require Export Koika.Member.
-Import ListNotations.
 
 Section Contexts.
   Context {K: Type}.
diff --git a/coq/IndexUtils.v b/coq/IndexUtils.v
index e7f99fec..ecd24122 100644
--- a/coq/IndexUtils.v
+++ b/coq/IndexUtils.v
@@ -1,9 +1,6 @@
 Require Coq.Logic.FinFun.
-Require Import Coq.Lists.List.
 Require Import Koika.Common Koika.Vect Koika.Member.
 
-Import ListNotations.
-
 Fixpoint all_indices (bound: nat) : vect (index bound) bound :=
   match bound as n return (vect (index n) n) with
   | 0 => vect_nil
diff --git a/coq/Interop.v b/coq/Interop.v
index b561ee91..c3a5eda6 100644
--- a/coq/Interop.v
+++ b/coq/Interop.v
@@ -1,7 +1,5 @@
-Require Import Coq.Strings.String Coq.Lists.List.
-Require Import Koika.Environments Koika.Types Koika.TypedSyntax Koika.Circuits.
+Require Import Koika.Common Koika.Environments Koika.Types Koika.TypedSyntax Koika.Circuits.
 Require Export Koika.Primitives.
-Import ListNotations.
 
 Inductive empty_ext_fn_t :=.
 Definition empty_Sigma (fn: empty_ext_fn_t)
diff --git a/coq/Member.v b/coq/Member.v
index 9fa2e80a..455c8695 100644
--- a/coq/Member.v
+++ b/coq/Member.v
@@ -1,8 +1,5 @@
-Require Import Coq.Strings.String Coq.Lists.List.
 Require Import Koika.Common.
 
-Import ListNotations.
-
 Inductive member {K: Type}: K -> list K -> Type :=
 | MemberHd: forall k sig, member k (k :: sig)
 | MemberTl: forall k k' sig, member k sig -> member k (k' :: sig).
diff --git a/coq/OneRuleAtATime.v b/coq/OneRuleAtATime.v
index 039a37f7..aeec4827 100644
--- a/coq/OneRuleAtATime.v
+++ b/coq/OneRuleAtATime.v
@@ -1,8 +1,6 @@
 Require Import Koika.Common Koika.Syntax Koika.TypedSyntax Koika.SemanticProperties.
 Require Import Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring Coq.setoid_ring.Ring.
-Require Import Coq.Lists.List.
 
-Import ListNotations.
 Open Scope bool_scope.
 
 Section Proof.
diff --git a/coq/Parsing.v b/coq/Parsing.v
index 06a91dc1..25d49dcb 100644
--- a/coq/Parsing.v
+++ b/coq/Parsing.v
@@ -1,7 +1,5 @@
-Require Coq.Lists.List.
-Require Import Coq.Strings.String.
-
 Require Import
+        Koika.Common
         Koika.Syntax
         Koika.IdentParsing.
 
@@ -10,8 +8,6 @@ Export Koika.Primitives.PrimUntyped.
 Export Coq.Strings.String.
 Export Coq.Lists.List.ListNotations.
 
-Open Scope string_scope.
-
 Declare Custom Entry koika.
 Declare Custom Entry koika_args.
 Declare Custom Entry koika_var.
diff --git a/coq/PrimitiveProperties.v b/coq/PrimitiveProperties.v
index 45964d06..5f72417c 100644
--- a/coq/PrimitiveProperties.v
+++ b/coq/PrimitiveProperties.v
@@ -1,8 +1,5 @@
-Require Import Coq.Lists.List.
 Require Import Koika.Primitives.
-
 Import BitFuns.
-Import ListNotations.
 
 Ltac min_t :=
   repeat match goal with
diff --git a/coq/SemanticProperties.v b/coq/SemanticProperties.v
index 2529a8bd..1d868199 100644
--- a/coq/SemanticProperties.v
+++ b/coq/SemanticProperties.v
@@ -1,5 +1,4 @@
-Require Export Coq.Lists.List Coq.Bool.Bool.
-Require Export Koika.Semantics.
+Require Export Koika.Common Koika.Semantics.
 
 Section Lists.
   Lemma list_find_opt_app {A B} (f: A -> option B) (l l': list A) :
diff --git a/coq/Semantics.v b/coq/Semantics.v
index b6dff454..01590341 100644
--- a/coq/Semantics.v
+++ b/coq/Semantics.v
@@ -1,6 +1,4 @@
-Require Import Coq.Lists.List Coq.Bool.Bool.
 Require Export Koika.Common Koika.Environments Koika.Vect Koika.Syntax Koika.TypedSyntax.
-Import ListNotations.
 
 Section Logs.
   Inductive LogEntryKind :=
diff --git a/coq/SyntaxMacros.v b/coq/SyntaxMacros.v
index dc3aca2f..9fb04c83 100644
--- a/coq/SyntaxMacros.v
+++ b/coq/SyntaxMacros.v
@@ -1,7 +1,4 @@
-Require Import Coq.Lists.List.
 Require Import Koika.Common Koika.Syntax Koika.TypedSyntax Koika.Primitives.
-Import ListNotations.
-
 Import PrimUntyped.
 
 Section SyntaxMacros.
@@ -51,8 +48,6 @@ Module Display.
     | Str (s: string)
     | Value (tau: type).
 
-    Open Scope string_scope.
-
     Notation intfun := (InternalFunction fn_name_t var_t uaction).
 
     Definition empty_printer : InternalFunction fn_name_t var_t uaction :=
@@ -75,7 +70,7 @@ Module Display.
            int_retType := int_retType;
            int_body := (USeq (display_utf8 s) int_body) |}
       | Value tau =>
-        let arg := "arg" ++ show offset in
+        let arg := String.append "arg" (show offset) in
         {| int_name := int_name;
            int_argspec := (arg, tau) :: int_argspec;
            int_retType := unit_t;
diff --git a/coq/TypeInference.v b/coq/TypeInference.v
index d556fd24..317d37d2 100644
--- a/coq/TypeInference.v
+++ b/coq/TypeInference.v
@@ -2,8 +2,6 @@ Require Import
         Koika.Common Koika.Environments
         Koika.Syntax Koika.TypedSyntax Koika.SyntaxMacros
         Koika.Desugaring Koika.ErrorReporting.
-Require Import Coq.Lists.List.
-Import ListNotations.
 
 Section ErrorReporting.
   Context {pos_t var_t fn_name_t reg_t ext_fn_t: Type}.
diff --git a/coq/TypedSyntax.v b/coq/TypedSyntax.v
index 3190a0a9..12647605 100644
--- a/coq/TypedSyntax.v
+++ b/coq/TypedSyntax.v
@@ -1,4 +1,3 @@
-Require Import Coq.Lists.List.
 Require Export Koika.Common Koika.Environments Koika.Types Koika.Primitives.
 
 Import PrimTyped PrimSignatures.
diff --git a/coq/TypedSyntaxTools.v b/coq/TypedSyntaxTools.v
index b0ba6a2a..ff654632 100644
--- a/coq/TypedSyntaxTools.v
+++ b/coq/TypedSyntaxTools.v
@@ -1,6 +1,4 @@
-Require Import Coq.Bool.Bool Coq.Lists.List.
 Require Import Koika.Member Koika.TypedSyntax.
-Import ListNotations.
 
 Section TypedSyntaxTools.
   Context {pos_t var_t rule_name_t reg_t ext_fn_t: Type}.
@@ -101,7 +99,7 @@ Section TypedSyntaxTools.
     Definition path_dependency_graph (path: list rule_name_t) : list (reg_t * list edge) :=
       let path_with_footprints := add_footprints path in
       let rules_by_register := compute_rules_by_registers path_with_footprints in
-      let deps_by_register := map REnv (fun reg rr => find_dependencies rr) rules_by_register in
+      let deps_by_register := Environments.map REnv (fun reg rr => find_dependencies rr) rules_by_register in
       to_alist REnv deps_by_register.
 
     Definition dependency_graph (s: scheduler) : list (list (reg_t * list edge)) :=
diff --git a/coq/Types.v b/coq/Types.v
index afad9cbb..5c7e4103 100644
--- a/coq/Types.v
+++ b/coq/Types.v
@@ -1,7 +1,5 @@
 Require Export Coq.Strings.String.
 Require Export Koika.Common Koika.Vect Koika.IndexUtils.
-Require Import Coq.Lists.List.
-Import ListNotations.
 
 (** * Definitions **)
 
diff --git a/coq/UntypedSyntaxTools.v b/coq/UntypedSyntaxTools.v
index 4bcdbbc6..557406ef 100644
--- a/coq/UntypedSyntaxTools.v
+++ b/coq/UntypedSyntaxTools.v
@@ -1,8 +1,5 @@
-Require Import Coq.Lists.List.
 Require Import Koika.Syntax.
 
-Import ListNotations.
-
 Section SyntaxTools.
   Section CoqErrorReporting.
     (* We don't have explicit positions in Coq, so the next best thing is to