From 7c4c60a7c790ff955e893f6f02301688e605b011 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 6 Mar 2019 02:06:12 -0500 Subject: Add support for reifying fancy identifiers --- src/Language.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'src') diff --git a/src/Language.v b/src/Language.v index 016ad8b04..4d4995e68 100644 --- a/src/Language.v +++ b/src/Language.v @@ -973,6 +973,26 @@ Module Compilers. | fancy_addm => Datatypes.Some fancy.addm | _ => Datatypes.None end. + + Definition of_fancy {s d : base.type} (idc : fancy.ident s d) : ident (s -> d) + := match idc in fancy.ident s d return ident (s -> d) with + | fancy.with_wordmax log2wordmax s d idc + => match idc in fancy.ident_with_wordmax s d return ident (s -> d) with + | fancy.add imm => fancy_add log2wordmax imm + | fancy.addc imm => fancy_addc log2wordmax imm + | fancy.sub imm => fancy_sub log2wordmax imm + | fancy.subb imm => fancy_subb log2wordmax imm + | fancy.mulll => fancy_mulll log2wordmax + | fancy.mullh => fancy_mullh log2wordmax + | fancy.mulhl => fancy_mulhl log2wordmax + | fancy.mulhh => fancy_mulhh log2wordmax + | fancy.selm => fancy_selm log2wordmax + | fancy.rshi x => fancy_rshi log2wordmax x + end + | fancy.selc => fancy_selc + | fancy.sell => fancy_sell + | fancy.addm => fancy_addm + end. End with_scope. Notation Some := option_Some. Notation None := option_None. @@ -1378,6 +1398,10 @@ Module Compilers. => let rA := base.reify A in then_tac (@ident.None rA) | ZRange.Build_zrange => then_tac ident.Build_zrange + | fancy.interp ?idc + => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in + then_tac ridc + | @gen_interp _ ?idc => then_tac idc | _ => else_tac () end end. -- cgit v1.2.3