\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-let debug s = prerr_endline (Lazy.force s) ;;
+(* let debug s = prerr_endline (Lazy.force s) ;;*)
let debug _ = ();;
let skel_dummy = NCic.Implicit `Type;;
| None -> assert false
;;
-let pos_of x t =
- match t with
- | NCic.Appl l -> pos_in_list x l
- | _ -> assert false
-;;
-
let rec count_prod = function
| NCic.Prod (_,_,x) -> 1 + count_prod x
| _ -> 0
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) ->
+ | NCic.Prod (name,ty,bo) ->
if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
else
(try
diverge (mk "") 0
;;
+exception Stop;;
let close_graph name t s d to_s from_d p a status =
let c =
let c_o_from_d =
product
(fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
- compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty)
+ compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty)
[c] from_d
in
let to_s_o_c_o_from_d =
product
(fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
- compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
+ compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
to_s c_o_from_d
in
to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
(metasenv,[]) upl
in
let bo = NCicUntrusted.apply_subst subst [] bo in
+ let p = NCicUntrusted.apply_subst subst [] p in
+ let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
let metasenv = toposort metasenv in
let bo = close_in_context bo metasenv in
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
- | _ -> assert false
+ | t -> raise Stop
in
let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
let src = only_head src in
let tgt = only_head tgt in
debug (lazy(
- "composite: "^
+ "composite " ^ name ^ ": "^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
with
| NCicTypeChecker.TypeCheckerFailure _
| NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> None
+ | NCicUnification.Uncertain _ | Stop -> None
) composites
in
composites
let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
in
- NCicLibrary.Serializer.register "ncoercion" aux_l
+ NCicLibrary.Serializer.register#run "ncoercion"
+ object(self : 'a NCicLibrary.register_type)
+ method run = aux_l
+ end
;;
let basic_eval_and_record_ncoercion infos status =