diff --git a/dependency-graph/A tour of metacoq.png b/dependency-graph/A tour of metacoq.png deleted file mode 100644 index bee4f97f0..000000000 Binary files a/dependency-graph/A tour of metacoq.png and /dev/null differ diff --git a/dependency-graph/depgraph-2020-03-20.dot b/dependency-graph/depgraph-2020-03-20.dot deleted file mode 100644 index b55eb4a33..000000000 --- a/dependency-graph/depgraph-2020-03-20.dot +++ /dev/null @@ -1,294 +0,0 @@ -digraph dependencies { -node[style=filled] -"checker/Substitution" -> "checker/All" -"template-coq/Universes"[label="Universes", color=aquamarine] -"pcuic/PCUICPretty" -> "safechecker/PCUICSafeChecker" -"template-coq/utils/MCEquality"[label="MCEquality", color=aquamarine] -"template-coq/Environment"[label="Environment", color=aquamarine] -"erasure/EWcbvEval" -> "erasure/EAll" -"pcuic/PCUICInduction"[label="PCUICInduction", color=lemonchiffon1] -"safechecker/PCUICSafeRetyping" -> "erasure/SafeErasureFunction" -"template-coq/utils/MCOption"[label="MCOption", color=aquamarine] -"checker/Closed" -> "checker/Weakening" -"template-coq/monad_utils" -> "template-coq/TemplateMonad/Core" -"template-coq/Ast" -> "template-coq/AstUtils" -"template-coq/utils" -> "template-coq/BasicAst" -"template-coq/AstUtils" -> "template-coq/Induction" -"erasure/ESubstitution" -> "erasure/ErasureCorrectness" -"pcuic/PCUICGeneration" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/utils/MCEquality" -> "template-coq/utils" -"template-coq/TemplateMonad"[label="TemplateMonad", color=aquamarine] -"erasure/EAst" -> "erasure/Extract" -"template-coq/TemplateMonad/Common"[label="Common", color=aquamarine] -"erasure/ELiftSubst" -> "erasure/EGlobalEnv" -"template-coq/UnivSubst" -> "template-coq/Extraction" -"template-coq/utils/MCRelations"[label="MCRelations", color=aquamarine] -"pcuic/PCUICInversion"[label="PCUICInversion", color=lemonchiffon1] -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Core" -"pcuic/PCUICRetyping"[label="PCUICRetyping", color=lemonchiffon1] -"pcuic/PCUICTyping" -> "pcuic/PCUICChecker" -"template-coq/AstUtils" -> "template-coq/WfInv" -"erasure/Extraction"[label="Extraction", color=tan] -"pcuic/PCUICNameless" -> "pcuic/PCUICSafeLemmata" -"pcuic/PCUICWeakening" -> "pcuic/PCUICUnivSubstitution" -"pcuic/PCUICChecker"[label="PCUICChecker", color=lemonchiffon1] -"pcuic/PCUICTyping" -> "pcuic/PCUICNameless" -"pcuic/PCUICParallelReduction"[label="PCUICParallelReduction", color=lemonchiffon1] -"template-coq/utils/MCRelations" -> "template-coq/utils/All_Forall" -"pcuic/PCUICAstUtils"[label="PCUICAstUtils", color=lemonchiffon1] -"pcuic/TemplateToPCUIC" -> "safechecker/SafeTemplateChecker" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICSafeLemmata"[label="PCUICSafeLemmata", color=lemonchiffon1] -"checker/Reflect"[label="Reflect", color=seagreen3] -"pcuic/PCUICTyping" -> "pcuic/PCUICMetaTheory" -"pcuic/PCUICWeakeningEnv" -> "pcuic/PCUICClosed" -"pcuic/PCUICPosition"[label="PCUICPosition", color=lemonchiffon1] -"erasure/SafeErasureFunction" -> "erasure/SafeTemplateErasure" -"template-coq/Environment" -> "pcuic/PCUICAst" -"template-coq/TemplateMonad/Core"[label="Core", color=aquamarine] -"template-coq/utils/MCProd" -> "template-coq/utils/All_Forall" -"checker/Retyping"[label="Retyping", color=seagreen3] -"checker/All"[label="checker/All", color=seagreen3] -"template-coq/utils/MCSquash" -> "template-coq/utils/All_Forall" -"pcuic/PCUICConversion" -> "pcuic/PCUICInversion" -"template-coq/utils/MCList" -> "template-coq/utils/All_Forall" -"template-coq/LiftSubst" -> "template-coq/UnivSubst" -"erasure/EAst"[label="EAst", color=tan] -"erasure/EAll"[label="EAll", color=tan] -"safechecker/PCUICSafeReduce"[label="PCUICSafeReduce", color=paleturquoise1] -"checker/Reflect" -> "checker/Generation" -"pcuic/PCUICAlpha"[label="PCUICAlpha", color=lemonchiffon1] -"template-coq/utils/MCCompare"[label="MCCompare", color=aquamarine] -"safechecker/PCUICSafeChecker" -> "safechecker/PCUICSafeRetyping" -"erasure/EGlobalEnv" -> "erasure/EPretty" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Constants" -"pcuic/PCUICTyping" -> "pcuic/PCUICNormal" -"erasure/EArities" -> "erasure/Prelim" -"template-coq/Typing" -> "checker/Normal" -"pcuic/PCUICInduction" -> "pcuic/PCUICLiftSubst" -"erasure/EWndEval"[label="EWndEval", color=tan] -"template-coq/UnivSubst" -> "template-coq/Typing" -"pcuic/PCUICPrincipality" -> "pcuic/PCUICValidity" -"erasure/SafeErasureFunction"[label="SafeErasureFunction", color=tan] -"pcuic/PCUICWeakening"[label="PCUICWeakening", color=lemonchiffon1] -"pcuic/PCUICAlpha" -> "pcuic/PCUICSR" -"pcuic/TemplateToPCUICCorrectness"[label="TemplateToPCUICCorrectness", color=lemonchiffon1] -"template-coq/common/uGraph" -> "safechecker/PCUICSafeConversion" -"erasure/ErasureFunction"[label="ErasureFunction", color=tan] -"template-coq/EnvironmentTyping" -> "pcuic/PCUICTyping" -"checker/Weakening" -> "checker/Substitution" -"template-coq/Pretty" -> "erasure/SafeTemplateErasure" -"template-coq/BasicAst"[label="BasicAst", color=aquamarine] -"template-coq/Loader" -> "template-coq/All" -"template-coq/UnivSubst"[label="UnivSubst", color=aquamarine] -"erasure/Extract" -> "erasure/EAll" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Core" -"erasure/EAst" -> "erasure/EInduction" -"pcuic/PCUICConfluence"[label="PCUICConfluence", color=lemonchiffon1] -"template-coq/Universes" -> "erasure/EAst" -"template-coq/Loader"[label="Loader", color=aquamarine] -"template-coq/EnvironmentTyping"[label="EnvironmentTyping", color=aquamarine] -"template-coq/utils/LibHypsNaming" -> "pcuic/PCUICTyping" -"template-coq/utils/MCOption" -> "template-coq/utils/All_Forall" -"pcuic/PCUICReduction" -> "pcuic/PCUICWeakening" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICEquality" -"pcuic/PCUICPrincipality"[label="PCUICPrincipality", color=lemonchiffon1] -"template-coq/utils/MCList"[label="MCList", color=aquamarine] -"safechecker/PCUICSafeRetyping"[label="PCUICSafeRetyping", color=paleturquoise1] -"pcuic/PCUICParallelReduction" -> "pcuic/PCUICParallelReductionConfluence" -"template-coq/utils/MCString"[label="MCString", color=aquamarine] -"erasure/ESubstitution"[label="ESubstitution", color=tan] -"safechecker/SafeTemplateChecker" -> "safechecker/Extraction" -"erasure/SafeTemplateErasure" -> "erasure/Extraction" -"template-coq/Universes" -> "template-coq/Environment" -"template-coq/utils/LibHypsNaming" -> "checker/WeakeningEnv" -"template-coq/utils/MCCompare" -> "template-coq/utils/MCString" -"safechecker/PCUICSafeConversion" -> "safechecker/PCUICSafeChecker" -"pcuic/PCUICMetaTheory"[label="PCUICMetaTheory", color=lemonchiffon1] -"pcuic/PCUICNormal" -> "pcuic/PCUICSafeLemmata" -"template-coq/TemplateMonad" -> "template-coq/Constants" -"safechecker/PCUICSafeConversion"[label="PCUICSafeConversion", color=paleturquoise1] -"checker/Generation"[label="Generation", color=seagreen3] -"pcuic/PCUICAstUtils" -> "pcuic/PCUICUtils" -"template-coq/Extraction"[label="Extraction", color=aquamarine] -"pcuic/PCUICUnivSubst"[label="PCUICUnivSubst", color=lemonchiffon1] -"template-coq/config" -> "template-coq/Universes" -"pcuic/PCUICInduction" -> "pcuic/PCUICReflect" -"pcuic/PCUICWeakeningEnv"[label="PCUICWeakeningEnv", color=lemonchiffon1] -"template-coq/Pretty"[label="Pretty", color=aquamarine] -"template-coq/monad_utils" -> "template-coq/Typing" -"template-coq/WfInv"[label="WfInv", color=aquamarine] -"pcuic/PCUICAstUtils" -> "pcuic/PCUICLiftSubst" -"pcuic/PCUICTyping" -> "pcuic/PCUICReduction" -"erasure/Prelim" -> "erasure/ESubstitution" -"template-coq/Constants" -> "template-coq/Loader" -"template-coq/utils/MCString" -> "template-coq/utils" -"pcuic/PCUICChecker" -> "pcuic/PCUICRetyping" -"pcuic/PCUICCheckerCompleteness"[label="PCUICCheckerCompleteness", color=lemonchiffon1] -"pcuic/PCUICSubstitution" -> "pcuic/PCUICParallelReduction" -"template-coq/All"[label="template-coq/All", color=aquamarine] -"erasure/ErasureCorrectness" -> "erasure/SafeErasureFunction" -"template-coq/TypingWf" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/PCUICTyping" -> "pcuic/PCUICWeakeningEnv" -"pcuic/PCUICEquality" -> "pcuic/PCUICPosition" -"erasure/ELiftSubst"[label="ELiftSubst", color=tan] -"erasure/ErasureFunction" -> "erasure/SafeTemplateErasure" -"safechecker/Extraction"[label="Extraction", color=paleturquoise1] -"template-coq/Universes" -> "template-coq/common/uGraph" -"checker/Generation" -> "checker/Substitution" -"checker/Checker"[label="Checker", color=seagreen3] -"safechecker/SafeTemplateChecker" -> "erasure/SafeTemplateErasure" -"template-coq/WfInv" -> "checker/WcbvEval" -"pcuic/PCUICSubstitution" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/Environment" -> "template-coq/Ast" -"template-coq/Typing"[label="Typing", color=aquamarine] -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICUnivSubst" -"template-coq/utils/MCArith" -> "template-coq/utils" -"template-coq/utils/MCProd"[label="MCProd", color=aquamarine] -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Extractable" -"pcuic/TemplateToPCUIC"[label="TemplateToPCUIC", color=lemonchiffon1] -"pcuic/PCUICGeneration" -> "pcuic/PCUICValidity" -"template-coq/Induction"[label="Induction", color=aquamarine] -"checker/Normal"[label="Normal", color=seagreen3] -"pcuic/PCUICMetaTheory" -> "erasure/EInversion" -"template-coq/Typing" -> "checker/Generation" -"pcuic/PCUICElimination" -> "erasure/Extract" -"pcuic/PCUICSR" -> "pcuic/PCUICSafeLemmata" - -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICElimination" -"template-coq/Constants"[label="Constants", color=aquamarine] -"pcuic/PCUICNormal"[label="PCUICNormal", color=lemonchiffon1] -"pcuic/PCUICGeneration"[label="PCUICGeneration", color=lemonchiffon1] -"pcuic/PCUICClosed" -> "pcuic/PCUICWeakening" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Extractable" -"template-coq/monad_utils" -> "template-coq/common/uGraph" -"pcuic/PCUICNameless"[label="PCUICNameless", color=lemonchiffon1] -"template-coq/common/uGraph" -> "checker/Checker" -"checker/WcbvEval"[label="WcbvEval", color=seagreen3] -"pcuic/PCUICSize" -> "pcuic/PCUICAstUtils" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Extraction" -"pcuic/PCUICParallelReductionConfluence" -> "pcuic/PCUICConfluence" -"pcuic/PCUICTyping" -> "pcuic/PCUICGeneration" -"checker/Reflect" -> "checker/WcbvEval" -"erasure/EInversion"[label="EInversion", color=tan] -"erasure/EWndEval" -> "erasure/EAll" -"erasure/EArities"[label="EArities", color=tan] -"pcuic/PCUICCumulativity"[label="PCUICCumulativity", color=lemonchiffon1] -"template-coq/utils/All_Forall"[label="All_Forall", color=aquamarine] -"checker/Reflect" -> "checker/Weakening" -"pcuic/PCUICSigmaCalculus"[label="PCUICSigmaCalculus", color=lemonchiffon1] -"erasure/EAst" -> "erasure/EAstUtils" -"pcuic/PCUICClosed"[label="PCUICClosed", color=lemonchiffon1] -"pcuic/PCUICSR"[label="PCUICSR", color=lemonchiffon1] -"template-coq/utils/MCArith"[label="MCArith", color=aquamarine] -"pcuic/PCUICSN"[label="PCUICSN", color=lemonchiffon1] -"template-coq/common/uGraph"[label="uGraph", color=aquamarine] -"erasure/EGlobalEnv" -> "erasure/EWndEval" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICSN" -"template-coq/utils/wGraph"[label="wGraph", color=aquamarine] -"template-coq/LiftSubst"[label="LiftSubst", color=aquamarine] -"pcuic/PCUICTyping"[label="PCUICTyping", color=lemonchiffon1] -"erasure/SafeTemplateErasure"[label="SafeTemplateErasure", color=tan] -"pcuic/PCUICEquality"[label="PCUICEquality", color=lemonchiffon1] -"pcuic/TemplateToPCUIC" -> "pcuic/TemplateToPCUICCorrectness" -"safechecker/SafeTemplateChecker"[label="SafeTemplateChecker", color=paleturquoise1] -"template-coq/LiftSubst" -> "template-coq/Pretty" -"erasure/EInversion" -> "erasure/ErasureCorrectness" -"template-coq/Typing" -> "checker/WeakeningEnv" -"template-coq/AstUtils" -> "template-coq/EnvironmentTyping" -"pcuic/PCUICSN" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICSafeChecker" -> "safechecker/SafeTemplateChecker" -"template-coq/utils/MCSquash"[label="MCSquash", color=aquamarine] -"template-coq/Typing" -> "template-coq/TypingWf" -"pcuic/PCUICWeakening" -> "pcuic/PCUICSigmaCalculus" -"pcuic/PCUICInversion" -> "pcuic/PCUICPrincipality" -"pcuic/PCUICReduction"[label="PCUICReduction", color=lemonchiffon1] -"pcuic/PCUICReduction" -> "pcuic/PCUICCumulativity" -"erasure/EAstUtils" -> "erasure/EGlobalEnv" -"template-coq/TemplateMonad/Core" -> "template-coq/TemplateMonad" -"pcuic/PCUICContextConversion" -> "pcuic/PCUICConversion" -"erasure/EWcbvEval"[label="EWcbvEval", color=tan] -"checker/Retyping" -> "checker/All" -"pcuic/PCUICSubstitution"[label="PCUICSubstitution", color=lemonchiffon1] -"checker/WeakeningEnv" -> "checker/Closed" -"template-coq/Pretty" -> "template-coq/Extraction" -"template-coq/monad_utils"[label="monad_utils", color=aquamarine] -"erasure/EWcbvEval" -> "erasure/Prelim" -"erasure/Extract"[label="Extract", color=tan] -"pcuic/PCUICReflect" -> "pcuic/PCUICEquality" -"pcuic/PCUICPretty"[label="PCUICPretty", color=lemonchiffon1] -"template-coq/AstUtils"[label="AstUtils", color=aquamarine] -"pcuic/PCUICValidity"[label="PCUICValidity", color=lemonchiffon1] -"erasure/EAstUtils"[label="EAstUtils", color=tan] -"template-coq/Induction" -> "checker/Reflect" -"pcuic/PCUICConversion"[label="PCUICConversion", color=lemonchiffon1] -"template-coq/Induction" -> "template-coq/LiftSubst" -"template-coq/Ast" -> "template-coq/TemplateMonad/Common" -"pcuic/PCUICAst" -> "pcuic/PCUICSize" -"pcuic/PCUICAst" -> "pcuic/PCUICCheckerCompleteness" -"pcuic/PCUICElimination"[label="PCUICElimination", color=lemonchiffon1] -"template-coq/EnvironmentTyping" -> "template-coq/Typing" -"pcuic/PCUICParallelReductionConfluence"[label="PCUICParallelReductionConfluence", color=lemonchiffon1] -"template-coq/utils/All_Forall" -> "template-coq/utils" -"template-coq/monad_utils" -> "pcuic/PCUICPosition" -"erasure/EInduction"[label="EInduction", color=tan] -"pcuic/PCUICContextConversion"[label="PCUICContextConversion", color=lemonchiffon1] -"template-coq/config"[label="config", color=aquamarine] -"pcuic/PCUICUtils"[label="PCUICUtils", color=lemonchiffon1] -"safechecker/PCUICSafeChecker"[label="PCUICSafeChecker", color=paleturquoise1] -"erasure/Extract" -> "erasure/EArities" -"template-coq/Ast"[label="Ast", color=aquamarine] -"template-coq/Typing" -> "safechecker/SafeTemplateChecker" -"pcuic/PCUICAst"[label="PCUICAst", color=lemonchiffon1] -"pcuic/PCUICUtils" -> "pcuic/PCUICTyping" -"pcuic/PCUICCumulativity" -> "pcuic/PCUICSubstitution" -"checker/Closed"[label="Closed", color=seagreen3] -"pcuic/PCUICAst" -> "pcuic/PCUICInduction" -"pcuic/PCUICWcbvEval"[label="PCUICWcbvEval", color=lemonchiffon1] -"pcuic/PCUICAst" -> "pcuic/TemplateToPCUIC" -"pcuic/PCUICReflect"[label="PCUICReflect", color=lemonchiffon1] -"pcuic/PCUICPosition" -> "pcuic/PCUICTyping" -"pcuic/PCUICUnivSubstitution"[label="PCUICUnivSubstitution", color=lemonchiffon1] -"template-coq/Typing" -> "template-coq/All" -"template-coq/utils"[label="utils", color=aquamarine] -"template-coq/BasicAst" -> "template-coq/Universes" -"erasure/EInduction" -> "erasure/ELiftSubst" -"pcuic/PCUICValidity" -> "pcuic/PCUICAlpha" -"template-coq/TypingWf"[label="TypingWf", color=aquamarine] -"pcuic/PCUICUnivSubstitution" -> "pcuic/PCUICConfluence" -"pcuic/PCUICWeakening" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICReduction" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICSize"[label="PCUICSize", color=lemonchiffon1] -"erasure/EPretty"[label="EPretty", color=tan] -"template-coq/TypingWf" -> "checker/Weakening" -"erasure/EPretty" -> "erasure/SafeTemplateErasure" -"template-coq/AstUtils" -> "pcuic/TemplateToPCUIC" -"erasure/EGlobalEnv" -> "erasure/EWcbvEval" -"pcuic/PCUICConversion" -> "pcuic/PCUICRetyping" -"erasure/ErasureCorrectness" -> "erasure/ErasureFunction" -"erasure/EGlobalEnv"[label="EGlobalEnv", color=tan] -"erasure/ErasureCorrectness"[label="ErasureCorrectness", color=tan] -"template-coq/utils" -> "template-coq/utils/wGraph" -"pcuic/PCUICConfluence" -> "pcuic/PCUICContextConversion" -"pcuic/PCUICRetyping" -> "erasure/EInversion" -"template-coq/Typing" -> "checker/Checker" -"erasure/Prelim" -> "erasure/EInversion" -"pcuic/PCUICChecker" -> "pcuic/PCUICPretty" -"pcuic/PCUICUnivSubst" -> "pcuic/PCUICTyping" -"erasure/Prelim"[label="Prelim", color=tan] -"template-coq/utils/LibHypsNaming"[label="LibHypsNaming", color=aquamarine] -"pcuic/PCUICLiftSubst"[label="PCUICLiftSubst", color=lemonchiffon1] -"checker/Checker" -> "checker/Retyping" -"template-coq/TemplateMonad/Extractable"[label="Extractable", color=aquamarine] -"template-coq/Typing" -> "checker/WcbvEval" -"template-coq/WfInv" -> "pcuic/TemplateToPCUICCorrectness" -"safechecker/PCUICSafeChecker" -> "erasure/Prelim" -"checker/Substitution"[label="Substitution", color=seagreen3] -"template-coq/utils/wGraph" -> "template-coq/common/uGraph" -"template-coq/All" -> "checker/All" -"checker/WeakeningEnv"[label="WeakeningEnv", color=seagreen3] -"template-coq/monad_utils" -> "pcuic/PCUICCheckerCompleteness" -"template-coq/common/uGraph" -> "template-coq/Constants" -"checker/Weakening"[label="Weakening", color=seagreen3] -"pcuic/PCUICWcbvEval" -> "erasure/EArities" -} diff --git a/dependency-graph/depgraph-2020-03-20.svg b/dependency-graph/depgraph-2020-03-20.svg deleted file mode 100644 index 0490b9be5..000000000 --- a/dependency-graph/depgraph-2020-03-20.svg +++ /dev/null @@ -1,1753 +0,0 @@ - - - - - - -dependencies - - - -checker/Substitution - -Substitution - - - -checker/All - -checker/All - - - -checker/Substitution->checker/All - - - - - -template-coq/Universes - -Universes - - - -template-coq/Environment - -Environment - - - -template-coq/Universes->template-coq/Environment - - - - - -erasure/EAst - -EAst - - - -template-coq/Universes->erasure/EAst - - - - - -template-coq/common/uGraph - -uGraph - - - -template-coq/Universes->template-coq/common/uGraph - - - - - -pcuic/PCUICPretty - -PCUICPretty - - - -safechecker/PCUICSafeChecker - -PCUICSafeChecker - - - -pcuic/PCUICPretty->safechecker/PCUICSafeChecker - - - - - -safechecker/PCUICSafeRetyping - -PCUICSafeRetyping - - - -safechecker/PCUICSafeChecker->safechecker/PCUICSafeRetyping - - - - - -safechecker/SafeTemplateChecker - -SafeTemplateChecker - - - -safechecker/PCUICSafeChecker->safechecker/SafeTemplateChecker - - - - - -erasure/Prelim - -Prelim - - - -safechecker/PCUICSafeChecker->erasure/Prelim - - - - - -template-coq/utils/MCEquality - -MCEquality - - - -template-coq/utils - -utils - - - -template-coq/utils/MCEquality->template-coq/utils - - - - - -template-coq/Ast - -Ast - - - -template-coq/Environment->template-coq/Ast - - - - - -pcuic/PCUICAst - -PCUICAst - - - -template-coq/Environment->pcuic/PCUICAst - - - - - -erasure/EWcbvEval - -EWcbvEval - - - -erasure/EAll - -EAll - - - -erasure/EWcbvEval->erasure/EAll - - - - - -erasure/EWcbvEval->erasure/Prelim - - - - - -pcuic/PCUICInduction - -PCUICInduction - - - -pcuic/PCUICLiftSubst - -PCUICLiftSubst - - - -pcuic/PCUICInduction->pcuic/PCUICLiftSubst - - - - - -pcuic/PCUICReflect - -PCUICReflect - - - -pcuic/PCUICInduction->pcuic/PCUICReflect - - - - - -erasure/SafeErasureFunction - -SafeErasureFunction - - - -safechecker/PCUICSafeRetyping->erasure/SafeErasureFunction - - - - - -erasure/SafeTemplateErasure - -SafeTemplateErasure - - - -erasure/SafeErasureFunction->erasure/SafeTemplateErasure - - - - - -template-coq/utils/MCOption - -MCOption - - - -template-coq/utils/All_Forall - -All_Forall - - - -template-coq/utils/MCOption->template-coq/utils/All_Forall - - - - - -checker/Closed - -Closed - - - -checker/Weakening - -Weakening - - - -checker/Closed->checker/Weakening - - - - - -checker/Weakening->checker/Substitution - - - - - -template-coq/monad_utils - -monad_utils - - - -template-coq/TemplateMonad/Core - -Core - - - -template-coq/monad_utils->template-coq/TemplateMonad/Core - - - - - -pcuic/PCUICPosition - -PCUICPosition - - - -template-coq/monad_utils->pcuic/PCUICPosition - - - - - -template-coq/Typing - -Typing - - - -template-coq/monad_utils->template-coq/Typing - - - - - -template-coq/monad_utils->template-coq/common/uGraph - - - - - -pcuic/PCUICCheckerCompleteness - -PCUICCheckerCompleteness - - - -template-coq/monad_utils->pcuic/PCUICCheckerCompleteness - - - - - -template-coq/TemplateMonad - -TemplateMonad - - - -template-coq/TemplateMonad/Core->template-coq/TemplateMonad - - - - - -template-coq/AstUtils - -AstUtils - - - -template-coq/Ast->template-coq/AstUtils - - - - - -template-coq/TemplateMonad/Common - -Common - - - -template-coq/Ast->template-coq/TemplateMonad/Common - - - - - -template-coq/AstUtils->template-coq/TemplateMonad/Core - - - - - -template-coq/Induction - -Induction - - - -template-coq/AstUtils->template-coq/Induction - - - - - -template-coq/WfInv - -WfInv - - - -template-coq/AstUtils->template-coq/WfInv - - - - - -pcuic/TemplateToPCUIC - -TemplateToPCUIC - - - -template-coq/AstUtils->pcuic/TemplateToPCUIC - - - - - -template-coq/TemplateMonad/Extractable - -Extractable - - - -template-coq/AstUtils->template-coq/TemplateMonad/Extractable - - - - - -template-coq/EnvironmentTyping - -EnvironmentTyping - - - -template-coq/AstUtils->template-coq/EnvironmentTyping - - - - - -template-coq/BasicAst - -BasicAst - - - -template-coq/utils->template-coq/BasicAst - - - - - -template-coq/utils/wGraph - -wGraph - - - -template-coq/utils->template-coq/utils/wGraph - - - - - -template-coq/BasicAst->template-coq/Universes - - - - - -checker/Reflect - -Reflect - - - -template-coq/Induction->checker/Reflect - - - - - -template-coq/LiftSubst - -LiftSubst - - - -template-coq/Induction->template-coq/LiftSubst - - - - - -erasure/ESubstitution - -ESubstitution - - - -erasure/ErasureCorrectness - -ErasureCorrectness - - - -erasure/ESubstitution->erasure/ErasureCorrectness - - - - - -erasure/ErasureCorrectness->erasure/SafeErasureFunction - - - - - -erasure/ErasureFunction - -ErasureFunction - - - -erasure/ErasureCorrectness->erasure/ErasureFunction - - - - - -pcuic/PCUICGeneration - -PCUICGeneration - - - -pcuic/TemplateToPCUICCorrectness - -TemplateToPCUICCorrectness - - - -pcuic/PCUICGeneration->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/PCUICValidity - -PCUICValidity - - - -pcuic/PCUICGeneration->pcuic/PCUICValidity - - - - - -template-coq/Constants - -Constants - - - -template-coq/TemplateMonad->template-coq/Constants - - - - - -erasure/Extract - -Extract - - - -erasure/EAst->erasure/Extract - - - - - -erasure/EInduction - -EInduction - - - -erasure/EAst->erasure/EInduction - - - - - -erasure/EAstUtils - -EAstUtils - - - -erasure/EAst->erasure/EAstUtils - - - - - -erasure/Extract->erasure/EAll - - - - - -erasure/EArities - -EArities - - - -erasure/Extract->erasure/EArities - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Core - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Extractable - - - - - -erasure/ELiftSubst - -ELiftSubst - - - -erasure/EGlobalEnv - -EGlobalEnv - - - -erasure/ELiftSubst->erasure/EGlobalEnv - - - - - -erasure/EGlobalEnv->erasure/EWcbvEval - - - - - -erasure/EPretty - -EPretty - - - -erasure/EGlobalEnv->erasure/EPretty - - - - - -erasure/EWndEval - -EWndEval - - - -erasure/EGlobalEnv->erasure/EWndEval - - - - - -template-coq/UnivSubst - -UnivSubst - - - -template-coq/Extraction - -Extraction - - - -template-coq/UnivSubst->template-coq/Extraction - - - - - -template-coq/UnivSubst->template-coq/Typing - - - - - -template-coq/utils/MCRelations - -MCRelations - - - -template-coq/utils/MCRelations->template-coq/utils/All_Forall - - - - - -pcuic/PCUICInversion - -PCUICInversion - - - -pcuic/PCUICPrincipality - -PCUICPrincipality - - - -pcuic/PCUICInversion->pcuic/PCUICPrincipality - - - - - -pcuic/PCUICRetyping - -PCUICRetyping - - - -erasure/EInversion - -EInversion - - - -pcuic/PCUICRetyping->erasure/EInversion - - - - - -pcuic/PCUICTyping - -PCUICTyping - - - -pcuic/PCUICTyping->pcuic/PCUICGeneration - - - - - -pcuic/PCUICChecker - -PCUICChecker - - - -pcuic/PCUICTyping->pcuic/PCUICChecker - - - - - -pcuic/PCUICNameless - -PCUICNameless - - - -pcuic/PCUICTyping->pcuic/PCUICNameless - - - - - -pcuic/PCUICMetaTheory - -PCUICMetaTheory - - - -pcuic/PCUICTyping->pcuic/PCUICMetaTheory - - - - - -pcuic/PCUICWeakeningEnv - -PCUICWeakeningEnv - - - -pcuic/PCUICTyping->pcuic/PCUICWeakeningEnv - - - - - -pcuic/PCUICNormal - -PCUICNormal - - - -pcuic/PCUICTyping->pcuic/PCUICNormal - - - - - -pcuic/PCUICReduction - -PCUICReduction - - - -pcuic/PCUICTyping->pcuic/PCUICReduction - - - - - -pcuic/PCUICChecker->pcuic/PCUICPretty - - - - - -pcuic/PCUICChecker->pcuic/PCUICRetyping - - - - - -template-coq/WfInv->pcuic/TemplateToPCUICCorrectness - - - - - -checker/WcbvEval - -WcbvEval - - - -template-coq/WfInv->checker/WcbvEval - - - - - -erasure/Extraction - -Extraction - - - -pcuic/PCUICSafeLemmata - -PCUICSafeLemmata - - - -pcuic/PCUICNameless->pcuic/PCUICSafeLemmata - - - - - -pcuic/PCUICElimination - -PCUICElimination - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICElimination - - - - - -pcuic/PCUICSN - -PCUICSN - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICSN - - - - - -pcuic/PCUICWeakening - -PCUICWeakening - - - -pcuic/PCUICUnivSubstitution - -PCUICUnivSubstitution - - - -pcuic/PCUICWeakening->pcuic/PCUICUnivSubstitution - - - - - -pcuic/PCUICSubstitution - -PCUICSubstitution - - - -pcuic/PCUICWeakening->pcuic/PCUICSubstitution - - - - - -pcuic/PCUICSigmaCalculus - -PCUICSigmaCalculus - - - -pcuic/PCUICWeakening->pcuic/PCUICSigmaCalculus - - - - - -pcuic/PCUICConfluence - -PCUICConfluence - - - -pcuic/PCUICUnivSubstitution->pcuic/PCUICConfluence - - - - - -pcuic/PCUICParallelReduction - -PCUICParallelReduction - - - -pcuic/PCUICParallelReductionConfluence - -PCUICParallelReductionConfluence - - - -pcuic/PCUICParallelReduction->pcuic/PCUICParallelReductionConfluence - - - - - -template-coq/utils/All_Forall->template-coq/utils - - - - - -pcuic/PCUICAstUtils - -PCUICAstUtils - - - -pcuic/PCUICAstUtils->pcuic/PCUICLiftSubst - - - - - -pcuic/PCUICUtils - -PCUICUtils - - - -pcuic/PCUICAstUtils->pcuic/PCUICUtils - - - - - -pcuic/TemplateToPCUIC->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/TemplateToPCUIC->safechecker/SafeTemplateChecker - - - - - -safechecker/SafeTemplateChecker->erasure/SafeTemplateErasure - - - - - -safechecker/Extraction - -Extraction - - - -safechecker/SafeTemplateChecker->safechecker/Extraction - - - - - -safechecker/PCUICSafeReduce - -PCUICSafeReduce - - - -safechecker/PCUICSafeConversion - -PCUICSafeConversion - - - -safechecker/PCUICSafeReduce->safechecker/PCUICSafeConversion - - - - - -safechecker/PCUICSafeConversion->safechecker/PCUICSafeChecker - - - - - -checker/Reflect->checker/Weakening - - - - - -checker/Generation - -Generation - - - -checker/Reflect->checker/Generation - - - - - -checker/Reflect->checker/WcbvEval - - - - - -pcuic/PCUICMetaTheory->erasure/EInversion - - - - - -pcuic/PCUICClosed - -PCUICClosed - - - -pcuic/PCUICWeakeningEnv->pcuic/PCUICClosed - - - - - -pcuic/PCUICClosed->pcuic/PCUICWeakening - - - - - -pcuic/PCUICPosition->pcuic/PCUICTyping - - - - - -erasure/SafeTemplateErasure->erasure/Extraction - - - - - -pcuic/PCUICAst->pcuic/PCUICInduction - - - - - -pcuic/PCUICAst->pcuic/TemplateToPCUIC - - - - - -pcuic/PCUICAst->pcuic/PCUICCheckerCompleteness - - - - - -pcuic/PCUICSize - -PCUICSize - - - -pcuic/PCUICAst->pcuic/PCUICSize - - - - - -template-coq/utils/MCProd - -MCProd - - - -template-coq/utils/MCProd->template-coq/utils/All_Forall - - - - - -checker/Retyping - -Retyping - - - -checker/Retyping->checker/All - - - - - -template-coq/utils/MCSquash - -MCSquash - - - -template-coq/utils/MCSquash->template-coq/utils/All_Forall - - - - - -pcuic/PCUICConversion - -PCUICConversion - - - -pcuic/PCUICConversion->pcuic/PCUICInversion - - - - - -pcuic/PCUICConversion->pcuic/PCUICRetyping - - - - - -template-coq/utils/MCList - -MCList - - - -template-coq/utils/MCList->template-coq/utils/All_Forall - - - - - -template-coq/LiftSubst->template-coq/UnivSubst - - - - - -template-coq/Pretty - -Pretty - - - -template-coq/LiftSubst->template-coq/Pretty - - - - - -checker/Generation->checker/Substitution - - - - - -pcuic/PCUICAlpha - -PCUICAlpha - - - -pcuic/PCUICSR - -PCUICSR - - - -pcuic/PCUICAlpha->pcuic/PCUICSR - - - - - -template-coq/utils/MCCompare - -MCCompare - - - -template-coq/utils/MCString - -MCString - - - -template-coq/utils/MCCompare->template-coq/utils/MCString - - - - - -erasure/EPretty->erasure/SafeTemplateErasure - - - - - -template-coq/TemplateMonad/Extractable->template-coq/Extraction - - - - - -template-coq/TemplateMonad/Extractable->template-coq/Constants - - - - - -template-coq/Loader - -Loader - - - -template-coq/Constants->template-coq/Loader - - - - - -pcuic/PCUICNormal->pcuic/PCUICSafeLemmata - - - - - -erasure/EArities->erasure/Prelim - - - - - -erasure/Prelim->erasure/ESubstitution - - - - - -erasure/Prelim->erasure/EInversion - - - - - -template-coq/Typing->safechecker/SafeTemplateChecker - - - - - -template-coq/Typing->checker/Generation - - - - - -checker/Normal - -Normal - - - -template-coq/Typing->checker/Normal - - - - - -template-coq/All - -template-coq/All - - - -template-coq/Typing->template-coq/All - - - - - -checker/WeakeningEnv - -WeakeningEnv - - - -template-coq/Typing->checker/WeakeningEnv - - - - - -template-coq/TypingWf - -TypingWf - - - -template-coq/Typing->template-coq/TypingWf - - - - - -checker/Checker - -Checker - - - -template-coq/Typing->checker/Checker - - - - - -template-coq/Typing->checker/WcbvEval - - - - - -pcuic/PCUICEquality - -PCUICEquality - - - -pcuic/PCUICLiftSubst->pcuic/PCUICEquality - - - - - -pcuic/PCUICUnivSubst - -PCUICUnivSubst - - - -pcuic/PCUICLiftSubst->pcuic/PCUICUnivSubst - - - - - -erasure/EWndEval->erasure/EAll - - - - - -pcuic/PCUICPrincipality->pcuic/PCUICValidity - - - - - -pcuic/PCUICValidity->pcuic/PCUICAlpha - - - - - -pcuic/PCUICSR->pcuic/PCUICSafeLemmata - - - - - -template-coq/common/uGraph->safechecker/PCUICSafeConversion - - - - - -template-coq/common/uGraph->template-coq/Constants - - - - - -template-coq/common/uGraph->checker/Checker - - - - - -erasure/ErasureFunction->erasure/SafeTemplateErasure - - - - - -template-coq/EnvironmentTyping->pcuic/PCUICTyping - - - - - -template-coq/EnvironmentTyping->template-coq/Typing - - - - - -template-coq/Pretty->template-coq/Extraction - - - - - -template-coq/Pretty->erasure/SafeTemplateErasure - - - - - -template-coq/Loader->template-coq/All - - - - - -template-coq/All->checker/All - - - - - -erasure/EInduction->erasure/ELiftSubst - - - - - -pcuic/PCUICContextConversion - -PCUICContextConversion - - - -pcuic/PCUICConfluence->pcuic/PCUICContextConversion - - - - - -template-coq/utils/LibHypsNaming - -LibHypsNaming - - - -template-coq/utils/LibHypsNaming->pcuic/PCUICTyping - - - - - -template-coq/utils/LibHypsNaming->checker/WeakeningEnv - - - - - -pcuic/PCUICReduction->pcuic/PCUICWeakening - - - - - -pcuic/PCUICCumulativity - -PCUICCumulativity - - - -pcuic/PCUICReduction->pcuic/PCUICCumulativity - - - - - -pcuic/PCUICWcbvEval - -PCUICWcbvEval - - - -pcuic/PCUICReduction->pcuic/PCUICWcbvEval - - - - - -pcuic/PCUICEquality->pcuic/PCUICPosition - - - - - -pcuic/PCUICParallelReductionConfluence->pcuic/PCUICConfluence - - - - - -template-coq/utils/MCString->template-coq/utils - - - - - -checker/WeakeningEnv->checker/Closed - - - - - -pcuic/PCUICUtils->pcuic/PCUICTyping - - - - - -pcuic/PCUICUnivSubst->pcuic/PCUICTyping - - - - - -template-coq/config - -config - - - -template-coq/config->template-coq/Universes - - - - - -pcuic/PCUICReflect->pcuic/PCUICEquality - - - - - -pcuic/PCUICSubstitution->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/PCUICSubstitution->pcuic/PCUICParallelReduction - - - - - -template-coq/TypingWf->checker/Weakening - - - - - -template-coq/TypingWf->pcuic/TemplateToPCUICCorrectness - - - - - -checker/Checker->checker/Retyping - - - - - -template-coq/utils/MCArith - -MCArith - - - -template-coq/utils/MCArith->template-coq/utils - - - - - -erasure/EInversion->erasure/ErasureCorrectness - - - - - -pcuic/PCUICElimination->erasure/Extract - - - - - -pcuic/PCUICSize->pcuic/PCUICAstUtils - - - - - -pcuic/PCUICCumulativity->pcuic/PCUICSubstitution - - - - - -erasure/EAstUtils->erasure/EGlobalEnv - - - - - -pcuic/PCUICSN->safechecker/PCUICSafeReduce - - - - - -template-coq/utils/wGraph->template-coq/common/uGraph - - - - - -pcuic/PCUICContextConversion->pcuic/PCUICConversion - - - - - -pcuic/PCUICWcbvEval->erasure/EArities - - - - - diff --git a/dependency-graph/depgraph-2020-09-24.dot b/dependency-graph/depgraph-2020-09-24.dot deleted file mode 100644 index 2bcd4867e..000000000 --- a/dependency-graph/depgraph-2020-09-24.dot +++ /dev/null @@ -1,316 +0,0 @@ -digraph dependencies { -node[style=filled] -"checker/All"[label="All", color=seagreen3] -"checker/Normal"[label="Normal", color=seagreen3] -"checker/Retyping"[label="Retyping", color=seagreen3] -"checker/WcbvEval"[label="WcbvEval", color=seagreen3] -"checker/Checker"[label="Checker", color=seagreen3] -"checker/Substitution"[label="Substitution", color=seagreen3] -"checker/Weakening"[label="Weakening", color=seagreen3] -"checker/Closed"[label="Closed", color=seagreen3] -"checker/WeakeningEnv"[label="WeakeningEnv", color=seagreen3] -"checker/Generation"[label="Generation", color=seagreen3] -"checker/Reflect"[label="Reflect", color=seagreen3] -"template-coq/Loader" -> "template-coq/All" -"template-coq/Typing" -> "template-coq/All" -"template-coq/Environment" -> "template-coq/Ast" -"template-coq/Ast" -> "template-coq/AstUtils" -"template-coq/utils" -> "template-coq/BasicAst" -"template-coq/TemplateMonad" -> "template-coq/Constants" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Constants" -"template-coq/common/uGraph" -> "template-coq/Constants" -"template-coq/Universes" -> "template-coq/Environment" -"template-coq/AstUtils" -> "template-coq/EnvironmentTyping" -"template-coq/AstUtils" -> "template-coq/Induction" -"template-coq/Induction" -> "template-coq/LiftSubst" -"template-coq/Constants" -> "template-coq/Loader" -"template-coq/TemplateMonad/Core" -> "template-coq/TemplateMonad" -"template-coq/Ast" -> "template-coq/TemplateMonad/Common" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Core" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Core" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Extractable" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Extractable" -"template-coq/EnvironmentTyping" -> "template-coq/Typing" -"template-coq/UnivSubst" -> "template-coq/Typing" -"template-coq/Typing" -> "template-coq/TypingWf" -"template-coq/LiftSubst" -> "template-coq/UnivSubst" -"template-coq/BasicAst" -> "template-coq/Universes" -"template-coq/config" -> "template-coq/Universes" -"template-coq/AstUtils" -> "template-coq/WfInv" -"template-coq/Universes" -> "template-coq/common/uGraph" -"template-coq/utils/wGraph" -> "template-coq/common/uGraph" -"template-coq/monad_utils" -> "template-coq/utils" -"template-coq/utils/MCUtils" -> "template-coq/utils" -"template-coq/utils/MCOption" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCSquash" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCPrelude" -> "template-coq/utils/MCList" -"template-coq/utils/MCRelations" -> "template-coq/utils/MCList" -"template-coq/utils/MCList" -> "template-coq/utils/MCOption" -"template-coq/utils/MCProd" -> "template-coq/utils/MCOption" -"template-coq/utils/MCCompare" -> "template-coq/utils/MCString" -"template-coq/utils/All_Forall" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCArith" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCEquality" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCString" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCUtils" -> "template-coq/utils/wGraph" -"template-coq/All" -> "checker/All" -"checker/Retyping" -> "checker/All" -"checker/Substitution" -> "checker/All" -"template-coq/Typing" -> "checker/Checker" -"template-coq/common/uGraph" -> "checker/Checker" -"template-coq/TypingWf" -> "checker/Closed" -"checker/Reflect" -> "checker/Closed" -"checker/WeakeningEnv" -> "checker/Closed" -"template-coq/Typing" -> "checker/Generation" -"checker/Reflect" -> "checker/Generation" -"template-coq/Typing" -> "checker/Normal" -"template-coq/Induction" -> "checker/Reflect" -"checker/Checker" -> "checker/Retyping" -"checker/Generation" -> "checker/Substitution" -"checker/Weakening" -> "checker/Substitution" -"template-coq/Typing" -> "checker/WcbvEval" -"template-coq/WfInv" -> "checker/WcbvEval" -"checker/Reflect" -> "checker/WcbvEval" -"checker/Closed" -> "checker/Weakening" -"template-coq/Typing" -> "checker/WeakeningEnv" -"template-coq/utils/LibHypsNaming" -> "checker/WeakeningEnv" -"safechecker/Extraction"[label="Extraction", color=paleturquoise1] -"safechecker/PCUICSafeRetyping"[label="PCUICSafeRetyping", color=paleturquoise1] -"safechecker/SafeTemplateChecker"[label="SafeTemplateChecker", color=paleturquoise1] -"safechecker/PCUICSafeChecker"[label="PCUICSafeChecker", color=paleturquoise1] -"safechecker/PCUICSafeConversion"[label="PCUICSafeConversion", color=paleturquoise1] -"safechecker/PCUICSafeReduce"[label="PCUICSafeReduce", color=paleturquoise1] -"pcuic/PCUICValidity" -> "pcuic/PCUICAlpha" -"pcuic/PCUICContexts" -> "pcuic/PCUICArities" -"template-coq/EnvironmentTyping" -> "pcuic/PCUICAst" -"pcuic/PCUICSize" -> "pcuic/PCUICAstUtils" -"template-coq/common/uGraph" -> "pcuic/PCUICAstUtils" -"pcuic/PCUICTyping" -> "pcuic/PCUICChecker" -"pcuic/PCUICWeakeningEnv" -> "pcuic/PCUICClosed" -"pcuic/PCUICParallelReductionConfluence" -> "pcuic/PCUICConfluence" -"pcuic/PCUICConfluence" -> "pcuic/PCUICContextConversion" -"pcuic/PCUICCtxShape" -> "pcuic/PCUICContexts" -"pcuic/PCUICContextConversion" -> "pcuic/PCUICConversion" -"pcuic/PCUICInversion" -> "pcuic/PCUICCtxShape" -"pcuic/PCUICNameless" -> "pcuic/PCUICCtxShape" -"template-coq/UnivSubst" -> "pcuic/PCUICCtxShape" -"pcuic/PCUICReduction" -> "pcuic/PCUICCumulativity" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICEquality" -"pcuic/PCUICReflect" -> "pcuic/PCUICEquality" -"pcuic/PCUICTyping" -> "pcuic/PCUICGeneration" -"pcuic/PCUICAst" -> "pcuic/PCUICInduction" -"pcuic/PCUICValidity" -> "pcuic/PCUICInductiveInversion" -"pcuic/PCUICSpine" -> "pcuic/PCUICInductives" -"pcuic/PCUICConversion" -> "pcuic/PCUICInversion" -"pcuic/PCUICAstUtils" -> "pcuic/PCUICLiftSubst" -"pcuic/PCUICInduction" -> "pcuic/PCUICLiftSubst" -"pcuic/PCUICTyping" -> "pcuic/PCUICNameless" -"pcuic/PCUICReduction" -> "pcuic/PCUICNormal" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICParallelReduction" -"pcuic/PCUICParallelReduction" -> "pcuic/PCUICParallelReductionConfluence" -"pcuic/PCUICEquality" -> "pcuic/PCUICPosition" -"pcuic/PCUICChecker" -> "pcuic/PCUICPretty" -"pcuic/PCUICSR" -> "pcuic/PCUICPrincipality" -"pcuic/PCUICPosition" -> "pcuic/PCUICReduction" -"pcuic/PCUICRelations" -> "pcuic/PCUICReduction" -"pcuic/PCUICUnivSubst" -> "pcuic/PCUICReduction" -"pcuic/PCUICInduction" -> "pcuic/PCUICReflect" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICSN" -"pcuic/PCUICAlpha" -> "pcuic/PCUICSR" -"pcuic/PCUICInductiveInversion" -> "pcuic/PCUICSR" -"pcuic/PCUICNormal" -> "pcuic/PCUICSafeLemmata" -"pcuic/PCUICPrincipality" -> "pcuic/PCUICSafeLemmata" -"pcuic/PCUICWeakening" -> "pcuic/PCUICSigmaCalculus" -"pcuic/PCUICAst" -> "pcuic/PCUICSize" -"pcuic/PCUICArities" -> "pcuic/PCUICSpine" -"pcuic/PCUICSigmaCalculus" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICUnivSubstitution" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICCumulativity" -> "pcuic/PCUICTyping" -"pcuic/PCUICUtils" -> "pcuic/PCUICTyping" -"template-coq/utils/LibHypsNaming" -> "pcuic/PCUICTyping" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICUnivSubst" -"pcuic/PCUICWeakening" -> "pcuic/PCUICUnivSubstitution" -"pcuic/PCUICAstUtils" -> "pcuic/PCUICUtils" -"pcuic/PCUICInductives" -> "pcuic/PCUICValidity" -"pcuic/PCUICClosed" -> "pcuic/PCUICWeakening" -"pcuic/PCUICGeneration" -> "pcuic/PCUICWeakening" -"pcuic/PCUICTyping" -> "pcuic/PCUICWeakeningEnv" -"pcuic/PCUICAst" -> "pcuic/TemplateToPCUIC" -"safechecker/SafeTemplateChecker" -> "safechecker/Extraction" -"pcuic/PCUICPretty" -> "safechecker/PCUICSafeChecker" -"safechecker/PCUICSafeConversion" -> "safechecker/PCUICSafeChecker" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICSN" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICSafeChecker" -> "safechecker/PCUICSafeRetyping" -"pcuic/TemplateToPCUIC" -> "safechecker/SafeTemplateChecker" -"template-coq/Typing" -> "safechecker/SafeTemplateChecker" -"safechecker/PCUICSafeChecker" -> "safechecker/SafeTemplateChecker" -"pcuic/PCUICToTemplateCorrectness"[label="PCUICToTemplateCorrectness", color=lemonchiffon1] -"pcuic/PCUICToTemplate"[label="PCUICToTemplate", color=lemonchiffon1] -"pcuic/TemplateToPCUICCorrectness"[label="TemplateToPCUICCorrectness", color=lemonchiffon1] -"pcuic/TemplateToPCUIC"[label="TemplateToPCUIC", color=lemonchiffon1] -"pcuic/PCUICSafeLemmata"[label="PCUICSafeLemmata", color=lemonchiffon1] -"pcuic/PCUICSigmaCalculus"[label="PCUICSigmaCalculus", color=lemonchiffon1] -"pcuic/PCUICSN"[label="PCUICSN", color=lemonchiffon1] -"pcuic/PCUICElimination"[label="PCUICElimination", color=lemonchiffon1] -"pcuic/PCUICCumulProp"[label="PCUICCumulProp", color=lemonchiffon1] -"pcuic/PCUICRetyping"[label="PCUICRetyping", color=lemonchiffon1] -"pcuic/PCUICPretty"[label="PCUICPretty", color=lemonchiffon1] -"pcuic/PCUICChecker"[label="PCUICChecker", color=lemonchiffon1] -"pcuic/PCUICWcbvEval"[label="PCUICWcbvEval", color=lemonchiffon1] -"pcuic/PCUICCSubst"[label="PCUICCSubst", color=lemonchiffon1] -"pcuic/PCUICCanonicity"[label="PCUICCanonicity", color=lemonchiffon1] -"pcuic/PCUICSR"[label="PCUICSR", color=lemonchiffon1] -"pcuic/PCUICInductiveInversion"[label="PCUICInductiveInversion", color=lemonchiffon1] -"pcuic/PCUICValidity"[label="PCUICValidity", color=lemonchiffon1] -"pcuic/PCUICInductives"[label="PCUICInductives", color=lemonchiffon1] -"pcuic/PCUICSpine"[label="PCUICSpine", color=lemonchiffon1] -"pcuic/PCUICArities"[label="PCUICArities", color=lemonchiffon1] -"pcuic/PCUICContexts"[label="PCUICContexts", color=lemonchiffon1] -"pcuic/PCUICCtxShape"[label="PCUICCtxShape", color=lemonchiffon1] -"pcuic/PCUICPrincipality"[label="PCUICPrincipality", color=lemonchiffon1] -"pcuic/PCUICAlpha"[label="PCUICAlpha", color=lemonchiffon1] -"pcuic/PCUICGeneration"[label="PCUICGeneration", color=lemonchiffon1] -"pcuic/PCUICConversion"[label="PCUICConversion", color=lemonchiffon1] -"pcuic/PCUICContextConversion"[label="PCUICContextConversion", color=lemonchiffon1] -"pcuic/PCUICConfluence"[label="PCUICConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReductionConfluence"[label="PCUICParallelReductionConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReduction"[label="PCUICParallelReduction", color=lemonchiffon1] -"pcuic/PCUICReduction"[label="PCUICReduction", color=lemonchiffon1] -"pcuic/PCUICCumulativity"[label="PCUICCumulativity", color=lemonchiffon1] -"pcuic/PCUICSubstitution"[label="PCUICSubstitution", color=lemonchiffon1] -"pcuic/PCUICUnivSubstitution"[label="PCUICUnivSubstitution", color=lemonchiffon1] -"pcuic/PCUICWeakening"[label="PCUICWeakening", color=lemonchiffon1] -"pcuic/PCUICClosed"[label="PCUICClosed", color=lemonchiffon1] -"pcuic/PCUICWeakeningEnv"[label="PCUICWeakeningEnv", color=lemonchiffon1] -"pcuic/PCUICEquality"[label="PCUICEquality", color=lemonchiffon1] -"pcuic/PCUICNameless"[label="PCUICNameless", color=lemonchiffon1] -"pcuic/PCUICNormal"[label="PCUICNormal", color=lemonchiffon1] -"pcuic/PCUICPosition"[label="PCUICPosition", color=lemonchiffon1] -"pcuic/PCUICInversion"[label="PCUICInversion", color=lemonchiffon1] -"pcuic/PCUICTyping"[label="PCUICTyping", color=lemonchiffon1] -"pcuic/PCUICUnivSubst"[label="PCUICUnivSubst", color=lemonchiffon1] -"pcuic/PCUICLiftSubst"[label="PCUICLiftSubst", color=lemonchiffon1] -"pcuic/PCUICReflect"[label="PCUICReflect", color=lemonchiffon1] -"pcuic/PCUICInduction"[label="PCUICInduction", color=lemonchiffon1] -"pcuic/PCUICAstUtils"[label="PCUICAstUtils", color=lemonchiffon1] -"pcuic/PCUICSize"[label="PCUICSize", color=lemonchiffon1] -"pcuic/PCUICAst"[label="PCUICAst", color=lemonchiffon1] -"pcuic/PCUICRelations"[label="PCUICRelations", color=lemonchiffon1] -"pcuic/PCUICUtils"[label="PCUICUtils", color=lemonchiffon1] -"pcuic/PCUICClosed" -> "pcuic/PCUICCSubst" -"pcuic/PCUICElimination" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICSN" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICWcbvEval" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICCumulProp" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICElimination" -"pcuic/PCUICChecker" -> "pcuic/PCUICRetyping" -"pcuic/PCUICConversion" -> "pcuic/PCUICRetyping" -"pcuic/PCUICAstUtils" -> "pcuic/PCUICToTemplate" -"template-coq/TypingWf" -> "pcuic/PCUICToTemplateCorrectness" -"template-coq/WfInv" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICGeneration" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICToTemplate" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICCSubst" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICSR" -> "pcuic/PCUICWcbvEval" -"template-coq/TypingWf" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/WfInv" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/PCUICSubstitution" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/TemplateToPCUIC" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/Extraction"[label="Extraction", color=aquamarine] -"template-coq/Constants"[label="Constants", color=aquamarine] -"template-coq/monad_utils"[label="monad_utils", color=aquamarine] -"template-coq/TemplateMonad/Extractable"[label="Extractable", color=aquamarine] -"template-coq/TemplateMonad/Core"[label="Core", color=aquamarine] -"template-coq/TemplateMonad/Common"[label="Common", color=aquamarine] -"template-coq/TemplateMonad"[label="TemplateMonad", color=aquamarine] -"template-coq/TypingWf"[label="TypingWf", color=aquamarine] -"template-coq/Typing"[label="Typing", color=aquamarine] -"template-coq/WfInv"[label="WfInv", color=aquamarine] -"template-coq/EnvironmentTyping"[label="EnvironmentTyping", color=aquamarine] -"template-coq/Pretty"[label="Pretty", color=aquamarine] -"template-coq/UnivSubst"[label="UnivSubst", color=aquamarine] -"template-coq/LiftSubst"[label="LiftSubst", color=aquamarine] -"template-coq/Induction"[label="Induction", color=aquamarine] -"template-coq/AstUtils"[label="AstUtils", color=aquamarine] -"template-coq/Ast"[label="Ast", color=aquamarine] -"template-coq/Environment"[label="Environment", color=aquamarine] -"template-coq/BasicAst"[label="BasicAst", color=aquamarine] -"template-coq/Universes"[label="Universes", color=aquamarine] -"template-coq/config"[label="config", color=aquamarine] -"template-coq/utils"[label="utils", color=aquamarine] -"template-coq/common/uGraph"[label="uGraph", color=aquamarine] -"template-coq/utils/MCUtils"[label="MCUtils", color=aquamarine] -"template-coq/utils/wGraph"[label="wGraph", color=aquamarine] -"template-coq/utils/MCString"[label="MCString", color=aquamarine] -"template-coq/utils/MCSquash"[label="MCSquash", color=aquamarine] -"template-coq/utils/MCRelations"[label="MCRelations", color=aquamarine] -"template-coq/utils/MCProd"[label="MCProd", color=aquamarine] -"template-coq/utils/MCOption"[label="MCOption", color=aquamarine] -"template-coq/utils/MCList"[label="MCList", color=aquamarine] -"template-coq/utils/LibHypsNaming"[label="LibHypsNaming", color=aquamarine] -"template-coq/utils/MCEquality"[label="MCEquality", color=aquamarine] -"template-coq/utils/MCCompare"[label="MCCompare", color=aquamarine] -"template-coq/utils/MCArith"[label="MCArith", color=aquamarine] -"template-coq/utils/All_Forall"[label="All_Forall", color=aquamarine] -"template-coq/utils/MCPrelude"[label="MCPrelude", color=aquamarine] -"template-coq/Pretty" -> "template-coq/Extraction" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Extraction" -"template-coq/UnivSubst" -> "template-coq/Extraction" -"template-coq/LiftSubst" -> "template-coq/Pretty" -"erasure/SafeTemplateErasure"[label="SafeTemplateErasure", color=tan] -"erasure/SafeErasureFunction"[label="SafeErasureFunction", color=tan] -"erasure/ErasureFunction"[label="ErasureFunction", color=tan] -"erasure/ErasureCorrectness"[label="ErasureCorrectness", color=tan] -"erasure/EArities"[label="EArities", color=tan] -"erasure/EInversion"[label="EInversion", color=tan] -"erasure/ESubstitution"[label="ESubstitution", color=tan] -"erasure/Prelim"[label="Prelim", color=tan] -"erasure/Extraction"[label="Extraction", color=tan] -"erasure/EAll"[label="EAll", color=tan] -"erasure/Extract"[label="Extract", color=tan] -"erasure/EGlobalEnv"[label="EGlobalEnv", color=tan] -"erasure/EWndEval"[label="EWndEval", color=tan] -"erasure/EWcbvEval"[label="EWcbvEval", color=tan] -"erasure/ECSubst"[label="ECSubst", color=tan] -"erasure/EPretty"[label="EPretty", color=tan] -"erasure/ELiftSubst"[label="ELiftSubst", color=tan] -"erasure/EInduction"[label="EInduction", color=tan] -"erasure/EAstUtils"[label="EAstUtils", color=tan] -"erasure/EAst"[label="EAst", color=tan] -"erasure/EWcbvEval" -> "erasure/EAll" -"erasure/EWndEval" -> "erasure/EAll" -"erasure/Extract" -> "erasure/EAll" -"pcuic/PCUICCanonicity" -> "erasure/EArities" -"erasure/Extract" -> "erasure/EArities" -"template-coq/Universes" -> "erasure/EAst" -"erasure/EAst" -> "erasure/EAstUtils" -"erasure/ELiftSubst" -> "erasure/ECSubst" -"erasure/EAst" -> "erasure/EInduction" -"pcuic/PCUICRetyping" -> "erasure/EInversion" -"erasure/Prelim" -> "erasure/EInversion" -"erasure/EInduction" -> "erasure/ELiftSubst" -"erasure/EGlobalEnv" -> "erasure/EPretty" -"erasure/Prelim" -> "erasure/ESubstitution" -"erasure/EAstUtils" -> "erasure/EGlobalEnv" -"erasure/ELiftSubst" -> "erasure/EGlobalEnv" -"erasure/ECSubst" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWndEval" -"erasure/EInversion" -> "erasure/ErasureCorrectness" -"erasure/ESubstitution" -> "erasure/ErasureCorrectness" -"erasure/ErasureCorrectness" -> "erasure/ErasureFunction" -"pcuic/PCUICElimination" -> "erasure/Extract" -"erasure/EAst" -> "erasure/Extract" -"erasure/SafeTemplateErasure" -> "erasure/Extraction" -"safechecker/PCUICSafeChecker" -> "erasure/Prelim" -"erasure/EArities" -> "erasure/Prelim" -"erasure/EWcbvEval" -> "erasure/Prelim" -"safechecker/PCUICSafeRetyping" -> "erasure/SafeErasureFunction" -"erasure/ErasureCorrectness" -> "erasure/SafeErasureFunction" -"safechecker/SafeTemplateChecker" -> "erasure/SafeTemplateErasure" -"template-coq/Pretty" -> "erasure/SafeTemplateErasure" -"erasure/EPretty" -> "erasure/SafeTemplateErasure" -"erasure/ErasureFunction" -> "erasure/SafeTemplateErasure" -"erasure/SafeErasureFunction" -> "erasure/SafeTemplateErasure" -} diff --git a/dependency-graph/depgraph-2020-09-24.svg b/dependency-graph/depgraph-2020-09-24.svg deleted file mode 100644 index 66a12248c..000000000 --- a/dependency-graph/depgraph-2020-09-24.svg +++ /dev/null @@ -1,1903 +0,0 @@ - - - - - - -dependencies - - - -checker/All - -All - - - -checker/Normal - -Normal - - - -checker/Retyping - -Retyping - - - -checker/Retyping->checker/All - - - - - -checker/WcbvEval - -WcbvEval - - - -checker/Checker - -Checker - - - -checker/Checker->checker/Retyping - - - - - -checker/Substitution - -Substitution - - - -checker/Substitution->checker/All - - - - - -checker/Weakening - -Weakening - - - -checker/Weakening->checker/Substitution - - - - - -checker/Closed - -Closed - - - -checker/Closed->checker/Weakening - - - - - -checker/WeakeningEnv - -WeakeningEnv - - - -checker/WeakeningEnv->checker/Closed - - - - - -checker/Generation - -Generation - - - -checker/Generation->checker/Substitution - - - - - -checker/Reflect - -Reflect - - - -checker/Reflect->checker/WcbvEval - - - - - -checker/Reflect->checker/Closed - - - - - -checker/Reflect->checker/Generation - - - - - -template-coq/Loader - -template-coq/Loader - - - -template-coq/All - -template-coq/All - - - -template-coq/Loader->template-coq/All - - - - - -template-coq/All->checker/All - - - - - -template-coq/Typing - -Typing - - - -template-coq/Typing->checker/Normal - - - - - -template-coq/Typing->checker/WcbvEval - - - - - -template-coq/Typing->checker/Checker - - - - - -template-coq/Typing->checker/WeakeningEnv - - - - - -template-coq/Typing->checker/Generation - - - - - -template-coq/Typing->template-coq/All - - - - - -template-coq/TypingWf - -TypingWf - - - -template-coq/Typing->template-coq/TypingWf - - - - - -safechecker/SafeTemplateChecker - -SafeTemplateChecker - - - -template-coq/Typing->safechecker/SafeTemplateChecker - - - - - -template-coq/Environment - -Environment - - - -template-coq/Ast - -Ast - - - -template-coq/Environment->template-coq/Ast - - - - - -template-coq/AstUtils - -AstUtils - - - -template-coq/Ast->template-coq/AstUtils - - - - - -template-coq/TemplateMonad/Common - -Common - - - -template-coq/Ast->template-coq/TemplateMonad/Common - - - - - -template-coq/TemplateMonad/Extractable - -Extractable - - - -template-coq/AstUtils->template-coq/TemplateMonad/Extractable - - - - - -template-coq/EnvironmentTyping - -EnvironmentTyping - - - -template-coq/AstUtils->template-coq/EnvironmentTyping - - - - - -template-coq/Induction - -Induction - - - -template-coq/AstUtils->template-coq/Induction - - - - - -template-coq/TemplateMonad/Core - -Core - - - -template-coq/AstUtils->template-coq/TemplateMonad/Core - - - - - -template-coq/WfInv - -WfInv - - - -template-coq/AstUtils->template-coq/WfInv - - - - - -template-coq/utils - -utils - - - -template-coq/BasicAst - -BasicAst - - - -template-coq/utils->template-coq/BasicAst - - - - - -template-coq/Universes - -Universes - - - -template-coq/BasicAst->template-coq/Universes - - - - - -template-coq/TemplateMonad - -TemplateMonad - - - -template-coq/Constants - -Constants - - - -template-coq/TemplateMonad->template-coq/Constants - - - - - -template-coq/Constants->template-coq/Loader - - - - - -template-coq/TemplateMonad/Extractable->template-coq/Constants - - - - - -template-coq/Extraction - -Extraction - - - -template-coq/TemplateMonad/Extractable->template-coq/Extraction - - - - - -template-coq/common/uGraph - -uGraph - - - -template-coq/common/uGraph->checker/Checker - - - - - -template-coq/common/uGraph->template-coq/Constants - - - - - -pcuic/PCUICAstUtils - -PCUICAstUtils - - - -template-coq/common/uGraph->pcuic/PCUICAstUtils - - - - - -template-coq/Universes->template-coq/Environment - - - - - -template-coq/Universes->template-coq/common/uGraph - - - - - -erasure/EAst - -EAst - - - -template-coq/Universes->erasure/EAst - - - - - -template-coq/EnvironmentTyping->template-coq/Typing - - - - - -pcuic/PCUICAst - -PCUICAst - - - -template-coq/EnvironmentTyping->pcuic/PCUICAst - - - - - -template-coq/Induction->checker/Reflect - - - - - -template-coq/LiftSubst - -LiftSubst - - - -template-coq/Induction->template-coq/LiftSubst - - - - - -template-coq/UnivSubst - -UnivSubst - - - -template-coq/LiftSubst->template-coq/UnivSubst - - - - - -template-coq/Pretty - -Pretty - - - -template-coq/LiftSubst->template-coq/Pretty - - - - - -template-coq/TemplateMonad/Core->template-coq/TemplateMonad - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Extractable - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Core - - - - - -template-coq/UnivSubst->template-coq/Typing - - - - - -pcuic/PCUICCtxShape - -PCUICCtxShape - - - -template-coq/UnivSubst->pcuic/PCUICCtxShape - - - - - -template-coq/UnivSubst->template-coq/Extraction - - - - - -template-coq/TypingWf->checker/Closed - - - - - -pcuic/PCUICToTemplateCorrectness - -PCUICToTemplateCorrectness - - - -template-coq/TypingWf->pcuic/PCUICToTemplateCorrectness - - - - - -pcuic/TemplateToPCUICCorrectness - -TemplateToPCUICCorrectness - - - -template-coq/TypingWf->pcuic/TemplateToPCUICCorrectness - - - - - -template-coq/config - -config - - - -template-coq/config->template-coq/Universes - - - - - -template-coq/WfInv->checker/WcbvEval - - - - - -template-coq/WfInv->pcuic/PCUICToTemplateCorrectness - - - - - -template-coq/WfInv->pcuic/TemplateToPCUICCorrectness - - - - - -template-coq/utils/wGraph - -wGraph - - - -template-coq/utils/wGraph->template-coq/common/uGraph - - - - - -template-coq/monad_utils - -monad_utils - - - -template-coq/monad_utils->template-coq/utils - - - - - -template-coq/utils/MCUtils - -MCUtils - - - -template-coq/utils/MCUtils->template-coq/utils - - - - - -template-coq/utils/MCUtils->template-coq/utils/wGraph - - - - - -template-coq/utils/MCOption - -MCOption - - - -template-coq/utils/All_Forall - -All_Forall - - - -template-coq/utils/MCOption->template-coq/utils/All_Forall - - - - - -template-coq/utils/All_Forall->template-coq/utils/MCUtils - - - - - -template-coq/utils/MCSquash - -MCSquash - - - -template-coq/utils/MCSquash->template-coq/utils/All_Forall - - - - - -template-coq/utils/MCPrelude - -MCPrelude - - - -template-coq/utils/MCList - -MCList - - - -template-coq/utils/MCPrelude->template-coq/utils/MCList - - - - - -template-coq/utils/MCList->template-coq/utils/MCOption - - - - - -template-coq/utils/MCRelations - -MCRelations - - - -template-coq/utils/MCRelations->template-coq/utils/MCList - - - - - -template-coq/utils/MCProd - -MCProd - - - -template-coq/utils/MCProd->template-coq/utils/MCOption - - - - - -template-coq/utils/MCCompare - -MCCompare - - - -template-coq/utils/MCString - -MCString - - - -template-coq/utils/MCCompare->template-coq/utils/MCString - - - - - -template-coq/utils/MCString->template-coq/utils/MCUtils - - - - - -template-coq/utils/MCArith - -MCArith - - - -template-coq/utils/MCArith->template-coq/utils/MCUtils - - - - - -template-coq/utils/MCEquality - -MCEquality - - - -template-coq/utils/MCEquality->template-coq/utils/MCUtils - - - - - -template-coq/utils/LibHypsNaming - -LibHypsNaming - - - -template-coq/utils/LibHypsNaming->checker/WeakeningEnv - - - - - -pcuic/PCUICTyping - -PCUICTyping - - - -template-coq/utils/LibHypsNaming->pcuic/PCUICTyping - - - - - -safechecker/Extraction - -Extraction - - - -safechecker/PCUICSafeRetyping - -PCUICSafeRetyping - - - -erasure/SafeErasureFunction - -SafeErasureFunction - - - -safechecker/PCUICSafeRetyping->erasure/SafeErasureFunction - - - - - -safechecker/SafeTemplateChecker->safechecker/Extraction - - - - - -erasure/SafeTemplateErasure - -SafeTemplateErasure - - - -safechecker/SafeTemplateChecker->erasure/SafeTemplateErasure - - - - - -safechecker/PCUICSafeChecker - -PCUICSafeChecker - - - -safechecker/PCUICSafeChecker->safechecker/PCUICSafeRetyping - - - - - -safechecker/PCUICSafeChecker->safechecker/SafeTemplateChecker - - - - - -erasure/Prelim - -Prelim - - - -safechecker/PCUICSafeChecker->erasure/Prelim - - - - - -safechecker/PCUICSafeConversion - -PCUICSafeConversion - - - -safechecker/PCUICSafeConversion->safechecker/PCUICSafeChecker - - - - - -safechecker/PCUICSafeReduce - -PCUICSafeReduce - - - -safechecker/PCUICSafeReduce->safechecker/PCUICSafeConversion - - - - - -pcuic/PCUICValidity - -PCUICValidity - - - -pcuic/PCUICAlpha - -PCUICAlpha - - - -pcuic/PCUICValidity->pcuic/PCUICAlpha - - - - - -pcuic/PCUICInductiveInversion - -PCUICInductiveInversion - - - -pcuic/PCUICValidity->pcuic/PCUICInductiveInversion - - - - - -pcuic/PCUICSR - -PCUICSR - - - -pcuic/PCUICAlpha->pcuic/PCUICSR - - - - - -pcuic/PCUICContexts - -PCUICContexts - - - -pcuic/PCUICArities - -PCUICArities - - - -pcuic/PCUICContexts->pcuic/PCUICArities - - - - - -pcuic/PCUICSpine - -PCUICSpine - - - -pcuic/PCUICArities->pcuic/PCUICSpine - - - - - -pcuic/PCUICSize - -PCUICSize - - - -pcuic/PCUICAst->pcuic/PCUICSize - - - - - -pcuic/PCUICInduction - -PCUICInduction - - - -pcuic/PCUICAst->pcuic/PCUICInduction - - - - - -pcuic/TemplateToPCUIC - -TemplateToPCUIC - - - -pcuic/PCUICAst->pcuic/TemplateToPCUIC - - - - - -pcuic/PCUICSize->pcuic/PCUICAstUtils - - - - - -pcuic/PCUICLiftSubst - -PCUICLiftSubst - - - -pcuic/PCUICAstUtils->pcuic/PCUICLiftSubst - - - - - -pcuic/PCUICUtils - -PCUICUtils - - - -pcuic/PCUICAstUtils->pcuic/PCUICUtils - - - - - -pcuic/PCUICToTemplate - -PCUICToTemplate - - - -pcuic/PCUICAstUtils->pcuic/PCUICToTemplate - - - - - -pcuic/PCUICChecker - -PCUICChecker - - - -pcuic/PCUICTyping->pcuic/PCUICChecker - - - - - -pcuic/PCUICWeakeningEnv - -PCUICWeakeningEnv - - - -pcuic/PCUICTyping->pcuic/PCUICWeakeningEnv - - - - - -pcuic/PCUICNameless - -PCUICNameless - - - -pcuic/PCUICTyping->pcuic/PCUICNameless - - - - - -pcuic/PCUICGeneration - -PCUICGeneration - - - -pcuic/PCUICTyping->pcuic/PCUICGeneration - - - - - -pcuic/PCUICPretty - -PCUICPretty - - - -pcuic/PCUICChecker->pcuic/PCUICPretty - - - - - -pcuic/PCUICRetyping - -PCUICRetyping - - - -pcuic/PCUICChecker->pcuic/PCUICRetyping - - - - - -pcuic/PCUICClosed - -PCUICClosed - - - -pcuic/PCUICWeakeningEnv->pcuic/PCUICClosed - - - - - -pcuic/PCUICWeakening - -PCUICWeakening - - - -pcuic/PCUICClosed->pcuic/PCUICWeakening - - - - - -pcuic/PCUICCSubst - -PCUICCSubst - - - -pcuic/PCUICClosed->pcuic/PCUICCSubst - - - - - -pcuic/PCUICParallelReductionConfluence - -PCUICParallelReductionConfluence - - - -pcuic/PCUICConfluence - -PCUICConfluence - - - -pcuic/PCUICParallelReductionConfluence->pcuic/PCUICConfluence - - - - - -pcuic/PCUICContextConversion - -PCUICContextConversion - - - -pcuic/PCUICConfluence->pcuic/PCUICContextConversion - - - - - -pcuic/PCUICConversion - -PCUICConversion - - - -pcuic/PCUICContextConversion->pcuic/PCUICConversion - - - - - -pcuic/PCUICCtxShape->pcuic/PCUICContexts - - - - - -pcuic/PCUICInversion - -PCUICInversion - - - -pcuic/PCUICConversion->pcuic/PCUICInversion - - - - - -pcuic/PCUICConversion->pcuic/PCUICRetyping - - - - - -pcuic/PCUICInversion->pcuic/PCUICCtxShape - - - - - -pcuic/PCUICNameless->pcuic/PCUICCtxShape - - - - - -pcuic/PCUICReduction - -PCUICReduction - - - -pcuic/PCUICCumulativity - -PCUICCumulativity - - - -pcuic/PCUICReduction->pcuic/PCUICCumulativity - - - - - -pcuic/PCUICNormal - -PCUICNormal - - - -pcuic/PCUICReduction->pcuic/PCUICNormal - - - - - -pcuic/PCUICCumulativity->pcuic/PCUICTyping - - - - - -pcuic/PCUICEquality - -PCUICEquality - - - -pcuic/PCUICLiftSubst->pcuic/PCUICEquality - - - - - -pcuic/PCUICUnivSubst - -PCUICUnivSubst - - - -pcuic/PCUICLiftSubst->pcuic/PCUICUnivSubst - - - - - -pcuic/PCUICPosition - -PCUICPosition - - - -pcuic/PCUICEquality->pcuic/PCUICPosition - - - - - -pcuic/PCUICReflect - -PCUICReflect - - - -pcuic/PCUICReflect->pcuic/PCUICEquality - - - - - -pcuic/PCUICGeneration->pcuic/PCUICWeakening - - - - - -pcuic/PCUICGeneration->pcuic/PCUICToTemplateCorrectness - - - - - -pcuic/PCUICInduction->pcuic/PCUICLiftSubst - - - - - -pcuic/PCUICInduction->pcuic/PCUICReflect - - - - - -pcuic/PCUICInductiveInversion->pcuic/PCUICSR - - - - - -pcuic/PCUICInductives - -PCUICInductives - - - -pcuic/PCUICSpine->pcuic/PCUICInductives - - - - - -pcuic/PCUICInductives->pcuic/PCUICValidity - - - - - -pcuic/PCUICSafeLemmata - -PCUICSafeLemmata - - - -pcuic/PCUICNormal->pcuic/PCUICSafeLemmata - - - - - -pcuic/PCUICSubstitution - -PCUICSubstitution - - - -pcuic/PCUICParallelReduction - -PCUICParallelReduction - - - -pcuic/PCUICSubstitution->pcuic/PCUICParallelReduction - - - - - -pcuic/PCUICSubstitution->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/PCUICParallelReduction->pcuic/PCUICParallelReductionConfluence - - - - - -pcuic/PCUICPosition->pcuic/PCUICReduction - - - - - -pcuic/PCUICPretty->safechecker/PCUICSafeChecker - - - - - -pcuic/PCUICPrincipality - -PCUICPrincipality - - - -pcuic/PCUICSR->pcuic/PCUICPrincipality - - - - - -pcuic/PCUICWcbvEval - -PCUICWcbvEval - - - -pcuic/PCUICSR->pcuic/PCUICWcbvEval - - - - - -pcuic/PCUICPrincipality->pcuic/PCUICSafeLemmata - - - - - -pcuic/PCUICRelations - -PCUICRelations - - - -pcuic/PCUICRelations->pcuic/PCUICReduction - - - - - -pcuic/PCUICUnivSubst->pcuic/PCUICReduction - - - - - -pcuic/PCUICSN - -PCUICSN - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICSN - - - - - -pcuic/PCUICCumulProp - -PCUICCumulProp - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICCumulProp - - - - - -pcuic/PCUICSN->safechecker/PCUICSafeReduce - - - - - -pcuic/PCUICCanonicity - -PCUICCanonicity - - - -pcuic/PCUICSN->pcuic/PCUICCanonicity - - - - - -pcuic/PCUICSigmaCalculus - -PCUICSigmaCalculus - - - -pcuic/PCUICWeakening->pcuic/PCUICSigmaCalculus - - - - - -pcuic/PCUICUnivSubstitution - -PCUICUnivSubstitution - - - -pcuic/PCUICWeakening->pcuic/PCUICUnivSubstitution - - - - - -pcuic/PCUICSigmaCalculus->pcuic/PCUICSubstitution - - - - - -pcuic/PCUICUnivSubstitution->pcuic/PCUICSubstitution - - - - - -pcuic/PCUICUtils->pcuic/PCUICTyping - - - - - -pcuic/TemplateToPCUIC->safechecker/SafeTemplateChecker - - - - - -pcuic/TemplateToPCUIC->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/PCUICToTemplate->pcuic/PCUICToTemplateCorrectness - - - - - -pcuic/PCUICElimination - -PCUICElimination - - - -pcuic/PCUICElimination->pcuic/PCUICCanonicity - - - - - -erasure/Extract - -Extract - - - -pcuic/PCUICElimination->erasure/Extract - - - - - -pcuic/PCUICCumulProp->pcuic/PCUICElimination - - - - - -erasure/EInversion - -EInversion - - - -pcuic/PCUICRetyping->erasure/EInversion - - - - - -pcuic/PCUICWcbvEval->pcuic/PCUICCanonicity - - - - - -pcuic/PCUICCSubst->pcuic/PCUICWcbvEval - - - - - -erasure/EArities - -EArities - - - -pcuic/PCUICCanonicity->erasure/EArities - - - - - -template-coq/Pretty->template-coq/Extraction - - - - - -template-coq/Pretty->erasure/SafeTemplateErasure - - - - - -erasure/Extraction - -Extraction - - - -erasure/SafeTemplateErasure->erasure/Extraction - - - - - -erasure/SafeErasureFunction->erasure/SafeTemplateErasure - - - - - -erasure/ErasureFunction - -ErasureFunction - - - -erasure/ErasureFunction->erasure/SafeTemplateErasure - - - - - -erasure/ErasureCorrectness - -ErasureCorrectness - - - -erasure/ErasureCorrectness->erasure/SafeErasureFunction - - - - - -erasure/ErasureCorrectness->erasure/ErasureFunction - - - - - -erasure/EArities->erasure/Prelim - - - - - -erasure/EInversion->erasure/ErasureCorrectness - - - - - -erasure/ESubstitution - -ESubstitution - - - -erasure/ESubstitution->erasure/ErasureCorrectness - - - - - -erasure/Prelim->erasure/EInversion - - - - - -erasure/Prelim->erasure/ESubstitution - - - - - -erasure/EAll - -EAll - - - -erasure/Extract->erasure/EArities - - - - - -erasure/Extract->erasure/EAll - - - - - -erasure/EGlobalEnv - -EGlobalEnv - - - -erasure/EWndEval - -EWndEval - - - -erasure/EGlobalEnv->erasure/EWndEval - - - - - -erasure/EWcbvEval - -EWcbvEval - - - -erasure/EGlobalEnv->erasure/EWcbvEval - - - - - -erasure/EPretty - -EPretty - - - -erasure/EGlobalEnv->erasure/EPretty - - - - - -erasure/EWndEval->erasure/EAll - - - - - -erasure/EWcbvEval->erasure/Prelim - - - - - -erasure/EWcbvEval->erasure/EAll - - - - - -erasure/ECSubst - -ECSubst - - - -erasure/ECSubst->erasure/EWcbvEval - - - - - -erasure/EPretty->erasure/SafeTemplateErasure - - - - - -erasure/ELiftSubst - -ELiftSubst - - - -erasure/ELiftSubst->erasure/EGlobalEnv - - - - - -erasure/ELiftSubst->erasure/ECSubst - - - - - -erasure/EInduction - -EInduction - - - -erasure/EInduction->erasure/ELiftSubst - - - - - -erasure/EAstUtils - -EAstUtils - - - -erasure/EAstUtils->erasure/EGlobalEnv - - - - - -erasure/EAst->erasure/Extract - - - - - -erasure/EAst->erasure/EInduction - - - - - -erasure/EAst->erasure/EAstUtils - - - - - diff --git a/dependency-graph/depgraph-2020-11-28.dot b/dependency-graph/depgraph-2020-11-28.dot deleted file mode 100644 index 80ee9705d..000000000 --- a/dependency-graph/depgraph-2020-11-28.dot +++ /dev/null @@ -1,346 +0,0 @@ -digraph dependencies { -node[style=filled] -"safechecker/Extraction"[label="Extraction", color=paleturquoise1] -"safechecker/PCUICSafeRetyping"[label="PCUICSafeRetyping", color=paleturquoise1] -"safechecker/SafeTemplateChecker"[label="SafeTemplateChecker", color=paleturquoise1] -"safechecker/PCUICSafeChecker"[label="PCUICSafeChecker", color=paleturquoise1] -"safechecker/PCUICTypeChecker"[label="PCUICTypeChecker", color=paleturquoise1] -"safechecker/PCUICWfEnv"[label="PCUICWfEnv", color=paleturquoise1] -"safechecker/PCUICWfReduction"[label="PCUICWfReduction", color=paleturquoise1] -"safechecker/PCUICSafeConversion"[label="PCUICSafeConversion", color=paleturquoise1] -"safechecker/PCUICEqualityDec"[label="PCUICEqualityDec", color=paleturquoise1] -"safechecker/PCUICSafeReduce"[label="PCUICSafeReduce", color=paleturquoise1] -"safechecker/PCUICErrors"[label="PCUICErrors", color=paleturquoise1] -"pcuic/PCUICValidity" -> "pcuic/PCUICAlpha" -"pcuic/PCUICWfUniverses" -> "pcuic/PCUICArities" -"template-coq/EnvironmentTyping" -> "pcuic/PCUICAst" -"pcuic/PCUICSize" -> "pcuic/PCUICAstUtils" -"template-coq/Reflect" -> "pcuic/PCUICAstUtils" -"template-coq/common/uGraph" -> "pcuic/PCUICAstUtils" -"pcuic/PCUICClosed" -> "pcuic/PCUICCSubst" -"pcuic/PCUICElimination" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICSN" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICWcbvEval" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICWeakeningEnv" -> "pcuic/PCUICClosed" -"pcuic/PCUICParallelReductionConfluence" -> "pcuic/PCUICConfluence" -"pcuic/PCUICConfluence" -> "pcuic/PCUICContextConversion" -"pcuic/PCUICContextRelation" -> "pcuic/PCUICContextConversion" -"pcuic/PCUICTyping" -> "pcuic/PCUICContextRelation" -"pcuic/PCUICCtxShape" -> "pcuic/PCUICContexts" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICConvCumInversion" -"pcuic/PCUICContextConversion" -> "pcuic/PCUICConversion" -"pcuic/PCUICInversion" -> "pcuic/PCUICCtxShape" -"pcuic/PCUICNameless" -> "pcuic/PCUICCtxShape" -"template-coq/UnivSubst" -> "pcuic/PCUICCtxShape" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICCumulProp" -"pcuic/PCUICReduction" -> "pcuic/PCUICCumulativity" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICElimination" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICEquality" -"pcuic/PCUICReflect" -> "pcuic/PCUICEquality" -"pcuic/PCUICTyping" -> "pcuic/PCUICGeneration" -"pcuic/PCUICTyping" -> "pcuic/PCUICGlobalEnv" -"pcuic/PCUICAstUtils" -> "pcuic/PCUICInduction" -"pcuic/PCUICValidity" -> "pcuic/PCUICInductiveInversion" -"pcuic/PCUICSpine" -> "pcuic/PCUICInductives" -"pcuic/PCUICConversion" -> "pcuic/PCUICInversion" -"pcuic/PCUICInduction" -> "pcuic/PCUICLiftSubst" -"pcuic/PCUICTyping" -> "pcuic/PCUICNameless" -"pcuic/PCUICContextRelation" -> "pcuic/PCUICNormal" -"template-coq/UnivSubst" -> "pcuic/PCUICNormal" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICParallelReduction" -"pcuic/PCUICParallelReduction" -> "pcuic/PCUICParallelReductionConfluence" -"pcuic/PCUICEquality" -> "pcuic/PCUICPosition" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICPretty" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICPrincipality" -"pcuic/PCUICPosition" -> "pcuic/PCUICReduction" -"pcuic/PCUICRelations" -> "pcuic/PCUICReduction" -"pcuic/PCUICUnivSubst" -> "pcuic/PCUICReduction" -"pcuic/PCUICInduction" -> "pcuic/PCUICReflect" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICSN" -"pcuic/PCUICAlpha" -> "pcuic/PCUICSR" -"pcuic/PCUICInductiveInversion" -> "pcuic/PCUICSR" -"pcuic/PCUICNormal" -> "pcuic/PCUICSafeLemmata" -"pcuic/PCUICSR" -> "pcuic/PCUICSafeLemmata" -"pcuic/PCUICWeakening" -> "pcuic/PCUICSigmaCalculus" -"pcuic/PCUICAst" -> "pcuic/PCUICSize" -"pcuic/PCUICArities" -> "pcuic/PCUICSpine" -"pcuic/PCUICSigmaCalculus" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICUnivSubstitution" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICCumulativity" -> "pcuic/PCUICTyping" -"pcuic/PCUICUtils" -> "pcuic/PCUICTyping" -"template-coq/utils/LibHypsNaming" -> "pcuic/PCUICTyping" -"pcuic/PCUICLiftSubst" -> "pcuic/PCUICUnivSubst" -"pcuic/PCUICWeakening" -> "pcuic/PCUICUnivSubstitution" -"pcuic/PCUICAstUtils" -> "pcuic/PCUICUtils" -"pcuic/PCUICInductives" -> "pcuic/PCUICValidity" -"pcuic/PCUICCSubst" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICSR" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICClosed" -> "pcuic/PCUICWeakening" -"pcuic/PCUICGeneration" -> "pcuic/PCUICWeakening" -"pcuic/PCUICTyping" -> "pcuic/PCUICWeakeningEnv" -"pcuic/PCUICContexts" -> "pcuic/PCUICWfUniverses" -"pcuic/PCUICAst" -> "pcuic/TemplateToPCUIC" -"template-coq/Environment" -> "template-coq/Ast" -"template-coq/Ast" -> "template-coq/AstUtils" -"template-coq/utils" -> "template-coq/BasicAst" -"template-coq/Universes" -> "template-coq/Environment" -"template-coq/AstUtils" -> "template-coq/EnvironmentTyping" -"template-coq/AstUtils" -> "template-coq/Induction" -"template-coq/Induction" -> "template-coq/LiftSubst" -"template-coq/Induction" -> "template-coq/Reflect" -"template-coq/EnvironmentTyping" -> "template-coq/Typing" -"template-coq/UnivSubst" -> "template-coq/Typing" -"template-coq/LiftSubst" -> "template-coq/UnivSubst" -"template-coq/BasicAst" -> "template-coq/Universes" -"template-coq/config" -> "template-coq/Universes" -"template-coq/Universes" -> "template-coq/common/uGraph" -"template-coq/utils/wGraph" -> "template-coq/common/uGraph" -"template-coq/utils/All_Forall" -> "template-coq/monad_utils" -"template-coq/monad_utils" -> "template-coq/utils" -"template-coq/utils/MCUtils" -> "template-coq/utils" -"template-coq/utils/MCOption" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCSquash" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCPrelude" -> "template-coq/utils/MCList" -"template-coq/utils/MCRelations" -> "template-coq/utils/MCList" -"template-coq/utils/MCList" -> "template-coq/utils/MCOption" -"template-coq/utils/MCProd" -> "template-coq/utils/MCOption" -"template-coq/utils/MCCompare" -> "template-coq/utils/MCString" -"template-coq/utils/All_Forall" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCArith" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCEquality" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCString" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCUtils" -> "template-coq/utils/wGraph" -"safechecker/SafeTemplateChecker" -> "safechecker/Extraction" -"pcuic/PCUICGlobalEnv" -> "safechecker/PCUICEqualityDec" -"pcuic/PCUICPretty" -> "safechecker/PCUICErrors" -"safechecker/PCUICTypeChecker" -> "safechecker/PCUICSafeChecker" -"pcuic/PCUICConvCumInversion" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICPrincipality" -> "safechecker/PCUICSafeConversion" -"safechecker/PCUICEqualityDec" -> "safechecker/PCUICSafeConversion" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICCanonicity" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICErrors" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeRetyping" -"safechecker/PCUICWfEnv" -> "safechecker/PCUICTypeChecker" -"safechecker/PCUICWfReduction" -> "safechecker/PCUICTypeChecker" -"pcuic/PCUICGlobalEnv" -> "safechecker/PCUICWfEnv" -"safechecker/PCUICSafeConversion" -> "safechecker/PCUICWfReduction" -"pcuic/TemplateToPCUIC" -> "safechecker/SafeTemplateChecker" -"template-coq/Typing" -> "safechecker/SafeTemplateChecker" -"safechecker/PCUICSafeChecker" -> "safechecker/SafeTemplateChecker" -"template-coq/Extraction"[label="Extraction", color=aquamarine] -"template-coq/Constants"[label="Constants", color=aquamarine] -"template-coq/monad_utils"[label="monad_utils", color=aquamarine] -"template-coq/TemplateMonad/Extractable"[label="Extractable", color=aquamarine] -"template-coq/TemplateMonad/Core"[label="Core", color=aquamarine] -"template-coq/TemplateMonad/Common"[label="Common", color=aquamarine] -"template-coq/TemplateMonad"[label="TemplateMonad", color=aquamarine] -"template-coq/TypingWf"[label="TypingWf", color=aquamarine] -"template-coq/Typing"[label="Typing", color=aquamarine] -"template-coq/WfInv"[label="WfInv", color=aquamarine] -"template-coq/EnvironmentTyping"[label="EnvironmentTyping", color=aquamarine] -"template-coq/Pretty"[label="Pretty", color=aquamarine] -"template-coq/UnivSubst"[label="UnivSubst", color=aquamarine] -"template-coq/LiftSubst"[label="LiftSubst", color=aquamarine] -"template-coq/Induction"[label="Induction", color=aquamarine] -"template-coq/Kernames"[label="Kernames", color=aquamarine] -"template-coq/Reflect"[label="Reflect", color=aquamarine] -"template-coq/AstUtils"[label="AstUtils", color=aquamarine] -"template-coq/Ast"[label="Ast", color=aquamarine] -"template-coq/Environment"[label="Environment", color=aquamarine] -"template-coq/BasicAst"[label="BasicAst", color=aquamarine] -"template-coq/Universes"[label="Universes", color=aquamarine] -"template-coq/config"[label="config", color=aquamarine] -"template-coq/utils"[label="utils", color=aquamarine] -"template-coq/common/uGraph"[label="uGraph", color=aquamarine] -"template-coq/utils/MCUtils"[label="MCUtils", color=aquamarine] -"template-coq/utils/wGraph"[label="wGraph", color=aquamarine] -"template-coq/utils/MCString"[label="MCString", color=aquamarine] -"template-coq/utils/MCSquash"[label="MCSquash", color=aquamarine] -"template-coq/utils/MCRelations"[label="MCRelations", color=aquamarine] -"template-coq/utils/MCProd"[label="MCProd", color=aquamarine] -"template-coq/utils/MCOption"[label="MCOption", color=aquamarine] -"template-coq/utils/MCList"[label="MCList", color=aquamarine] -"template-coq/utils/LibHypsNaming"[label="LibHypsNaming", color=aquamarine] -"template-coq/utils/MCEquality"[label="MCEquality", color=aquamarine] -"template-coq/utils/MCCompare"[label="MCCompare", color=aquamarine] -"template-coq/utils/MCArith"[label="MCArith", color=aquamarine] -"template-coq/utils/All_Forall"[label="All_Forall", color=aquamarine] -"template-coq/utils/MCPrelude"[label="MCPrelude", color=aquamarine] -"template-coq/TemplateMonad" -> "template-coq/Constants" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Constants" -"template-coq/common/uGraph" -> "template-coq/Constants" -"template-coq/Pretty" -> "template-coq/Extraction" -"template-coq/Reflect" -> "template-coq/Extraction" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Extraction" -"template-coq/UnivSubst" -> "template-coq/Extraction" -"template-coq/AstUtils" -> "template-coq/Kernames" -"template-coq/LiftSubst" -> "template-coq/Pretty" -"template-coq/TemplateMonad/Core" -> "template-coq/TemplateMonad" -"template-coq/Ast" -> "template-coq/TemplateMonad/Common" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Core" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Core" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Extractable" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Extractable" -"template-coq/Typing" -> "template-coq/TypingWf" -"template-coq/AstUtils" -> "template-coq/WfInv" -"checker/All"[label="All", color=seagreen3] -"checker/Normal"[label="Normal", color=seagreen3] -"checker/Retyping"[label="Retyping", color=seagreen3] -"checker/WcbvEval"[label="WcbvEval", color=seagreen3] -"checker/Checker"[label="Checker", color=seagreen3] -"checker/Substitution"[label="Substitution", color=seagreen3] -"checker/Weakening"[label="Weakening", color=seagreen3] -"checker/Closed"[label="Closed", color=seagreen3] -"checker/WeakeningEnv"[label="WeakeningEnv", color=seagreen3] -"checker/Generation"[label="Generation", color=seagreen3] -"template-coq/Loader" -> "template-coq/All" -"template-coq/Typing" -> "template-coq/All" -"template-coq/Constants" -> "template-coq/Loader" -"template-coq/All" -> "checker/All" -"checker/Retyping" -> "checker/All" -"checker/Substitution" -> "checker/All" -"template-coq/Typing" -> "checker/Checker" -"template-coq/common/uGraph" -> "checker/Checker" -"template-coq/Reflect" -> "checker/Closed" -"template-coq/TypingWf" -> "checker/Closed" -"checker/WeakeningEnv" -> "checker/Closed" -"template-coq/Reflect" -> "checker/Generation" -"template-coq/Typing" -> "checker/Generation" -"template-coq/Typing" -> "checker/Normal" -"checker/Checker" -> "checker/Retyping" -"checker/Generation" -> "checker/Substitution" -"checker/Weakening" -> "checker/Substitution" -"template-coq/Reflect" -> "checker/WcbvEval" -"template-coq/Typing" -> "checker/WcbvEval" -"template-coq/WfInv" -> "checker/WcbvEval" -"checker/Closed" -> "checker/Weakening" -"template-coq/Typing" -> "checker/WeakeningEnv" -"template-coq/utils/LibHypsNaming" -> "checker/WeakeningEnv" -"erasure/Erasure"[label="Erasure", color=tan] -"erasure/EOptimizePropDiscr"[label="EOptimizePropDiscr", color=tan] -"erasure/ErasureFunction"[label="ErasureFunction", color=tan] -"erasure/ErasureCorrectness"[label="ErasureCorrectness", color=tan] -"erasure/EArities"[label="EArities", color=tan] -"erasure/EInversion"[label="EInversion", color=tan] -"erasure/ESubstitution"[label="ESubstitution", color=tan] -"erasure/Prelim"[label="Prelim", color=tan] -"erasure/Extraction"[label="Extraction", color=tan] -"erasure/EAll"[label="EAll", color=tan] -"erasure/EDeps"[label="EDeps", color=tan] -"erasure/Extract"[label="Extract", color=tan] -"erasure/EGlobalEnv"[label="EGlobalEnv", color=tan] -"erasure/EWndEval"[label="EWndEval", color=tan] -"erasure/EWcbvEval"[label="EWcbvEval", color=tan] -"erasure/ECSubst"[label="ECSubst", color=tan] -"erasure/EPretty"[label="EPretty", color=tan] -"erasure/EReflect"[label="EReflect", color=tan] -"erasure/ELiftSubst"[label="ELiftSubst", color=tan] -"erasure/EInduction"[label="EInduction", color=tan] -"erasure/EAstUtils"[label="EAstUtils", color=tan] -"erasure/EAst"[label="EAst", color=tan] -"erasure/EWcbvEval" -> "erasure/EAll" -"erasure/EWndEval" -> "erasure/EAll" -"erasure/Extract" -> "erasure/EAll" -"pcuic/PCUICCanonicity" -> "erasure/EArities" -"pcuic/PCUICPrincipality" -> "erasure/EArities" -"erasure/Extract" -> "erasure/EArities" -"template-coq/Universes" -> "erasure/EAst" -"template-coq/Kernames" -> "erasure/EAstUtils" -"erasure/EAst" -> "erasure/EAstUtils" -"erasure/ELiftSubst" -> "erasure/ECSubst" -"erasure/ESubstitution" -> "erasure/EDeps" -"erasure/EAst" -> "erasure/EInduction" -"erasure/Prelim" -> "erasure/EInversion" -"erasure/EInduction" -> "erasure/ELiftSubst" -"erasure/ErasureFunction" -> "erasure/EOptimizePropDiscr" -"erasure/EGlobalEnv" -> "erasure/EPretty" -"pcuic/PCUICReflect" -> "erasure/EReflect" -"erasure/EInduction" -> "erasure/EReflect" -"erasure/Prelim" -> "erasure/ESubstitution" -"erasure/EAstUtils" -> "erasure/EGlobalEnv" -"erasure/ELiftSubst" -> "erasure/EGlobalEnv" -"erasure/EReflect" -> "erasure/EGlobalEnv" -"pcuic/PCUICWcbvEval" -> "erasure/EWcbvEval" -"erasure/ECSubst" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWndEval" -"pcuic/TemplateToPCUIC" -> "erasure/Erasure" -"template-coq/Pretty" -> "erasure/Erasure" -"erasure/EOptimizePropDiscr" -> "erasure/Erasure" -"erasure/EPretty" -> "erasure/Erasure" -"erasure/EDeps" -> "erasure/ErasureCorrectness" -"erasure/EInversion" -> "erasure/ErasureCorrectness" -"safechecker/PCUICSafeRetyping" -> "erasure/ErasureFunction" -"erasure/ErasureCorrectness" -> "erasure/ErasureFunction" -"pcuic/PCUICElimination" -> "erasure/Extract" -"erasure/EGlobalEnv" -> "erasure/Extract" -"erasure/Erasure" -> "erasure/Extraction" -"safechecker/PCUICErrors" -> "erasure/Prelim" -"erasure/EArities" -> "erasure/Prelim" -"erasure/EWcbvEval" -> "erasure/Prelim" -"pcuic/PCUICToTemplateCorrectness"[label="PCUICToTemplateCorrectness", color=lemonchiffon1] -"pcuic/PCUICToTemplate"[label="PCUICToTemplate", color=lemonchiffon1] -"pcuic/TemplateToPCUICCorrectness"[label="TemplateToPCUICCorrectness", color=lemonchiffon1] -"pcuic/TemplateToPCUIC"[label="TemplateToPCUIC", color=lemonchiffon1] -"pcuic/PCUICSafeLemmata"[label="PCUICSafeLemmata", color=lemonchiffon1] -"pcuic/PCUICSigmaCalculus"[label="PCUICSigmaCalculus", color=lemonchiffon1] -"pcuic/PCUICPrincipality"[label="PCUICPrincipality", color=lemonchiffon1] -"pcuic/PCUICSN"[label="PCUICSN", color=lemonchiffon1] -"pcuic/PCUICElimination"[label="PCUICElimination", color=lemonchiffon1] -"pcuic/PCUICCumulProp"[label="PCUICCumulProp", color=lemonchiffon1] -"pcuic/PCUICPretty"[label="PCUICPretty", color=lemonchiffon1] -"pcuic/PCUICWcbvEval"[label="PCUICWcbvEval", color=lemonchiffon1] -"pcuic/PCUICCSubst"[label="PCUICCSubst", color=lemonchiffon1] -"pcuic/PCUICCanonicity"[label="PCUICCanonicity", color=lemonchiffon1] -"pcuic/PCUICSR"[label="PCUICSR", color=lemonchiffon1] -"pcuic/PCUICInductiveInversion"[label="PCUICInductiveInversion", color=lemonchiffon1] -"pcuic/PCUICValidity"[label="PCUICValidity", color=lemonchiffon1] -"pcuic/PCUICInductives"[label="PCUICInductives", color=lemonchiffon1] -"pcuic/PCUICSpine"[label="PCUICSpine", color=lemonchiffon1] -"pcuic/PCUICWfUniverses"[label="PCUICWfUniverses", color=lemonchiffon1] -"pcuic/PCUICArities"[label="PCUICArities", color=lemonchiffon1] -"pcuic/PCUICContexts"[label="PCUICContexts", color=lemonchiffon1] -"pcuic/PCUICCtxShape"[label="PCUICCtxShape", color=lemonchiffon1] -"pcuic/PCUICAlpha"[label="PCUICAlpha", color=lemonchiffon1] -"pcuic/PCUICGeneration"[label="PCUICGeneration", color=lemonchiffon1] -"pcuic/PCUICConvCumInversion"[label="PCUICConvCumInversion", color=lemonchiffon1] -"pcuic/PCUICConversion"[label="PCUICConversion", color=lemonchiffon1] -"pcuic/PCUICContextConversion"[label="PCUICContextConversion", color=lemonchiffon1] -"pcuic/PCUICContextRelation"[label="PCUICContextRelation", color=lemonchiffon1] -"pcuic/PCUICConfluence"[label="PCUICConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReductionConfluence"[label="PCUICParallelReductionConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReduction"[label="PCUICParallelReduction", color=lemonchiffon1] -"pcuic/PCUICReduction"[label="PCUICReduction", color=lemonchiffon1] -"pcuic/PCUICCumulativity"[label="PCUICCumulativity", color=lemonchiffon1] -"pcuic/PCUICSubstitution"[label="PCUICSubstitution", color=lemonchiffon1] -"pcuic/PCUICUnivSubstitution"[label="PCUICUnivSubstitution", color=lemonchiffon1] -"pcuic/PCUICWeakening"[label="PCUICWeakening", color=lemonchiffon1] -"pcuic/PCUICClosed"[label="PCUICClosed", color=lemonchiffon1] -"pcuic/PCUICWeakeningEnv"[label="PCUICWeakeningEnv", color=lemonchiffon1] -"pcuic/PCUICEquality"[label="PCUICEquality", color=lemonchiffon1] -"pcuic/PCUICNameless"[label="PCUICNameless", color=lemonchiffon1] -"pcuic/PCUICNormal"[label="PCUICNormal", color=lemonchiffon1] -"pcuic/PCUICPosition"[label="PCUICPosition", color=lemonchiffon1] -"pcuic/PCUICInversion"[label="PCUICInversion", color=lemonchiffon1] -"pcuic/PCUICGlobalEnv"[label="PCUICGlobalEnv", color=lemonchiffon1] -"pcuic/PCUICTyping"[label="PCUICTyping", color=lemonchiffon1] -"pcuic/PCUICUnivSubst"[label="PCUICUnivSubst", color=lemonchiffon1] -"pcuic/PCUICLiftSubst"[label="PCUICLiftSubst", color=lemonchiffon1] -"pcuic/PCUICReflect"[label="PCUICReflect", color=lemonchiffon1] -"pcuic/PCUICInduction"[label="PCUICInduction", color=lemonchiffon1] -"pcuic/PCUICAstUtils"[label="PCUICAstUtils", color=lemonchiffon1] -"pcuic/PCUICSize"[label="PCUICSize", color=lemonchiffon1] -"pcuic/PCUICAst"[label="PCUICAst", color=lemonchiffon1] -"pcuic/PCUICRelations"[label="PCUICRelations", color=lemonchiffon1] -"pcuic/PCUICUtils"[label="PCUICUtils", color=lemonchiffon1] -"pcuic/PCUICAstUtils" -> "pcuic/PCUICToTemplate" -"template-coq/TypingWf" -> "pcuic/PCUICToTemplateCorrectness" -"template-coq/WfInv" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICGeneration" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICToTemplate" -> "pcuic/PCUICToTemplateCorrectness" -"template-coq/TypingWf" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/WfInv" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/PCUICSubstitution" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/TemplateToPCUIC" -> "pcuic/TemplateToPCUICCorrectness" -} diff --git a/dependency-graph/depgraph-2020-11-28.png b/dependency-graph/depgraph-2020-11-28.png deleted file mode 100644 index bee4f97f0..000000000 Binary files a/dependency-graph/depgraph-2020-11-28.png and /dev/null differ diff --git a/dependency-graph/depgraph-2020-11-28.svg b/dependency-graph/depgraph-2020-11-28.svg deleted file mode 100644 index 99d9832d7..000000000 --- a/dependency-graph/depgraph-2020-11-28.svg +++ /dev/null @@ -1,6059 +0,0 @@ - - - - - - image/svg+xml - - - - - - - - - - dependencies - - - safechecker/Extraction - - Extraction - - - - safechecker/PCUICSafeRetyping - - PCUICSafeRetyping - - - - erasure/ErasureFunction - - ErasureFunction - - - - safechecker/PCUICSafeRetyping->erasure/ErasureFunction - - - - - - safechecker/SafeTemplateChecker - - SafeTemplateChecker - - - - safechecker/SafeTemplateChecker->safechecker/Extraction - - - - - - safechecker/PCUICSafeChecker - - PCUICSafeChecker - - - - safechecker/PCUICSafeChecker->safechecker/SafeTemplateChecker - - - - - - safechecker/PCUICTypeChecker - - PCUICTypeChecker - - - - safechecker/PCUICTypeChecker->safechecker/PCUICSafeChecker - - - - - - safechecker/PCUICWfEnv - - PCUICWfEnv - - - - safechecker/PCUICWfEnv->safechecker/PCUICTypeChecker - - - - - - safechecker/PCUICWfReduction - - PCUICWfReduction - - - - safechecker/PCUICWfReduction->safechecker/PCUICTypeChecker - - - - - - safechecker/PCUICSafeConversion - - PCUICSafeConversion - - - - safechecker/PCUICSafeConversion->safechecker/PCUICWfReduction - - - - - - safechecker/PCUICEqualityDec - - PCUICEqualityDec - - - - safechecker/PCUICEqualityDec->safechecker/PCUICSafeConversion - - - - - - safechecker/PCUICSafeReduce - - PCUICSafeReduce - - - - safechecker/PCUICSafeReduce->safechecker/PCUICSafeRetyping - - - - - - safechecker/PCUICSafeReduce->safechecker/PCUICSafeConversion - - - - - - safechecker/PCUICErrors - - PCUICErrors - - - - safechecker/PCUICErrors->safechecker/PCUICSafeReduce - - - - - - erasure/Prelim - - Prelim - - - - safechecker/PCUICErrors->erasure/Prelim - - - - - - pcuic/PCUICValidity - - PCUICValidity - - - - pcuic/PCUICAlpha - - PCUICAlpha - - - - pcuic/PCUICValidity->pcuic/PCUICAlpha - - - - - - pcuic/PCUICInductiveInversion - - PCUICInductiveInversion - - - - pcuic/PCUICValidity->pcuic/PCUICInductiveInversion - - - - - - pcuic/PCUICSR - - PCUICSR - - - - pcuic/PCUICAlpha->pcuic/PCUICSR - - - - - - pcuic/PCUICWfUniverses - - PCUICWfUniverses - - - - pcuic/PCUICArities - - PCUICArities - - - - pcuic/PCUICWfUniverses->pcuic/PCUICArities - - - - - - pcuic/PCUICSpine - - PCUICSpine - - - - pcuic/PCUICArities->pcuic/PCUICSpine - - - - - - template-coq/EnvironmentTyping - - EnvironmentTyping - - - - pcuic/PCUICAst - - PCUICAst - - - - template-coq/EnvironmentTyping->pcuic/PCUICAst - - - - - - template-coq/Typing - - Typing - - - - template-coq/EnvironmentTyping->template-coq/Typing - - - - - - pcuic/PCUICSize - - PCUICSize - - - - - pcuic/TemplateToPCUIC - - TemplateToPCUIC - - - - - pcuic/PCUICAstUtils - - PCUICAstUtils - - - - pcuic/PCUICSize->pcuic/PCUICAstUtils - - - - - pcuic/PCUICInduction - - PCUICInduction - - - - pcuic/PCUICAstUtils->pcuic/PCUICInduction - - - - - - pcuic/PCUICUtils - - PCUICUtils - - - - pcuic/PCUICAstUtils->pcuic/PCUICUtils - - - - - - pcuic/PCUICToTemplate - - PCUICToTemplate - - - - pcuic/PCUICAstUtils->pcuic/PCUICToTemplate - - - - - - template-coq/Reflect - - Reflect - - - - template-coq/Reflect->pcuic/PCUICAstUtils - - - - - template-coq/Extraction - - Extraction - - - - template-coq/Reflect->template-coq/Extraction - - - - - - - - - - - - template-coq/common/uGraph - - uGraph - - - - - template-coq/Constants - - Constants - - - - template-coq/common/uGraph->template-coq/Constants - - - - - - - - pcuic/PCUICClosed - - PCUICClosed - - - - pcuic/PCUICCSubst - - PCUICCSubst - - - - pcuic/PCUICClosed->pcuic/PCUICCSubst - - - - - - pcuic/PCUICWeakening - - PCUICWeakening - - - - pcuic/PCUICClosed->pcuic/PCUICWeakening - - - - - - pcuic/PCUICWcbvEval - - PCUICWcbvEval - - - - pcuic/PCUICCSubst->pcuic/PCUICWcbvEval - - - - - - pcuic/PCUICElimination - - PCUICElimination - - - - pcuic/PCUICCanonicity - - PCUICCanonicity - - - - pcuic/PCUICElimination->pcuic/PCUICCanonicity - - - - - - erasure/Extract - - Extract - - - - pcuic/PCUICElimination->erasure/Extract - - - - - - pcuic/PCUICCanonicity->safechecker/PCUICSafeReduce - - - - - - erasure/EArities - - EArities - - - - pcuic/PCUICCanonicity->erasure/EArities - - - - - - pcuic/PCUICSN - - PCUICSN - - - - pcuic/PCUICSN->pcuic/PCUICCanonicity - - - - - - pcuic/PCUICWcbvEval->pcuic/PCUICCanonicity - - - - - - erasure/EWcbvEval - - EWcbvEval - - - - pcuic/PCUICWcbvEval->erasure/EWcbvEval - - - - - - pcuic/PCUICWeakeningEnv - - PCUICWeakeningEnv - - - - pcuic/PCUICWeakeningEnv->pcuic/PCUICClosed - - - - - - pcuic/PCUICParallelReductionConfluence - - PCUICParallelReductionConfluence - - - - pcuic/PCUICConfluence - - PCUICConfluence - - - - pcuic/PCUICParallelReductionConfluence->pcuic/PCUICConfluence - - - - - - pcuic/PCUICContextConversion - - PCUICContextConversion - - - - pcuic/PCUICConfluence->pcuic/PCUICContextConversion - - - - - - pcuic/PCUICConversion - - PCUICConversion - - - - pcuic/PCUICContextConversion->pcuic/PCUICConversion - - - - - - pcuic/PCUICContextRelation - - PCUICContextRelation - - - - pcuic/PCUICContextRelation->pcuic/PCUICContextConversion - - - - - - pcuic/PCUICNormal - - PCUICNormal - - - - pcuic/PCUICContextRelation->pcuic/PCUICNormal - - - - - - pcuic/PCUICTyping - - PCUICTyping - - - - pcuic/PCUICTyping->pcuic/PCUICWeakeningEnv - - - - - - pcuic/PCUICTyping->pcuic/PCUICContextRelation - - - - - - pcuic/PCUICNameless - - PCUICNameless - - - - pcuic/PCUICTyping->pcuic/PCUICNameless - - - - - - pcuic/PCUICGeneration - - PCUICGeneration - - - - pcuic/PCUICTyping->pcuic/PCUICGeneration - - - - - - pcuic/PCUICGlobalEnv - - PCUICGlobalEnv - - - - pcuic/PCUICTyping->pcuic/PCUICGlobalEnv - - - - - - pcuic/PCUICCtxShape - - PCUICCtxShape - - - - pcuic/PCUICContexts - - PCUICContexts - - - - pcuic/PCUICCtxShape->pcuic/PCUICContexts - - - - - - pcuic/PCUICContexts->pcuic/PCUICWfUniverses - - - - - - pcuic/PCUICCumulProp - - PCUICCumulProp - - - - pcuic/PCUICCumulProp->pcuic/PCUICElimination - - - - - - pcuic/PCUICConvCumInversion - - PCUICConvCumInversion - - - - pcuic/PCUICCumulProp->pcuic/PCUICConvCumInversion - - - - - - pcuic/PCUICPrincipality - - PCUICPrincipality - - - - pcuic/PCUICCumulProp->pcuic/PCUICPrincipality - - - - - - pcuic/PCUICConvCumInversion->safechecker/PCUICSafeConversion - - - - - - pcuic/PCUICInversion - - PCUICInversion - - - - pcuic/PCUICConversion->pcuic/PCUICInversion - - - - - - pcuic/PCUICInversion->pcuic/PCUICCtxShape - - - - - - pcuic/PCUICNameless->pcuic/PCUICCtxShape - - - - - - template-coq/UnivSubst - - UnivSubst - - - - template-coq/UnivSubst->pcuic/PCUICCtxShape - - - - - - template-coq/UnivSubst->pcuic/PCUICNormal - - - - - - template-coq/UnivSubst->template-coq/Typing - - - - - - template-coq/UnivSubst->template-coq/Extraction - - - - - - pcuic/PCUICSafeLemmata - - PCUICSafeLemmata - - - - pcuic/PCUICSafeLemmata->pcuic/PCUICSN - - - - - - pcuic/PCUICSafeLemmata->pcuic/PCUICCumulProp - - - - - - pcuic/PCUICReduction - - PCUICReduction - - - - pcuic/PCUICCumulativity - - PCUICCumulativity - - - - pcuic/PCUICReduction->pcuic/PCUICCumulativity - - - - - - pcuic/PCUICCumulativity->pcuic/PCUICTyping - - - - - - pcuic/PCUICLiftSubst - - PCUICLiftSubst - - - - pcuic/PCUICEquality - - PCUICEquality - - - - pcuic/PCUICLiftSubst->pcuic/PCUICEquality - - - - - - pcuic/PCUICPretty - - PCUICPretty - - - - pcuic/PCUICLiftSubst->pcuic/PCUICPretty - - - - - - pcuic/PCUICUnivSubst - - PCUICUnivSubst - - - - pcuic/PCUICLiftSubst->pcuic/PCUICUnivSubst - - - - - - pcuic/PCUICPosition - - PCUICPosition - - - - pcuic/PCUICEquality->pcuic/PCUICPosition - - - - - - pcuic/PCUICReflect - - PCUICReflect - - - - pcuic/PCUICReflect->pcuic/PCUICEquality - - - - - - erasure/EReflect - - EReflect - - - - pcuic/PCUICReflect->erasure/EReflect - - - - - - pcuic/PCUICGeneration->pcuic/PCUICWeakening - - - - - - pcuic/PCUICToTemplateCorrectness - - PCUICToTemplateCorrectness - - - - pcuic/PCUICGeneration->pcuic/PCUICToTemplateCorrectness - - - - - - pcuic/PCUICGlobalEnv->safechecker/PCUICWfEnv - - - - - - pcuic/PCUICGlobalEnv->safechecker/PCUICEqualityDec - - - - - - pcuic/PCUICInduction->pcuic/PCUICLiftSubst - - - - - - pcuic/PCUICInduction->pcuic/PCUICReflect - - - - - - pcuic/PCUICInductiveInversion->pcuic/PCUICSR - - - - - - pcuic/PCUICInductives - - PCUICInductives - - - - pcuic/PCUICSpine->pcuic/PCUICInductives - - - - - - pcuic/PCUICInductives->pcuic/PCUICValidity - - - - - - pcuic/PCUICNormal->pcuic/PCUICSafeLemmata - - - - - - pcuic/PCUICSubstitution - - PCUICSubstitution - - - - pcuic/PCUICParallelReduction - - PCUICParallelReduction - - - - pcuic/PCUICSubstitution->pcuic/PCUICParallelReduction - - - - - - pcuic/TemplateToPCUICCorrectness - - TemplateToPCUICCorrectness - - - - pcuic/PCUICSubstitution->pcuic/TemplateToPCUICCorrectness - - - - - - pcuic/PCUICParallelReduction->pcuic/PCUICParallelReductionConfluence - - - - - - pcuic/PCUICPosition->pcuic/PCUICReduction - - - - - - pcuic/PCUICPretty->safechecker/PCUICErrors - - - - - - pcuic/PCUICPrincipality->safechecker/PCUICSafeConversion - - - - - - pcuic/PCUICPrincipality->erasure/EArities - - - - - - pcuic/PCUICRelations - - PCUICRelations - - - - pcuic/PCUICRelations->pcuic/PCUICReduction - - - - - - pcuic/PCUICUnivSubst->pcuic/PCUICReduction - - - - - - pcuic/PCUICSR->pcuic/PCUICWcbvEval - - - - - - pcuic/PCUICSR->pcuic/PCUICSafeLemmata - - - - - - pcuic/PCUICSigmaCalculus - - PCUICSigmaCalculus - - - - pcuic/PCUICWeakening->pcuic/PCUICSigmaCalculus - - - - - - pcuic/PCUICUnivSubstitution - - PCUICUnivSubstitution - - - - pcuic/PCUICWeakening->pcuic/PCUICUnivSubstitution - - - - - - pcuic/PCUICSigmaCalculus->pcuic/PCUICSubstitution - - - - - - pcuic/PCUICUnivSubstitution->pcuic/PCUICSubstitution - - - - - - pcuic/PCUICUtils->pcuic/PCUICTyping - - - - - - template-coq/utils/LibHypsNaming - - LibHypsNaming - - - - template-coq/utils/LibHypsNaming->pcuic/PCUICTyping - - - - - - - - pcuic/TemplateToPCUIC->safechecker/SafeTemplateChecker - - - - - - erasure/Erasure - - Erasure - - - - pcuic/TemplateToPCUIC->erasure/Erasure - - - - - - pcuic/TemplateToPCUIC->pcuic/TemplateToPCUICCorrectness - - - - - - template-coq/Environment - - Environment - - - - template-coq/Ast - - Ast - - - - template-coq/Environment->template-coq/Ast - - - - - - template-coq/AstUtils - - AstUtils - - - - template-coq/Ast->template-coq/AstUtils - - - - - - template-coq/TemplateMonad/Common - - Common - - - - template-coq/Ast->template-coq/TemplateMonad/Common - - - - - - template-coq/AstUtils->template-coq/EnvironmentTyping - - - - - - template-coq/Induction - - Induction - - - - template-coq/AstUtils->template-coq/Induction - - - - - - template-coq/TemplateMonad/Extractable - - Extractable - - - - template-coq/AstUtils->template-coq/TemplateMonad/Extractable - - - - - - template-coq/TemplateMonad/Core - - Core - - - - template-coq/AstUtils->template-coq/TemplateMonad/Core - - - - - - template-coq/WfInv - - WfInv - - - - template-coq/AstUtils->template-coq/WfInv - - - - - - template-coq/Kernames - - Kernames - - - - template-coq/AstUtils->template-coq/Kernames - - - - - - template-coq/utils - - utils - - - - template-coq/BasicAst - - BasicAst - - - - template-coq/utils->template-coq/BasicAst - - - - - - template-coq/Universes - - Universes - - - - template-coq/BasicAst->template-coq/Universes - - - - - - template-coq/Universes->template-coq/common/uGraph - - - - - - template-coq/Universes->template-coq/Environment - - - - - - erasure/EAst - - EAst - - - - template-coq/Universes->erasure/EAst - - - - - - template-coq/Induction->template-coq/Reflect - - - - - - template-coq/LiftSubst - - LiftSubst - - - - template-coq/Induction->template-coq/LiftSubst - - - - - - template-coq/LiftSubst->template-coq/UnivSubst - - - - - - template-coq/Pretty - - Pretty - - - - template-coq/LiftSubst->template-coq/Pretty - - - - - - template-coq/Typing->safechecker/SafeTemplateChecker - - - - - - template-coq/TypingWf - - TypingWf - - - - template-coq/Typing->template-coq/TypingWf - - - - - - - - - - - - template-coq/All - - template-coq/All - - - - template-coq/Typing->template-coq/All - - - - - - template-coq/config - - config - - - - template-coq/config->template-coq/Universes - - - - - - template-coq/utils/wGraph - - wGraph - - - - template-coq/utils/wGraph->template-coq/common/uGraph - - - - - - template-coq/utils/All_Forall - - All_Forall - - - - template-coq/monad_utils - - monad_utils - - - - template-coq/utils/All_Forall->template-coq/monad_utils - - - - - - template-coq/utils/MCUtils - - MCUtils - - - - template-coq/utils/All_Forall->template-coq/utils/MCUtils - - - - - - template-coq/monad_utils->template-coq/utils - - - - - - template-coq/utils/MCUtils->template-coq/utils - - - - - - template-coq/utils/MCUtils->template-coq/utils/wGraph - - - - - - template-coq/utils/MCOption - - MCOption - - - - template-coq/utils/MCOption->template-coq/utils/All_Forall - - - - - - template-coq/utils/MCSquash - - MCSquash - - - - template-coq/utils/MCSquash->template-coq/utils/All_Forall - - - - - - template-coq/utils/MCPrelude - - MCPrelude - - - - template-coq/utils/MCList - - MCList - - - - template-coq/utils/MCPrelude->template-coq/utils/MCList - - - - - - template-coq/utils/MCList->template-coq/utils/MCOption - - - - - - template-coq/utils/MCRelations - - MCRelations - - - - template-coq/utils/MCRelations->template-coq/utils/MCList - - - - - - template-coq/utils/MCProd - - MCProd - - - - template-coq/utils/MCProd->template-coq/utils/MCOption - - - - - - template-coq/utils/MCCompare - - MCCompare - - - - template-coq/utils/MCString - - MCString - - - - template-coq/utils/MCCompare->template-coq/utils/MCString - - - - - - template-coq/utils/MCString->template-coq/utils/MCUtils - - - - - - template-coq/utils/MCArith - - MCArith - - - - template-coq/utils/MCArith->template-coq/utils/MCUtils - - - - - - template-coq/utils/MCEquality - - MCEquality - - - - template-coq/utils/MCEquality->template-coq/utils/MCUtils - - - - - - template-coq/Loader - - template-coq/Loader - - - - template-coq/Constants->template-coq/Loader - - - - - - template-coq/TemplateMonad/Extractable->template-coq/Extraction - - - - - - template-coq/TemplateMonad/Extractable->template-coq/Constants - - - - - - template-coq/TemplateMonad - - TemplateMonad - - - - template-coq/TemplateMonad/Core->template-coq/TemplateMonad - - - - - - template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Extractable - - - - - - template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Core - - - - - - template-coq/TemplateMonad->template-coq/Constants - - - - - - - template-coq/TypingWf->pcuic/PCUICToTemplateCorrectness - - - - - - template-coq/TypingWf->pcuic/TemplateToPCUICCorrectness - - - - - - - template-coq/WfInv->pcuic/PCUICToTemplateCorrectness - - - - - - template-coq/WfInv->pcuic/TemplateToPCUICCorrectness - - - - - - template-coq/Pretty->template-coq/Extraction - - - - - - template-coq/Pretty->erasure/Erasure - - - - - - erasure/EAstUtils - - EAstUtils - - - - template-coq/Kernames->erasure/EAstUtils - - - - - - - - - - - - - - - - - template-coq/Loader->template-coq/All - - - - - - - erasure/Extraction - - Extraction - - - - erasure/Erasure->erasure/Extraction - - - - - - erasure/EOptimizePropDiscr - - EOptimizePropDiscr - - - - erasure/EOptimizePropDiscr->erasure/Erasure - - - - - - erasure/ErasureFunction->erasure/EOptimizePropDiscr - - - - - - erasure/ErasureCorrectness - - ErasureCorrectness - - - - erasure/ErasureCorrectness->erasure/ErasureFunction - - - - - - erasure/EArities->erasure/Prelim - - - - - - erasure/EInversion - - EInversion - - - - erasure/EInversion->erasure/ErasureCorrectness - - - - - - erasure/ESubstitution - - ESubstitution - - - - erasure/EDeps - - EDeps - - - - erasure/ESubstitution->erasure/EDeps - - - - - - erasure/Prelim->erasure/EInversion - - - - - - erasure/Prelim->erasure/ESubstitution - - - - - - erasure/EAll - - EAll - - - - erasure/EDeps->erasure/ErasureCorrectness - - - - - - erasure/Extract->erasure/EArities - - - - - - erasure/Extract->erasure/EAll - - - - - - erasure/EGlobalEnv - - EGlobalEnv - - - - erasure/EGlobalEnv->erasure/Extract - - - - - - erasure/EWndEval - - EWndEval - - - - erasure/EGlobalEnv->erasure/EWndEval - - - - - - erasure/EGlobalEnv->erasure/EWcbvEval - - - - - - erasure/EPretty - - EPretty - - - - erasure/EGlobalEnv->erasure/EPretty - - - - - - erasure/EWndEval->erasure/EAll - - - - - - erasure/EWcbvEval->erasure/Prelim - - - - - - erasure/EWcbvEval->erasure/EAll - - - - - - erasure/ECSubst - - ECSubst - - - - erasure/ECSubst->erasure/EWcbvEval - - - - - - erasure/EPretty->erasure/Erasure - - - - - - erasure/EReflect->erasure/EGlobalEnv - - - - - - erasure/ELiftSubst - - ELiftSubst - - - - erasure/ELiftSubst->erasure/EGlobalEnv - - - - - - erasure/ELiftSubst->erasure/ECSubst - - - - - - erasure/EInduction - - EInduction - - - - erasure/EInduction->erasure/EReflect - - - - - - erasure/EInduction->erasure/ELiftSubst - - - - - - erasure/EAstUtils->erasure/EGlobalEnv - - - - - - erasure/EAst->erasure/EInduction - - - - - - erasure/EAst->erasure/EAstUtils - - - - - - pcuic/PCUICToTemplate->pcuic/PCUICToTemplateCorrectness - - - - - - diff --git a/dependency-graph/depgraph-2022-01-26.dot b/dependency-graph/depgraph-2022-01-26.dot deleted file mode 100644 index 03f209dc4..000000000 --- a/dependency-graph/depgraph-2022-01-26.dot +++ /dev/null @@ -1,435 +0,0 @@ -digraph dependencies { -node[style=filled] -"safechecker/Extraction"[label="Extraction", color=paleturquoise1] -"safechecker/PCUICConsistency"[label="PCUICConsistency", color=paleturquoise1] -"safechecker/PCUICSafeRetyping"[label="PCUICSafeRetyping", color=paleturquoise1] -"safechecker/SafeTemplateChecker"[label="SafeTemplateChecker", color=paleturquoise1] -"safechecker/PCUICSafeChecker"[label="PCUICSafeChecker", color=paleturquoise1] -"safechecker/PCUICTypeChecker"[label="PCUICTypeChecker", color=paleturquoise1] -"safechecker/PCUICWfEnv"[label="PCUICWfEnv", color=paleturquoise1] -"safechecker/PCUICWfReduction"[label="PCUICWfReduction", color=paleturquoise1] -"safechecker/PCUICSafeConversion"[label="PCUICSafeConversion", color=paleturquoise1] -"safechecker/PCUICSafeReduce"[label="PCUICSafeReduce", color=paleturquoise1] -"safechecker/PCUICErrors"[label="PCUICErrors", color=paleturquoise1] -"pcuic/PCUICTyping" -> "pcuic/Bidirectional/BDEnvironmentTyping" -"template-coq/AstUtils" -> "pcuic/Bidirectional/BDEnvironmentTyping" -"pcuic/Bidirectional/BDToPCUIC" -> "pcuic/Bidirectional/BDFromPCUIC" -"pcuic/Bidirectional/BDTyping" -> "pcuic/Bidirectional/BDToPCUIC" -"pcuic/PCUICSR" -> "pcuic/Bidirectional/BDToPCUIC" -"pcuic/Bidirectional/BDEnvironmentTyping" -> "pcuic/Bidirectional/BDTyping" -"pcuic/PCUICCumulativity" -> "pcuic/Bidirectional/BDTyping" -"pcuic/Bidirectional/BDFromPCUIC" -> "pcuic/Bidirectional/BDUnique" -"pcuic/Conversion/PCUICWeakeningEnvConv" -> "pcuic/Conversion/PCUICClosedConv" -"pcuic/Conversion/PCUICUnivSubstitutionConv" -> "pcuic/Conversion/PCUICInstConv" -"pcuic/Typing/PCUICWeakeningTyp" -> "pcuic/Conversion/PCUICInstConv" -"pcuic/Conversion/PCUICRenameConv" -> "pcuic/Conversion/PCUICOnFreeVarsConv" -"pcuic/Typing/PCUICClosedTyp" -> "pcuic/Conversion/PCUICRenameConv" -"pcuic/Conversion/PCUICWeakeningEnvConv" -> "pcuic/Conversion/PCUICUnivSubstitutionConv" -"pcuic/Conversion/PCUICRenameConv" -> "pcuic/Conversion/PCUICWeakeningConv" -"pcuic/PCUICContextSubst" -> "pcuic/Conversion/PCUICWeakeningEnvConv" -"pcuic/PCUICCumulativity" -> "pcuic/Conversion/PCUICWeakeningEnvConv" -"pcuic/PCUICGlobalEnv" -> "pcuic/Conversion/PCUICWeakeningEnvConv" -"pcuic/PCUICGuardCondition" -> "pcuic/Conversion/PCUICWeakeningEnvConv" -"pcuic/PCUICInductiveInversion" -> "pcuic/PCUICAlpha" -"pcuic/PCUICContexts" -> "pcuic/PCUICArities" -"pcuic/PCUICInversion" -> "pcuic/PCUICArities" -"pcuic/PCUICWfUniverses" -> "pcuic/PCUICArities" -"pcuic/utils/PCUICPrimitive" -> "pcuic/PCUICAst" -"pcuic/PCUICReduction" -> "pcuic/PCUICCSubst" -"pcuic/PCUICTyping" -> "pcuic/PCUICCSubst" -"pcuic/PCUICElimination" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICWcbvEval" -> "pcuic/PCUICCanonicity" -"pcuic/PCUICEquality" -> "pcuic/PCUICCasesContexts" -"pcuic/PCUICSigmaCalculus" -> "pcuic/PCUICCasesContexts" -"pcuic/PCUICParallelReductionConfluence" -> "pcuic/PCUICConfluence" -"pcuic/PCUICRedTypeIrrelevance" -> "pcuic/PCUICConfluence" -"pcuic/PCUICWellScopedCumulativity" -> "pcuic/PCUICContextConversion" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICContextReduction" -"pcuic/Syntax/PCUICLiftSubst" -> "pcuic/PCUICContextSubst" -"pcuic/PCUICGeneration" -> "pcuic/PCUICContexts" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICContexts" -"pcuic/Typing/PCUICUnivSubstitutionTyp" -> "pcuic/PCUICContexts" -"pcuic/PCUICContextConversion" -> "pcuic/PCUICConversion" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICCumulProp" -"pcuic/PCUICReduction" -> "pcuic/PCUICCumulativity" -"pcuic/Syntax/PCUICOnFreeVars" -> "pcuic/PCUICCumulativitySpec" -"pcuic/utils/PCUICOnOne" -> "pcuic/PCUICCumulativitySpec" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICElimination" -"pcuic/Syntax/PCUICLiftSubst" -> "pcuic/PCUICEquality" -"pcuic/Syntax/PCUICReflect" -> "pcuic/PCUICEquality" -"pcuic/PCUICWfUniverses" -> "pcuic/PCUICEqualityDec" -"pcuic/PCUICTyping" -> "pcuic/PCUICGeneration" -"pcuic/PCUICTyping" -> "pcuic/PCUICGlobalEnv" -"pcuic/PCUICReduction" -> "pcuic/PCUICGuardCondition" -"pcuic/Syntax/PCUICInstDef" -> "pcuic/PCUICGuardCondition" -"pcuic/Syntax/PCUICNamelessDef" -> "pcuic/PCUICGuardCondition" -"pcuic/PCUICValidity" -> "pcuic/PCUICInductiveInversion" -"pcuic/PCUICSpine" -> "pcuic/PCUICInductives" -"pcuic/PCUICConversion" -> "pcuic/PCUICInversion" -"pcuic/PCUICSR" -> "pcuic/PCUICNormal" -"template-coq/UnivSubst" -> "pcuic/PCUICNormal" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICParallelReduction" -"pcuic/Syntax/PCUICDepth" -> "pcuic/PCUICParallelReduction" -"pcuic/PCUICParallelReduction" -> "pcuic/PCUICParallelReductionConfluence" -"pcuic/PCUICCumulProp" -> "pcuic/PCUICPrincipality" -"pcuic/PCUICContextReduction" -> "pcuic/PCUICRedTypeIrrelevance" -"pcuic/Syntax/PCUICClosed" -> "pcuic/PCUICReduction" -"pcuic/Syntax/PCUICPosition" -> "pcuic/PCUICReduction" -"pcuic/Syntax/PCUICTactics" -> "pcuic/PCUICReduction" -"pcuic/utils/PCUICOnOne" -> "pcuic/PCUICReduction" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICSN" -"pcuic/PCUICAlpha" -> "pcuic/PCUICSR" -"pcuic/PCUICNormal" -> "pcuic/PCUICSafeLemmata" -"pcuic/Syntax/PCUICLiftSubst" -> "pcuic/PCUICSigmaCalculus" -"pcuic/PCUICArities" -> "pcuic/PCUICSpine" -"pcuic/PCUICCasesContexts" -> "pcuic/PCUICSpine" -"pcuic/Typing/PCUICContextConversionTyp" -> "pcuic/PCUICSpine" -"pcuic/Typing/PCUICInstTyp" -> "pcuic/PCUICSubstitution" -"pcuic/PCUICCumulativitySpec" -> "pcuic/PCUICTyping" -"pcuic/Syntax/PCUICPosition" -> "pcuic/PCUICTyping" -"pcuic/utils/PCUICUtils" -> "pcuic/PCUICTyping" -"pcuic/PCUICInductives" -> "pcuic/PCUICValidity" -"pcuic/PCUICCSubst" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICInversion" -> "pcuic/PCUICWcbvEval" -"pcuic/PCUICConfluence" -> "pcuic/PCUICWellScopedCumulativity" -"pcuic/PCUICGeneration" -> "pcuic/PCUICWfUniverses" -"pcuic/PCUICSubstitution" -> "pcuic/PCUICWfUniverses" -"pcuic/utils/PCUICAstUtils" -> "pcuic/Syntax/PCUICCases" -"pcuic/PCUICSigmaCalculus" -> "pcuic/Syntax/PCUICClosed" -"pcuic/Syntax/PCUICUnivSubst" -> "pcuic/Syntax/PCUICClosed" -"pcuic/Syntax/PCUICInduction" -> "pcuic/Syntax/PCUICDepth" -"pcuic/Syntax/PCUICCases" -> "pcuic/Syntax/PCUICInduction" -"template-coq/utils/LibHypsNaming" -> "pcuic/Syntax/PCUICInduction" -"pcuic/Syntax/PCUICRenameDef" -> "pcuic/Syntax/PCUICInstDef" -"pcuic/Syntax/PCUICInduction" -> "pcuic/Syntax/PCUICLiftSubst" -"pcuic/PCUICTyping" -> "pcuic/Syntax/PCUICNamelessDef" -"pcuic/PCUICEquality" -> "pcuic/Syntax/PCUICOnFreeVars" -"pcuic/Syntax/PCUICClosed" -> "pcuic/Syntax/PCUICOnFreeVars" -"template-coq/utils/MCPred" -> "pcuic/Syntax/PCUICOnFreeVars" -"pcuic/PCUICEquality" -> "pcuic/Syntax/PCUICPosition" -"pcuic/Syntax/PCUICInduction" -> "pcuic/Syntax/PCUICReflect" -"pcuic/PCUICTyping" -> "pcuic/Syntax/PCUICRenameDef" -"pcuic/PCUICSigmaCalculus" -> "pcuic/Syntax/PCUICTactics" -"pcuic/Syntax/PCUICInduction" -> "pcuic/Syntax/PCUICUnivSubst" -"pcuic/Syntax/PCUICCases" -> "pcuic/TemplateToPCUIC" -"template-coq/AstUtils" -> "pcuic/TemplateToPCUIC" -"pcuic/Conversion/PCUICClosedConv" -> "pcuic/Typing/PCUICClosedTyp" -"pcuic/Typing/PCUICWeakeningEnvTyp" -> "pcuic/Typing/PCUICClosedTyp" -"pcuic/PCUICConversion" -> "pcuic/Typing/PCUICContextConversionTyp" -"pcuic/Conversion/PCUICInstConv" -> "pcuic/Typing/PCUICInstTyp" -"pcuic/Conversion/PCUICOnFreeVarsConv" -> "pcuic/Typing/PCUICRenameTyp" -"pcuic/Conversion/PCUICUnivSubstitutionConv" -> "pcuic/Typing/PCUICUnivSubstitutionTyp" -"pcuic/Typing/PCUICWeakeningEnvTyp" -> "pcuic/Typing/PCUICUnivSubstitutionTyp" -"pcuic/Conversion/PCUICWeakeningEnvConv" -> "pcuic/Typing/PCUICWeakeningEnvTyp" -"pcuic/Conversion/PCUICWeakeningConv" -> "pcuic/Typing/PCUICWeakeningTyp" -"pcuic/Typing/PCUICRenameTyp" -> "pcuic/Typing/PCUICWeakeningTyp" -"pcuic/utils/PCUICSize" -> "pcuic/utils/PCUICAstUtils" -"template-coq/common/uGraph" -> "pcuic/utils/PCUICAstUtils" -"pcuic/PCUICAst" -> "pcuic/utils/PCUICOnOne" -"pcuic/utils/PCUICAstUtils" -> "pcuic/utils/PCUICPretty" -"template-coq/EnvironmentTyping" -> "pcuic/utils/PCUICPrimitive" -"template-coq/Reflect" -> "pcuic/utils/PCUICPrimitive" -"pcuic/PCUICAst" -> "pcuic/utils/PCUICSize" -"template-coq/config" -> "pcuic/utils/PCUICUtils" -"template-coq/utils" -> "pcuic/utils/PCUICUtils" -"template-coq/EnvironmentTyping" -> "template-coq/Ast" -"template-coq/Ast" -> "template-coq/AstUtils" -"template-coq/utils" -> "template-coq/BasicAst" -"template-coq/Universes" -> "template-coq/Environment" -"template-coq/Environment" -> "template-coq/EnvironmentTyping" -"template-coq/AstUtils" -> "template-coq/Induction" -"template-coq/WfAst" -> "template-coq/LiftSubst" -"template-coq/Universes" -> "template-coq/Reflect" -"template-coq/Induction" -> "template-coq/ReflectAst" -"template-coq/Reflect" -> "template-coq/ReflectAst" -"template-coq/Induction" -> "template-coq/TermEquality" -"template-coq/Reflect" -> "template-coq/TermEquality" -"template-coq/LiftSubst" -> "template-coq/Typing" -"template-coq/ReflectAst" -> "template-coq/Typing" -"template-coq/TermEquality" -> "template-coq/Typing" -"template-coq/Induction" -> "template-coq/UnivSubst" -"template-coq/BasicAst" -> "template-coq/Universes" -"template-coq/config" -> "template-coq/Universes" -"template-coq/UnivSubst" -> "template-coq/WfAst" -"template-coq/Universes" -> "template-coq/common/uGraph" -"template-coq/utils/wGraph" -> "template-coq/common/uGraph" -"template-coq/utils/All_Forall" -> "template-coq/monad_utils" -"template-coq/monad_utils" -> "template-coq/utils" -"template-coq/utils/MCUtils" -> "template-coq/utils" -"template-coq/utils/MCOption" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCSquash" -> "template-coq/utils/All_Forall" -"template-coq/utils/MCPrelude" -> "template-coq/utils/MCList" -"template-coq/utils/MCRelations" -> "template-coq/utils/MCList" -"template-coq/utils/MCList" -> "template-coq/utils/MCOption" -"template-coq/utils/MCProd" -> "template-coq/utils/MCOption" -"template-coq/utils/MCReflect" -> "template-coq/utils/MCOption" -"template-coq/utils/MCOption" -> "template-coq/utils/MCPred" -"template-coq/utils/MCPrelude" -> "template-coq/utils/MCReflect" -"template-coq/utils/MCCompare" -> "template-coq/utils/MCString" -"template-coq/utils/All_Forall" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCArith" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCEquality" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCString" -> "template-coq/utils/MCUtils" -"template-coq/utils/MCUtils" -> "template-coq/utils/wGraph" -"safechecker/SafeTemplateChecker" -> "safechecker/Extraction" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICConsistency" -"pcuic/utils/PCUICPretty" -> "safechecker/PCUICErrors" -"safechecker/PCUICTypeChecker" -> "safechecker/PCUICSafeChecker" -"pcuic/PCUICEqualityDec" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICPrincipality" -> "safechecker/PCUICSafeConversion" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeConversion" -"pcuic/PCUICCanonicity" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICErrors" -> "safechecker/PCUICSafeReduce" -"safechecker/PCUICWfReduction" -> "safechecker/PCUICSafeReduce" -"pcuic/Bidirectional/BDUnique" -> "safechecker/PCUICSafeRetyping" -"safechecker/PCUICSafeReduce" -> "safechecker/PCUICSafeRetyping" -"pcuic/Bidirectional/BDUnique" -> "safechecker/PCUICTypeChecker" -"safechecker/PCUICSafeConversion" -> "safechecker/PCUICTypeChecker" -"safechecker/PCUICWfEnv" -> "safechecker/PCUICTypeChecker" -"pcuic/PCUICGlobalEnv" -> "safechecker/PCUICWfEnv" -"pcuic/PCUICSN" -> "safechecker/PCUICWfReduction" -"pcuic/utils/PCUICPretty" -> "safechecker/PCUICWfReduction" -"pcuic/TemplateToPCUIC" -> "safechecker/SafeTemplateChecker" -"template-coq/Typing" -> "safechecker/SafeTemplateChecker" -"safechecker/PCUICSafeChecker" -> "safechecker/SafeTemplateChecker" -"template-coq/Extraction"[label="Extraction", color=aquamarine] -"template-coq/Constants"[label="Constants", color=aquamarine] -"template-coq/monad_utils"[label="monad_utils", color=aquamarine] -"template-coq/TemplateMonad/Extractable"[label="Extractable", color=aquamarine] -"template-coq/TemplateMonad/Core"[label="Core", color=aquamarine] -"template-coq/TemplateMonad/Common"[label="Common", color=aquamarine] -"template-coq/TemplateMonad"[label="TemplateMonad", color=aquamarine] -"template-coq/Checker"[label="Checker", color=aquamarine] -"template-coq/WcbvEval"[label="WcbvEval", color=aquamarine] -"template-coq/Normal"[label="Normal", color=aquamarine] -"template-coq/TypingWf"[label="TypingWf", color=aquamarine] -"template-coq/Reduction"[label="Reduction", color=aquamarine] -"template-coq/Typing"[label="Typing", color=aquamarine] -"template-coq/TermEquality"[label="TermEquality", color=aquamarine] -"template-coq/Pretty"[label="Pretty", color=aquamarine] -"template-coq/UnivSubst"[label="UnivSubst", color=aquamarine] -"template-coq/LiftSubst"[label="LiftSubst", color=aquamarine] -"template-coq/WfAst"[label="WfAst", color=aquamarine] -"template-coq/EnvironmentTyping"[label="EnvironmentTyping", color=aquamarine] -"template-coq/Induction"[label="Induction", color=aquamarine] -"template-coq/Kernames"[label="Kernames", color=aquamarine] -"template-coq/ReflectAst"[label="ReflectAst", color=aquamarine] -"template-coq/Reflect"[label="Reflect", color=aquamarine] -"template-coq/AstUtils"[label="AstUtils", color=aquamarine] -"template-coq/Ast"[label="Ast", color=aquamarine] -"template-coq/Environment"[label="Environment", color=aquamarine] -"template-coq/BasicAst"[label="BasicAst", color=aquamarine] -"template-coq/Universes"[label="Universes", color=aquamarine] -"template-coq/config"[label="config", color=aquamarine] -"template-coq/utils"[label="utils", color=aquamarine] -"template-coq/common/uGraph"[label="uGraph", color=aquamarine] -"template-coq/utils/MCUtils"[label="MCUtils", color=aquamarine] -"template-coq/utils/wGraph"[label="wGraph", color=aquamarine] -"template-coq/utils/MCString"[label="MCString", color=aquamarine] -"template-coq/utils/MCSquash"[label="MCSquash", color=aquamarine] -"template-coq/utils/MCRelations"[label="MCRelations", color=aquamarine] -"template-coq/utils/MCPred"[label="MCPred", color=aquamarine] -"template-coq/utils/MCProd"[label="MCProd", color=aquamarine] -"template-coq/utils/MCOption"[label="MCOption", color=aquamarine] -"template-coq/utils/MCList"[label="MCList", color=aquamarine] -"template-coq/utils/LibHypsNaming"[label="LibHypsNaming", color=aquamarine] -"template-coq/utils/MCEquality"[label="MCEquality", color=aquamarine] -"template-coq/utils/MCCompare"[label="MCCompare", color=aquamarine] -"template-coq/utils/MCArith"[label="MCArith", color=aquamarine] -"template-coq/utils/All_Forall"[label="All_Forall", color=aquamarine] -"template-coq/utils/MCReflect"[label="MCReflect", color=aquamarine] -"template-coq/utils/MCPrelude"[label="MCPrelude", color=aquamarine] -"template-coq/Typing" -> "template-coq/Checker" -"template-coq/common/uGraph" -> "template-coq/Checker" -"template-coq/TemplateMonad" -> "template-coq/Constants" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Constants" -"template-coq/common/uGraph" -> "template-coq/Constants" -"template-coq/Pretty" -> "template-coq/Extraction" -"template-coq/Reflect" -> "template-coq/Extraction" -"template-coq/TemplateMonad/Extractable" -> "template-coq/Extraction" -"template-coq/AstUtils" -> "template-coq/Kernames" -"template-coq/Typing" -> "template-coq/Normal" -"template-coq/LiftSubst" -> "template-coq/Pretty" -"template-coq/Typing" -> "template-coq/Reduction" -"template-coq/TemplateMonad/Core" -> "template-coq/TemplateMonad" -"template-coq/Ast" -> "template-coq/TemplateMonad/Common" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Core" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Core" -"template-coq/AstUtils" -> "template-coq/TemplateMonad/Extractable" -"template-coq/TemplateMonad/Common" -> "template-coq/TemplateMonad/Extractable" -"template-coq/Typing" -> "template-coq/TypingWf" -"template-coq/TypingWf" -> "template-coq/WcbvEval" -"erasure/Erasure"[label="Erasure", color=tan] -"erasure/EOptimizePropDiscr"[label="EOptimizePropDiscr", color=tan] -"erasure/ErasureFunction"[label="ErasureFunction", color=tan] -"erasure/ErasureCorrectness"[label="ErasureCorrectness", color=tan] -"erasure/EArities"[label="EArities", color=tan] -"erasure/EInversion"[label="EInversion", color=tan] -"erasure/ESubstitution"[label="ESubstitution", color=tan] -"erasure/Prelim"[label="Prelim", color=tan] -"erasure/Extraction"[label="Extraction", color=tan] -"erasure/EAll"[label="EAll", color=tan] -"erasure/EDeps"[label="EDeps", color=tan] -"erasure/Extract"[label="Extract", color=tan] -"erasure/EGlobalEnv"[label="EGlobalEnv", color=tan] -"erasure/EWndEval"[label="EWndEval", color=tan] -"erasure/EWcbvEval"[label="EWcbvEval", color=tan] -"erasure/ECSubst"[label="ECSubst", color=tan] -"erasure/EPretty"[label="EPretty", color=tan] -"erasure/EReflect"[label="EReflect", color=tan] -"erasure/ELiftSubst"[label="ELiftSubst", color=tan] -"erasure/EInduction"[label="EInduction", color=tan] -"erasure/EAstUtils"[label="EAstUtils", color=tan] -"erasure/EAst"[label="EAst", color=tan] -"pcuic/PCUICTyping" -> "pcuic/PCUICExpandLets" -"pcuic/PCUICCanonicity" -> "pcuic/PCUICExpandLetsCorrectness" -"pcuic/PCUICExpandLets" -> "pcuic/PCUICExpandLetsCorrectness" -"pcuic/PCUICInductiveInversion" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/TemplateToPCUIC" -> "pcuic/TemplateToPCUICCorrectness" -"template-coq/TypingWf" -> "pcuic/TemplateToPCUICCorrectness" -"pcuic/PCUICCanonicity" -> "pcuic/TemplateToPCUICWcbvEval" -"pcuic/TemplateToPCUICCorrectness" -> "pcuic/TemplateToPCUICWcbvEval" -"template-coq/WcbvEval" -> "pcuic/TemplateToPCUICWcbvEval" -"erasure/EWcbvEval" -> "erasure/EAll" -"erasure/EWndEval" -> "erasure/EAll" -"erasure/Extract" -> "erasure/EAll" -"pcuic/PCUICCanonicity" -> "erasure/EArities" -"pcuic/PCUICPrincipality" -> "erasure/EArities" -"erasure/Extract" -> "erasure/EArities" -"pcuic/utils/PCUICPrimitive" -> "erasure/EAst" -"template-coq/Kernames" -> "erasure/EAstUtils" -"erasure/EAst" -> "erasure/EAstUtils" -"erasure/ELiftSubst" -> "erasure/ECSubst" -"erasure/ESubstitution" -> "erasure/EDeps" -"erasure/EAst" -> "erasure/EInduction" -"erasure/Prelim" -> "erasure/EInversion" -"erasure/EInduction" -> "erasure/ELiftSubst" -"erasure/ErasureFunction" -> "erasure/EOptimizePropDiscr" -"erasure/EGlobalEnv" -> "erasure/EPretty" -"pcuic/Syntax/PCUICReflect" -> "erasure/EReflect" -"erasure/EInduction" -> "erasure/EReflect" -"erasure/Prelim" -> "erasure/ESubstitution" -"erasure/EAstUtils" -> "erasure/EGlobalEnv" -"erasure/ECSubst" -> "erasure/EGlobalEnv" -"erasure/EReflect" -> "erasure/EGlobalEnv" -"pcuic/PCUICWcbvEval" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWcbvEval" -"erasure/EGlobalEnv" -> "erasure/EWndEval" -"pcuic/PCUICExpandLetsCorrectness" -> "erasure/Erasure" -"pcuic/TemplateToPCUICWcbvEval" -> "erasure/Erasure" -"template-coq/Pretty" -> "erasure/Erasure" -"erasure/EOptimizePropDiscr" -> "erasure/Erasure" -"erasure/EPretty" -> "erasure/Erasure" -"erasure/EDeps" -> "erasure/ErasureCorrectness" -"erasure/EInversion" -> "erasure/ErasureCorrectness" -"safechecker/PCUICSafeRetyping" -> "erasure/ErasureFunction" -"erasure/ErasureCorrectness" -> "erasure/ErasureFunction" -"pcuic/PCUICElimination" -> "erasure/Extract" -"erasure/EGlobalEnv" -> "erasure/Extract" -"erasure/Erasure" -> "erasure/Extraction" -"safechecker/PCUICErrors" -> "erasure/Prelim" -"erasure/EArities" -> "erasure/Prelim" -"erasure/EWcbvEval" -> "erasure/Prelim" -"pcuic/Bidirectional/BDStrengthening"[label="BDStrengthening", color=lemonchiffon1] -"pcuic/Bidirectional/BDUnique"[label="BDUnique", color=lemonchiffon1] -"pcuic/Bidirectional/BDFromPCUIC"[label="BDFromPCUIC", color=lemonchiffon1] -"pcuic/Bidirectional/BDToPCUIC"[label="BDToPCUIC", color=lemonchiffon1] -"pcuic/Bidirectional/BDTyping"[label="BDTyping", color=lemonchiffon1] -"pcuic/Bidirectional/BDEnvironmentTyping"[label="BDEnvironmentTyping", color=lemonchiffon1] -"pcuic/PCUICExpandLetsCorrectness"[label="PCUICExpandLetsCorrectness", color=lemonchiffon1] -"pcuic/PCUICExpandLets"[label="PCUICExpandLets", color=lemonchiffon1] -"pcuic/PCUICToTemplateCorrectness"[label="PCUICToTemplateCorrectness", color=lemonchiffon1] -"pcuic/PCUICToTemplate"[label="PCUICToTemplate", color=lemonchiffon1] -"pcuic/TemplateToPCUICWcbvEval"[label="TemplateToPCUICWcbvEval", color=lemonchiffon1] -"pcuic/TemplateToPCUICCorrectness"[label="TemplateToPCUICCorrectness", color=lemonchiffon1] -"pcuic/TemplateToPCUIC"[label="TemplateToPCUIC", color=lemonchiffon1] -"pcuic/PCUICSafeLemmata"[label="PCUICSafeLemmata", color=lemonchiffon1] -"pcuic/PCUICSigmaCalculus"[label="PCUICSigmaCalculus", color=lemonchiffon1] -"pcuic/PCUICPrincipality"[label="PCUICPrincipality", color=lemonchiffon1] -"pcuic/PCUICSN"[label="PCUICSN", color=lemonchiffon1] -"pcuic/PCUICElimination"[label="PCUICElimination", color=lemonchiffon1] -"pcuic/PCUICCumulProp"[label="PCUICCumulProp", color=lemonchiffon1] -"pcuic/PCUICWcbvEval"[label="PCUICWcbvEval", color=lemonchiffon1] -"pcuic/PCUICCSubst"[label="PCUICCSubst", color=lemonchiffon1] -"pcuic/PCUICCanonicity"[label="PCUICCanonicity", color=lemonchiffon1] -"pcuic/PCUICSR"[label="PCUICSR", color=lemonchiffon1] -"pcuic/PCUICInductiveInversion"[label="PCUICInductiveInversion", color=lemonchiffon1] -"pcuic/PCUICValidity"[label="PCUICValidity", color=lemonchiffon1] -"pcuic/PCUICInductives"[label="PCUICInductives", color=lemonchiffon1] -"pcuic/PCUICSpine"[label="PCUICSpine", color=lemonchiffon1] -"pcuic/PCUICWfUniverses"[label="PCUICWfUniverses", color=lemonchiffon1] -"pcuic/PCUICArities"[label="PCUICArities", color=lemonchiffon1] -"pcuic/PCUICContexts"[label="PCUICContexts", color=lemonchiffon1] -"pcuic/PCUICAlpha"[label="PCUICAlpha", color=lemonchiffon1] -"pcuic/PCUICGeneration"[label="PCUICGeneration", color=lemonchiffon1] -"pcuic/PCUICRedTypeIrrelevance"[label="PCUICRedTypeIrrelevance", color=lemonchiffon1] -"pcuic/PCUICConvCumInversion"[label="PCUICConvCumInversion", color=lemonchiffon1] -"pcuic/PCUICConversion"[label="PCUICConversion", color=lemonchiffon1] -"pcuic/PCUICContextConversion"[label="PCUICContextConversion", color=lemonchiffon1] -"pcuic/PCUICWellScopedCumulativity"[label="PCUICWellScopedCumulativity", color=lemonchiffon1] -"pcuic/PCUICConfluence"[label="PCUICConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReductionConfluence"[label="PCUICParallelReductionConfluence", color=lemonchiffon1] -"pcuic/PCUICParallelReduction"[label="PCUICParallelReduction", color=lemonchiffon1] -"pcuic/PCUICCumulativitySpec"[label="PCUICCumulativitySpec", color=lemonchiffon1] -"pcuic/PCUICCumulativity"[label="PCUICCumulativity", color=lemonchiffon1] -"pcuic/PCUICContextReduction"[label="PCUICContextReduction", color=lemonchiffon1] -"pcuic/PCUICSubstitution"[label="PCUICSubstitution", color=lemonchiffon1] -"pcuic/PCUICEqualityDec"[label="PCUICEqualityDec", color=lemonchiffon1] -"pcuic/PCUICEquality"[label="PCUICEquality", color=lemonchiffon1] -"pcuic/PCUICNormal"[label="PCUICNormal", color=lemonchiffon1] -"pcuic/PCUICInversion"[label="PCUICInversion", color=lemonchiffon1] -"pcuic/PCUICGlobalEnv"[label="PCUICGlobalEnv", color=lemonchiffon1] -"pcuic/PCUICGuardCondition"[label="PCUICGuardCondition", color=lemonchiffon1] -"pcuic/PCUICTyping"[label="PCUICTyping", color=lemonchiffon1] -"pcuic/PCUICReduction"[label="PCUICReduction", color=lemonchiffon1] -"pcuic/PCUICCasesContexts"[label="PCUICCasesContexts", color=lemonchiffon1] -"pcuic/PCUICContextSubst"[label="PCUICContextSubst", color=lemonchiffon1] -"pcuic/Typing/PCUICContextConversionTyp"[label="PCUICContextConversionTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICClosedTyp"[label="PCUICClosedTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICUnivSubstitutionTyp"[label="PCUICUnivSubstitutionTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICWeakeningTyp"[label="PCUICWeakeningTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICWeakeningEnvTyp"[label="PCUICWeakeningEnvTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICInstTyp"[label="PCUICInstTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICRenameTyp"[label="PCUICRenameTyp", color=lemonchiffon1] -"pcuic/Typing/PCUICNamelessTyp"[label="PCUICNamelessTyp", color=lemonchiffon1] -"pcuic/Conversion/PCUICOnFreeVarsConv"[label="PCUICOnFreeVarsConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICClosedConv"[label="PCUICClosedConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICWeakeningConv"[label="PCUICWeakeningConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICUnivSubstitutionConv"[label="PCUICUnivSubstitutionConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICWeakeningEnvConv"[label="PCUICWeakeningEnvConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICInstConv"[label="PCUICInstConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICRenameConv"[label="PCUICRenameConv", color=lemonchiffon1] -"pcuic/Conversion/PCUICNamelessConv"[label="PCUICNamelessConv", color=lemonchiffon1] -"pcuic/Syntax/PCUICClosed"[label="PCUICClosed", color=lemonchiffon1] -"pcuic/Syntax/PCUICUnivSubst"[label="PCUICUnivSubst", color=lemonchiffon1] -"pcuic/Syntax/PCUICTactics"[label="PCUICTactics", color=lemonchiffon1] -"pcuic/Syntax/PCUICLiftSubst"[label="PCUICLiftSubst", color=lemonchiffon1] -"pcuic/Syntax/PCUICInstDef"[label="PCUICInstDef", color=lemonchiffon1] -"pcuic/Syntax/PCUICRenameDef"[label="PCUICRenameDef", color=lemonchiffon1] -"pcuic/Syntax/PCUICOnFreeVars"[label="PCUICOnFreeVars", color=lemonchiffon1] -"pcuic/Syntax/PCUICNamelessDef"[label="PCUICNamelessDef", color=lemonchiffon1] -"pcuic/Syntax/PCUICReflect"[label="PCUICReflect", color=lemonchiffon1] -"pcuic/Syntax/PCUICPosition"[label="PCUICPosition", color=lemonchiffon1] -"pcuic/Syntax/PCUICDepth"[label="PCUICDepth", color=lemonchiffon1] -"pcuic/Syntax/PCUICInduction"[label="PCUICInduction", color=lemonchiffon1] -"pcuic/Syntax/PCUICCases"[label="PCUICCases", color=lemonchiffon1] -"pcuic/utils/PCUICPretty"[label="PCUICPretty", color=lemonchiffon1] -"pcuic/utils/PCUICSize"[label="PCUICSize", color=lemonchiffon1] -"pcuic/utils/PCUICUtils"[label="PCUICUtils", color=lemonchiffon1] -"pcuic/utils/PCUICAstUtils"[label="PCUICAstUtils", color=lemonchiffon1] -"pcuic/utils/PCUICPrimitive"[label="PCUICPrimitive", color=lemonchiffon1] -"pcuic/utils/PCUICOnOne"[label="PCUICOnOne", color=lemonchiffon1] -"pcuic/PCUICAst"[label="PCUICAst", color=lemonchiffon1] -"pcuic/Bidirectional/BDFromPCUIC" -> "pcuic/Bidirectional/BDStrengthening" -"pcuic/Conversion/PCUICUnivSubstitutionConv" -> "pcuic/Conversion/PCUICNamelessConv" -"pcuic/Typing/PCUICClosedTyp" -> "pcuic/Conversion/PCUICNamelessConv" -"pcuic/PCUICNormal" -> "pcuic/PCUICConvCumInversion" -"template-coq/AstUtils" -> "pcuic/PCUICToTemplate" -"pcuic/Syntax/PCUICCases" -> "pcuic/PCUICToTemplate" -"template-coq/Reduction" -> "pcuic/PCUICToTemplateCorrectness" -"template-coq/TypingWf" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICSafeLemmata" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/PCUICToTemplate" -> "pcuic/PCUICToTemplateCorrectness" -"pcuic/Conversion/PCUICNamelessConv" -> "pcuic/Typing/PCUICNamelessTyp" -"pcuic/PCUICConversion" -> "pcuic/Typing/PCUICNamelessTyp" -} diff --git a/dependency-graph/depgraph-2022-01-26.png b/dependency-graph/depgraph-2022-01-26.png deleted file mode 100644 index f67628794..000000000 Binary files a/dependency-graph/depgraph-2022-01-26.png and /dev/null differ diff --git a/dependency-graph/depgraph-2022-01-26.svg b/dependency-graph/depgraph-2022-01-26.svg deleted file mode 100644 index be52c4546..000000000 --- a/dependency-graph/depgraph-2022-01-26.svg +++ /dev/null @@ -1,2605 +0,0 @@ - - - - - - -dependencies - - - -safechecker/Extraction - -Extraction - - - -safechecker/PCUICConsistency - -PCUICConsistency - - - -safechecker/PCUICSafeRetyping - -PCUICSafeRetyping - - - -erasure/ErasureFunction - -ErasureFunction - - - -safechecker/PCUICSafeRetyping->erasure/ErasureFunction - - - - - -safechecker/SafeTemplateChecker - -SafeTemplateChecker - - - -safechecker/SafeTemplateChecker->safechecker/Extraction - - - - - -safechecker/PCUICSafeChecker - -PCUICSafeChecker - - - -safechecker/PCUICSafeChecker->safechecker/SafeTemplateChecker - - - - - -safechecker/PCUICTypeChecker - -PCUICTypeChecker - - - -safechecker/PCUICTypeChecker->safechecker/PCUICSafeChecker - - - - - -safechecker/PCUICWfEnv - -PCUICWfEnv - - - -safechecker/PCUICWfEnv->safechecker/PCUICTypeChecker - - - - - -safechecker/PCUICWfReduction - -PCUICWfReduction - - - -safechecker/PCUICSafeReduce - -PCUICSafeReduce - - - -safechecker/PCUICWfReduction->safechecker/PCUICSafeReduce - - - - - -safechecker/PCUICSafeConversion - -PCUICSafeConversion - - - -safechecker/PCUICSafeConversion->safechecker/PCUICTypeChecker - - - - - -safechecker/PCUICSafeReduce->safechecker/PCUICConsistency - - - - - -safechecker/PCUICSafeReduce->safechecker/PCUICSafeRetyping - - - - - -safechecker/PCUICSafeReduce->safechecker/PCUICSafeConversion - - - - - -safechecker/PCUICErrors - -PCUICErrors - - - -safechecker/PCUICErrors->safechecker/PCUICSafeReduce - - - - - -erasure/Prelim - -Prelim - - - -safechecker/PCUICErrors->erasure/Prelim - - - - - -pcuic/PCUICTyping - -PCUICTyping - - - -pcuic/Bidirectional/BDEnvironmentTyping - -BDEnvironmentTyping - - - -pcuic/PCUICTyping->pcuic/Bidirectional/BDEnvironmentTyping - - - - - -pcuic/PCUICGlobalEnv - -PCUICGlobalEnv - - - -pcuic/PCUICTyping->pcuic/PCUICGlobalEnv - - - - - -pcuic/PCUICCSubst - -PCUICCSubst - - - -pcuic/PCUICTyping->pcuic/PCUICCSubst - - - - - -pcuic/PCUICGeneration - -PCUICGeneration - - - -pcuic/PCUICTyping->pcuic/PCUICGeneration - - - - - -pcuic/Syntax/PCUICNamelessDef - -PCUICNamelessDef - - - -pcuic/PCUICTyping->pcuic/Syntax/PCUICNamelessDef - - - - - -pcuic/Syntax/PCUICRenameDef - -PCUICRenameDef - - - -pcuic/PCUICTyping->pcuic/Syntax/PCUICRenameDef - - - - - -pcuic/PCUICExpandLets - -PCUICExpandLets - - - -pcuic/PCUICTyping->pcuic/PCUICExpandLets - - - - - -pcuic/Bidirectional/BDTyping - -BDTyping - - - -pcuic/Bidirectional/BDEnvironmentTyping->pcuic/Bidirectional/BDTyping - - - - - -template-coq/AstUtils - -AstUtils - - - -template-coq/AstUtils->pcuic/Bidirectional/BDEnvironmentTyping - - - - - -pcuic/TemplateToPCUIC - -TemplateToPCUIC - - - -template-coq/AstUtils->pcuic/TemplateToPCUIC - - - - - -template-coq/Induction - -Induction - - - -template-coq/AstUtils->template-coq/Induction - - - - - -template-coq/TemplateMonad/Extractable - -Extractable - - - -template-coq/AstUtils->template-coq/TemplateMonad/Extractable - - - - - -template-coq/TemplateMonad/Core - -Core - - - -template-coq/AstUtils->template-coq/TemplateMonad/Core - - - - - -template-coq/Kernames - -Kernames - - - -template-coq/AstUtils->template-coq/Kernames - - - - - -pcuic/PCUICToTemplate - -PCUICToTemplate - - - -template-coq/AstUtils->pcuic/PCUICToTemplate - - - - - -pcuic/Bidirectional/BDToPCUIC - -BDToPCUIC - - - -pcuic/Bidirectional/BDFromPCUIC - -BDFromPCUIC - - - -pcuic/Bidirectional/BDToPCUIC->pcuic/Bidirectional/BDFromPCUIC - - - - - -pcuic/Bidirectional/BDUnique - -BDUnique - - - -pcuic/Bidirectional/BDFromPCUIC->pcuic/Bidirectional/BDUnique - - - - - -pcuic/Bidirectional/BDStrengthening - -BDStrengthening - - - -pcuic/Bidirectional/BDFromPCUIC->pcuic/Bidirectional/BDStrengthening - - - - - -pcuic/Bidirectional/BDTyping->pcuic/Bidirectional/BDToPCUIC - - - - - -pcuic/PCUICSR - -PCUICSR - - - -pcuic/PCUICSR->pcuic/Bidirectional/BDToPCUIC - - - - - -pcuic/PCUICNormal - -PCUICNormal - - - -pcuic/PCUICSR->pcuic/PCUICNormal - - - - - -pcuic/PCUICCumulativity - -PCUICCumulativity - - - -pcuic/PCUICCumulativity->pcuic/Bidirectional/BDTyping - - - - - -pcuic/Conversion/PCUICWeakeningEnvConv - -PCUICWeakeningEnvConv - - - -pcuic/PCUICCumulativity->pcuic/Conversion/PCUICWeakeningEnvConv - - - - - -pcuic/Bidirectional/BDUnique->safechecker/PCUICSafeRetyping - - - - - -pcuic/Bidirectional/BDUnique->safechecker/PCUICTypeChecker - - - - - -pcuic/Conversion/PCUICClosedConv - -PCUICClosedConv - - - -pcuic/Conversion/PCUICWeakeningEnvConv->pcuic/Conversion/PCUICClosedConv - - - - - -pcuic/Conversion/PCUICUnivSubstitutionConv - -PCUICUnivSubstitutionConv - - - -pcuic/Conversion/PCUICWeakeningEnvConv->pcuic/Conversion/PCUICUnivSubstitutionConv - - - - - -pcuic/Typing/PCUICWeakeningEnvTyp - -PCUICWeakeningEnvTyp - - - -pcuic/Conversion/PCUICWeakeningEnvConv->pcuic/Typing/PCUICWeakeningEnvTyp - - - - - -pcuic/Typing/PCUICClosedTyp - -PCUICClosedTyp - - - -pcuic/Conversion/PCUICClosedConv->pcuic/Typing/PCUICClosedTyp - - - - - -pcuic/Conversion/PCUICInstConv - -PCUICInstConv - - - -pcuic/Conversion/PCUICUnivSubstitutionConv->pcuic/Conversion/PCUICInstConv - - - - - -pcuic/Typing/PCUICUnivSubstitutionTyp - -PCUICUnivSubstitutionTyp - - - -pcuic/Conversion/PCUICUnivSubstitutionConv->pcuic/Typing/PCUICUnivSubstitutionTyp - - - - - -pcuic/Conversion/PCUICNamelessConv - -PCUICNamelessConv - - - -pcuic/Conversion/PCUICUnivSubstitutionConv->pcuic/Conversion/PCUICNamelessConv - - - - - -pcuic/Typing/PCUICInstTyp - -PCUICInstTyp - - - -pcuic/Conversion/PCUICInstConv->pcuic/Typing/PCUICInstTyp - - - - - -pcuic/Typing/PCUICWeakeningTyp - -PCUICWeakeningTyp - - - -pcuic/Typing/PCUICWeakeningTyp->pcuic/Conversion/PCUICInstConv - - - - - -pcuic/Conversion/PCUICRenameConv - -PCUICRenameConv - - - -pcuic/Conversion/PCUICOnFreeVarsConv - -PCUICOnFreeVarsConv - - - -pcuic/Conversion/PCUICRenameConv->pcuic/Conversion/PCUICOnFreeVarsConv - - - - - -pcuic/Conversion/PCUICWeakeningConv - -PCUICWeakeningConv - - - -pcuic/Conversion/PCUICRenameConv->pcuic/Conversion/PCUICWeakeningConv - - - - - -pcuic/Typing/PCUICRenameTyp - -PCUICRenameTyp - - - -pcuic/Conversion/PCUICOnFreeVarsConv->pcuic/Typing/PCUICRenameTyp - - - - - -pcuic/Typing/PCUICClosedTyp->pcuic/Conversion/PCUICRenameConv - - - - - -pcuic/Typing/PCUICClosedTyp->pcuic/Conversion/PCUICNamelessConv - - - - - -pcuic/Conversion/PCUICWeakeningConv->pcuic/Typing/PCUICWeakeningTyp - - - - - -pcuic/PCUICContextSubst - -PCUICContextSubst - - - -pcuic/PCUICContextSubst->pcuic/Conversion/PCUICWeakeningEnvConv - - - - - -pcuic/PCUICGlobalEnv->safechecker/PCUICWfEnv - - - - - -pcuic/PCUICGlobalEnv->pcuic/Conversion/PCUICWeakeningEnvConv - - - - - -pcuic/PCUICGuardCondition - -PCUICGuardCondition - - - -pcuic/PCUICGuardCondition->pcuic/Conversion/PCUICWeakeningEnvConv - - - - - -pcuic/PCUICInductiveInversion - -PCUICInductiveInversion - - - -pcuic/PCUICAlpha - -PCUICAlpha - - - -pcuic/PCUICInductiveInversion->pcuic/PCUICAlpha - - - - - -pcuic/TemplateToPCUICCorrectness - -TemplateToPCUICCorrectness - - - -pcuic/PCUICInductiveInversion->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/PCUICAlpha->pcuic/PCUICSR - - - - - -pcuic/PCUICContexts - -PCUICContexts - - - -pcuic/PCUICArities - -PCUICArities - - - -pcuic/PCUICContexts->pcuic/PCUICArities - - - - - -pcuic/PCUICSpine - -PCUICSpine - - - -pcuic/PCUICArities->pcuic/PCUICSpine - - - - - -pcuic/PCUICInversion - -PCUICInversion - - - -pcuic/PCUICInversion->pcuic/PCUICArities - - - - - -pcuic/PCUICWcbvEval - -PCUICWcbvEval - - - -pcuic/PCUICInversion->pcuic/PCUICWcbvEval - - - - - -pcuic/PCUICWfUniverses - -PCUICWfUniverses - - - -pcuic/PCUICWfUniverses->pcuic/PCUICArities - - - - - -pcuic/PCUICEqualityDec - -PCUICEqualityDec - - - -pcuic/PCUICWfUniverses->pcuic/PCUICEqualityDec - - - - - -pcuic/utils/PCUICPrimitive - -PCUICPrimitive - - - -pcuic/PCUICAst - -PCUICAst - - - -pcuic/utils/PCUICPrimitive->pcuic/PCUICAst - - - - - -erasure/EAst - -EAst - - - -pcuic/utils/PCUICPrimitive->erasure/EAst - - - - - -pcuic/utils/PCUICOnOne - -PCUICOnOne - - - -pcuic/PCUICAst->pcuic/utils/PCUICOnOne - - - - - -pcuic/utils/PCUICSize - -PCUICSize - - - -pcuic/PCUICAst->pcuic/utils/PCUICSize - - - - - -pcuic/PCUICReduction - -PCUICReduction - - - -pcuic/PCUICReduction->pcuic/PCUICCumulativity - - - - - -pcuic/PCUICReduction->pcuic/PCUICGuardCondition - - - - - -pcuic/PCUICReduction->pcuic/PCUICCSubst - - - - - -pcuic/PCUICCSubst->pcuic/PCUICWcbvEval - - - - - -pcuic/PCUICElimination - -PCUICElimination - - - -pcuic/PCUICCanonicity - -PCUICCanonicity - - - -pcuic/PCUICElimination->pcuic/PCUICCanonicity - - - - - -erasure/Extract - -Extract - - - -pcuic/PCUICElimination->erasure/Extract - - - - - -pcuic/PCUICCanonicity->safechecker/PCUICSafeReduce - - - - - -erasure/EArities - -EArities - - - -pcuic/PCUICCanonicity->erasure/EArities - - - - - -pcuic/PCUICExpandLetsCorrectness - -PCUICExpandLetsCorrectness - - - -pcuic/PCUICCanonicity->pcuic/PCUICExpandLetsCorrectness - - - - - -pcuic/TemplateToPCUICWcbvEval - -TemplateToPCUICWcbvEval - - - -pcuic/PCUICCanonicity->pcuic/TemplateToPCUICWcbvEval - - - - - -pcuic/PCUICWcbvEval->pcuic/PCUICCanonicity - - - - - -erasure/EWcbvEval - -EWcbvEval - - - -pcuic/PCUICWcbvEval->erasure/EWcbvEval - - - - - -pcuic/PCUICEquality - -PCUICEquality - - - -pcuic/PCUICCasesContexts - -PCUICCasesContexts - - - -pcuic/PCUICEquality->pcuic/PCUICCasesContexts - - - - - -pcuic/Syntax/PCUICOnFreeVars - -PCUICOnFreeVars - - - -pcuic/PCUICEquality->pcuic/Syntax/PCUICOnFreeVars - - - - - -pcuic/Syntax/PCUICPosition - -PCUICPosition - - - -pcuic/PCUICEquality->pcuic/Syntax/PCUICPosition - - - - - -pcuic/PCUICCasesContexts->pcuic/PCUICSpine - - - - - -pcuic/PCUICSigmaCalculus - -PCUICSigmaCalculus - - - -pcuic/PCUICSigmaCalculus->pcuic/PCUICCasesContexts - - - - - -pcuic/Syntax/PCUICClosed - -PCUICClosed - - - -pcuic/PCUICSigmaCalculus->pcuic/Syntax/PCUICClosed - - - - - -pcuic/Syntax/PCUICTactics - -PCUICTactics - - - -pcuic/PCUICSigmaCalculus->pcuic/Syntax/PCUICTactics - - - - - -pcuic/PCUICParallelReductionConfluence - -PCUICParallelReductionConfluence - - - -pcuic/PCUICConfluence - -PCUICConfluence - - - -pcuic/PCUICParallelReductionConfluence->pcuic/PCUICConfluence - - - - - -pcuic/PCUICWellScopedCumulativity - -PCUICWellScopedCumulativity - - - -pcuic/PCUICConfluence->pcuic/PCUICWellScopedCumulativity - - - - - -pcuic/PCUICRedTypeIrrelevance - -PCUICRedTypeIrrelevance - - - -pcuic/PCUICRedTypeIrrelevance->pcuic/PCUICConfluence - - - - - -pcuic/PCUICContextConversion - -PCUICContextConversion - - - -pcuic/PCUICWellScopedCumulativity->pcuic/PCUICContextConversion - - - - - -pcuic/PCUICConversion - -PCUICConversion - - - -pcuic/PCUICContextConversion->pcuic/PCUICConversion - - - - - -pcuic/PCUICSubstitution - -PCUICSubstitution - - - -pcuic/PCUICSubstitution->pcuic/PCUICContexts - - - - - -pcuic/PCUICSubstitution->pcuic/PCUICWfUniverses - - - - - -pcuic/PCUICContextReduction - -PCUICContextReduction - - - -pcuic/PCUICSubstitution->pcuic/PCUICContextReduction - - - - - -pcuic/PCUICParallelReduction - -PCUICParallelReduction - - - -pcuic/PCUICSubstitution->pcuic/PCUICParallelReduction - - - - - -pcuic/PCUICContextReduction->pcuic/PCUICRedTypeIrrelevance - - - - - -pcuic/Syntax/PCUICLiftSubst - -PCUICLiftSubst - - - -pcuic/Syntax/PCUICLiftSubst->pcuic/PCUICContextSubst - - - - - -pcuic/Syntax/PCUICLiftSubst->pcuic/PCUICEquality - - - - - -pcuic/Syntax/PCUICLiftSubst->pcuic/PCUICSigmaCalculus - - - - - -pcuic/PCUICGeneration->pcuic/PCUICContexts - - - - - -pcuic/PCUICGeneration->pcuic/PCUICWfUniverses - - - - - -pcuic/Typing/PCUICUnivSubstitutionTyp->pcuic/PCUICContexts - - - - - -pcuic/PCUICConversion->pcuic/PCUICInversion - - - - - -pcuic/Typing/PCUICContextConversionTyp - -PCUICContextConversionTyp - - - -pcuic/PCUICConversion->pcuic/Typing/PCUICContextConversionTyp - - - - - -pcuic/Typing/PCUICNamelessTyp - -PCUICNamelessTyp - - - -pcuic/PCUICConversion->pcuic/Typing/PCUICNamelessTyp - - - - - -pcuic/PCUICSafeLemmata - -PCUICSafeLemmata - - - -pcuic/PCUICCumulProp - -PCUICCumulProp - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICCumulProp - - - - - -pcuic/PCUICSN - -PCUICSN - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICSN - - - - - -pcuic/PCUICToTemplateCorrectness - -PCUICToTemplateCorrectness - - - -pcuic/PCUICSafeLemmata->pcuic/PCUICToTemplateCorrectness - - - - - -pcuic/PCUICCumulProp->pcuic/PCUICElimination - - - - - -pcuic/PCUICPrincipality - -PCUICPrincipality - - - -pcuic/PCUICCumulProp->pcuic/PCUICPrincipality - - - - - -pcuic/PCUICCumulativitySpec - -PCUICCumulativitySpec - - - -pcuic/Syntax/PCUICOnFreeVars->pcuic/PCUICCumulativitySpec - - - - - -pcuic/PCUICCumulativitySpec->pcuic/PCUICTyping - - - - - -pcuic/utils/PCUICOnOne->pcuic/PCUICReduction - - - - - -pcuic/utils/PCUICOnOne->pcuic/PCUICCumulativitySpec - - - - - -pcuic/Syntax/PCUICReflect - -PCUICReflect - - - -pcuic/Syntax/PCUICReflect->pcuic/PCUICEquality - - - - - -erasure/EReflect - -EReflect - - - -pcuic/Syntax/PCUICReflect->erasure/EReflect - - - - - -pcuic/PCUICEqualityDec->safechecker/PCUICSafeConversion - - - - - -pcuic/Syntax/PCUICInstDef - -PCUICInstDef - - - -pcuic/Syntax/PCUICInstDef->pcuic/PCUICGuardCondition - - - - - -pcuic/Syntax/PCUICNamelessDef->pcuic/PCUICGuardCondition - - - - - -pcuic/PCUICValidity - -PCUICValidity - - - -pcuic/PCUICValidity->pcuic/PCUICInductiveInversion - - - - - -pcuic/PCUICInductives - -PCUICInductives - - - -pcuic/PCUICSpine->pcuic/PCUICInductives - - - - - -pcuic/PCUICInductives->pcuic/PCUICValidity - - - - - -pcuic/PCUICNormal->pcuic/PCUICSafeLemmata - - - - - -pcuic/PCUICConvCumInversion - -PCUICConvCumInversion - - - -pcuic/PCUICNormal->pcuic/PCUICConvCumInversion - - - - - -template-coq/UnivSubst - -UnivSubst - - - -template-coq/UnivSubst->pcuic/PCUICNormal - - - - - -template-coq/WfAst - -WfAst - - - -template-coq/UnivSubst->template-coq/WfAst - - - - - -pcuic/PCUICParallelReduction->pcuic/PCUICParallelReductionConfluence - - - - - -pcuic/Syntax/PCUICDepth - -PCUICDepth - - - -pcuic/Syntax/PCUICDepth->pcuic/PCUICParallelReduction - - - - - -pcuic/PCUICPrincipality->safechecker/PCUICSafeConversion - - - - - -pcuic/PCUICPrincipality->erasure/EArities - - - - - -pcuic/Syntax/PCUICClosed->pcuic/PCUICReduction - - - - - -pcuic/Syntax/PCUICClosed->pcuic/Syntax/PCUICOnFreeVars - - - - - -pcuic/Syntax/PCUICPosition->pcuic/PCUICTyping - - - - - -pcuic/Syntax/PCUICPosition->pcuic/PCUICReduction - - - - - -pcuic/Syntax/PCUICTactics->pcuic/PCUICReduction - - - - - -pcuic/PCUICSN->safechecker/PCUICWfReduction - - - - - -pcuic/Typing/PCUICContextConversionTyp->pcuic/PCUICSpine - - - - - -pcuic/Typing/PCUICInstTyp->pcuic/PCUICSubstitution - - - - - -pcuic/utils/PCUICUtils - -PCUICUtils - - - -pcuic/utils/PCUICUtils->pcuic/PCUICTyping - - - - - -pcuic/utils/PCUICAstUtils - -PCUICAstUtils - - - -pcuic/Syntax/PCUICCases - -PCUICCases - - - -pcuic/utils/PCUICAstUtils->pcuic/Syntax/PCUICCases - - - - - -pcuic/utils/PCUICPretty - -PCUICPretty - - - -pcuic/utils/PCUICAstUtils->pcuic/utils/PCUICPretty - - - - - -pcuic/Syntax/PCUICInduction - -PCUICInduction - - - -pcuic/Syntax/PCUICCases->pcuic/Syntax/PCUICInduction - - - - - -pcuic/Syntax/PCUICCases->pcuic/TemplateToPCUIC - - - - - -pcuic/Syntax/PCUICCases->pcuic/PCUICToTemplate - - - - - -pcuic/Syntax/PCUICUnivSubst - -PCUICUnivSubst - - - -pcuic/Syntax/PCUICUnivSubst->pcuic/Syntax/PCUICClosed - - - - - -pcuic/Syntax/PCUICInduction->pcuic/Syntax/PCUICLiftSubst - - - - - -pcuic/Syntax/PCUICInduction->pcuic/Syntax/PCUICReflect - - - - - -pcuic/Syntax/PCUICInduction->pcuic/Syntax/PCUICDepth - - - - - -pcuic/Syntax/PCUICInduction->pcuic/Syntax/PCUICUnivSubst - - - - - -template-coq/utils/LibHypsNaming - -LibHypsNaming - - - -template-coq/utils/LibHypsNaming->pcuic/Syntax/PCUICInduction - - - - - -pcuic/Syntax/PCUICRenameDef->pcuic/Syntax/PCUICInstDef - - - - - -template-coq/utils/MCPred - -MCPred - - - -template-coq/utils/MCPred->pcuic/Syntax/PCUICOnFreeVars - - - - - -pcuic/TemplateToPCUIC->safechecker/SafeTemplateChecker - - - - - -pcuic/TemplateToPCUIC->pcuic/TemplateToPCUICCorrectness - - - - - -pcuic/Typing/PCUICWeakeningEnvTyp->pcuic/Typing/PCUICClosedTyp - - - - - -pcuic/Typing/PCUICWeakeningEnvTyp->pcuic/Typing/PCUICUnivSubstitutionTyp - - - - - -pcuic/Typing/PCUICRenameTyp->pcuic/Typing/PCUICWeakeningTyp - - - - - -pcuic/utils/PCUICSize->pcuic/utils/PCUICAstUtils - - - - - -template-coq/common/uGraph - -uGraph - - - -template-coq/common/uGraph->pcuic/utils/PCUICAstUtils - - - - - -template-coq/Constants - -Constants - - - -template-coq/common/uGraph->template-coq/Constants - - - - - -template-coq/Checker - -Checker - - - -template-coq/common/uGraph->template-coq/Checker - - - - - -pcuic/utils/PCUICPretty->safechecker/PCUICWfReduction - - - - - -pcuic/utils/PCUICPretty->safechecker/PCUICErrors - - - - - -template-coq/EnvironmentTyping - -EnvironmentTyping - - - -template-coq/EnvironmentTyping->pcuic/utils/PCUICPrimitive - - - - - -template-coq/Ast - -Ast - - - -template-coq/EnvironmentTyping->template-coq/Ast - - - - - -template-coq/Reflect - -Reflect - - - -template-coq/Reflect->pcuic/utils/PCUICPrimitive - - - - - -template-coq/ReflectAst - -ReflectAst - - - -template-coq/Reflect->template-coq/ReflectAst - - - - - -template-coq/TermEquality - -TermEquality - - - -template-coq/Reflect->template-coq/TermEquality - - - - - -template-coq/Extraction - -Extraction - - - -template-coq/Reflect->template-coq/Extraction - - - - - -template-coq/config - -config - - - -template-coq/config->pcuic/utils/PCUICUtils - - - - - -template-coq/Universes - -Universes - - - -template-coq/config->template-coq/Universes - - - - - -template-coq/utils - -utils - - - -template-coq/utils->pcuic/utils/PCUICUtils - - - - - -template-coq/BasicAst - -BasicAst - - - -template-coq/utils->template-coq/BasicAst - - - - - -template-coq/Ast->template-coq/AstUtils - - - - - -template-coq/TemplateMonad/Common - -Common - - - -template-coq/Ast->template-coq/TemplateMonad/Common - - - - - -template-coq/BasicAst->template-coq/Universes - - - - - -template-coq/Universes->template-coq/common/uGraph - - - - - -template-coq/Universes->template-coq/Reflect - - - - - -template-coq/Environment - -Environment - - - -template-coq/Universes->template-coq/Environment - - - - - -template-coq/Environment->template-coq/EnvironmentTyping - - - - - -template-coq/Induction->template-coq/UnivSubst - - - - - -template-coq/Induction->template-coq/ReflectAst - - - - - -template-coq/Induction->template-coq/TermEquality - - - - - -template-coq/LiftSubst - -LiftSubst - - - -template-coq/WfAst->template-coq/LiftSubst - - - - - -template-coq/Typing - -Typing - - - -template-coq/LiftSubst->template-coq/Typing - - - - - -template-coq/Pretty - -Pretty - - - -template-coq/LiftSubst->template-coq/Pretty - - - - - -template-coq/ReflectAst->template-coq/Typing - - - - - -template-coq/TermEquality->template-coq/Typing - - - - - -template-coq/Typing->safechecker/SafeTemplateChecker - - - - - -template-coq/Typing->template-coq/Checker - - - - - -template-coq/Normal - -Normal - - - -template-coq/Typing->template-coq/Normal - - - - - -template-coq/TypingWf - -TypingWf - - - -template-coq/Typing->template-coq/TypingWf - - - - - -template-coq/Reduction - -Reduction - - - -template-coq/Typing->template-coq/Reduction - - - - - -template-coq/utils/wGraph - -wGraph - - - -template-coq/utils/wGraph->template-coq/common/uGraph - - - - - -template-coq/utils/All_Forall - -All_Forall - - - -template-coq/monad_utils - -monad_utils - - - -template-coq/utils/All_Forall->template-coq/monad_utils - - - - - -template-coq/utils/MCUtils - -MCUtils - - - -template-coq/utils/All_Forall->template-coq/utils/MCUtils - - - - - -template-coq/monad_utils->template-coq/utils - - - - - -template-coq/utils/MCUtils->template-coq/utils - - - - - -template-coq/utils/MCUtils->template-coq/utils/wGraph - - - - - -template-coq/utils/MCOption - -MCOption - - - -template-coq/utils/MCOption->template-coq/utils/MCPred - - - - - -template-coq/utils/MCOption->template-coq/utils/All_Forall - - - - - -template-coq/utils/MCSquash - -MCSquash - - - -template-coq/utils/MCSquash->template-coq/utils/All_Forall - - - - - -template-coq/utils/MCPrelude - -MCPrelude - - - -template-coq/utils/MCList - -MCList - - - -template-coq/utils/MCPrelude->template-coq/utils/MCList - - - - - -template-coq/utils/MCReflect - -MCReflect - - - -template-coq/utils/MCPrelude->template-coq/utils/MCReflect - - - - - -template-coq/utils/MCList->template-coq/utils/MCOption - - - - - -template-coq/utils/MCRelations - -MCRelations - - - -template-coq/utils/MCRelations->template-coq/utils/MCList - - - - - -template-coq/utils/MCProd - -MCProd - - - -template-coq/utils/MCProd->template-coq/utils/MCOption - - - - - -template-coq/utils/MCReflect->template-coq/utils/MCOption - - - - - -template-coq/utils/MCCompare - -MCCompare - - - -template-coq/utils/MCString - -MCString - - - -template-coq/utils/MCCompare->template-coq/utils/MCString - - - - - -template-coq/utils/MCString->template-coq/utils/MCUtils - - - - - -template-coq/utils/MCArith - -MCArith - - - -template-coq/utils/MCArith->template-coq/utils/MCUtils - - - - - -template-coq/utils/MCEquality - -MCEquality - - - -template-coq/utils/MCEquality->template-coq/utils/MCUtils - - - - - -template-coq/TemplateMonad/Extractable->template-coq/Extraction - - - - - -template-coq/TemplateMonad/Extractable->template-coq/Constants - - - - - -template-coq/TemplateMonad - -TemplateMonad - - - -template-coq/TemplateMonad/Core->template-coq/TemplateMonad - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Extractable - - - - - -template-coq/TemplateMonad/Common->template-coq/TemplateMonad/Core - - - - - -template-coq/TemplateMonad->template-coq/Constants - - - - - -template-coq/WcbvEval - -WcbvEval - - - -template-coq/WcbvEval->pcuic/TemplateToPCUICWcbvEval - - - - - -template-coq/TypingWf->template-coq/WcbvEval - - - - - -template-coq/TypingWf->pcuic/TemplateToPCUICCorrectness - - - - - -template-coq/TypingWf->pcuic/PCUICToTemplateCorrectness - - - - - -template-coq/Reduction->pcuic/PCUICToTemplateCorrectness - - - - - -template-coq/Pretty->template-coq/Extraction - - - - - -erasure/Erasure - -Erasure - - - -template-coq/Pretty->erasure/Erasure - - - - - -erasure/EAstUtils - -EAstUtils - - - -template-coq/Kernames->erasure/EAstUtils - - - - - -erasure/Extraction - -Extraction - - - -erasure/Erasure->erasure/Extraction - - - - - -erasure/EOptimizePropDiscr - -EOptimizePropDiscr - - - -erasure/EOptimizePropDiscr->erasure/Erasure - - - - - -erasure/ErasureFunction->erasure/EOptimizePropDiscr - - - - - -erasure/ErasureCorrectness - -ErasureCorrectness - - - -erasure/ErasureCorrectness->erasure/ErasureFunction - - - - - -erasure/EArities->erasure/Prelim - - - - - -erasure/EInversion - -EInversion - - - -erasure/EInversion->erasure/ErasureCorrectness - - - - - -erasure/ESubstitution - -ESubstitution - - - -erasure/EDeps - -EDeps - - - -erasure/ESubstitution->erasure/EDeps - - - - - -erasure/Prelim->erasure/EInversion - - - - - -erasure/Prelim->erasure/ESubstitution - - - - - -erasure/EAll - -EAll - - - -erasure/EDeps->erasure/ErasureCorrectness - - - - - -erasure/Extract->erasure/EArities - - - - - -erasure/Extract->erasure/EAll - - - - - -erasure/EGlobalEnv - -EGlobalEnv - - - -erasure/EGlobalEnv->erasure/Extract - - - - - -erasure/EWndEval - -EWndEval - - - -erasure/EGlobalEnv->erasure/EWndEval - - - - - -erasure/EGlobalEnv->erasure/EWcbvEval - - - - - -erasure/EPretty - -EPretty - - - -erasure/EGlobalEnv->erasure/EPretty - - - - - -erasure/EWndEval->erasure/EAll - - - - - -erasure/EWcbvEval->erasure/Prelim - - - - - -erasure/EWcbvEval->erasure/EAll - - - - - -erasure/ECSubst - -ECSubst - - - -erasure/ECSubst->erasure/EGlobalEnv - - - - - -erasure/EPretty->erasure/Erasure - - - - - -erasure/EReflect->erasure/EGlobalEnv - - - - - -erasure/ELiftSubst - -ELiftSubst - - - -erasure/ELiftSubst->erasure/ECSubst - - - - - -erasure/EInduction - -EInduction - - - -erasure/EInduction->erasure/EReflect - - - - - -erasure/EInduction->erasure/ELiftSubst - - - - - -erasure/EAstUtils->erasure/EGlobalEnv - - - - - -erasure/EAst->erasure/EInduction - - - - - -erasure/EAst->erasure/EAstUtils - - - - - -pcuic/PCUICExpandLets->pcuic/PCUICExpandLetsCorrectness - - - - - -pcuic/PCUICExpandLetsCorrectness->erasure/Erasure - - - - - -pcuic/TemplateToPCUICCorrectness->pcuic/TemplateToPCUICWcbvEval - - - - - -pcuic/TemplateToPCUICWcbvEval->erasure/Erasure - - - - - -pcuic/PCUICToTemplate->pcuic/PCUICToTemplateCorrectness - - - - - -pcuic/Conversion/PCUICNamelessConv->pcuic/Typing/PCUICNamelessTyp - - - - -