diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-18 23:45:42 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-18 23:45:42 -0400 |
| commit | 34683d1f31c13863464b4e508c7e8bd64254fd50 (patch) | |
| tree | 34371ed911481e89124fa5155025619f8f7a54c8 /src/Arithmetic | |
| parent | 85051f702e4a525f617c467688c1ad397b0a5399 (diff) | |
Unfold more things in basesystem_partial_evaluation_unfolder
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 62 |
1 files changed, 47 insertions, 15 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 2c6ac52db..f813c2ac0 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -999,21 +999,52 @@ Create HintDb basesystem_partial_evaluation_unfolder. Hint Unfold id - Positional.to_associational_cps Positional.to_associational - Positional.eval Positional.zeros Positional.add_to_nth_cps - Positional.add_to_nth Positional.place_cps Positional.place - Positional.from_associational_cps Positional.from_associational - Positional.carry_cps Positional.carry - Positional.chained_carries_cps Positional.chained_carries - Positional.sub_cps Positional.sub Positional.split_cps - Positional.scmul_cps Positional.unbalanced_sub_cps - Positional.negate_snd_cps Positional.add_cps Positional.opp_cps - Associational.eval Associational.multerm Associational.mul_cps - Associational.mul Associational.split_cps Associational.split - Associational.reduce_cps Associational.reduce - Associational.carryterm_cps Associational.carryterm - Associational.carry_cps Associational.carry - Associational.negate_snd_cps Associational.negate_snd div modulo + Associational.eval + Associational.multerm + Associational.mul_cps + Associational.mul + Associational.split_cps + Associational.split + Associational.reduce_cps + Associational.reduce + Associational.negate_snd_cps + Associational.negate_snd + Associational.carryterm_cps + Associational.carryterm + Associational.carry_cps + Associational.carry + Positional.to_associational_cps + Positional.to_associational + Positional.eval + Positional.zeros + Positional.add_to_nth_cps + Positional.add_to_nth + Positional.place_cps + Positional.place + Positional.from_associational_cps + Positional.from_associational + Positional.carry_cps + Positional.carry + Positional.chained_carries_cps + Positional.chained_carries + Positional.encode + Positional.add_cps + Positional.mul_cps + Positional.reduce_cps + Positional.carry_reduce_cps + Positional.negate_snd_cps + Positional.split_cps + Positional.scmul_cps + Positional.unbalanced_sub_cps + Positional.sub_cps + Positional.sub + Positional.opp_cps + Positional.Fencode + Positional.Fdecode + Positional.eval_from + Positional.select_cps + Positional.select + modulo div id_tuple_with_alt id_tuple'_with_alt Z.add_get_carry_full : basesystem_partial_evaluation_unfolder. @@ -1026,6 +1057,7 @@ Hint Unfold Z.add_get_carry_full Z.mul_split : basesystem_partial_evaluation_unfolder. + Ltac basesystem_partial_evaluation_unfolder t := eval cbv |