diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/bugs/closed/5096.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/bugs/closed/5096.v')
-rw-r--r-- | test-suite/bugs/closed/5096.v | 219 |
1 files changed, 219 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v new file mode 100644 index 00000000..20a537ab --- /dev/null +++ b/test-suite/bugs/closed/5096.v @@ -0,0 +1,219 @@ +Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List. + +Set Asymmetric Patterns. + +Notation eta x := (fst x, snd x). + +Inductive expr {var : Type} : Type := +| Const : expr +| LetIn : expr -> (var -> expr) -> expr. + +Definition Expr := forall var, @expr var. + +Fixpoint count_binders (e : @expr unit) : nat := +match e with +| LetIn _ eC => 1 + @count_binders (eC tt) +| _ => 0 +end. + +Definition CountBinders (e : Expr) : nat := count_binders (e _). + +Class Context (Name : Type) (var : Type) := + { ContextT : Type; + extendb : ContextT -> Name -> var -> ContextT; + empty : ContextT }. +Coercion ContextT : Context >-> Sortclass. +Arguments ContextT {_ _ _}, {_ _} _. +Arguments extendb {_ _ _} _ _ _. +Arguments empty {_ _ _}. + +Module Export Named. +Inductive expr Name : Type := +| Const : expr Name +| LetIn : Name -> expr Name -> expr Name -> expr Name. +End Named. + +Global Arguments Const {_}. +Global Arguments LetIn {_} _ _ _. + +Definition split_onames {Name : Type} (ls : list (option Name)) + : option (Name) * list (option Name) + := match ls with + | cons n ls' + => (n, ls') + | nil => (None, nil) + end. + +Section internal. + Context (InName OutName : Type) + {InContext : Context InName (OutName)} + {ReverseContext : Context OutName (InName)} + (InName_beq : InName -> InName -> bool). + + Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext) + (e : expr InName) (new_names : list (option OutName)) + : option (expr OutName) + := match e in Named.expr _ return option (expr _) with + | Const => Some Const + | LetIn n ex eC + => let '(n', new_names') := eta (split_onames new_names) in + match n', @register_reassign ctxi ctxr ex nil with + | Some n', Some x + => let ctxi := @extendb _ _ _ ctxi n n' in + let ctxr := @extendb _ _ _ ctxr n' n in + option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names') + | None, Some x + => let ctxi := ctxi in + @register_reassign ctxi ctxr eC new_names' + | _, None => None + end + end. + +End internal. + +Global Instance pos_context (var : Type) : Context positive var + := { ContextT := PositiveMap.t var; + extendb ctx key v := PositiveMap.add key v ctx; + empty := PositiveMap.empty _ }. + +Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _. + +Section language5. + Context (Name : Type). + + Local Notation expr := (@Top.expr Name). + Local Notation nexpr := (@Named.expr Name). + + Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e} + : option (nexpr) + := match e in @Top.expr _ return option (nexpr) with + | Top.Const => Some Named.Const + | Top.LetIn ex eC + => match @ocompile ex nil, split_onames ls with + | Some x, (Some n, ls')%core + => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls') + | _, _ => None + end + end. + + Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls). +End language5. + +Global Arguments compile {_} e ls. + +Fixpoint merge_liveness (ls1 ls2 : list unit) := + match ls1, ls2 with + | cons x xs, cons y ys => cons tt (@merge_liveness xs ys) + | nil, ls | ls, nil => ls + end. + +Section internal1. + Context (Name : Type) + (OutName : Type) + {Context : Context Name (list unit)}. + + Definition compute_livenessf_step + (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit) + (ctx : Context) + (e : expr Name) (prefix : list unit) + : list unit + := match e with + | Const => prefix + | LetIn n ex eC + => let lx := @compute_livenessf ctx ex prefix in + let lx := merge_liveness lx (prefix ++ repeat tt 1) in + let ctx := @extendb _ _ _ ctx n (lx) in + @compute_livenessf ctx eC (prefix ++ repeat tt 1) + end. + + Fixpoint compute_liveness ctx e prefix + := @compute_livenessf_step (@compute_liveness) ctx e prefix. + + Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName) + : list (option OutName) + := match ls with + | nil => nil + | cons live xs + => match lsn with + | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn' + | nil => def :: @insert_dead_names_gen def xs nil + end + end. + Definition insert_dead_names def (e : expr Name) + := insert_dead_names_gen def (compute_liveness empty e nil). +End internal1. + +Global Arguments insert_dead_names {_ _ _} def e lsn. + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. + +Section language7. + Context {Context : Context unit (positive)}. + + Local Notation nexpr := (@Named.expr unit). + + Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit) + : option (nexpr) + := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in + match e with + | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *) + (fun names => register_reassign empty empty e names) + | None => None + end. +End language7. + +Global Arguments CompileAndEliminateDeadCode {_} e ls. + +Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var + := {| ContextT := Ctx; + extendb ctx n v := extendb ctx (f n) v; + empty := empty |}. + +Definition Register := Datatypes.unit. + +Global Instance RegisterContext {var : Type} : Context Register var + := ContextOn (fun _ => 1%positive) (pos_context var). + +Definition syntax := Named.expr Register. + +Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls) + := match res return match res with None => _ | _ => _ end with + | Some v => v + | None => I + end. + +Definition dummy_registers (n : nat) : list Register + := List.map (fun _ => tt) (seq 0 n). +Definition DefaultRegisters (e : Expr) : list Register + := dummy_registers (CountBinders e). + +Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e). + +Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200). +Notation "#[ var ]#" := (@Top.Const var). + +Definition compiled_syntax : Expr := fun (var : Type) => +( + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + slet x1 := #[ var ]# in + @Top.Const var). + +Definition v := + Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)). + +Timeout 2 Eval vm_compute in v. |