diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-05 14:29:06 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-05 14:29:06 -0500 |
commit | 9bd13e1e66b72ec985e907eb8befb8d394ed2ae0 (patch) | |
tree | 8d06fb54203a31553786e32293cd41163bc4a06c /src/Language.v | |
parent | 36da58eb94445de10f78c17cb01f01ef62a815b9 (diff) |
Revert "Fix reification of literals"
This reverts commit 36da58eb94445de10f78c17cb01f01ef62a815b9.
It doesn't work without access to var in reification of ident (also we
need to produce ident, not expr)
Diffstat (limited to 'src/Language.v')
-rw-r--r-- | src/Language.v | 58 |
1 files changed, 29 insertions, 29 deletions
diff --git a/src/Language.v b/src/Language.v index a9a22c148..d3d417d35 100644 --- a/src/Language.v +++ b/src/Language.v @@ -1127,34 +1127,6 @@ Module Compilers. Notation LiteralZRange := (@Literal base.type.zrange). Definition literal {T} (v : T) := v. - Definition reify_list {var} {t} (ls : list (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.list t)) - := Datatypes.list_rect - (fun _ => _) - (expr.Ident ident.nil) - (fun x _ xs => expr.Ident ident.cons @ x @ xs)%expr - ls. - - Definition reify_option {var} {t} (v : option (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.option t)) - := Datatypes.option_rect - (fun _ => _) - (fun x => expr.Ident ident.Some @ x)%expr - (expr.Ident ident.None) - v. - - Fixpoint smart_Literal {var} {t:base.type} : base.interp t -> @expr.expr base.type ident var (type.base t) - := match t with - | base.type.type_base t => fun v => expr.Ident (ident.Literal v) - | base.type.prod A B - => fun '((a, b) : base.interp A * base.interp B) - => expr.Ident ident.pair @ (@smart_Literal var A a) @ (@smart_Literal var B b) - | base.type.list A - => fun v : list (base.interp A) - => reify_list (List.map (@smart_Literal var A) v) - | base.type.option A - => fun v : option (base.interp A) - => reify_option (option_map (@smart_Literal var A) v) - end%expr. - (** TODO: MOVE ME? *) Module Thunked. Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P @@ -1223,7 +1195,7 @@ Module Compilers. | S => then_tac Nat_succ | @literal ?T => let rT := base.reify T in - then_tac (@ident.smart_Literal rT) + then_tac (@ident.Literal rT) | @Datatypes.nil ?T => let rT := base.reify T in then_tac (@ident.nil rT) @@ -1408,6 +1380,34 @@ Module Compilers. end end. + Definition reify_list {var} {t} (ls : list (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.list t)) + := Datatypes.list_rect + (fun _ => _) + (expr.Ident ident.nil) + (fun x _ xs => expr.Ident ident.cons @ x @ xs)%expr + ls. + + Definition reify_option {var} {t} (v : option (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.option t)) + := Datatypes.option_rect + (fun _ => _) + (fun x => expr.Ident ident.Some @ x)%expr + (expr.Ident ident.None) + v. + + Fixpoint smart_Literal {var} {t:base.type} : base.interp t -> @expr.expr base.type ident var (type.base t) + := match t with + | base.type.type_base t => fun v => expr.Ident (ident.Literal v) + | base.type.prod A B + => fun '((a, b) : base.interp A * base.interp B) + => expr.Ident ident.pair @ (@smart_Literal var A a) @ (@smart_Literal var B b) + | base.type.list A + => fun v : list (base.interp A) + => reify_list (List.map (@smart_Literal var A) v) + | base.type.option A + => fun v : option (base.interp A) + => reify_option (option_map (@smart_Literal var A) v) + end%expr. + Module Export Notations. Delimit Scope ident_scope with ident. Bind Scope ident_scope with ident. |