Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous and current version work).

Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 113 insertions, 99 deletions

diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4b4a25e718..e0d779ca38 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -429,21 +429,22 @@ module Coercion = struct
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
-    if n = 0 then
-      let (evd', val', type') = 
-	try 
-	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
-	  let sigma = evars_of isevars in
-	    try
-	      coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
-	    with NoSubtacCoercion ->
-	      error_actual_type_loc loc env sigma cj t
-      in
-      let val' = match val' with Some v -> v | None -> assert(false) in
-	(evd',{ uj_val = val'; uj_type = t })
-    else
-      (isevars, cj)
+    match n with
+	None ->
+	  let (evd', val', type') = 
+	    try 
+	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoCoercion ->
+	      let sigma = evars_of isevars in
+		try
+		  coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+		with NoSubtacCoercion ->
+		  error_actual_type_loc loc env sigma cj t
+	  in
+	  let val' = match val' with Some v -> v | None -> assert(false) in
+	    (evd',{ uj_val = val'; uj_type = t })
+      | Some (init, cur) ->
+	  (isevars, cj)
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
     (try 
@@ -453,20 +454,25 @@ module Coercion = struct
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
+    let nabsinit, nabs = 
+      match abs with
+	  None -> 0, 0
+	| Some (init, cur) -> init, cur
+    in
     let (rels, rng) = 
       (* a little more effort to get products is needed *) 
-      try decompose_prod_n abs t
+      try decompose_prod_n nabs t
       with _ -> 
 	trace (str "decompose_prod_n failed");
 	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
     in
       (* The final range free variables must have been replaced by evars, we accept only that evars
 	 in rng are applied to free vars. *)
-      if noccur_with_meta 0 (succ abs) rng then (
-	trace (str "No occur between 0 and " ++ int (succ abs));
+      if noccur_with_meta 0 (succ (nabsinit - nabs)) rng then (
+	trace (str "No occur between 0 and " ++ int (succ (nabsinit - nabs)));
 	let env', t, t' = 
 	  let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
-	    env', rng, lift abs t'
+	    env', rng, lift nabs t'
 	in
 	  try 
 	    pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 94f2d70ac4..1b92c69110 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,6 +56,7 @@ let interp_gen kind isevars env
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
   let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
     
@@ -69,9 +70,10 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c 
 
 let interp_open_constr isevars env c =
-  let c = SPretyping.pretype_gen isevars env ([], []) (OfType None) 
-	    (Constrintern.intern_constr (Evd.evars_of !isevars) env c) in
-    evar_nf isevars c
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
+  let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+  let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
+    evar_nf isevars c'
 
 let interp_constr_judgment isevars env c =
   let j = 
@@ -204,22 +206,22 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 			       Ppconstr.pr_constr_expr body)
 		in
 		let env', binders_rel = interp_context isevars env0 bl in
-		let before, ((argname, _, argtyp) as arg), after = list_chop_hd n binders_rel in
+		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
 		let argid = match argname with Name n -> n | _ -> assert(false) in
 		let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
 		let envwf = push_rel_context before env0 in
 		let wf_rel = interp_constr isevars envwf r in
 		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
-		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| wf_rel; mkRel 1 |])) in
+		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
 		let argid' = id_of_string (string_of_id argid ^ "'") in
 		let before_length, after_length = List.length before, List.length after in
 		let full_length = before_length + 1 + after_length in
-		let wfarg = (Name argid, None, 
-			     mkSubset (Name argid') argtyp 
-			       (mkApp (wf_rel, [|mkRel 1; mkRel (full_length + 1)|])))
+		let wfarg len = (Name argid, None, 
+				 mkSubset (Name argid') argtyp 
+				   (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
 		in
-		let new_bl = before @ (arg :: accarg :: after')
-		and intern_bl =  before @ (wfarg :: after)
+		let new_bl = after' @ (accarg :: arg :: before)
+		and intern_bl =  after @ (wfarg (before_length + 1) :: before)
 		in
 		let intern_env = push_rel_context intern_bl env0 in
 		let env' = push_rel_context new_bl env0 in
@@ -227,7 +229,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
 		let arity' = interp_type isevars env' arityc in
 		let arity' = it_mkProd_or_LetIn arity' new_bl in
-		let fun_bl = before @ (arg :: (Name recname, None, arity) :: after') in
+		let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
+		let _ = 
+		  let pr c = my_print_constr env c in
+		  let prr = Printer.pr_rel_context env in
+		    trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+			     str "Intern bl" ++ prr intern_bl ++ spc () ++
+			     str "Extern bl" ++ prr new_bl ++ spc () ++
+			     str "Intern arity: " ++ pr intern_arity)
+		in
 		let impl = 
 		  if Impargs.is_implicit_args()
 		  then Impargs.compute_implicits intern_env arity'
@@ -256,11 +266,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		   let def = abstract_constr_expr def bl in
 		     isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
 		       def arity
-	       | Some (n, artyp, wfrel, bl, intern_bl, intern_arity) ->
-		   let rec_sign = push_rel_context bl rec_sign in
+	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
+		   let rec_sign = push_rel_context fun_bl rec_sign in
 		   let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
 				def intern_arity
-		   in isevars, info, cstr)
+		   in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -328,19 +338,13 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       let evm = Evd.evars_of isevars in
       let _, _, typ = arrec.(i) in
       let id = namerec.(i) in
-      let def = 
-	match info with 
-	    Some (n, artyp, wfrel, funbl, bl, arity) ->
-	      def (* mkApp (def, *)
-
-	  | None -> def
-		     in
-	(* Generalize by the recursive prototypes  *)
+      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
+      (* Generalize by the recursive prototypes  *)
       let def = 
 	Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
       and typ = 
-	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
-      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 
+	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
+      in
       (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
       (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
       (*let ce = 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d620c8e9fa..6c165dada1 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -74,6 +74,7 @@ let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
 open Pp
 
 let my_print_constr = Termops.print_constr_env
+let my_print_constr_expr = Ppconstr.pr_constr_expr
 let my_print_context = Termops.print_rel_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a53016484b..92a995c891 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -47,6 +47,7 @@ val acc_inv : constr lazy_t
 val extconstr : constr -> constr_expr
 val extsort : sorts -> constr_expr
 val my_print_constr : env -> constr -> std_ppcmds
+val my_print_constr_expr : constr_expr -> std_ppcmds
 val my_print_evardefs : evar_defs -> std_ppcmds
 val my_print_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ec1246b745..4ad85af9a8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -352,7 +352,7 @@ let find_tomatch_tycon isevars env loc = function
   | Some (_,ind,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
-      Some (0, inductive_template isevars env loc ind)
+      mk_tycon (inductive_template isevars env loc ind)
   | None, None -> 
       empty_tycon
 
@@ -412,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.isevars (make_judge current typ) (0, indt)).uj_val in
+		  pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
 	    let sigma = Evd.evars_of !(pb.isevars) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
@@ -1663,7 +1663,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
-       | Some (0, t) ->
+       | Some (None, t) ->
 	   let names,pred = 
 	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
 	   in Some (build_initial_predicate false names pred)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 841e6b0347..b1b02ffd01 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -160,13 +160,6 @@ module Default = struct
       with Reduction.NotConvertible -> raise NoCoercion
   open Pp
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
-(*     (try *)
-(*        msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
-(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
-(* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
-(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
-(* 	      Termops.print_env env); *)
-(*      with _ -> ()); *)
     try (the_conv_x_leq env t c1 isevars, v, t)
     with Reduction.NotConvertible ->
       (try 
@@ -225,18 +218,20 @@ module Default = struct
 	
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj (n, t) =
-    if n = 0 then
-      let (evd', val', type') = 
-	try 
-	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
-	  let sigma = evars_of isevars in
-	    error_actual_type_loc loc env sigma cj t
-      in
-      let val' = match val' with Some v -> v | None -> assert(false) in
-	(evd',{ uj_val = val'; uj_type = t })
-    else
-      (isevars, cj)
+    match n with
+	None ->
+	  let (evd', val', type') = 
+	    try 
+	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoCoercion ->
+	      let sigma = evars_of isevars in
+		error_actual_type_loc loc env sigma cj t
+	  in
+	  let val' = match val' with Some v -> v | None -> assert(false) in
+	    (evd',{ uj_val = val'; uj_type = t })
+      | Some (init, cur) -> (isevars, cj)
+      
+      
 
   open Pp
   let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e9f605ecb5..79e25a5afc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -556,7 +556,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 
 (* Operations on value/type constraints *)
 
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
 
 type val_constraint = constr option
@@ -578,8 +578,9 @@ type val_constraint = constr option
 (* The empty type constraint *)
 let empty_tycon = None
 
-let mk_tycon_type c = (0, c)
-let mk_abstr_tycon_type n c = (n, c)
+let mk_tycon_type c = (None, c)
+let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
+						  is current abstraction *)
 
 (* Builds a type constraint *)
 let mk_tycon ty = Some (mk_tycon_type ty)
@@ -651,28 +652,35 @@ let split_tycon loc env isevars tycon =
     match tycon with
       | None -> isevars,(Anonymous,None,None)
       | Some (abs, c) ->
-	  if abs = 0 then real_split c
-	  else if abs = 1 then 
-		isevars, (Anonymous, None, mk_tycon c)
-	      else
-		isevars, (Anonymous, None, Some (pred abs, c))
+	  (match abs with
+	       None -> real_split c
+	     | Some (init, cur) ->
+	       if cur = 1 then isevars, (Anonymous, None, 
+					 Some (Some (init, 0), c))
+	       else
+		 isevars, (Anonymous, None, Some (Some (init, pred cur), c)))
 
 let valcon_of_tycon x = 
   match x with
-    | Some (0, t) -> Some t
+    | Some (None, t) -> Some t
     | _ -> None
 	
-let lift_tycon_type n (abs, c) = 
-  let abs' = abs + n in 
-    if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
-    else (abs', c)
+let lift_tycon_type n (abs, t) =
+  abs, lift n t
+(*  match abs with 
+      None -> (abs, lift n t)
+    | Some (init, abs) ->
+	let abs' = abs + n in 
+	  if abs' < 0 then raise (Invalid_argument "lift_tycon_type")
+	  else (Some (init, abs'), lift n t)*)
 
 let lift_tycon n = option_app (lift_tycon_type n)
 
 let pr_tycon_type env (abs, t) =
-  if abs = 0 then Termops.print_constr_env env t
-  else str "Abstract " ++ int abs ++ str " " ++ Termops.print_constr_env env t
-
+  match abs with 
+      None -> Termops.print_constr_env env t
+    | Some (init, cur) -> str "Abstract (" ++ int init ++ str ","  ++ int cur ++ str ") " ++ Termops.print_constr_env env t
+	
 let pr_tycon env = function
     None -> str "None"
   | Some t -> pr_tycon_type env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7260b5ad35..8c5fe9c99b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -87,7 +87,7 @@ val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
 
 val judge_of_new_Type : unit -> unsafe_judgment
 
-type type_constraint_type = int * constr
+type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
 
 type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 217a9714be..b3590492ab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -259,14 +259,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [(evars_of isevars)] and *)
   (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env isevars lvar c =
-(*    (try 
-       msgnl (str "pretype with tycon: " ++
-	      Evarutil.pr_tycon env tycon ++ str " with evars: " ++ spc () ++
-	      Evd.pr_evar_defs !isevars ++ str " in env: " ++ spc () ++
-	      Termops.print_env env);
-     with _ -> ());*)
-    match c with
+  let rec pretype (tycon : type_constraint) env isevars lvar = function
     | RRef (loc,ref) ->
 	inh_conv_coerce_to_tycon loc env isevars
 	  (pretype_ref isevars env ref)
@@ -294,7 +287,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RHole (loc,k) ->
 	let ty =
           match tycon with 
-            | Some (n, ty) when n = 0 -> ty
+            | Some (None, ty) -> ty
             | None | Some _ ->
 		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
 	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
@@ -357,9 +350,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let ftycon = 
 	  match tycon with
 	      None -> None
-	    | Some (n, ty) ->
-		if n = 0 then mk_abstr_tycon length ty
-		else Some (n + length, ty)
+	    | Some (None, ty) -> mk_abstr_tycon length ty
+	    | Some (Some (init, cur), ty) ->
+		Some (Some (length + init, cur), ty)
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
@@ -375,11 +368,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
 		      let tycon = 
-			match tycon with
+			match tycon with			    
 			    Some (abs, ty) ->
-			      isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-			      (abs, ty);			      
-			      Some (pred abs, nf_isevar !isevars ty)
+			      (match abs with
+				   None ->
+				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				       (abs, ty);
+				     Some (None, nf_isevar !isevars ty)
+				 | Some (init, cur) ->
+				     isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
+				       (abs, ty);
+				     Some (Some (init, pred cur), nf_isevar !isevars ty))
 			  | None -> None
 		      in 
 			apply_rec env (n+1) 
@@ -532,7 +531,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  jtyp.uj_val, jtyp.uj_type
 	    | None -> 
 		let p = match tycon with
-		  | Some (n, ty) when n = 0 -> ty
+		  | Some (None, ty) -> ty
 		  | None | Some _ ->
                       e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
 		in