From 3e57bde4e0ff1b9f65976f2de4d48a78131d4db3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 25 Apr 2016 13:31:45 +0200
Subject: Optimization in building a return clause by pattern-matching: do not
 build a default case if the pattern is irrefutable. It did not matter in
 practice because we did not check for unused clauses in this case.

---
 pretyping/cases.ml | 35 ++++++++++++++++++++---------------
 1 file changed, 20 insertions(+), 15 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3d6fa38d0d..0923dfeef2 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1759,12 +1759,12 @@ let build_inversion_problem loc env sigma tms t =
       Pushed (true,((tm,tmtyp),deps,na)))
       dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
-  (* [eqn1] is the first clause of the auxiliary pattern-matching that
+  (* [main_eqn] is the main clause of the auxiliary pattern-matching that
      serves as skeleton for the return type: [patl] is the
      substructure of constructors extracted from the list of
      constraints on the inductive types of the multiple terms matched
      in the original pattern-matching problem Xi *)
-  let eqn1 =
+  let main_eqn =
     { patterns = patl;
       alias_stack = [];
       eqn_loc = Loc.ghost;
@@ -1775,19 +1775,24 @@ let build_inversion_problem loc env sigma tms t =
               rhs_vars = List.map fst subst;
               avoid_ids = avoid;
 	      it = Some (lift n t) } } in
-  (* [eqn2] is the default clause of the auxiliary pattern-matching: it will
-     catch the clauses of the original pattern-matching problem Xi whose
-     type constraints are incompatible with the constraints on the
+  (* [catch_all] is a catch-all default clause of the auxiliary
+     pattern-matching, if needed: it will catch the clauses
+     of the original pattern-matching problem Xi whose type
+     constraints are incompatible with the constraints on the
      inductive types of the multiple terms matched in Xi *)
-  let eqn2 =
-    { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
-      alias_stack = [];
-      eqn_loc = Loc.ghost;
-      used = ref false;
-      rhs = { rhs_env = pb_env;
-              rhs_vars = [];
-	      avoid_ids = avoid0;
-	      it = None } } in
+  let catch_all_eqn =
+    if List.for_all (irrefutable env) patl then
+      (* No need for a catch all clause *)
+      []
+    else
+      [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+          alias_stack = [];
+          eqn_loc = Loc.ghost;
+          used = ref false;
+          rhs = { rhs_env = pb_env;
+                  rhs_vars = [];
+	          avoid_ids = avoid0;
+	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
       return type of the original problem Xi *)
   (* let sigma, s = Evd.new_sort_variable sigma in *)
@@ -1804,7 +1809,7 @@ let build_inversion_problem loc env sigma tms t =
       pred      = (*ty *) mkSort s;
       tomatch   = sub_tms;
       history   = start_history n;
-      mat       = [eqn1;eqn2];
+      mat       = main_eqn :: catch_all_eqn;
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon loc env pb_env s subst} in
-- 
cgit v1.2.3


From 016f2dc3aee608b149097cc08d0720227addc18a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 29 Apr 2016 11:13:54 +0200
Subject: Fix incorrect cbv reduction of primitive projections. (Bug #4634)

As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.

The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8d..afd86420e9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
         when red_set (info_flags info) fIOTA && Projection.unfolded p ->
       let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
-	cbv_stack_value info env (arg, stk)
+	cbv_stack_value info env (strip_appl arg stk)
 
     (* may be reduced later by application *)
     | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
-- 
cgit v1.2.3