- NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
-;;
-
-let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
- let status, src, cpos =
- let rec aux cpos ctx = function
- | NCic.Prod (name,ty,bo) ->
- if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
- else
- (try
- let metasenv,subst,status,src =
- GrafiteDisambiguate.disambiguate_nterm
- None status ctx [] [] ("",0,src) in
- let src = NCicUntrusted.apply_subst subst [] src in
- (* CHECK that the declared pattern matches the abstraction *)
- let _ = NCicUnification.unify status metasenv subst ctx ty src in
- let src = cleanup_skel () src in
- status, src, cpos
- with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _
- | MultiPassDisambiguator.DisambiguationError _ ->
- raise (GrafiteTypes.Command_error "bad source pattern"))
- | _ -> assert false
- in
- aux 0 [] ty
- in
- let status, tgt, arity =
- let metasenv,subst,status,tgt =
- GrafiteDisambiguate.disambiguate_nterm
- None status [] [] [] ("",0,tgt) in
- let tgt = NCicUntrusted.apply_subst subst [] tgt in
- (* CHECK che sia unificabile mancante *)
- let rec count_prod = function
- | NCic.Prod (_,_,x) -> 1 + count_prod x
- | _ -> 0
- in
- let arity = count_prod tgt in
- let tgt=
- if arity > 0 then cleanup_funclass_skel tgt
- else cleanup_skel () tgt
- in
- status, tgt, arity
- in
- status, src, tgt, cpos, arity