Make evarconv and unification able to handle eta for records in presence

of metas/evars

4 files changed, 83 insertions, 60 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1a699f4af..23358bab5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -319,41 +319,33 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 	   destroy beta-redexes that can be used for 1st-order unification *)
         let term1 = apprec_nohdbeta ts env evd term1 in
         let term2 = apprec_nohdbeta ts env evd term2 in
-	let default () = evar_eqappr_x ts env evd pbty
-          (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
-          (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
-	in
         begin match kind_of_term term1, kind_of_term term2 with
-        | Evar ev, _ when Evd.is_undefined evd (fst ev) ->
-          (match solve_simple_eqn (evar_conv_x ts) env evd
-	    (position_problem true pbty,ev,term2) with
-	    | UnifFailure (_, Pretype_errors.OccurCheck _) -> default ()
-	    | x -> x)
-        | _, Evar ev when Evd.is_undefined evd (fst ev) ->
-          (match solve_simple_eqn (evar_conv_x ts) env evd
-            (position_problem false pbty,ev,term1) with
-	    | UnifFailure (_, Pretype_errors.OccurCheck _) -> default ()
-	    | x -> x)
-        | _ -> default ()
+        | Evar ev, _ when Evd.is_undefined evd (fst ev)
+	&& noccur_evar env evd (fst ev) term2 ->
+          solve_simple_eqn (evar_conv_x ts) env evd
+            (position_problem true pbty,ev,term2)
+        | _, Evar ev when Evd.is_undefined evd (fst ev)
+	&& noccur_evar env evd (fst ev) term1 ->
+          solve_simple_eqn (evar_conv_x ts) env evd
+            (position_problem false pbty,ev,term1)
+        | _ ->
+          evar_eqappr_x ts env evd pbty
+            (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
+            (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
         end
 
 and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
   let default_fail i = (* costly *)
     UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in
-  let miller_pfenning on_left fallback ev lF apprM evd =
-    let tM = Stack.zip apprM in
-    let cont res = 
-      match res with
+  let miller_pfenning on_left fallback ev lF tM evd =
+    match is_unification_pattern_evar env evd ev lF tM with
       | None -> fallback ()
       | Some l1' -> (* Miller-Pfenning's patterns unification *)
 	let t2 = nf_evar evd tM in
 	let t2 = solve_pattern_eqn env l1' t2 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem on_left pbty,ev,t2) 
-    in
-      try cont (is_unification_pattern_evar_occur env evd ev lF tM)
-      with Occur -> UnifFailure (evd,OccurCheck (fst ev,tM))
   in
   let consume_stack on_left (termF,skF) (termO,skO) evd =
     let switch f a b = if on_left then f a b else f b a in
@@ -393,12 +385,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let not_only_app = Stack.not_purely_applicative skM in
     let f1 i =
       match Stack.list_of_app_stack skF with
-	| None -> default_fail evd
-	| Some lF ->  miller_pfenning on_left
-	  (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
-	      switch (fun x y -> Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) i)) apprF apprM
+      | None -> default_fail evd
+      | Some lF -> 
+        let tM = Stack.zip apprM in
+	  miller_pfenning on_left
+	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
+	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
 	    else default_fail i)
-	  ev lF apprM i
+	  ev lF tM i
     and f3 i =
 	switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
 	  (whd_betaiota_deltazeta_for_iota_state ts env i cstsM vM)
@@ -406,22 +400,26 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     ise_try evd [f1; (consume_stack on_left apprF apprM); f3] in
   let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
     let switch f a b = if on_left then f a b else f b a in
-    let f1 evd = 
-      match Stack.list_of_app_stack skF with
-      | None -> consume_stack on_left apprF apprR evd
-      | Some lF ->
-	miller_pfenning on_left
-	  (fun () -> (* Postpone the use of an heuristic *)
-	    switch (fun x y ->
-	      Success (add_conv_pb (pbty,env,Stack.zip x,Stack.zip y) evd)) apprF apprR)
-	  ev lF apprR evd
-    in
-    let f2 evd =
+    let eta evd =
       match kind_of_term termR with
       | Lambda _ -> eta env evd false skR termR skF termF
       | Construct u -> eta_constructor ts env evd skR u skF termF
       | _ -> UnifFailure (evd,NotSameHead)
-    in ise_try evd [f1;f2] in
+    in
+    let f evd =
+      match Stack.list_of_app_stack skF with
+      | None -> consume_stack on_left apprF apprR evd
+      | Some lF ->
+        let tR = Stack.zip apprR in
+	  miller_pfenning on_left
+	    (fun () ->
+	      ise_try evd 
+	        [eta;(* Postpone the use of an heuristic *)
+		 (fun i -> switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+	           (Stack.zip apprF) tR)])
+	    ev lF tR evd
+    in ise_try evd [f; eta]
+  in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 14bc45e0c..6d7765808 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -418,23 +418,16 @@ let is_unification_pattern_meta env nb m l t =
   else
     None
 
-let is_unification_pattern_evar_occur env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l
+let is_unification_pattern_evar env evd (evk,args) l t =
+  if List.for_all (fun x -> isRel x || isVar x) l 
+    && noccur_evar env evd evk t
   then
-    if not (noccur_evar env evd evk t) then raise Occur
-    else
-      let args = remove_instance_local_defs evd evk args in
-      let n = List.length args in
-	match find_unification_pattern_args env (args @ l) t with
-	| Some l -> Some (List.skipn n l)
-	| _ -> None
-  else
-    if noccur_evar env evd evk t then None
-    else raise Occur
-
-let is_unification_pattern_evar env evd ev l t =
-  try is_unification_pattern_evar_occur env evd ev l t
-  with Occur -> None
+    let args = remove_instance_local_defs evd evk args in
+    let n = List.length args in
+      match find_unification_pattern_args env (args @ l) t with
+      | Some l -> Some (List.skipn n l)
+      | _ -> None
+  else None
 
 let is_unification_pattern_pure_evar env evd (evk,args) t =
   let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index a0d0f6fdf..0d0f3c0e5 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -51,10 +51,6 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
 
 val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
 
-(** Raises [Occur] if the evar occurs in the evar-expanded version of the term. *)
-val is_unification_pattern_evar_occur : env -> evar_map -> existential -> constr list ->
-  constr -> constr list option
-
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> constr list option
 
@@ -63,6 +59,8 @@ val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
 
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
+val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
+
 exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f7e2916b..29ed69b2d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -450,6 +450,30 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN =
 	else error_cannot_unify env sigma (m,n)
     else sigma
 
+let is_eta_constructor_app env f l1 =
+  match kind_of_term f with
+  | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+    let mib = lookup_mind (fst ind) env in
+      (match mib.Declarations.mind_record with
+      | Some (exp,projs) when Array.length projs > 0
+        && mib.Declarations.mind_finite -> 
+        Array.length projs == Array.length l1 - mib.Declarations.mind_nparams
+      | _ -> false)
+  | _ -> false
+
+let eta_constructor_app env f l1 term =
+  match kind_of_term f with
+  | Construct (((_, i as ind), j), u) ->
+    let mib = lookup_mind (fst ind) env in
+      (match mib.Declarations.mind_record with
+      | Some (exp,projs) ->
+        let pars = mib.Declarations.mind_nparams in
+	let l1' = Array.sub l1 pars (Array.length l1 - pars) in
+	let l2 = Array.map (fun p -> mkProj (p, term)) projs in
+	  l1', l2
+      | _ -> assert false)
+  | _ -> assert false
+
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_head_evar sigma curm
@@ -548,8 +572,18 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| _, Lambda (na,t2,c2) when flags.modulo_eta ->
 	    unirec_rec (push (na,t2) curenvnb) CONV true wt substn
 	      (mkApp (lift 1 cM,[|mkRel 1|])) c2
-	(* For records, eta-expansion is done through unify_app -> expand -> infer_conv *)
 
+	(* For records *)
+	| App (f, l1), _ when flags.modulo_eta && is_eta_constructor_app env f l1 ->
+	  let l1', l2' = eta_constructor_app env f l1 cN in
+	   Array.fold_left2 
+	     (unirec_rec curenvnb CONV true wt) substn l1' l2'
+
+	| _, App (f, l2) when flags.modulo_eta && is_eta_constructor_app env f l2 ->
+	  let l2', l1' = eta_constructor_app env f l2 cM in
+	   Array.fold_left2 
+	     (unirec_rec curenvnb CONV true wt) substn l1' l2'
+	   
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             (try 
 	       Array.fold_left2 (unirec_rec curenvnb CONV true wt)