diff options
28 files changed, 93 insertions, 66 deletions
diff --git a/_CoqProject b/_CoqProject index e0e88e441..d266f8fcf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -86,6 +86,7 @@ src/Compilers/Named/Compile.v src/Compilers/Named/CompileInterp.v src/Compilers/Named/CompileProperties.v src/Compilers/Named/CompileWf.v +src/Compilers/Named/Context.v src/Compilers/Named/ContextDefinitions.v src/Compilers/Named/ContextOn.v src/Compilers/Named/ContextProperties.v diff --git a/src/Compilers/MapCastByDeBruijn.v b/src/Compilers/MapCastByDeBruijn.v index 0964847a6..0eb137a06 100644 --- a/src/Compilers/MapCastByDeBruijn.v +++ b/src/Compilers/MapCastByDeBruijn.v @@ -1,4 +1,5 @@ Require Import Crypto.Compilers.SmartMap. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.MapCast. Require Import Crypto.Compilers.Named.InterpretToPHOAS. diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v index 5d8156f09..10e09242a 100644 --- a/src/Compilers/MapCastByDeBruijnInterp.v +++ b/src/Compilers/MapCastByDeBruijnInterp.v @@ -1,6 +1,7 @@ Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.Relations. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.MapCastInterp. diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v index 7bc58042f..7c1e386b5 100644 --- a/src/Compilers/MapCastByDeBruijnWf.v +++ b/src/Compilers/MapCastByDeBruijnWf.v @@ -1,6 +1,7 @@ Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.Relations. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.MapCastWf. diff --git a/src/Compilers/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v index 1c7e42258..9368900e4 100644 --- a/src/Compilers/Named/CompileInterp.v +++ b/src/Compilers/Named/CompileInterp.v @@ -1,4 +1,5 @@ (** * PHOAS → Named Representation of Gallina *) +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.NameUtil. Require Import Crypto.Compilers.Named.NameUtilProperties. diff --git a/src/Compilers/Named/CompileWf.v b/src/Compilers/Named/CompileWf.v index aea8cb2b1..b04c207d2 100644 --- a/src/Compilers/Named/CompileWf.v +++ b/src/Compilers/Named/CompileWf.v @@ -1,4 +1,5 @@ (** * PHOAS → Named Representation of Gallina *) +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.Named.ContextDefinitions. diff --git a/src/Compilers/Named/Context.v b/src/Compilers/Named/Context.v new file mode 100644 index 000000000..ba0ad6feb --- /dev/null +++ b/src/Compilers/Named/Context.v @@ -0,0 +1,65 @@ +(** * Contexts for Named Representation of Gallina *) +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.SmartMap. +Require Import Crypto.Util.Notations. + +Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) := + { ContextT : Type; + lookupb : ContextT -> Name -> forall {t : base_type_code}, option (var t); + extendb : ContextT -> Name -> forall {t : base_type_code}, var t -> ContextT; + removeb : ContextT -> Name -> base_type_code -> ContextT; + empty : ContextT }. +Coercion ContextT : Context >-> Sortclass. +Arguments ContextT {_ _ _ _}, {_ _ _} _. +Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _. +Arguments extendb {_ _ _ _} _ _ [_] _. +Arguments removeb {_ _ _ _} _ _ _. +Arguments empty {_ _ _ _}. + +Section language. + Context {base_type_code : Type} + {Name : Type} + {var : base_type_code -> Type} + {Context : Context Name var}. + + Local Notation flat_type := (flat_type base_type_code). + + Fixpoint extend (ctx : Context) {t : flat_type} + (n : interp_flat_type (fun _ => Name) t) (v : interp_flat_type var t) + : Context + := match t return interp_flat_type (fun _ => Name) t -> interp_flat_type var t -> Context with + | Tbase t => fun n v => extendb ctx n v + | Unit => fun _ _ => ctx + | Prod A B => fun n v + => let ctx := @extend ctx A (fst n) (fst v) in + let ctx := @extend ctx B (snd n) (snd v) in + ctx + end n v. + + Fixpoint remove (ctx : Context) {t : flat_type} + (n : interp_flat_type (fun _ => Name) t) + : Context + := match t return interp_flat_type (fun _ => Name) t -> Context with + | Tbase t => fun n => removeb ctx n t + | Unit => fun _ => ctx + | Prod A B => fun n + => let ctx := @remove ctx A (fst n) in + let ctx := @remove ctx B (snd n) in + ctx + end n. + + Definition lookup (ctx : Context) {t} + : interp_flat_type (fun _ => Name) t -> option (interp_flat_type var t) + := smart_interp_flat_map + (g := fun t => option (interp_flat_type var t)) + (fun t v => lookupb ctx v) + (Some tt) + (fun A B x y => match x, y with + | Some x', Some y' => Some (x', y')%core + | _, _ => None + end). +End language. + +Global Arguments extend {_ _ _ _} ctx {_} _ _. +Global Arguments remove {_ _ _ _} ctx {_} _. +Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _. diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v index 6e1a3e64a..386a1a363 100644 --- a/src/Compilers/Named/ContextDefinitions.v +++ b/src/Compilers/Named/ContextDefinitions.v @@ -1,5 +1,5 @@ Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Decidable. diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v index 6c06d3fbe..5e51f7585 100644 --- a/src/Compilers/Named/ContextOn.v +++ b/src/Compilers/Named/ContextOn.v @@ -1,5 +1,5 @@ (** * Transfer [Context] across an injection *) -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Section language. Context {base_type_code Name1 Name2 : Type} diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v index c2a9ca828..2f6b8d209 100644 --- a/src/Compilers/Named/ContextProperties.v +++ b/src/Compilers/Named/ContextProperties.v @@ -1,5 +1,5 @@ Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.ContextProperties.Tactics. Require Import Crypto.Util.Decidable. diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v index 96653ac99..95edcff8f 100644 --- a/src/Compilers/Named/ContextProperties/NameUtil.v +++ b/src/Compilers/Named/ContextProperties/NameUtil.v @@ -2,7 +2,7 @@ Require Import Coq.omega.Omega. Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Wf. -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.NameUtil. Require Import Crypto.Compilers.Named.NameUtilProperties. diff --git a/src/Compilers/Named/ContextProperties/SmartMap.v b/src/Compilers/Named/ContextProperties/SmartMap.v index 7cf761a34..9018bce76 100644 --- a/src/Compilers/Named/ContextProperties/SmartMap.v +++ b/src/Compilers/Named/ContextProperties/SmartMap.v @@ -1,7 +1,7 @@ Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.ContextProperties. Require Import Crypto.Compilers.Named.ContextProperties.Tactics. diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v index 312370834..c2e1e8a7d 100644 --- a/src/Compilers/Named/DeadCodeElimination.v +++ b/src/Compilers/Named/DeadCodeElimination.v @@ -1,5 +1,6 @@ (** * PHOAS → Named Representation of Gallina *) Require Import Coq.PArith.BinPos Coq.Lists.List. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Compile. Require Import Crypto.Compilers.Named.RegisterAssign. diff --git a/src/Compilers/Named/EstablishLiveness.v b/src/Compilers/Named/EstablishLiveness.v index 5d1255af3..c2d6c273a 100644 --- a/src/Compilers/Named/EstablishLiveness.v +++ b/src/Compilers/Named/EstablishLiveness.v @@ -2,6 +2,7 @@ Require Import Coq.Lists.List. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.SmartMap. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.CountLets. Require Import Crypto.Util.ListUtil. diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v index 1ea45cbbe..5519881c8 100644 --- a/src/Compilers/Named/FMapContext.v +++ b/src/Compilers/Named/FMapContext.v @@ -1,7 +1,7 @@ Require Import Coq.Bool.Sumbool. Require Import Coq.FSets.FMapInterface. Require Import Coq.FSets.FMapFacts. -Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Equality. diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v index 5ed1e7cf2..d82740cb4 100644 --- a/src/Compilers/Named/IdContext.v +++ b/src/Compilers/Named/IdContext.v @@ -1,4 +1,6 @@ +Require Import Coq.Lists.List. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Section language. diff --git a/src/Compilers/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v index dc737a38d..1ccad6cad 100644 --- a/src/Compilers/Named/InterpretToPHOAS.v +++ b/src/Compilers/Named/InterpretToPHOAS.v @@ -1,3 +1,4 @@ +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.SmartMap. diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v index 0772721f6..88fb2d8a0 100644 --- a/src/Compilers/Named/InterpretToPHOASInterp.v +++ b/src/Compilers/Named/InterpretToPHOASInterp.v @@ -1,3 +1,4 @@ +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.Named.ContextDefinitions. diff --git a/src/Compilers/Named/InterpretToPHOASWf.v b/src/Compilers/Named/InterpretToPHOASWf.v index c0e59d10e..fd35ab12c 100644 --- a/src/Compilers/Named/InterpretToPHOASWf.v +++ b/src/Compilers/Named/InterpretToPHOASWf.v @@ -1,3 +1,4 @@ +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.Named.ContextDefinitions. diff --git a/src/Compilers/Named/MapCast.v b/src/Compilers/Named/MapCast.v index 83c477765..fddee84fa 100644 --- a/src/Compilers/Named/MapCast.v +++ b/src/Compilers/Named/MapCast.v @@ -1,6 +1,7 @@ Require Import Coq.Bool.Sumbool. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Local Open Scope nexpr_scope. diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v index f3842e691..cb4d3062c 100644 --- a/src/Compilers/Named/MapCastInterp.v +++ b/src/Compilers/Named/MapCastInterp.v @@ -3,6 +3,7 @@ Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.ContextProperties. diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v index cd8a2e720..9f82004bc 100644 --- a/src/Compilers/Named/MapCastWf.v +++ b/src/Compilers/Named/MapCastWf.v @@ -3,6 +3,7 @@ Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.ContextProperties. diff --git a/src/Compilers/Named/RegisterAssign.v b/src/Compilers/Named/RegisterAssign.v index d1e871fd0..869d959ec 100644 --- a/src/Compilers/Named/RegisterAssign.v +++ b/src/Compilers/Named/RegisterAssign.v @@ -1,5 +1,6 @@ (** * Reassign registers *) Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.PositiveContext. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.NameUtil. diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v index c58fcc9d1..0af2bb33e 100644 --- a/src/Compilers/Named/Syntax.v +++ b/src/Compilers/Named/Syntax.v @@ -1,26 +1,10 @@ (** * Named Representation of Gallina *) -Require Import Coq.Classes.RelationClasses. Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.SmartMap. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.Tuple. -(*Require Import Crypto.Util.Tactics.*) Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. -Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) := - { ContextT : Type; - lookupb : ContextT -> Name -> forall {t : base_type_code}, option (var t); - extendb : ContextT -> Name -> forall {t : base_type_code}, var t -> ContextT; - removeb : ContextT -> Name -> base_type_code -> ContextT; - empty : ContextT }. -Coercion ContextT : Context >-> Sortclass. -Arguments ContextT {_ _ _ _}, {_ _ _} _. -Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _. -Arguments extendb {_ _ _ _} _ _ [_] _. -Arguments removeb {_ _ _ _} _ _ _. -Arguments empty {_ _ _ _}. - Local Open Scope ctype_scope. Local Open Scope expr_scope. Delimit Scope nexpr_scope with nexpr. @@ -52,46 +36,6 @@ Module Export Named. Definition invert_Abs {t} (e : expr t) : exprf (codomain t) := match e with Abs _ _ n f => f end. - Section with_context. - Context {var : base_type_code -> Type} - {Context : Context Name var}. - - Fixpoint extend (ctx : Context) {t : flat_type} - (n : interp_flat_type_gen (fun _ => Name) t) (v : interp_flat_type_gen var t) - : Context - := match t return interp_flat_type_gen (fun _ => Name) t -> interp_flat_type_gen var t -> Context with - | Tbase t => fun n v => extendb ctx n v - | Unit => fun _ _ => ctx - | Prod A B => fun n v - => let ctx := @extend ctx A (fst n) (fst v) in - let ctx := @extend ctx B (snd n) (snd v) in - ctx - end n v. - - Fixpoint remove (ctx : Context) {t : flat_type} - (n : interp_flat_type_gen (fun _ => Name) t) - : Context - := match t return interp_flat_type_gen (fun _ => Name) t -> Context with - | Tbase t => fun n => removeb ctx n t - | Unit => fun _ => ctx - | Prod A B => fun n - => let ctx := @remove ctx A (fst n) in - let ctx := @remove ctx B (snd n) in - ctx - end n. - - Definition lookup (ctx : Context) {t} - : interp_flat_type_gen (fun _ => Name) t -> option (interp_flat_type_gen var t) - := smart_interp_flat_map - (g := fun t => option (interp_flat_type_gen var t)) - (fun t v => lookupb ctx v) - (Some tt) - (fun A B x y => match x, y with - | Some x', Some y' => Some (x', y')%core - | _, _ => None - end). - End with_context. - Section with_val_context. Context (Context : Context Name interp_base_type) (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). @@ -133,9 +77,6 @@ Global Arguments Pair {_ _ _ _} _ {_} _. Global Arguments Abs {_ _ _ _ _} _ _. Global Arguments invert_Abs {_ _ _ _} _. Global Arguments Abs_name {_ _ _ _} _. -Global Arguments extend {_ _ _ _} ctx {_} _ _. -Global Arguments remove {_ _ _ _} ctx {_} _. -Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _. Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _. Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _. diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v index df2213b21..fec1de5ed 100644 --- a/src/Compilers/Named/Wf.v +++ b/src/Compilers/Named/Wf.v @@ -1,4 +1,5 @@ Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Util.PointedProp. diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v index b44811b06..580dcb438 100644 --- a/src/Compilers/Named/WfInterp.v +++ b/src/Compilers/Named/WfInterp.v @@ -1,4 +1,5 @@ Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Util.PointedProp. diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v index 0db93721e..229e5f869 100644 --- a/src/Compilers/TestCase.v +++ b/src/Compilers/TestCase.v @@ -1,5 +1,6 @@ Require Import Coq.omega.Omega Coq.micromega.Psatz. Require Import Coq.PArith.BinPos Coq.Lists.List. +Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.Compile. Require Import Crypto.Compilers.Named.RegisterAssign. diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v index 900ac92a9..adb29e81f 100644 --- a/src/Specific/FancyMachine256/Core.v +++ b/src/Specific/FancyMachine256/Core.v @@ -8,6 +8,7 @@ Require Export Crypto.LegacyArithmetic.ArchitectureToZLike. Require Export Crypto.LegacyArithmetic.ArchitectureToZLikeProofs. Require Export Crypto.Util.Tuple. Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod. +Require Import Crypto.Compilers.Named.Context. Require Export Crypto.Compilers.Named.Syntax. Require Export Crypto.Compilers.Named.PositiveContext. Require Import Crypto.Compilers.Named.DeadCodeElimination. |