Fix warnings and coqdep issues

CertiCoq · Mar 23, 2020 · 2ca697d · 2ca697d
1 parent a2dbc30
commit 2ca697d
Show file tree

Hide file tree

Showing 15 changed files with 39 additions and 33 deletions.
diff --git a/theories/L1g/instances.v b/theories/L1g/instances.v
@@ -6,6 +6,10 @@ Require Import certiClasses.
 Require Import Common.Common.
 Require Import Common.classes.
 Require Import certiClasses2.
+Require Import SquiggleEq.UsefulTypes.
+Require Import DecidableClass.
+Require Import String.
+Require Import certiClasses.
 
 Instance bigStepOpSemL1gTerm: BigStepOpSem (Program Term) (Program Term).
 Proof.
@@ -20,9 +24,6 @@ Instance WfL1gTerm: GoodTerm (Program L1g.compile.Term) :=
       mkPgm trm env => WFapp trm /\ WFaEnv WFapp env
     end.
 
-Require Import SquiggleEq.UsefulTypes.
-Require Import DecidableClass.
-
 Lemma nth_pres_WFapp:
   forall (us:list Term),
     WFapps us -> forall n t, List.nth_error us n = Some t -> WFapp t.
@@ -79,10 +80,10 @@ Local Generalizable Variable Lj.
 
 Axiom debug : forall {A}, String.string -> A -> A.
 Extract Constant debug => "(fun msg x -> Certicoq_debug.certicoq_msg_debug msg; x)".
-Require Import String.
+
 (** When defining [Show] instance for your own datatypes, you sometimes need to
     start a new line for better printing. [nl] is a shorthand for it. *)
-    Definition nl : string := String (Ascii.ascii_of_nat 10) EmptyString.
+Definition nl : string := String (Ascii.ascii_of_nat 10) EmptyString.
 
 Definition translateTo `{CerticoqTranslation (Program L1g.compile.Term) Lj}
   (p:Template.Ast.program): exception Lj :=
@@ -94,8 +95,6 @@ Definition translateTo `{CerticoqTranslation (Program L1g.compile.Term) Lj}
 
 Arguments translateTo Lj {H} p.
 
-Require Import certiClasses.
-
 Definition ctranslateTo {Term Value BigStep WF QH ObsS }
   (Lj: @CerticoqLanguage Term Value BigStep WF QH ObsS)
    `{CerticoqTranslation (Program L1g.compile.Term) (cTerm Lj)}

diff --git a/theories/L4_deBruijn/L4_2_to_L4_5.v b/theories/L4_deBruijn/L4_2_to_L4_5.v
@@ -35,6 +35,11 @@ Require Import Datatypes.
 Require Import SetoidList.
 Require Import List.
 
+Require Import Common.ExtLibMisc.
+Require Import ExtLib.Structures.Monads.
+Require Import ExtLib.Data.Monads.OptionMonad.
+Import Monad.MonadNotation.
+
 Definition L4_5_Term :Type := (@NTerm NVar L4_5Opid).
 Definition L4_5_BTerm :Type := (@BTerm NVar L4_5Opid).
 
@@ -55,12 +60,6 @@ Typeclasses eauto :=4.
 
 Open Scope program_scope.
 
-Require Import List.
-
-Require Import Common.ExtLibMisc.
-Require Import ExtLib.Structures.Monads.
-Require Import ExtLib.Data.Monads.OptionMonad.
-Import Monad.MonadNotation.
 Open Scope monad_scope.
 
 (* modified from L4.polyEval.eval_n to remove the cases for \box *)

diff --git a/theories/L4_deBruijn/instances.v b/theories/L4_deBruijn/instances.v
@@ -132,7 +132,7 @@ Existing Instance dummyEnvBigStep | 1000000.
 (* very low priority *)
 Existing Instance dummyEnvWf | 1000000.
 
-Let L4Term := prod ienv  L4.expression.exp.
+Local Definition L4Term := prod ienv L4.expression.exp.
 
 Instance certiL4eval: BigStepOpSem L4.expression.exp L4.expression.exp := eval.
 Global Instance L4_evaln : BigStepOpSemExec (ienv * L4.expression.exp)

diff --git a/theories/L6_PCPS/Heap/bounds.v b/theories/L6_PCPS/Heap/bounds.v
@@ -2,7 +2,8 @@ From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx Ensembles_
      List_util functions tactics map_util.
 
 From CertiCoq.L6.Heap Require Import heap heap_defs 
-     cc_log_rel compat closure_conversion closure_conversion_util GC.
+     cc_log_rel compat GC.
+Require Import CertiCoq.L6.Heap.closure_conversion CertiCoq.L6.Heap.closure_conversion_util.
 
 From Coq Require Import ZArith.Znumtheory Arith Arith.Wf_nat Relations.Relations
                         Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums

diff --git a/theories/L6_PCPS/Heap/closure_conversion_correct.v b/theories/L6_PCPS/Heap/closure_conversion_correct.v
@@ -2,8 +2,8 @@ From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx Ensembles_
      List_util functions tactics map_util.
 
 From CertiCoq.L6.Heap Require Import heap heap_defs heap_equiv space_sem
-     cc_log_rel closure_conversion closure_conversion_util bounds
-     invariants GC.
+     cc_log_rel bounds invariants GC.
+Require Import CertiCoq.L6.Heap.closure_conversion CertiCoq.L6.Heap.closure_conversion_util.
 
 From Coq Require Import ZArith.Znumtheory Relations.Relations Arith.Wf_nat
                         Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums

diff --git a/theories/L6_PCPS/Heap/closure_conversion_corresp.v b/theories/L6_PCPS/Heap/closure_conversion_corresp.v
@@ -4,7 +4,8 @@
 
 From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx
                          Ensembles_util List_util hoare functions tactics.
-From CertiCoq.L6.Heap Require Import closure_conversion closure_conversion_util.
+
+Require Import CertiCoq.L6.Heap.closure_conversion CertiCoq.L6.Heap.closure_conversion_util.
 
 From compcert.lib Require Import Coqlib.
 

diff --git a/theories/L6_PCPS/Heap/closure_conversion_util.v b/theories/L6_PCPS/Heap/closure_conversion_util.v
@@ -4,8 +4,8 @@
 
 From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx
                          Ensembles_util List_util functions tactics.
-From CertiCoq.L6.Heap Require Import closure_conversion heap heap_defs space_sem compat.
-
+From CertiCoq.L6.Heap Require Import heap heap_defs space_sem compat.
+Require Import CertiCoq.L6.Heap.closure_conversion.
 From compcert.lib Require Import Coqlib.
 
 From Coq Require Import ZArith.Znumtheory ArithRing Relations.Relations Arith.Wf_nat

diff --git a/theories/L6_PCPS/Heap/compat.v b/theories/L6_PCPS/Heap/compat.v
@@ -8,7 +8,8 @@ From Coq Require Import NArith.BinNat Relations.Relations MSets.MSets
 From CertiCoq.L6 Require Import functions cps ctx cps_util identifiers ctx Ensembles_util
      List_util tactics set_util map_util.
 
-From CertiCoq.L6.Heap Require Import heap heap_defs heap_equiv GC space_sem cc_log_rel closure_conversion.
+From CertiCoq.L6.Heap Require Import heap heap_defs heap_equiv GC space_sem cc_log_rel.
+Require Import CertiCoq.L6.Heap.closure_conversion.
 
 From compcert.lib Require Import Coqlib.
 

diff --git a/theories/L6_PCPS/Heap/invariants.v b/theories/L6_PCPS/Heap/invariants.v
@@ -2,7 +2,8 @@ From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx Ensembles_
      List_util functions tactics map_util.
 
 From CertiCoq.L6.Heap Require Import heap heap_defs heap_equiv space_sem
-     cc_log_rel closure_conversion closure_conversion_util bounds GC.
+     cc_log_rel bounds GC.
+Require Import CertiCoq.L6.Heap.closure_conversion CertiCoq.L6.Heap.closure_conversion_util.
 
 From Coq Require Import ZArith.Znumtheory Relations.Relations Arith.Wf_nat
                         Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums

diff --git a/theories/L6_PCPS/Heap/log_rel_defs.v b/theories/L6_PCPS/Heap/log_rel_defs.v
@@ -8,6 +8,7 @@ From Coq Require Import NArith.BinNat Relations.Relations MSets.MSets
 From CertiCoq.L6 Require Import functions cps eval cps_util identifiers ctx Ensembles_util set_util
                  List_util Heap.heap Heap.heap_defs Heap.space_sem Heap.GC tactics map_util.
 From compcert Require Import lib.Coqlib.
+Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses.
 
 
 Module LogRelDefs (H : Heap).
@@ -49,7 +50,7 @@ Module LogRelDefs (H : Heap).
   Definition Inj := loc -> loc.
 
   (** Tag for closure records *)
-  Variable (clo_tag : cTag).
+  Parameter (clo_tag : cTag).
 
   Definition exp_rel : Type :=
     IInv -> IInv -> Inv -> Inj ->
@@ -122,8 +123,6 @@ Module LogRelDefs (H : Heap).
 
     End ExpRelDef.
 
-
-    Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses.
 
     Definition fun_body_args : Tlist :=      
       Tcons IInv (Tcons IInv (Tcons Inv (Tcons Inj (Tcons (list value) (Tcons (heap block) (Tcons (list value) (Tcons (heap block) (Tcons Conf (Tcons Conf Tnil))))))))).    

diff --git a/theories/L6_PCPS/Heap/toplevel.v b/theories/L6_PCPS/Heap/toplevel.v
@@ -2,8 +2,10 @@ From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx Ensembles_
      List_util functions tactics map_util.
 
 From CertiCoq.L6.Heap Require Import heap heap_impl heap_defs heap_equiv space_sem
-     cc_log_rel closure_conversion closure_conversion_util bounds
-     invariants GC closure_conversion_correct.
+     cc_log_rel bounds invariants GC.
+
+Require Import CertiCoq.L6.Heap.closure_conversion CertiCoq.L6.Heap.closure_conversion_util
+  CertiCoq.L6.Heap.closure_conversion_correct.
 
 From Coq Require Import ZArith.Znumtheory Relations.Relations Arith.Wf_nat
                         Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums NArith.Ndist

diff --git a/theories/L6_PCPS/closure_conversion_correct.v b/theories/L6_PCPS/closure_conversion_correct.v
@@ -3,8 +3,8 @@
  *)
 
 From CertiCoq.L6 Require Import cps size_cps cps_util set_util hoisting identifiers ctx
-                       Ensembles_util List_util functions closure_conversion
-                       closure_conversion_util eval logical_relations.
+                       Ensembles_util List_util functions eval logical_relations.
+Require Import CertiCoq.L6.closure_conversion CertiCoq.L6.closure_conversion_util.
 Require Import compcert.lib.Coqlib.
 From Coq Require Import ZArith.Znumtheory Relations.Relations Arith.Wf_nat
                         Lists.List MSets.MSets MSets.MSetRBT Numbers.BinNums

diff --git a/theories/L6_PCPS/closure_conversion_corresp.v b/theories/L6_PCPS/closure_conversion_corresp.v
@@ -3,8 +3,8 @@
  *)
 
 From CertiCoq.L6 Require Import cps cps_util set_util identifiers ctx hoare Ensembles_util
-               List_util closure_conversion closure_conversion_util
-               functions logical_relations eval.
+               List_util functions logical_relations eval.
+Require Import CertiCoq.L6.closure_conversion CertiCoq.L6.closure_conversion_util.
 Require Import CertiCoq.L6.closure_conversion_correct.
 Require Import compcert.lib.Coqlib.
 Require Import Coq.ZArith.Znumtheory Coq.Relations.Relations Coq.Arith.Wf_nat.

diff --git a/theories/L6_PCPS/instances.v b/theories/L6_PCPS/instances.v
@@ -8,8 +8,9 @@ From CertiCoq.Common Require Import certiClasses certiClassesLinkable Common.
 Require Import Coq.Unicode.Utf8.
 
 Require Import ZArith.
-From CertiCoq.L6 Require Import cps cps_util eval shrink_cps L5_to_L6 beta_contraction uncurry closure_conversion
+From CertiCoq.L6 Require Import cps cps_util eval shrink_cps L5_to_L6 beta_contraction uncurry 
      hoisting Heap.dead_param_elim lambda_lifting.
+Require Import CertiCoq.L6.closure_conversion.
 From CertiCoq.L7 Require Import L6_to_Clight.
 
 

diff --git a/theories/L6_PCPS/shrink_cps.v b/theories/L6_PCPS/shrink_cps.v
@@ -1401,7 +1401,9 @@ Section CONTRACT.
            | _ => existT _ (Eapp f' t ys', count, im) (ble_refl im)
          end)
     end.
-    Solve Obligations with (program_simpl; unfold term_sub_inl_size; simpl;  rewrite <- Nat.add_succ_r;  rewrite <- Nat.add_lt_mono_l;  eapply Nat.le_lt_trans; [apply sub_set_size | (simpl; unfold lt; reflexivity)]).
+    Solve Obligations with (program_simpl; unfold term_sub_inl_size; simpl;
+      rewrite <- ?Nat.add_succ_r;  rewrite <- ?Nat.add_lt_mono_l;  
+      try (eapply Nat.le_lt_trans; [apply sub_set_size | (simpl; unfold lt; reflexivity)])).
   Next Obligation. 
     unfold term_sub_inl_size in *; simpl in *.
     assert (term_size k < term_size (Ecase v cl))%nat.