Documenting check_record + changing a possibly undefined int into int option.

6 files changed, 64 insertions, 34 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 80cb631653..0b6ead8c6f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -112,20 +112,20 @@ let occur_rigidly ev evd t =
     | Case _ -> false
   in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
 
-(* [check_conv_record env sigma (t1,l1) (t2,l2)] tries to decompose the problem
-   (t1 l1) = (t2 l2) into a problem
+(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
+   the problem (t1 stack1) = (t2 stack2) into a problem
 
-     l1 = params1@c1::extra_args1
-     l2 = us2@extra_args2
-     (t1 params1 c1) = (proji params (c xs))
-     (t2 us2) = (cstr us)
+     stack1 = params1@[c1]@extra_args1
+     stack2 = us2@extra_args2
+     t1 params1 c1 = proji params (c xs)
+     t2 us2 = head us
      extra_args1 = extra_args2
 
    by finding a record R and an object c := [xs:bs](Build_R params v1..vn)
-   with vi = (cstr us), for which we know that the i-th projection proji
+   with vi = (head us), for which we know that the i-th projection proji
    satisfies
 
-      (proji params (c xs)) = (cstr us)
+      proji params (c xs) = head us
 
    Rem: such objects, usable for conversion, are defined in the objdef
    table; practically, it amounts to "canonically" equip t2 into a
@@ -175,8 +175,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
   let c' = subst_univs_level_constr subst c in
   let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (subst_univs_level_constr subst) bs in
-  let f, _ = decompose_app_vect t' in
-    ctx',(t2, f),c',bs',(Stack.append_app_list params Stack.empty,params1),
+  let h, _ = decompose_app_vect t' in
+    ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n,Stack.zip(t2,sk2))
 
@@ -786,13 +786,36 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
       end
 
-and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
+  (* Tries to unify the states
+
+        (proji params1 c1 | sk1)   =   (proji params2 (c (?xs:bs)) | sk2)
+
+     and the terms
+
+        h us  =  h2 us2
+
+     where
+
+     c = the constant for the canonical structure (i.e. some term of the form
+         fun (xs:bs) => Build_R params v1 .. vi-1 (h us) vi+1 .. vn)
+     bs = the types of the parameters of the canonical structure
+     c1 = the main argument of the canonical projection
+     sk1, sk2 = the surrounding stacks of the conversion problem
+     params1, params2 = the params of the projection (empty if a primitive proj)
+
+     knowing that
+
+       (proji params1 c1 | sk1)   =   (h2 us2 | sk2)
+
+     had to be initially resolved
+  *)
   let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
-  if Reductionops.Stack.compare_shape ts ts1 then
+  if Reductionops.Stack.compare_shape sk1 sk2 then
     let (evd',ks,_,test) =
       List.fold_left
 	(fun (i,ks,m,test) b ->
-	  if Int.equal m n then 
+	  if match n with Some n -> Int.equal m n | None -> false then
 	    let ty = Retyping.get_type_of env i t2 in
 	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
 	      (i,t2::ks, m-1, test)
@@ -800,7 +823,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
             let (i',ev) = new_evar env i ~src:dloc (substl ks b) in
 	    (i', ev :: ks, m - 1,test))
-	(evd,[],List.length bs - 1,fun i -> Success i) bs
+	(evd,[],List.length bs,fun i -> Success i) bs
     in
     let app = mkApp (c, Array.rev_of_list ks) in
     ise_and evd'
@@ -813,10 +836,10 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
            (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
-       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
+       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
        test;
-       (fun i -> evar_conv_x trs env i CONV h 
-	 (fst (decompose_app_vect (substl ks h'))))]
+       (fun i -> evar_conv_x trs env i CONV h2
+	 (fst (decompose_app_vect (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index f559db2537..dd9c622dc9 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -48,7 +48,7 @@ val check_conv_record : env -> evar_map ->
   * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * types Stack.t) *
     (constr Stack.t * types Stack.t) * constr *
-    (int * constr)
+    (int option * constr)
 
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c62d567904..3f2eacf879 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1106,10 +1106,10 @@ let opp_problem = function None -> None | Some b -> Some (not b)
 
 let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in
-  try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
-  with CannotProject (evd,ev2) ->
   try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
   with CannotProject (evd,ev1) ->
+  try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+  with CannotProject (evd,ev2) ->
   add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f836c2327e..ad68a70d3b 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,16 +114,18 @@ let find_projection = function
 
   c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
 
-  If ti has the form (ci ui1...uir) where ci is a global reference and
-if the corresponding projection Li of the structure R is defined, one
-declare a "conversion" between ci and Li
+  If ti has the form (ci ui1...uir) where ci is a global reference (or
+  a sort, or a product or a reference to a parameter) and if the 
+  corresponding projection Li of the structure R is defined, one
+  declares a "conversion" between ci and Li.
 
     x1:B1..xk:Bk |- (Li a1..am (c x1..xk)) =_conv (ci ui1...uir)
 
-that maps the pair (Li,ci) to the following data
+  that maps the pair (Li,ci) to the following data
 
     o_DEF = c
     o_TABS = B1...Bk
+    o_INJ = Some n        (when ci is a reference to the parameter xi)
     o_PARAMS = a1...am
     o_NARAMS = m
     o_TCOMP = ui1...uir
@@ -133,7 +135,7 @@ that maps the pair (Li,ci) to the following data
 type obj_typ = {
   o_DEF : constr;
   o_CTX : Univ.ContextSet.t;
-  o_INJ : int;      (* position of trivial argument (negative= none) *)
+  o_INJ : int option;      (* position of trivial argument if any *)
   o_TABS : constr list;    (* ordered *)
   o_TPARAMS : constr list; (* ordered *)
   o_NPARAMS : int;
@@ -173,15 +175,15 @@ let cs_pattern_of_constr t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
-	  try Const_cs (global_of_constr f) , -1, Array.to_list vargs
+	  try Const_cs (global_of_constr f) , None, Array.to_list vargs
           with e when Errors.noncritical e -> raise Not_found
 	end
-    | Rel n -> Default_cs, pred n, []
-    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
-    | Sort s -> Sort_cs (family_of_sort s), -1, []
+    | Rel n -> Default_cs, Some n, []
+    | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b]
+    | Sort s -> Sort_cs (family_of_sort s), None, []
     | _ ->
 	begin
-	  try Const_cs (global_of_constr t) , -1, []
+	  try Const_cs (global_of_constr t) , None, []
           with e when Errors.noncritical e -> raise Not_found
 	end
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 4a03d9bc53..054a3205aa 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -48,6 +48,7 @@ val find_projection : global_reference -> struc_typ
     the effective components of a structure and the projections of the  
     structure *)
 
+(** A cs_pattern characterizes the form of a component of canonical structure *)
 type cs_pattern =
     Const_cs of global_reference
   | Prod_cs
@@ -57,13 +58,15 @@ type cs_pattern =
 type obj_typ = {
   o_DEF : constr;
   o_CTX : Univ.ContextSet.t;
-  o_INJ : int;      (** position of trivial argument *)
+  o_INJ : int option;      (** position of trivial argument *)
   o_TABS : constr list;    (** ordered *)
   o_TPARAMS : constr list; (** ordered *)
   o_NPARAMS : int;
   o_TCOMPS : constr list } (** ordered *)
 
-val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+(** Return the form of the component of a canonical structure *)
+val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
 val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3c89bf27a2..7ea074b748 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -970,11 +970,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
       let (evd,ks,_) =
 	List.fold_left
 	  (fun (evd,ks,m) b ->
-	    if Int.equal m n then (evd,t2::ks, m-1) else
+	    if match n with Some n -> Int.equal m n | None -> false then
+                (evd,t2::ks, m-1)
+            else
               let mv = new_meta () in
 	      let evd' = meta_declare mv (substl ks b) evd in
 	      (evd', mkMeta mv :: ks, m - 1))
-	  (sigma,[],List.length bs - 1) bs
+	  (sigma,[],List.length bs) bs
       in
       try
       let opt' = {opt with with_types = false} in