aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-08-28 09:39:30 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-08 12:45:58 +0200
commit108ede6e7aa4383474581bc428ff05b94097c92d (patch)
tree4315c802d37b99196338eadfb2e410d8bf410027
parent0f8d1b92c37c80e96df2a157a78188d6d94b6e35 (diff)
Documenting the code when preference is given to expansion of default
clause in pattern-matching or not.
-rw-r--r--pretyping/cases.ml11
1 files changed, 11 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ef196e0a7..05e09b968 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1466,6 +1466,14 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
compile pb
in
let sigma = !(pb.evdref) in
+ (* If the "match" was orginally over a variable, as in "match x with
+ O => true | n => n end", we give preference to non-expansion in
+ the default clause (i.e. "match x with O => true | n => n end"
+ rather than "match x with O => true | S p => S p end";
+ computationally, this avoids reallocating constructors in cbv
+ evaluation; the drawback is that it might duplicate the instances
+ of the term to match when the corresponding variable is
+ substituted by a non-evaluated expression *)
if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then
(* Try to compile first using non expanded alias *)
try
@@ -1473,6 +1481,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
else just_pop ()
with e when precatchable_exception e ->
(* Try then to compile using expanded alias *)
+ (* Could be needed in case of dependent return clause *)
pb.evdref := sigma;
f expanded expanded_typ
else
@@ -1480,6 +1489,8 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
try f expanded expanded_typ
with e when precatchable_exception e ->
(* Try then to compile using non expanded alias *)
+ (* Could be needed in case of a recursive call which requires to
+ be on a variable for size reasons *)
pb.evdref := sigma;
if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
else just_pop ()