Move erasure to its own directory

Author: mattam82

Diff for: Makefile

@@ -1,25 +1,29 @@
-all: template-coq checker
+all: template-coq checker extraction
 
 .PHONY: all template-coq checker install html clean mrproper .merlin test-suite translations
 
 install: 
 	$(MAKE) -C template-coq install
 	$(MAKE) -C checker install
+	$(MAKE) -C extraction install
 
 html: all
 	$(MAKE) -C template-coq html
+	$(MAKE) -C extraction html
 	mv template-coq/html/*.html html
 	rm template-coq/html/coqdoc.css
 	rm -d template-coq/html
 
 clean:
 	$(MAKE) -C template-coq clean
+	$(MAKE) -C extraction clean
 	$(MAKE) -C checker clean
 	$(MAKE) -C test-suite clean
 	$(MAKE) -C translations clean
 
 mrproper:
 	$(MAKE) -C template-coq mrproper
+	$(MAKE) -C extraction mrproper
 	$(MAKE) -C checker mrproper
 
 .merlin:
@@ -29,6 +33,9 @@ mrproper:
 template-coq:
 	$(MAKE) -C template-coq
 
+extraction: template-coq
+	$(MAKE) -C extraction
+
 checker: template-coq
 	./movefiles.sh
 	$(MAKE) -C checker

Diff for: extraction/_CoqProject

@@ -0,0 +1,10 @@
+-R theories Extraction
+-Q ../template-coq/theories Template
+
+theories/Ast.v
+theories/Induction.v
+theories/LiftSubst.v
+theories/UnivSubst.v
+theories/WcbvEval.v
+theories/Typing.v
+theories/Erase.v

Diff for: template-coq/theories/Erasure/Ast.v renamed to extraction/theories/Ast.v

@@ -6,9 +6,9 @@ Require Import List. Import ListNotations.
 From Template Require Import monad_utils.
 From Template Require Export univ uGraph Ast.
 
-(** Erased terms
+(** Extracted terms
 
-  These are the terms produced by erasure:
+  These are the terms produced by extraction:
   compared to kernel terms, all proofs are translated to [tBox] and
   casts are removed.
 *)

Diff for: template-coq/theories/Erasure/Erase.v renamed to extraction/theories/Erase.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import config utils monad_utils Ast univ Induction LiftSubst UnivSubst Typing Checker Retyping MetaTheory WcbvEval.
-From Template Require AstUtils Erasure.Ast Erasure.WcbvEval.
+From Extraction Require Ast WcbvEval.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.

Diff for: template-coq/theories/Erasure/Induction.v renamed to extraction/theories/Induction.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license.   *)
 
 From Template Require Import univ.
-From Template.Erasure Require Import Ast.
+From Extraction Require Import Ast.
 Require Import List Program.
 Require Import BinPos.
 Require Import Coq.Arith.Compare_dec Bool.

Diff for: template-coq/theories/Erasure/LiftSubst.v renamed to extraction/theories/LiftSubst.v

@@ -1,10 +1,10 @@
 (* Distributed under the terms of the MIT license.   *)
 
 Require Import List Program.
-Require Import Erasure.Ast.
+Require Import Ast.
 Require Import BinPos.
 Require Import Coq.Arith.Compare_dec Bool.
-Require Import Erasure.Induction.
+Require Import Induction.
 
 (** * Lifting and substitution for the AST
 

Diff for: template-coq/theories/Erasure/Typing.v renamed to extraction/theories/Typing.v

@@ -2,8 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 Require Import Template.config Template.utils Template.kernel.univ.
-From Template.Erasure Require Import Ast Induction LiftSubst UnivSubst.
-From Template Require AstUtils Loader.
+From Extraction Require Import Ast Induction LiftSubst UnivSubst.
 Require Import String.
 Local Open Scope string_scope.
 Set Asymmetric Patterns.

Diff for: template-coq/theories/Erasure/UnivSubst.v renamed to extraction/theories/UnivSubst.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import utils univ.
-From Template.Erasure Require Import Ast Induction LiftSubst.
+From Extraction Require Import Ast Induction LiftSubst.
 From Template Require AstUtils.
 Require Import String.
 Local Open Scope string_scope.

Diff for: template-coq/theories/Erasure/WcbvEval.v renamed to extraction/theories/WcbvEval.v

@@ -2,7 +2,7 @@
 
 From Coq Require Import Bool String List Program BinPos Compare_dec Omega.
 From Template Require Import config utils Ast univ.
-From Template.Erasure Require Import Ast Induction LiftSubst UnivSubst Typing.
+From Extraction Require Import Ast Induction LiftSubst UnivSubst Typing.
 From Template Require AstUtils.
 Require Import String.
 Local Open Scope string_scope.
@@ -298,16 +298,3 @@ Section Wcbv.
   Admitted. (* FIXME complete *)
 
 End Wcbv.
-
-(** Well-typed closed programs can't go wrong: they always evaluate to a value. *)
-
-Conjecture closed_typed_wcbeval : forall (Σ : global_context) t T,
-    Σ ;;; [] |- t : T -> exists u, eval (fst Σ) [] t u.
-
-(** Evaluation is a subrelation of reduction: *)
-
-Lemma wcbeval_red : forall (Σ : global_declarations) Γ t u,
-    eval Σ Γ t u -> red Σ Γ t u.
-Proof.
-  induction 1; try constructor; eauto.
-Admitted. (** TODO: Congruence lemmas of red for all constructions (as done in Coq in Coq) *)

Diff for: template-coq/_CoqProject

@@ -29,12 +29,5 @@ theories/MetaTheory.v
 theories/Checker.v
 theories/WcbvEval.v
 theories/Retyping.v
-theories/Erasure/Ast.v
-theories/Erasure/Induction.v
-theories/Erasure/LiftSubst.v
-theories/Erasure/UnivSubst.v
-theories/Erasure/WcbvEval.v
-theories/Erasure/Typing.v
-theories/Erasure/Erase.v
 theories/All.v
 theories/Extraction.v