diff options
Diffstat (limited to 'src/Reflection/Named/Compile.v')
| -rw-r--r-- | src/Reflection/Named/Compile.v | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v index b6b4f7b3c..e37815597 100644 --- a/src/Reflection/Named/Compile.v +++ b/src/Reflection/Named/Compile.v @@ -25,36 +25,41 @@ Section language. Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name). Local Notation nexpr := (@Named.expr base_type_code interp_base_type op Name). - Fixpoint compilef {t} (e : exprf t) (ls : list Name) {struct e} + Fixpoint ocompilef {t} (e : exprf t) (ls : list (option Name)) {struct e} : option (nexprf t) := match e in @Syntax.exprf _ _ _ _ t return option (nexprf t) with | Const _ x => Some (Named.Const x) | Var _ x => Some (Named.Var x) - | Op _ _ op args => option_map (Named.Op op) (@compilef _ args ls) + | Op _ _ op args => option_map (Named.Op op) (@ocompilef _ args ls) | LetIn tx ex _ eC - => match @compilef _ ex nil, split_names tx ls with + => match @ocompilef _ ex nil, split_onames tx ls with | Some x, (Some n, ls')%core - => option_map (fun C => Named.LetIn tx n x C) (@compilef _ (eC n) ls') + => option_map (fun C => Named.LetIn tx n x C) (@ocompilef _ (eC n) ls') | _, _ => None end - | Pair _ ex _ ey => match @compilef _ ex nil, @compilef _ ey nil with + | Pair _ ex _ ey => match @ocompilef _ ex nil, @ocompilef _ ey nil with | Some x, Some y => Some (Named.Pair x y) | _, _ => None end end. - Fixpoint compile {t} (e : expr t) (ls : list Name) {struct e} + Fixpoint ocompile {t} (e : expr t) (ls : list (option Name)) {struct e} : option (nexpr t) := match e in @Syntax.expr _ _ _ _ t return option (nexpr t) with - | Return _ x => option_map Named.Return (compilef x ls) + | Return _ x => option_map Named.Return (ocompilef x ls) | Abs _ _ f => match ls with - | cons n ls' - => option_map (Named.Abs n) (@compile _ (f n) ls') + | cons (Some n) ls' + => option_map (Named.Abs n) (@ocompile _ (f n) ls') | _ => None end end. + + Definition compilef {t} (e : exprf t) (ls : list Name) := @ocompilef t e (List.map (@Some _) ls). + Definition compile {t} (e : expr t) (ls : list Name) := @ocompile t e (List.map (@Some _) ls). End language. +Global Arguments ocompilef {_ _ _ _ _} e ls. +Global Arguments ocompile {_ _ _ _ _} e ls. Global Arguments compilef {_ _ _ _ _} e ls. Global Arguments compile {_ _ _ _ _} e ls. |