diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-20 22:51:34 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-20 22:51:34 -0400 |
commit | 585cae5eb315fa0cd3f4d38d47be0476c6d8bd2c (patch) | |
tree | 14620cb4026a9e4e5252528ba12171ada5819b1e /src | |
parent | 32ea43cdf7c50599c340f001b5344410c7e2d6af (diff) |
Add GeneralizeVar
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/GeneralizeVar.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/src/Compilers/GeneralizeVar.v b/src/Compilers/GeneralizeVar.v new file mode 100644 index 000000000..882d8137b --- /dev/null +++ b/src/Compilers/GeneralizeVar.v @@ -0,0 +1,29 @@ +(** * Generalize [var] in [exprf] *) +Require Import Coq.PArith.BinPos. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.InterpretToPHOAS. +Require Import Crypto.Compilers.Named.Compile. +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Named.PositiveContext.Defaults. +Require Import Crypto.Compilers.Syntax. + +(** N.B. This procedure only works when there are no nested lets, + i.e., nothing like [let x := let y := z in w] in the PHOAS syntax + tree. This is a limitation of [compile]. *) + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type} + (base_type_code_beq : base_type_code -> base_type_code -> bool) + (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y) + (failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)). + + Local Notation PContext var := (PositiveContext _ var _ base_type_code_bl_transparent). + + Definition GeneralizeVar {t} (e : @Syntax.expr base_type_code op (fun _ => FMapPositive.PositiveMap.key) t) + : option (@Syntax.Expr base_type_code op (domain t -> codomain t)) + := let e := compile e (default_names_for (fun _ => 1%positive) e) in + let e := option_map (InterpToPHOAS (Context:=fun var => PContext var) failb) e in + e. +End language. |