diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 26 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 26 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 5 |
3 files changed, 39 insertions, 18 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 93e1c1157..55625232b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -115,15 +115,22 @@ let apprec_nohdbeta env evd c = let check_conv_record (t1,l1) (t2,l2) = try let proji = global_of_constr t1 in - let cstr = global_of_constr t2 in - let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = - lookup_canonical_conversion (proji, cstr) in + let canon_s = + begin + try + let cstr = global_of_constr t2 in + lookup_canonical_conversion (proji, Some cstr) + with _ -> lookup_canonical_conversion (proji,None) + end in + let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = + canon_s in let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 | _ -> assert false in let us2,extra_args2 = list_chop (List.length us) l2 in - c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1 + c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1, + (n,applist(t2,l2)) with _ -> raise Not_found @@ -466,14 +473,15 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | (Rel _ | Var _ | Const _ | Evar _), _ -> assert false | _, (Rel _ | Var _ | Const _ | Evar _) -> assert false -and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = - let (evd',ks) = +and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = + let (evd',ks,_) = List.fold_left - (fun (i,ks) b -> + (fun (i,ks,m) b -> + if m=0 then (i,t2::ks, n-1) else let dloc = (dummy_loc,InternalHole) in let (i',ev) = new_evar i env ~src:dloc (substl ks b) in - (i', ev :: ks)) - (evd,[]) bs + (i', ev :: ks, n - 1)) + (evd,[],n) bs in ise_and evd' [(fun i -> diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4b93388d6..73ff31180 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -115,12 +115,13 @@ that maps the pair (Li,ci) to the following data type obj_typ = { o_DEF : constr; + o_INJ : int; (* position of trivial argument (negative= none) *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) o_TCOMPS : constr list } (* ordered *) let object_table = - (ref [] : ((global_reference * global_reference) * obj_typ) list ref) + (ref [] : ((global_reference * global_reference option) * obj_typ) list ref) let canonical_projections () = !object_table @@ -128,14 +129,15 @@ let keep_true_projections projs kinds = map_succeed (function (p,true) -> p | _ -> failwith "") (List.combine projs kinds) -(* Intended to always success *) +(* Intended to always succeed *) let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in let lt = List.rev (List.map snd lt) in let args = snd (decompose_app t) in - let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in + let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = + lookup_structure ind in let params, projs = list_chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in @@ -145,12 +147,22 @@ let compute_canonical_projections (con,ind) = match spopt with | Some proji_sp -> let c, args = decompose_app t in - (try (ConstRef proji_sp, global_of_constr c, args) :: l - with Not_found -> l) + begin + try + let ogc,oinj = + try Some (global_of_constr c) , -1 + with _ -> + try + None,pred (destRel c) + with _ -> raise Not_found + in + ((ConstRef proji_sp, ogc,oinj , args) :: l) + with Not_found -> l + end | _ -> l) [] lps in - List.map (fun (refi,c,argj) -> - (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) + List.map (fun (refi,c,inj,argj) -> + (refi,c),{o_DEF=v; o_INJ=inj; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp let open_canonical_structure i (_,o) = diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index c8942b5d4..321584b5b 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -38,11 +38,12 @@ val find_projection_nparams : global_reference -> int type obj_typ = { o_DEF : constr; + o_INJ : int; (* position of trivial argument *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) o_TCOMPS : constr list } (* ordered *) -val lookup_canonical_conversion : (global_reference * global_reference) -> obj_typ +val lookup_canonical_conversion : (global_reference * global_reference option) -> obj_typ val declare_canonical_structure : global_reference -> unit val canonical_projections : unit -> - ((global_reference * global_reference) * obj_typ) list + ((global_reference * global_reference option) * obj_typ) list |