Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q

(refolding of cbn is smarter)

4 files changed, 67 insertions, 45 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0b304b351..964852ee0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -173,6 +173,17 @@ module Cst_stack = struct
     | (cst,params,[])::_ -> Some(cst,params)
     | _ -> None
 
+  (** [best_replace d cst_l c] makes the best replacement for [d]
+      by [cst_l] in [c] *)
+  let best_replace d cst_l c =
+    let reconstruct_head = List.fold_left
+      (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
+    List.fold_right
+      (fun (cst,params,args) t -> Termops.replace_term
+	(reconstruct_head d args)
+	(applist (cst, List.rev params))
+	t) cst_l c
+
   let pr l =
     let open Pp in
     let p_c = Termops.print_constr in
@@ -218,6 +229,7 @@ sig
   val args_size : 'a t -> int
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
+  val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t
   val zip : ?refold:bool -> constr * constr t -> constr
 end =
 struct
@@ -436,6 +448,18 @@ struct
     | Some (_,el,_) -> el
     | None -> raise Not_found
 
+  (** This function breaks the abstraction of Cst_stack ! *)
+  let best_state (_,sk as s) l =
+    let rec aux sk def = function
+      |(cst, params, []) -> (cst, append_app_list (List.rev params) sk)
+      |(cst, params, (i,t)::q) -> match decomp sk with
+	| Some (el,sk') when Constr.equal el t.(i) ->
+	  if i = pred (Array.length t)
+	  then aux sk' def (cst, params, q)
+	  else aux sk' def (cst, params, (succ i,t)::q)
+	| _ -> def
+    in List.fold_left (aux sk) s l
+
   let rec zip ?(refold=false) = function
     | f, [] -> f
     | f, (App (i,a,j) :: s) ->
@@ -443,18 +467,11 @@ struct
 		then a
 		else Array.sub a i (j - i + 1) in
        zip ~refold (mkApp (f, a'), s)
-    | f, (Case (ci,rt,br,cst_sk)::s) when refold ->
-      (match Cst_stack.best_cst cst_sk with
-      | Some (cst, params) -> zip ~refold (cst, append_app_list (List.rev params) s)
-      | None -> zip ~refold (mkCase (ci,rt,f,br), s)
-      )
+    | f, (Case (ci,rt,br,cst_l)::s) when refold ->
+      zip ~refold (best_state (mkCase (ci,rt,f,br), s) cst_l)
     | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
-    | f, (Fix (fix,st,cst_sk)::s) when refold ->
-      (match Cst_stack.best_cst cst_sk with
-      | Some (cst, params) -> zip ~refold (cst, append_app_list (List.rev params)
-	(st @ (append_app [|f|] s)))
-      | None ->  zip ~refold (mkFix fix, st @ (append_app [|f|] s))
-      )
+    | f, (Fix (fix,st,cst_l)::s) when refold ->
+      zip ~refold (best_state (mkFix fix, st @ (append_app [|f|] s)) cst_l)
   | f, (Fix (fix,st,_)::s) -> zip ~refold
     (mkFix fix, st @ (append_app [|f|] s))
   | f, (Shift n::s) -> zip ~refold (lift n f, s)
@@ -545,7 +562,7 @@ let apply_subst recfun env cst_l t stack =
   in aux env cst_l t stack
 
 let stacklam recfun env t stack =
-apply_subst (fun _ -> recfun) env [] t stack
+apply_subst (fun _ -> recfun) env Cst_stack.empty t stack
 
 let beta_applist (c,l) =
   stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
@@ -593,13 +610,11 @@ let magicaly_constant_of_fixbody env bd = function
     with
     | Not_found -> bd
 
-let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst_l =
+let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
   let make_Fi j =
     let ind = nbodies-j-1 in
-    if Int.equal bodynum ind && not (Option.is_empty (Cst_stack.best_cst cst_l)) then
-      let (c,params) = Option.get (Cst_stack.best_cst cst_l) in
-      applist(c, List.rev params)
+    if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
     else
       let bd = mkCoFix (ind,typedbodies) in
       match env with
@@ -608,6 +623,13 @@ let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) cst_l =
   let closure = List.init nbodies make_Fi in
   substl closure bodies.(bodynum)
 
+(** Similar to the "fix" case below *)
+let reduce_and_refold_cofix recfun env cst_l cofix sk =
+  let raw_answer = contract_cofix ~env cofix in
+  apply_subst
+    (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk'))
+    [] Cst_stack.empty raw_answer sk
+
 let reduce_mind_case mia =
   match kind_of_term mia.mconstr with
     | Construct ((ind_sp,i),u) ->
@@ -615,20 +637,18 @@ let reduce_mind_case mia =
 	let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
         applist (mia.mlf.(i-1),real_cargs)
     | CoFix cofix ->
-	let cofix_def = contract_cofix cofix Cst_stack.empty in
+	let cofix_def = contract_cofix cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
 (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
    Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
 
-let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies)) cst_l =
+let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies)) =
     let nbodies = Array.length recindices in
     let make_Fi j =
       let ind = nbodies-j-1 in
-      if Int.equal bodynum ind && not (Option.is_empty (Cst_stack.best_cst cst_l)) then
-	let (c,params) = Option.get (Cst_stack.best_cst cst_l) in
-	applist(c, List.rev params)
+      if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
       else
 	let bd = mkFix ((recindices,ind),typedbodies) in
 	match env with
@@ -637,6 +657,16 @@ let contract_fix ?env ((recindices,bodynum),(names,types,bodies as typedbodies))
     let closure = List.init nbodies make_Fi in
     substl closure bodies.(bodynum)
 
+(** First we substitute the Rel bodynum by the fixpoint and then we try to
+    replace the fixpoint by the best constant from [cst_l]
+    Other rels are directly substituted by constants "magically found from the
+    context" in contract_fix *)
+let reduce_and_refold_fix recfun env cst_l fix sk =
+  let raw_answer = contract_fix ~env fix in
+  apply_subst
+    (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk'))
+    [] Cst_stack.empty raw_answer sk
+
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum && bodynum < Array.length recindices);
   let recargnum = Array.get recindices bodynum in
@@ -663,19 +693,8 @@ type 'a reduced_state =
 *)
 let rec whd_state_gen ?csts tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack as s) =
-    let best_state (_,sk as s) l =
-      let rec aux sk def = function
-	|(cst, params, []) -> (cst, Stack.append_app_list (List.rev params) sk)
-	|(cst, params, (i,t)::q) -> match Stack.decomp sk with
-	  | None -> def
-	  | Some (el,sk') ->
-	    let () = Cst_stack.sanity el t.(i) in
-	    if i = pred (Array.length t)
-	    then aux sk' def (cst, params, q)
-	    else aux sk' def (cst, params, (succ i,t)::q)
-      in List.fold_left (aux sk) s l in
     let fold () =
-      if tactic_mode then (best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+      if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
     in
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
@@ -781,8 +800,10 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	  whrec Cst_stack.empty (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst_l)::s'') ->
 	  let x' = Stack.zip(x,args) in
-	  whrec Cst_stack.empty ((if tactic_mode then contract_fix ~env f else contract_fix f) cst_l,
-		      s' @ (Stack.append_app [|x'|] s''))
+	  let out_sk = s' @ (Stack.append_app [|x'|] s'') in
+	  if tactic_mode
+	  then reduce_and_refold_fix whrec env cst_l f out_sk
+	  else whrec Cst_stack.empty (contract_fix f, out_sk)
 	|_ -> fold ()
       else fold ()
 
@@ -790,9 +811,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
-	  whrec Cst_stack.empty ((if tactic_mode
-	    then contract_cofix ~env cofix
-	    else contract_cofix cofix) cst_l, stack)
+	  if tactic_mode
+	  then reduce_and_refold_cofix whrec env cst_l cofix stack
+	  else whrec Cst_stack.empty (contract_cofix cofix, stack)
 	|_ -> fold ()
       else fold ()
 
@@ -861,8 +882,8 @@ let local_whd_state_gen flags sigma =
 	|args, (Stack.Proj (n,m,p) :: s') ->
 	  whrec (Stack.nth args (n+m), s')
 	|args, (Stack.Fix (f,s',cst)::s'') ->
-          let x' = Stack.zip(x,args) in
-            whrec (contract_fix f cst, s' @ (Stack.append_app [|x'|] s''))
+	  let x' = Stack.zip(x,args) in
+	  whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s''))
 	|_ -> s
       else s
 
@@ -870,7 +891,7 @@ let local_whd_state_gen flags sigma =
       if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') ->
-	  whrec (contract_cofix cofix Cst_stack.empty, stack)
+	  whrec (contract_cofix cofix, stack)
 	|_ -> s
       else s
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ef013d5b1..873973198 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -40,6 +40,7 @@ module Cst_stack : sig
   val add_args : 'a array -> 'a t -> 'a t
   val add_cst : 'a -> 'a t -> 'a t
   val best_cst : 'a t -> ('a * 'a list) option
+  val best_replace : constr -> constr t -> constr -> constr
   val pr : constr t -> Pp.std_ppcmds
 end
 
@@ -89,6 +90,7 @@ module Stack : sig
   val tail : int -> 'a t -> 'a t
   val nth : 'a t -> int -> 'a
 
+  val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t
   val zip : ?refold:bool -> constr * constr t -> constr
 end
 
@@ -229,8 +231,7 @@ val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
 val is_arity : env ->  evar_map -> constr -> bool
 val is_sort : env -> evar_map -> types -> bool
 
-val contract_fix : ?env:Environ.env -> fixpoint ->
-  constr Cst_stack.t -> constr
+val contract_fix : ?env:Environ.env -> fixpoint -> constr
 val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option
 
 (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 18723f645..5693cf298 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -454,7 +454,7 @@ let reduce_fix whdfun sigma fix stack =
         let (recarg'hd,_ as recarg') = whdfun sigma recarg in
         let stack' = List.assign stack recargnum (applist recarg') in
 	(match kind_of_term recarg'hd with
-           | Construct _ -> Reduced (contract_fix fix Reductionops.Cst_stack.empty, stack')
+           | Construct _ -> Reduced (contract_fix fix, stack')
 	   | _ -> NotReducible)
 
 let contract_fix_use_function env sigma f
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 22f3dcd64..fe1ec9398 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -268,7 +268,7 @@ Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison :=
     | 1, 1 => r
   end.
 
-Definition compare x y := compare_cont Eq x y.
+Definition compare := compare_cont Eq.
 
 Infix "?=" := compare (at level 70, no associativity) : positive_scope.