From 0bbbdfede48aed7a74ac2fb95440256ed60fb6e8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Feb 2019 18:17:11 -0500 Subject: Add support for reifying `zrange` and `option` This is needed to reify statements for the rewriter. --- src/GENERATEDIdentifiersWithoutTypes.v | 594 ++++++++++++++++++++++----------- 1 file changed, 404 insertions(+), 190 deletions(-) (limited to 'src/GENERATEDIdentifiersWithoutTypes.v') diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v index a5e96870f..d2651f53b 100644 --- a/src/GENERATEDIdentifiersWithoutTypes.v +++ b/src/GENERATEDIdentifiersWithoutTypes.v @@ -23,7 +23,7 @@ Module Compilers. Module base. Local Notation einterp := type.interp. Module type. - Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type). + Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type) | option (A : type). End type. Notation type := type.type. @@ -32,18 +32,20 @@ Module Compilers. | Compilers.base.type.type_base t => type.type_base t | Compilers.base.type.prod A B => type.prod (relax A) (relax B) | Compilers.base.type.list A => type.list (relax A) + | Compilers.base.type.option A => type.option (relax A) end. Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : Compilers.base.type := match ptype with | type.var p => match PositiveMap.find p evar_map with - | Some t => t - | None => Compilers.base.type.type_base base.type.unit + | Datatypes.Some t => t + | Datatypes.None => Compilers.base.type.type_base base.type.unit end | type.type_base t => Compilers.base.type.type_base t | type.prod A B => Compilers.base.type.prod (subst_default A evar_map) (subst_default B evar_map) | type.list A => Compilers.base.type.list (subst_default A evar_map) + | type.option A => Compilers.base.type.option (subst_default A evar_map) end. Fixpoint collect_vars (t : type) : PositiveSet.t @@ -52,6 +54,7 @@ Module Compilers. | type.type_base t => PositiveSet.empty | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B) | type.list A => collect_vars A + | type.option A => collect_vars A end. Module Notations. @@ -435,6 +438,13 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (Compilers.base.type.type_base base.type.Z) -> (fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.bool))%ptype + | Z_ltb : ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.bool))%ptype | Z_geb : ident ((fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> @@ -442,6 +452,13 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (Compilers.base.type.type_base base.type.Z) -> (fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.bool))%ptype + | Z_gtb : ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.bool))%ptype | Z_of_nat : ident ((fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> @@ -480,6 +497,20 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (Compilers.base.type.type_base base.type.Z) -> (fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.Z))%ptype + | Z_min : ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z))%ptype + | Z_max : ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z))%ptype | Z_bneg : ident ((fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> @@ -605,6 +636,41 @@ print_ident = r"""Inductive ident : defaults.type -> Set := (fun x : Compilers.base.type => type.base x) (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype + | option_Some : forall A : Compilers.base.type, + ident + ((fun x : Compilers.base.type => type.base x) A -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.option A))%ptype + | option_None : forall A : Compilers.base.type, + ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.option A)) + | option_rect : forall A P : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) A -> + (fun x : Compilers.base.type => type.base x) P) -> + ((fun x : Compilers.base.type => type.base x) ()%etype -> + (fun x : Compilers.base.type => type.base x) P) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.option A) -> + (fun x : Compilers.base.type => type.base x) P)%ptype + | Build_zrange : ident + ((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.zrange))%ptype + | zrange_rect : forall P : Compilers.base.type, + ident + (((fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type => type.base x) P) -> + (fun x : Compilers.base.type => type.base x) + (Compilers.base.type.type_base base.type.zrange) -> + (fun x : Compilers.base.type => type.base x) P)%ptype | fancy_add : Z -> Z -> ident @@ -755,13 +821,17 @@ show_match_ident = r"""match # with | ident.Z_log2_up => | ident.Z_eqb => | ident.Z_leb => + | ident.Z_ltb => | ident.Z_geb => + | ident.Z_gtb => | ident.Z_of_nat => | ident.Z_to_nat => | ident.Z_shiftr => | ident.Z_shiftl => | ident.Z_land => | ident.Z_lor => + | ident.Z_min => + | ident.Z_max => | ident.Z_bneg => | ident.Z_lnot_modulo => | ident.Z_mul_split => @@ -776,6 +846,11 @@ show_match_ident = r"""match # with | ident.Z_cc_m => | ident.Z_cast range => | ident.Z_cast2 range => + | ident.option_Some A => + | ident.option_None A => + | ident.option_rect A P => + | ident.Build_zrange => + | ident.zrange_rect P => | ident.fancy_add log2wordmax imm => | ident.fancy_addc log2wordmax imm => | ident.fancy_sub log2wordmax imm => @@ -804,7 +879,7 @@ indent0 = ' ' indent1 = ' ' + indent0 indent2 = ' ' + indent1 #exts = ('Unit', 'Z', 'Bool', 'Nat') -base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat')] +base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat', 'zrange')] type_or_set = 'Type' ctors = [i.strip('|=> ').split(' ') for i in show_match_ident.split('\n') if i.strip().startswith('|')] assert(ctors[0][0] == 'ident.Literal') @@ -862,7 +937,7 @@ Module Compilers. Module base. Local Notation einterp := type.interp. Module type. - Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type). + Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type) | option (A : type). End type. Notation type := type.type. @@ -871,18 +946,20 @@ Module Compilers. | Compilers.base.type.type_base t => type.type_base t | Compilers.base.type.prod A B => type.prod (relax A) (relax B) | Compilers.base.type.list A => type.list (relax A) + | Compilers.base.type.option A => type.option (relax A) end. Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : Compilers.base.type := match ptype with | type.var p => match PositiveMap.find p evar_map with - | Some t => t - | None => Compilers.base.type.type_base base.type.unit + | Datatypes.Some t => t + | Datatypes.None => Compilers.base.type.type_base base.type.unit end | type.type_base t => Compilers.base.type.type_base t | type.prod A B => Compilers.base.type.prod (subst_default A evar_map) (subst_default B evar_map) | type.list A => Compilers.base.type.list (subst_default A evar_map) + | type.option A => Compilers.base.type.option (subst_default A evar_map) end. Fixpoint collect_vars (t : type) : PositiveSet.t @@ -891,6 +968,7 @@ Module Compilers. | type.type_base t => PositiveSet.empty | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B) | type.list A => collect_vars A + | type.option A => collect_vars A end. Module Notations. @@ -1050,14 +1128,14 @@ retcode += addnewline((r"""%sDefinition is_simple (idc : ident) : bool '\n | '.join(pctor + ' => ' + ('true' if len(named_ttype) == 0 else 'false') for pctor, named_ttype in zip(pctors, named_ttypes_with_prefix)))).replace('\n', '\n' + indent2)) -retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : option (full_types pidc) - := match pidc, idc return option (full_types pidc) with +retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : Datatypes.option (full_types pidc) + := match pidc, idc return Datatypes.option (full_types pidc) with | %s | %s - => None + => Datatypes.None end%%cps. """ % (indent2, prefix, - '\n | '.join(pctor + ', ' + ' '.join(ctor) + ' => Some ' + make_pair_of_types(named_ttype, ctype, ctor) + '\n | '.join(pctor + ', ' + ' '.join(ctor) + ' => Datatypes.Some ' + make_pair_of_types(named_ttype, ctype, ctor) for pctor, ctor, named_ttype, ctype in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes)), '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2)) @@ -1149,18 +1227,18 @@ retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : Evar assert(ctors[0][0] == 'ident.Literal') assert(len(ctypes[0]) == 1) -retcode += addnewline((r"""%sDefinition unify {t t'} (pidc : ident t) (idc : %sident.ident t') : option (type_of_list (@arg_types t pidc)) - := match pidc, idc return option (type_of_list (arg_types pidc)) with +retcode += addnewline((r"""%sDefinition unify {t t'} (pidc : ident t) (idc : %sident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc)) + := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with | %s | %s | %s - => None + => Datatypes.None end%%cps. """ % (indent1, prefix, - '\n | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Some ' + fold_right_pair(ctor[-len(ctype):]) + '\n | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Datatypes.Some ' + fold_right_pair(ctor[-len(ctype):]) for pctor, ctor, ctype in zip(pctors[:1], ctors_with_prefix[:1], ctypes[:1]) for ty in base_types), - '\n | '.join('@' + pctor + ', ' + ' '.join([ctor[0]] + [i + "'" for i in ctor[1:]]) + ' => Some ' + ('tt' if len(ctype) == 0 else fold_right_pair([i + "'" for i in ctor[-len(ctype):]])) + '\n | '.join('@' + pctor + ', ' + ' '.join([ctor[0]] + [i + "'" for i in ctor[1:]]) + ' => Datatypes.Some ' + ('tt' if len(ctype) == 0 else fold_right_pair([i + "'" for i in ctor[-len(ctype):]])) for pctor, ctor, ctype in zip(pctors_with_args[1:], ctors_with_prefix[1:], ctypes[1:])), '\n | '.join('@' + pctor + ', _' for pctor, named_ttype in zip(pctors_with_underscores, named_ttypes)))).replace('\n', '\n' + indent1)) @@ -1178,8 +1256,8 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident """ % (indent1, prefix, '\n | '.join(' '.join(ctor) + ' => @' + pctor + ' ' + ' '.join(relax_type_var(n, t) for n, t in named_ttype) for ctor, pctor, named_ttype in zip(ctors_with_prefix, pctors, named_ttypes)))).replace('\n', '\n' + indent1)) # # -#retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t -# := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t with +#retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t +# := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t with # | %s # end. #""" % (indent1, prefix, type_or_set, prefix, prefix, type_or_set, prefix, @@ -1188,7 +1266,7 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident # + 'fun ' + ('_ => ' if len(ctype) == 0 else ((ctor[-1] + ' => ') if len(ctype) == 1 else "arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(ctype):]), len(ctype)))) + "@" + ' '.join(ctor) # + ('' if not do_adjust_type(ctor, ctype) else # (') : ' -# + ('match arg_types (of_typed_ident %s) return %s with Some t => t | None => unit end -> _' +# + ('match arg_types (of_typed_ident %s) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> _' # % (('%s' if ' ' not in ' '.join(ctor) else '(@%s)') % ' '.join(ctor), # type_or_set)) # + ' (* COQBUG(https://github.com/coq/coq/issues/7726) *)')) @@ -1197,20 +1275,20 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident -#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> option (P idc1 -> P idc2) +#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> Datatypes.option (P idc1 -> P idc2) # := match idc1, idc2 with # | %s -# => fun T k => k (Some (fun v => v)) +# => fun T k => k (Datatypes.Some (fun v => v)) # | %s -# => fun T k => k None +# => fun T k => k Datatypes.None # end%%cps. #""" % (indent2, # '\n | '.join(pctor + ', ' + pctor for pctor in pctors), # '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2)) -#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> option T) -# : option (ident -> T) +#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> Datatypes.option T) +# : Datatypes.option (ident -> T) # := (%s; -# Some (fun c +# Datatypes.Some (fun c # => match c with # | %s # end))%%option. @@ -1326,13 +1404,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up | Z_eqb | Z_leb + | Z_ltb | Z_geb + | Z_gtb | Z_of_nat | Z_to_nat | Z_shiftr | Z_shiftl | Z_land | Z_lor + | Z_min + | Z_max | Z_bneg | Z_lnot_modulo | Z_mul_split @@ -1347,6 +1429,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m | Z_cast | Z_cast2 + | option_Some + | option_None + | option_rect + | Build_zrange + | zrange_rect | fancy_add | fancy_addc | fancy_sub @@ -1407,13 +1494,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up => unit | Z_eqb => unit | Z_leb => unit + | Z_ltb => unit | Z_geb => unit + | Z_gtb => unit | Z_of_nat => unit | Z_to_nat => unit | Z_shiftr => unit | Z_shiftl => unit | Z_land => unit | Z_lor => unit + | Z_min => unit + | Z_max => unit | Z_bneg => unit | Z_lnot_modulo => unit | Z_mul_split => unit @@ -1428,6 +1519,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m => unit | Z_cast => zrange | Z_cast2 => zrange * zrange + | option_Some => Compilers.base.type + | option_None => Compilers.base.type + | option_rect => Compilers.base.type * Compilers.base.type + | Build_zrange => unit + | zrange_rect => Compilers.base.type | fancy_add => Z * Z | fancy_addc => Z * Z | fancy_sub => Z * Z @@ -1489,13 +1585,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up => true | Z_eqb => true | Z_leb => true + | Z_ltb => true | Z_geb => true + | Z_gtb => true | Z_of_nat => true | Z_to_nat => true | Z_shiftr => true | Z_shiftl => true | Z_land => true | Z_lor => true + | Z_min => true + | Z_max => true | Z_bneg => true | Z_lnot_modulo => true | Z_mul_split => true @@ -1510,6 +1610,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m => true | Z_cast => true | Z_cast2 => true + | option_Some => false + | option_None => false + | option_rect => false + | Build_zrange => true + | zrange_rect => false | fancy_add => true | fancy_addc => true | fancy_sub => true @@ -1525,86 +1630,95 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | fancy_addm => true end. - Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : option (full_types pidc) - := match pidc, idc return option (full_types pidc) with - | Literal, Compilers.ident.Literal t v => Some (existT _ t v) - | Nat_succ, Compilers.ident.Nat_succ => Some tt - | Nat_pred, Compilers.ident.Nat_pred => Some tt - | Nat_max, Compilers.ident.Nat_max => Some tt - | Nat_mul, Compilers.ident.Nat_mul => Some tt - | Nat_add, Compilers.ident.Nat_add => Some tt - | Nat_sub, Compilers.ident.Nat_sub => Some tt - | Nat_eqb, Compilers.ident.Nat_eqb => Some tt - | nil, Compilers.ident.nil t => Some t - | cons, Compilers.ident.cons t => Some t - | pair, Compilers.ident.pair A B => Some (A, B) - | fst, Compilers.ident.fst A B => Some (A, B) - | snd, Compilers.ident.snd A B => Some (A, B) - | prod_rect, Compilers.ident.prod_rect A B T => Some (A, B, T) - | bool_rect, Compilers.ident.bool_rect T => Some T - | nat_rect, Compilers.ident.nat_rect P => Some P - | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Some (P, Q) - | list_rect, Compilers.ident.list_rect A P => Some (A, P) - | list_case, Compilers.ident.list_case A P => Some (A, P) - | List_length, Compilers.ident.List_length T => Some T - | List_seq, Compilers.ident.List_seq => Some tt - | List_firstn, Compilers.ident.List_firstn A => Some A - | List_skipn, Compilers.ident.List_skipn A => Some A - | List_repeat, Compilers.ident.List_repeat A => Some A - | List_combine, Compilers.ident.List_combine A B => Some (A, B) - | List_map, Compilers.ident.List_map A B => Some (A, B) - | List_app, Compilers.ident.List_app A => Some A - | List_rev, Compilers.ident.List_rev A => Some A - | List_flat_map, Compilers.ident.List_flat_map A B => Some (A, B) - | List_partition, Compilers.ident.List_partition A => Some A - | List_fold_right, Compilers.ident.List_fold_right A B => Some (A, B) - | List_update_nth, Compilers.ident.List_update_nth T => Some T - | List_nth_default, Compilers.ident.List_nth_default T => Some T - | Z_add, Compilers.ident.Z_add => Some tt - | Z_mul, Compilers.ident.Z_mul => Some tt - | Z_pow, Compilers.ident.Z_pow => Some tt - | Z_sub, Compilers.ident.Z_sub => Some tt - | Z_opp, Compilers.ident.Z_opp => Some tt - | Z_div, Compilers.ident.Z_div => Some tt - | Z_modulo, Compilers.ident.Z_modulo => Some tt - | Z_log2, Compilers.ident.Z_log2 => Some tt - | Z_log2_up, Compilers.ident.Z_log2_up => Some tt - | Z_eqb, Compilers.ident.Z_eqb => Some tt - | Z_leb, Compilers.ident.Z_leb => Some tt - | Z_geb, Compilers.ident.Z_geb => Some tt - | Z_of_nat, Compilers.ident.Z_of_nat => Some tt - | Z_to_nat, Compilers.ident.Z_to_nat => Some tt - | Z_shiftr, Compilers.ident.Z_shiftr => Some tt - | Z_shiftl, Compilers.ident.Z_shiftl => Some tt - | Z_land, Compilers.ident.Z_land => Some tt - | Z_lor, Compilers.ident.Z_lor => Some tt - | Z_bneg, Compilers.ident.Z_bneg => Some tt - | Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Some tt - | Z_mul_split, Compilers.ident.Z_mul_split => Some tt - | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Some tt - | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Some tt - | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Some tt - | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Some tt - | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Some tt - | Z_zselect, Compilers.ident.Z_zselect => Some tt - | Z_add_modulo, Compilers.ident.Z_add_modulo => Some tt - | Z_rshi, Compilers.ident.Z_rshi => Some tt - | Z_cc_m, Compilers.ident.Z_cc_m => Some tt - | Z_cast, Compilers.ident.Z_cast range => Some range - | Z_cast2, Compilers.ident.Z_cast2 range => Some range - | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Some (log2wordmax, imm) - | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Some (log2wordmax, imm) - | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Some (log2wordmax, imm) - | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Some (log2wordmax, imm) - | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Some log2wordmax - | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Some log2wordmax - | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Some log2wordmax - | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Some log2wordmax - | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Some (log2wordmax, x) - | fancy_selc, Compilers.ident.fancy_selc => Some tt - | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Some log2wordmax - | fancy_sell, Compilers.ident.fancy_sell => Some tt - | fancy_addm, Compilers.ident.fancy_addm => Some tt + Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : Datatypes.option (full_types pidc) + := match pidc, idc return Datatypes.option (full_types pidc) with + | Literal, Compilers.ident.Literal t v => Datatypes.Some (existT _ t v) + | Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt + | Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt + | Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt + | Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt + | Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt + | Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt + | Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt + | nil, Compilers.ident.nil t => Datatypes.Some t + | cons, Compilers.ident.cons t => Datatypes.Some t + | pair, Compilers.ident.pair A B => Datatypes.Some (A, B) + | fst, Compilers.ident.fst A B => Datatypes.Some (A, B) + | snd, Compilers.ident.snd A B => Datatypes.Some (A, B) + | prod_rect, Compilers.ident.prod_rect A B T => Datatypes.Some (A, B, T) + | bool_rect, Compilers.ident.bool_rect T => Datatypes.Some T + | nat_rect, Compilers.ident.nat_rect P => Datatypes.Some P + | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Datatypes.Some (P, Q) + | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P) + | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P) + | List_length, Compilers.ident.List_length T => Datatypes.Some T + | List_seq, Compilers.ident.List_seq => Datatypes.Some tt + | List_firstn, Compilers.ident.List_firstn A => Datatypes.Some A + | List_skipn, Compilers.ident.List_skipn A => Datatypes.Some A + | List_repeat, Compilers.ident.List_repeat A => Datatypes.Some A + | List_combine, Compilers.ident.List_combine A B => Datatypes.Some (A, B) + | List_map, Compilers.ident.List_map A B => Datatypes.Some (A, B) + | List_app, Compilers.ident.List_app A => Datatypes.Some A + | List_rev, Compilers.ident.List_rev A => Datatypes.Some A + | List_flat_map, Compilers.ident.List_flat_map A B => Datatypes.Some (A, B) + | List_partition, Compilers.ident.List_partition A => Datatypes.Some A + | List_fold_right, Compilers.ident.List_fold_right A B => Datatypes.Some (A, B) + | List_update_nth, Compilers.ident.List_update_nth T => Datatypes.Some T + | List_nth_default, Compilers.ident.List_nth_default T => Datatypes.Some T + | Z_add, Compilers.ident.Z_add => Datatypes.Some tt + | Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt + | Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt + | Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt + | Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt + | Z_div, Compilers.ident.Z_div => Datatypes.Some tt + | Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt + | Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt + | Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt + | Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt + | Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt + | Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt + | Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt + | Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt + | Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt + | Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt + | Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt + | Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt + | Z_land, Compilers.ident.Z_land => Datatypes.Some tt + | Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt + | Z_min, Compilers.ident.Z_min => Datatypes.Some tt + | Z_max, Compilers.ident.Z_max => Datatypes.Some tt + | Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt + | Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt + | Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt + | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt + | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt + | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt + | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt + | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt + | Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt + | Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt + | Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt + | Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt + | Z_cast, Compilers.ident.Z_cast range => Datatypes.Some range + | Z_cast2, Compilers.ident.Z_cast2 range => Datatypes.Some range + | option_Some, Compilers.ident.option_Some A => Datatypes.Some A + | option_None, Compilers.ident.option_None A => Datatypes.Some A + | option_rect, Compilers.ident.option_rect A P => Datatypes.Some (A, P) + | Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt + | zrange_rect, Compilers.ident.zrange_rect P => Datatypes.Some P + | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Datatypes.Some (log2wordmax, imm) + | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Datatypes.Some (log2wordmax, imm) + | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Datatypes.Some (log2wordmax, imm) + | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Datatypes.Some (log2wordmax, imm) + | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Datatypes.Some log2wordmax + | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Datatypes.Some log2wordmax + | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Datatypes.Some log2wordmax + | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Datatypes.Some log2wordmax + | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Datatypes.Some (log2wordmax, x) + | fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt + | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Datatypes.Some log2wordmax + | fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt + | fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt | Literal, _ | Nat_succ, _ | Nat_pred, _ @@ -1649,13 +1763,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up, _ | Z_eqb, _ | Z_leb, _ + | Z_ltb, _ | Z_geb, _ + | Z_gtb, _ | Z_of_nat, _ | Z_to_nat, _ | Z_shiftr, _ | Z_shiftl, _ | Z_land, _ | Z_lor, _ + | Z_min, _ + | Z_max, _ | Z_bneg, _ | Z_lnot_modulo, _ | Z_mul_split, _ @@ -1670,6 +1788,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m, _ | Z_cast, _ | Z_cast2, _ + | option_Some, _ + | option_None, _ + | option_rect, _ + | Build_zrange, _ + | zrange_rect, _ | fancy_add, _ | fancy_addc, _ | fancy_sub, _ @@ -1683,7 +1806,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | fancy_selm, _ | fancy_sell, _ | fancy_addm, _ - => None + => Datatypes.None end%cps. Definition type_of (pidc : ident) : full_types pidc -> Compilers.type Compilers.base.type @@ -1732,13 +1855,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_eqb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype | Z_leb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype + | Z_ltb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype | Z_geb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype + | Z_gtb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype | Z_of_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_to_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype | Z_shiftr => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_shiftl => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_land => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_lor => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype + | Z_min => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype + | Z_max => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_bneg => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_lnot_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_mul_split => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype @@ -1753,6 +1880,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_cast => fun range => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype | Z_cast2 => fun range => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype + | option_Some => fun A => (type.base A -> type.base (Compilers.base.type.option A))%ptype + | option_None => fun A => (type.base (Compilers.base.type.option A)) + | option_rect => fun arg => let '(A, P) := eta2 arg in ((type.base A -> type.base P) -> (type.base ()%etype -> type.base P) -> type.base (Compilers.base.type.option A) -> type.base P)%ptype + | Build_zrange => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.zrange))%ptype + | zrange_rect => fun P => ((type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base P) -> type.base (Compilers.base.type.type_base base.type.zrange) -> type.base P)%ptype | fancy_add => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype | fancy_addc => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype | fancy_sub => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype @@ -1814,13 +1946,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up => fun _ => @Compilers.ident.Z_log2_up | Z_eqb => fun _ => @Compilers.ident.Z_eqb | Z_leb => fun _ => @Compilers.ident.Z_leb + | Z_ltb => fun _ => @Compilers.ident.Z_ltb | Z_geb => fun _ => @Compilers.ident.Z_geb + | Z_gtb => fun _ => @Compilers.ident.Z_gtb | Z_of_nat => fun _ => @Compilers.ident.Z_of_nat | Z_to_nat => fun _ => @Compilers.ident.Z_to_nat | Z_shiftr => fun _ => @Compilers.ident.Z_shiftr | Z_shiftl => fun _ => @Compilers.ident.Z_shiftl | Z_land => fun _ => @Compilers.ident.Z_land | Z_lor => fun _ => @Compilers.ident.Z_lor + | Z_min => fun _ => @Compilers.ident.Z_min + | Z_max => fun _ => @Compilers.ident.Z_max | Z_bneg => fun _ => @Compilers.ident.Z_bneg | Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo | Z_mul_split => fun _ => @Compilers.ident.Z_mul_split @@ -1835,6 +1971,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m => fun _ => @Compilers.ident.Z_cc_m | Z_cast => fun range => @Compilers.ident.Z_cast range | Z_cast2 => fun range => @Compilers.ident.Z_cast2 range + | option_Some => fun A => @Compilers.ident.option_Some A + | option_None => fun A => @Compilers.ident.option_None A + | option_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of option_rect arg') with (A, P) => @Compilers.ident.option_rect A P end + | Build_zrange => fun _ => @Compilers.ident.Build_zrange + | zrange_rect => fun P => @Compilers.ident.zrange_rect P | fancy_add => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_add arg') with (log2wordmax, imm) => @Compilers.ident.fancy_add log2wordmax imm end | fancy_addc => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_addc arg') with (log2wordmax, imm) => @Compilers.ident.fancy_addc log2wordmax imm end | fancy_sub => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_sub arg') with (log2wordmax, imm) => @Compilers.ident.fancy_sub log2wordmax imm end @@ -1903,13 +2044,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.Z_log2_up => f _ Compilers.ident.Z_log2_up | Compilers.ident.Z_eqb => f _ Compilers.ident.Z_eqb | Compilers.ident.Z_leb => f _ Compilers.ident.Z_leb + | Compilers.ident.Z_ltb => f _ Compilers.ident.Z_ltb | Compilers.ident.Z_geb => f _ Compilers.ident.Z_geb + | Compilers.ident.Z_gtb => f _ Compilers.ident.Z_gtb | Compilers.ident.Z_of_nat => f _ Compilers.ident.Z_of_nat | Compilers.ident.Z_to_nat => f _ Compilers.ident.Z_to_nat | Compilers.ident.Z_shiftr => f _ Compilers.ident.Z_shiftr | Compilers.ident.Z_shiftl => f _ Compilers.ident.Z_shiftl | Compilers.ident.Z_land => f _ Compilers.ident.Z_land | Compilers.ident.Z_lor => f _ Compilers.ident.Z_lor + | Compilers.ident.Z_min => f _ Compilers.ident.Z_min + | Compilers.ident.Z_max => f _ Compilers.ident.Z_max | Compilers.ident.Z_bneg => f _ Compilers.ident.Z_bneg | Compilers.ident.Z_lnot_modulo => f _ Compilers.ident.Z_lnot_modulo | Compilers.ident.Z_mul_split => f _ Compilers.ident.Z_mul_split @@ -1924,6 +2069,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.Z_cc_m => f _ Compilers.ident.Z_cc_m | Compilers.ident.Z_cast range => f _ (@Compilers.ident.Z_cast range) | Compilers.ident.Z_cast2 range => f _ (@Compilers.ident.Z_cast2 range) + | Compilers.ident.option_Some A => f _ (@Compilers.ident.option_Some A) + | Compilers.ident.option_None A => f _ (@Compilers.ident.option_None A) + | Compilers.ident.option_rect A P => f _ (@Compilers.ident.option_rect A P) + | Compilers.ident.Build_zrange => f _ Compilers.ident.Build_zrange + | Compilers.ident.zrange_rect P => f _ (@Compilers.ident.zrange_rect P) | Compilers.ident.fancy_add log2wordmax imm => f _ (@Compilers.ident.fancy_add log2wordmax imm) | Compilers.ident.fancy_addc log2wordmax imm => f _ (@Compilers.ident.fancy_addc log2wordmax imm) | Compilers.ident.fancy_sub log2wordmax imm => f _ (@Compilers.ident.fancy_sub log2wordmax imm) @@ -1984,13 +2134,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_log2_up : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_eqb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype | Z_leb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype + | Z_ltb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype | Z_geb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype + | Z_gtb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype | Z_of_nat : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.Z))%ptype | Z_to_nat : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.nat))%ptype | Z_shiftr : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_shiftl : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_land : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_lor : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype + | Z_min : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype + | Z_max : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_bneg : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_lnot_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_mul_split : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype @@ -2005,6 +2159,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Z_cc_m : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_cast : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype | Z_cast2 : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype + | option_Some {A : base.type} : ident (type.base A -> type.base (base.type.option A))%ptype + | option_None {A : base.type} : ident (type.base (base.type.option A)) + | option_rect {A : base.type} {P : base.type} : ident ((type.base A -> type.base P) -> (type.base ()%pbtype -> type.base P) -> type.base (base.type.option A) -> type.base P)%ptype + | Build_zrange : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.zrange))%ptype + | zrange_rect {P : base.type} : ident ((type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base P) -> type.base (base.type.type_base base.type.zrange) -> type.base P)%ptype | fancy_add : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype | fancy_addc : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype | fancy_sub : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype @@ -2065,13 +2224,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_log2_up => Raw.ident.Z_log2_up | @Z_eqb => Raw.ident.Z_eqb | @Z_leb => Raw.ident.Z_leb + | @Z_ltb => Raw.ident.Z_ltb | @Z_geb => Raw.ident.Z_geb + | @Z_gtb => Raw.ident.Z_gtb | @Z_of_nat => Raw.ident.Z_of_nat | @Z_to_nat => Raw.ident.Z_to_nat | @Z_shiftr => Raw.ident.Z_shiftr | @Z_shiftl => Raw.ident.Z_shiftl | @Z_land => Raw.ident.Z_land | @Z_lor => Raw.ident.Z_lor + | @Z_min => Raw.ident.Z_min + | @Z_max => Raw.ident.Z_max | @Z_bneg => Raw.ident.Z_bneg | @Z_lnot_modulo => Raw.ident.Z_lnot_modulo | @Z_mul_split => Raw.ident.Z_mul_split @@ -2086,6 +2249,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_cc_m => Raw.ident.Z_cc_m | @Z_cast => Raw.ident.Z_cast | @Z_cast2 => Raw.ident.Z_cast2 + | @option_Some A => Raw.ident.option_Some + | @option_None A => Raw.ident.option_None + | @option_rect A P => Raw.ident.option_rect + | @Build_zrange => Raw.ident.Build_zrange + | @zrange_rect P => Raw.ident.zrange_rect | @fancy_add => Raw.ident.fancy_add | @fancy_addc => Raw.ident.fancy_addc | @fancy_sub => Raw.ident.fancy_sub @@ -2147,13 +2315,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_log2_up => [] | @Z_eqb => [] | @Z_leb => [] + | @Z_ltb => [] | @Z_geb => [] + | @Z_gtb => [] | @Z_of_nat => [] | @Z_to_nat => [] | @Z_shiftr => [] | @Z_shiftl => [] | @Z_land => [] | @Z_lor => [] + | @Z_min => [] + | @Z_max => [] | @Z_bneg => [] | @Z_lnot_modulo => [] | @Z_mul_split => [] @@ -2168,6 +2340,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_cc_m => [] | @Z_cast => [zrange : Type] | @Z_cast2 => [zrange * zrange : Type] + | @option_Some A => [] + | @option_None A => [] + | @option_rect A P => [] + | @Build_zrange => [] + | @zrange_rect P => [] | @fancy_add => [Z : Type; Z : Type] | @fancy_addc => [Z : Type; Z : Type] | @fancy_sub => [Z : Type; Z : Type] @@ -2229,13 +2406,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_log2_up => fun _ => @Compilers.ident.Z_log2_up | @Z_eqb => fun _ => @Compilers.ident.Z_eqb | @Z_leb => fun _ => @Compilers.ident.Z_leb + | @Z_ltb => fun _ => @Compilers.ident.Z_ltb | @Z_geb => fun _ => @Compilers.ident.Z_geb + | @Z_gtb => fun _ => @Compilers.ident.Z_gtb | @Z_of_nat => fun _ => @Compilers.ident.Z_of_nat | @Z_to_nat => fun _ => @Compilers.ident.Z_to_nat | @Z_shiftr => fun _ => @Compilers.ident.Z_shiftr | @Z_shiftl => fun _ => @Compilers.ident.Z_shiftl | @Z_land => fun _ => @Compilers.ident.Z_land | @Z_lor => fun _ => @Compilers.ident.Z_lor + | @Z_min => fun _ => @Compilers.ident.Z_min + | @Z_max => fun _ => @Compilers.ident.Z_max | @Z_bneg => fun _ => @Compilers.ident.Z_bneg | @Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo | @Z_mul_split => fun _ => @Compilers.ident.Z_mul_split @@ -2250,6 +2431,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_cc_m => fun _ => @Compilers.ident.Z_cc_m | @Z_cast => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast range | @Z_cast2 => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast2 range + | @option_Some A => fun _ => @Compilers.ident.option_Some _ + | @option_None A => fun _ => @Compilers.ident.option_None _ + | @option_rect A P => fun _ => @Compilers.ident.option_rect _ _ + | @Build_zrange => fun _ => @Compilers.ident.Build_zrange + | @zrange_rect P => fun _ => @Compilers.ident.zrange_rect _ | @fancy_add => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_add log2wordmax imm | @fancy_addc => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_addc log2wordmax imm | @fancy_sub => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_sub log2wordmax imm @@ -2265,89 +2451,99 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @fancy_addm => fun _ => @Compilers.ident.fancy_addm end. - Definition unify {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') : option (type_of_list (@arg_types t pidc)) - := match pidc, idc return option (type_of_list (arg_types pidc)) with - | @Literal Compilers.base.type.unit, Compilers.ident.Literal Compilers.base.type.unit v => Some (v, tt) - | @Literal Compilers.base.type.Z, Compilers.ident.Literal Compilers.base.type.Z v => Some (v, tt) - | @Literal Compilers.base.type.bool, Compilers.ident.Literal Compilers.base.type.bool v => Some (v, tt) - | @Literal Compilers.base.type.nat, Compilers.ident.Literal Compilers.base.type.nat v => Some (v, tt) - | @Nat_succ, Compilers.ident.Nat_succ => Some tt - | @Nat_pred, Compilers.ident.Nat_pred => Some tt - | @Nat_max, Compilers.ident.Nat_max => Some tt - | @Nat_mul, Compilers.ident.Nat_mul => Some tt - | @Nat_add, Compilers.ident.Nat_add => Some tt - | @Nat_sub, Compilers.ident.Nat_sub => Some tt - | @Nat_eqb, Compilers.ident.Nat_eqb => Some tt - | @nil t, Compilers.ident.nil t' => Some tt - | @cons t, Compilers.ident.cons t' => Some tt - | @pair A B, Compilers.ident.pair A' B' => Some tt - | @fst A B, Compilers.ident.fst A' B' => Some tt - | @snd A B, Compilers.ident.snd A' B' => Some tt - | @prod_rect A B T, Compilers.ident.prod_rect A' B' T' => Some tt - | @bool_rect T, Compilers.ident.bool_rect T' => Some tt - | @nat_rect P, Compilers.ident.nat_rect P' => Some tt - | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Some tt - | @list_rect A P, Compilers.ident.list_rect A' P' => Some tt - | @list_case A P, Compilers.ident.list_case A' P' => Some tt - | @List_length T, Compilers.ident.List_length T' => Some tt - | @List_seq, Compilers.ident.List_seq => Some tt - | @List_firstn A, Compilers.ident.List_firstn A' => Some tt - | @List_skipn A, Compilers.ident.List_skipn A' => Some tt - | @List_repeat A, Compilers.ident.List_repeat A' => Some tt - | @List_combine A B, Compilers.ident.List_combine A' B' => Some tt - | @List_map A B, Compilers.ident.List_map A' B' => Some tt - | @List_app A, Compilers.ident.List_app A' => Some tt - | @List_rev A, Compilers.ident.List_rev A' => Some tt - | @List_flat_map A B, Compilers.ident.List_flat_map A' B' => Some tt - | @List_partition A, Compilers.ident.List_partition A' => Some tt - | @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Some tt - | @List_update_nth T, Compilers.ident.List_update_nth T' => Some tt - | @List_nth_default T, Compilers.ident.List_nth_default T' => Some tt - | @Z_add, Compilers.ident.Z_add => Some tt - | @Z_mul, Compilers.ident.Z_mul => Some tt - | @Z_pow, Compilers.ident.Z_pow => Some tt - | @Z_sub, Compilers.ident.Z_sub => Some tt - | @Z_opp, Compilers.ident.Z_opp => Some tt - | @Z_div, Compilers.ident.Z_div => Some tt - | @Z_modulo, Compilers.ident.Z_modulo => Some tt - | @Z_log2, Compilers.ident.Z_log2 => Some tt - | @Z_log2_up, Compilers.ident.Z_log2_up => Some tt - | @Z_eqb, Compilers.ident.Z_eqb => Some tt - | @Z_leb, Compilers.ident.Z_leb => Some tt - | @Z_geb, Compilers.ident.Z_geb => Some tt - | @Z_of_nat, Compilers.ident.Z_of_nat => Some tt - | @Z_to_nat, Compilers.ident.Z_to_nat => Some tt - | @Z_shiftr, Compilers.ident.Z_shiftr => Some tt - | @Z_shiftl, Compilers.ident.Z_shiftl => Some tt - | @Z_land, Compilers.ident.Z_land => Some tt - | @Z_lor, Compilers.ident.Z_lor => Some tt - | @Z_bneg, Compilers.ident.Z_bneg => Some tt - | @Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Some tt - | @Z_mul_split, Compilers.ident.Z_mul_split => Some tt - | @Z_add_get_carry, Compilers.ident.Z_add_get_carry => Some tt - | @Z_add_with_carry, Compilers.ident.Z_add_with_carry => Some tt - | @Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Some tt - | @Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Some tt - | @Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Some tt - | @Z_zselect, Compilers.ident.Z_zselect => Some tt - | @Z_add_modulo, Compilers.ident.Z_add_modulo => Some tt - | @Z_rshi, Compilers.ident.Z_rshi => Some tt - | @Z_cc_m, Compilers.ident.Z_cc_m => Some tt - | @Z_cast, Compilers.ident.Z_cast range' => Some (range', tt) - | @Z_cast2, Compilers.ident.Z_cast2 range' => Some (range', tt) - | @fancy_add, Compilers.ident.fancy_add log2wordmax' imm' => Some (log2wordmax', (imm', tt)) - | @fancy_addc, Compilers.ident.fancy_addc log2wordmax' imm' => Some (log2wordmax', (imm', tt)) - | @fancy_sub, Compilers.ident.fancy_sub log2wordmax' imm' => Some (log2wordmax', (imm', tt)) - | @fancy_subb, Compilers.ident.fancy_subb log2wordmax' imm' => Some (log2wordmax', (imm', tt)) - | @fancy_mulll, Compilers.ident.fancy_mulll log2wordmax' => Some (log2wordmax', tt) - | @fancy_mullh, Compilers.ident.fancy_mullh log2wordmax' => Some (log2wordmax', tt) - | @fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax' => Some (log2wordmax', tt) - | @fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax' => Some (log2wordmax', tt) - | @fancy_rshi, Compilers.ident.fancy_rshi log2wordmax' x' => Some (log2wordmax', (x', tt)) - | @fancy_selc, Compilers.ident.fancy_selc => Some tt - | @fancy_selm, Compilers.ident.fancy_selm log2wordmax' => Some (log2wordmax', tt) - | @fancy_sell, Compilers.ident.fancy_sell => Some tt - | @fancy_addm, Compilers.ident.fancy_addm => Some tt + Definition unify {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc)) + := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with + | @Literal Compilers.base.type.unit, Compilers.ident.Literal Compilers.base.type.unit v => Datatypes.Some (v, tt) + | @Literal Compilers.base.type.Z, Compilers.ident.Literal Compilers.base.type.Z v => Datatypes.Some (v, tt) + | @Literal Compilers.base.type.bool, Compilers.ident.Literal Compilers.base.type.bool v => Datatypes.Some (v, tt) + | @Literal Compilers.base.type.nat, Compilers.ident.Literal Compilers.base.type.nat v => Datatypes.Some (v, tt) + | @Literal Compilers.base.type.zrange, Compilers.ident.Literal Compilers.base.type.zrange v => Datatypes.Some (v, tt) + | @Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt + | @Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt + | @Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt + | @Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt + | @Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt + | @Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt + | @Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt + | @nil t, Compilers.ident.nil t' => Datatypes.Some tt + | @cons t, Compilers.ident.cons t' => Datatypes.Some tt + | @pair A B, Compilers.ident.pair A' B' => Datatypes.Some tt + | @fst A B, Compilers.ident.fst A' B' => Datatypes.Some tt + | @snd A B, Compilers.ident.snd A' B' => Datatypes.Some tt + | @prod_rect A B T, Compilers.ident.prod_rect A' B' T' => Datatypes.Some tt + | @bool_rect T, Compilers.ident.bool_rect T' => Datatypes.Some tt + | @nat_rect P, Compilers.ident.nat_rect P' => Datatypes.Some tt + | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Datatypes.Some tt + | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt + | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt + | @List_length T, Compilers.ident.List_length T' => Datatypes.Some tt + | @List_seq, Compilers.ident.List_seq => Datatypes.Some tt + | @List_firstn A, Compilers.ident.List_firstn A' => Datatypes.Some tt + | @List_skipn A, Compilers.ident.List_skipn A' => Datatypes.Some tt + | @List_repeat A, Compilers.ident.List_repeat A' => Datatypes.Some tt + | @List_combine A B, Compilers.ident.List_combine A' B' => Datatypes.Some tt + | @List_map A B, Compilers.ident.List_map A' B' => Datatypes.Some tt + | @List_app A, Compilers.ident.List_app A' => Datatypes.Some tt + | @List_rev A, Compilers.ident.List_rev A' => Datatypes.Some tt + | @List_flat_map A B, Compilers.ident.List_flat_map A' B' => Datatypes.Some tt + | @List_partition A, Compilers.ident.List_partition A' => Datatypes.Some tt + | @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Datatypes.Some tt + | @List_update_nth T, Compilers.ident.List_update_nth T' => Datatypes.Some tt + | @List_nth_default T, Compilers.ident.List_nth_default T' => Datatypes.Some tt + | @Z_add, Compilers.ident.Z_add => Datatypes.Some tt + | @Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt + | @Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt + | @Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt + | @Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt + | @Z_div, Compilers.ident.Z_div => Datatypes.Some tt + | @Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt + | @Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt + | @Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt + | @Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt + | @Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt + | @Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt + | @Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt + | @Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt + | @Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt + | @Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt + | @Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt + | @Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt + | @Z_land, Compilers.ident.Z_land => Datatypes.Some tt + | @Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt + | @Z_min, Compilers.ident.Z_min => Datatypes.Some tt + | @Z_max, Compilers.ident.Z_max => Datatypes.Some tt + | @Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt + | @Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt + | @Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt + | @Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt + | @Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt + | @Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt + | @Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt + | @Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt + | @Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt + | @Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt + | @Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt + | @Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt + | @Z_cast, Compilers.ident.Z_cast range' => Datatypes.Some (range', tt) + | @Z_cast2, Compilers.ident.Z_cast2 range' => Datatypes.Some (range', tt) + | @option_Some A, Compilers.ident.option_Some A' => Datatypes.Some tt + | @option_None A, Compilers.ident.option_None A' => Datatypes.Some tt + | @option_rect A P, Compilers.ident.option_rect A' P' => Datatypes.Some tt + | @Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt + | @zrange_rect P, Compilers.ident.zrange_rect P' => Datatypes.Some tt + | @fancy_add, Compilers.ident.fancy_add log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt)) + | @fancy_addc, Compilers.ident.fancy_addc log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt)) + | @fancy_sub, Compilers.ident.fancy_sub log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt)) + | @fancy_subb, Compilers.ident.fancy_subb log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt)) + | @fancy_mulll, Compilers.ident.fancy_mulll log2wordmax' => Datatypes.Some (log2wordmax', tt) + | @fancy_mullh, Compilers.ident.fancy_mullh log2wordmax' => Datatypes.Some (log2wordmax', tt) + | @fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax' => Datatypes.Some (log2wordmax', tt) + | @fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax' => Datatypes.Some (log2wordmax', tt) + | @fancy_rshi, Compilers.ident.fancy_rshi log2wordmax' x' => Datatypes.Some (log2wordmax', (x', tt)) + | @fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt + | @fancy_selm, Compilers.ident.fancy_selm log2wordmax' => Datatypes.Some (log2wordmax', tt) + | @fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt + | @fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt | @Literal _, _ | @Nat_succ, _ | @Nat_pred, _ @@ -2392,13 +2588,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_log2_up, _ | @Z_eqb, _ | @Z_leb, _ + | @Z_ltb, _ | @Z_geb, _ + | @Z_gtb, _ | @Z_of_nat, _ | @Z_to_nat, _ | @Z_shiftr, _ | @Z_shiftl, _ | @Z_land, _ | @Z_lor, _ + | @Z_min, _ + | @Z_max, _ | @Z_bneg, _ | @Z_lnot_modulo, _ | @Z_mul_split, _ @@ -2413,6 +2613,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @Z_cc_m, _ | @Z_cast, _ | @Z_cast2, _ + | @option_Some _, _ + | @option_None _, _ + | @option_rect _ _, _ + | @Build_zrange, _ + | @zrange_rect _, _ | @fancy_add, _ | @fancy_addc, _ | @fancy_sub, _ @@ -2426,7 +2631,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @fancy_selm, _ | @fancy_sell, _ | @fancy_addm, _ - => None + => Datatypes.None end%cps. Definition of_typed_ident {t} (idc : Compilers.ident.ident t) : ident (type.relax t) @@ -2475,13 +2680,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.Z_log2_up => @Z_log2_up | Compilers.ident.Z_eqb => @Z_eqb | Compilers.ident.Z_leb => @Z_leb + | Compilers.ident.Z_ltb => @Z_ltb | Compilers.ident.Z_geb => @Z_geb + | Compilers.ident.Z_gtb => @Z_gtb | Compilers.ident.Z_of_nat => @Z_of_nat | Compilers.ident.Z_to_nat => @Z_to_nat | Compilers.ident.Z_shiftr => @Z_shiftr | Compilers.ident.Z_shiftl => @Z_shiftl | Compilers.ident.Z_land => @Z_land | Compilers.ident.Z_lor => @Z_lor + | Compilers.ident.Z_min => @Z_min + | Compilers.ident.Z_max => @Z_max | Compilers.ident.Z_bneg => @Z_bneg | Compilers.ident.Z_lnot_modulo => @Z_lnot_modulo | Compilers.ident.Z_mul_split => @Z_mul_split @@ -2496,6 +2705,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | Compilers.ident.Z_cc_m => @Z_cc_m | Compilers.ident.Z_cast range => @Z_cast | Compilers.ident.Z_cast2 range => @Z_cast2 + | Compilers.ident.option_Some A => @option_Some (base.relax A) + | Compilers.ident.option_None A => @option_None (base.relax A) + | Compilers.ident.option_rect A P => @option_rect (base.relax A) (base.relax P) + | Compilers.ident.Build_zrange => @Build_zrange + | Compilers.ident.zrange_rect P => @zrange_rect (base.relax P) | Compilers.ident.fancy_add log2wordmax imm => @fancy_add | Compilers.ident.fancy_addc log2wordmax imm => @fancy_addc | Compilers.ident.fancy_sub log2wordmax imm => @fancy_sub -- cgit v1.2.3