From 32ea43cdf7c50599c340f001b5344410c7e2d6af Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 20 Oct 2017 21:04:38 -0400 Subject: Add a version of exprf that lives in Set --- src/Compilers/InSet/Syntax.v | 84 ++++++++++++++++++++++++++ src/Compilers/InSet/Typeify.v | 58 ++++++++++++++++++ src/Compilers/InSet/TypeifyInterp.v | 114 ++++++++++++++++++++++++++++++++++++ 3 files changed, 256 insertions(+) create mode 100644 src/Compilers/InSet/Syntax.v create mode 100644 src/Compilers/InSet/Typeify.v create mode 100644 src/Compilers/InSet/TypeifyInterp.v (limited to 'src') diff --git a/src/Compilers/InSet/Syntax.v b/src/Compilers/InSet/Syntax.v new file mode 100644 index 000000000..4a3bb7a46 --- /dev/null +++ b/src/Compilers/InSet/Syntax.v @@ -0,0 +1,84 @@ +(** * PHOAS Representation of Gallina, in [Set] *) +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Compilers.Syntax. + +(** Universes are annoying. See, e.g., + [bug#5996](https://github.com/coq/coq/issues/5996), where using + [pattern] and [constr:(...)] to replace [Set] with [Type] breaks + things. Because we need to get reflective syntax by patterning [Z + : Set], we make a version of [exprf] in [Set]. We build the + minimial infrastructure needed to get this sort of expression into + the [Type]-based one. *) + +Delimit Scope set_expr_scope with set_expr. +Local Open Scope set_expr_scope. +Section language. + Context (base_type_code : Set). + + Local Notation flat_type := (flat_type base_type_code). + + Let Tbase' := @Tbase base_type_code. + Local Coercion Tbase' : base_type_code >-> flat_type. + + Section interp. + Context (interp_base_type : base_type_code -> Set). + Fixpoint interp_flat_type (t : flat_type) := + match t with + | Tbase t => interp_base_type t + | Unit => unit + | Prod x y => prod (interp_flat_type x) (interp_flat_type y) + end. + End interp. + + Section expr_param. + Context (interp_base_type : base_type_code -> Set). + Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Set). + Local Notation interp_flat_type_gen := interp_flat_type. + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + Section expr. + Context {var : base_type_code -> Set}. + + Inductive exprf : flat_type -> Set := + | TT : exprf Unit + | Var {t} (v : var t) : exprf t + | Op {t1 tR} (opc : op t1 tR) (args : exprf t1) : exprf tR + | LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type_gen var tx -> exprf tC) : exprf tC + | Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty). + Bind Scope set_expr_scope with exprf. + End expr. + + Section interp. + Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst). + + Definition interpf_step + (interpf : forall {t} (e : @exprf interp_flat_type t), interp_flat_type t) + {t} (e : @exprf interp_flat_type t) : interp_flat_type t + := match e in exprf t return interp_flat_type t with + | TT => tt + | Var _ x => x + | Op _ _ op args => @interp_op _ _ op (@interpf _ args) + | LetIn _ ex _ eC => dlet x := @interpf _ ex in @interpf _ (eC x) + | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey) + end. + + Fixpoint interpf {t} e + := @interpf_step (@interpf) t e. + End interp. + End expr_param. +End language. +Global Arguments Var {_ _ _ _} _. +Global Arguments TT {_ _ _}. +Global Arguments Op {_ _ _ _ _} _ _. +Global Arguments LetIn {_ _ _ _} _ {_} _. +Global Arguments Pair {_ _ _ _} _ {_} _. +Global Arguments Abs {_ _ _ _ _} _. +Global Arguments interp_flat_type {_} _ _. +Global Arguments interpf {_ _ _} interp_op {t} _. + +Module Export Notations. + Notation "'slet' x .. y := A 'in' b" := (LetIn A%set_expr (fun x => .. (fun y => b%set_expr) .. )) : set_expr_scope. + Notation "( x , y , .. , z )" := (Pair .. (Pair x%set_expr y%set_expr) .. z%set_expr) : set_expr_scope. + Notation "( )" := TT : set_expr_scope. + Notation "()" := TT : set_expr_scope. +End Notations. diff --git a/src/Compilers/InSet/Typeify.v b/src/Compilers/InSet/Typeify.v new file mode 100644 index 000000000..d2fbad987 --- /dev/null +++ b/src/Compilers/InSet/Typeify.v @@ -0,0 +1,58 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.InSet.Syntax. + +Section language. + Context {base_type_code : Set} + {op : flat_type base_type_code -> flat_type base_type_code -> Set} + {var : base_type_code -> Set}. + + Fixpoint typeify_interp_flat_type {t} + : InSet.Syntax.interp_flat_type var t -> Compilers.Syntax.interp_flat_type var t + := match t with + | Tbase T => fun v => v + | Unit => fun v => v + | Prod A B => fun ab : InSet.Syntax.interp_flat_type _ A * InSet.Syntax.interp_flat_type _ B + => (@typeify_interp_flat_type _ (fst ab), + @typeify_interp_flat_type _ (snd ab)) + end. + Fixpoint untypeify_interp_flat_type {t} + : Compilers.Syntax.interp_flat_type var t -> InSet.Syntax.interp_flat_type var t + := match t with + | Tbase T => fun v => v + | Unit => fun v => v + | Prod A B => fun ab : Compilers.Syntax.interp_flat_type _ A * Compilers.Syntax.interp_flat_type _ B + => (@untypeify_interp_flat_type _ (fst ab), + @untypeify_interp_flat_type _ (snd ab)) + end. + + Fixpoint typeify {t} (e : @InSet.Syntax.exprf base_type_code op var t) + : @Compilers.Syntax.exprf base_type_code op var t + := match e with + | TT => Compilers.Syntax.TT + | Var t v => Compilers.Syntax.Var v + | Op t1 tR opc args => Compilers.Syntax.Op opc (@typeify _ args) + | LetIn tx ex tC eC + => Compilers.Syntax.LetIn + (@typeify _ ex) + (fun x => @typeify _ (eC (untypeify_interp_flat_type x))) + | Pair tx ex ty ey => Compilers.Syntax.Pair + (@typeify _ ex) + (@typeify _ ey) + end. + + Fixpoint untypeify {t} (e : @Compilers.Syntax.exprf base_type_code op var t) + : @InSet.Syntax.exprf base_type_code op var t + := match e with + | Compilers.Syntax.TT => TT + | Compilers.Syntax.Var t v => Var v + | Compilers.Syntax.Op t1 tR opc args => Op opc (@untypeify _ args) + | Compilers.Syntax.LetIn tx ex tC eC + => LetIn + (@untypeify _ ex) + (fun x => @untypeify _ (eC (typeify_interp_flat_type x))) + | Compilers.Syntax.Pair tx ex ty ey + => Pair + (@untypeify _ ex) + (@untypeify _ ey) + end. +End language. diff --git a/src/Compilers/InSet/TypeifyInterp.v b/src/Compilers/InSet/TypeifyInterp.v new file mode 100644 index 000000000..77790eec8 --- /dev/null +++ b/src/Compilers/InSet/TypeifyInterp.v @@ -0,0 +1,114 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.InSet.Syntax. +Require Import Crypto.Compilers.InSet.Typeify. + + +Local Ltac t := + repeat first [ reflexivity + | progress simpl in * + | apply (f_equal2 (@pair _ _)) + | solve [ auto ] + | progress cbv [LetIn.Let_In] + | progress autorewrite with core + | progress intros + | match goal with + | [ v : _ * _ |- _ ] => destruct v + | [ H : _ |- _ ] => rewrite H + end ]. + +Section language. + Context {base_type_code : Set} + {op : flat_type base_type_code -> flat_type base_type_code -> Set} + {interp_base_type : base_type_code -> Set}. + + Lemma typeify_untypeify_interp_flat_type {t} v + : @typeify_interp_flat_type base_type_code interp_base_type t (untypeify_interp_flat_type v) = v. + Proof using Type. induction t; t. Qed. + Lemma untypeify_typeify_interp_flat_type {t} v + : @untypeify_interp_flat_type base_type_code interp_base_type t (typeify_interp_flat_type v) = v. + Proof using Type. induction t; t. Qed. + Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type. + + Section gen. + Context {interp_op : forall s d, op s d -> Compilers.Syntax.interp_flat_type interp_base_type s -> Compilers.Syntax.interp_flat_type interp_base_type d} + {interp_op' : forall s d, op s d -> InSet.Syntax.interp_flat_type interp_base_type s -> InSet.Syntax.interp_flat_type interp_base_type d} + (untypeify_interp_op + : forall s d opc args, + untypeify_interp_flat_type (interp_op s d opc args) + = interp_op' s d opc (untypeify_interp_flat_type args)) + (typeify_interp_op + : forall s d opc args, + typeify_interp_flat_type (interp_op' s d opc args) + = interp_op s d opc (typeify_interp_flat_type args)). + + Local Notation interpf := (Compilers.Syntax.interpf interp_op). + Local Notation interpf' := (InSet.Syntax.interpf interp_op'). + Local Notation typeify := (typeify (var:=interp_base_type)). + + Lemma interpf_typeify {t} e + : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e). + Proof using typeify_interp_op. induction e; t. Qed. + Lemma interpf_untypeify {t} e + : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e). + Proof using untypeify_interp_op. induction e; t. Qed. + + Lemma interpf_typeify_untypeify {t} e + : interpf (typeify (untypeify (t:=t) e)) = interpf e. + Proof using Type. induction e; t. Qed. + Lemma interpf_untypeify_typeify {t} e + : interpf' (untypeify (t:=t) (typeify e)) = interpf' e. + Proof using Type. induction e; t. Qed. + End gen. +End language. + +Module Compilers. + Import Compilers.Syntax. + Section language. + Context {base_type_code : Set} + {op : flat_type base_type_code -> flat_type base_type_code -> Set} + {interp_base_type : base_type_code -> Set} + {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}. + + Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type. + + Local Notation interp_op' := + (fun s d opc args => untypeify_interp_flat_type (interp_op s d opc (typeify_interp_flat_type args))). + + Local Notation interpf := (Compilers.Syntax.interpf interp_op). + Local Notation interpf' := (InSet.Syntax.interpf interp_op'). + Local Notation typeify := (typeify (var:=interp_base_type)). + + Lemma interpf_typeify {t} e + : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e). + Proof using Type. apply interpf_typeify; t. Qed. + Lemma interpf_untypeify {t} e + : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e). + Proof using Type. apply interpf_untypeify; t. Qed. + End language. +End Compilers. + +Module InSet. + Import InSet.Syntax. + Section language. + Context {base_type_code : Set} + {op : flat_type base_type_code -> flat_type base_type_code -> Set} + {interp_base_type : base_type_code -> Set} + {interp_op' : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}. + + Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type. + + Local Notation interp_op := + (fun s d opc args => typeify_interp_flat_type (interp_op' s d opc (untypeify_interp_flat_type args))). + + Local Notation interpf := (Compilers.Syntax.interpf interp_op). + Local Notation interpf' := (InSet.Syntax.interpf interp_op'). + Local Notation typeify := (typeify (var:=interp_base_type)). + + Lemma interpf_typeify {t} e + : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e). + Proof using Type. apply interpf_typeify; t. Qed. + Lemma interpf_untypeify {t} e + : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e). + Proof using Type. apply interpf_untypeify; t. Qed. + End language. +End InSet. -- cgit v1.2.3