| _ -> skel_dummy
;;
-let src_tgt_of_ty_cpos_arity ty cpos arity =
+let src_tgt_of_ty_cpos_arity status ty cpos arity =
let pis = count_prod ty in
let tpos = pis - arity in
let rec pi_nth i j = function
| NCic.Meta _
| NCic.Implicit _ as x -> x
| NCic.Rel _ -> skel_dummy
- | t -> NCicUtils.map (fun _ () -> ()) () aux t
+ | t -> NCicUtils.map status (fun _ () -> ()) () aux t
in
aux () t
in
mask (pi_tail 0 tpos ty)
;;
-let rec cleanup_skel () = function
+let rec cleanup_skel status () = function
| NCic.Meta _ -> skel_dummy
- | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skel t
+ | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
;;
-let close_in_context t metasenv =
+let close_in_context status t metasenv =
let rec aux m_subst subst ctx = function
| (i,(tag,[],ty)) :: tl ->
let name = "x" ^ string_of_int (List.length ctx) in
let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
- let ty = NCicUntrusted.apply_subst (m_subst (List.length ctx)) ctx ty in
+ let ty = NCicUntrusted.apply_subst status (m_subst (List.length ctx)) ctx ty in
let m_subst m =
(i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
in
since metas occurring in t have an empty context,
the substitution i build makes sense (i.e, the Rel
I pun in the subst will not be lifted by subst_meta *)
- NCicUntrusted.apply_subst subst ctx
- (NCicSubstitution.lift (List.length ctx) t)
+ NCicUntrusted.apply_subst status subst ctx
+ (NCicSubstitution.lift status (List.length ctx) t)
| _ -> assert false
in
aux (fun _ -> []) [] [] metasenv
;;
-let toposort metasenv =
+let toposort status metasenv =
let module T = HTopoSort.Make(
struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
in
let deps (_,(_,_,t)) =
List.filter (fun (j,_) ->
- List.mem j (NCicUntrusted.metas_of_term [] [] t)) metasenv
+ List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
in
T.topological_sort metasenv deps
;;
(try
let metasenv,subst,status,src =
GrafiteDisambiguate.disambiguate_nterm
- status None ctx [] [] ("",0,src) in
- let src = NCicUntrusted.apply_subst subst [] src in
+ status `XTSort ctx [] [] ("",0,src) in
+ let src = NCicUntrusted.apply_subst status 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
+ let src = cleanup_skel status () src in
status, src, cpos
with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _
- | MultiPassDisambiguator.DisambiguationError _ ->
- raise (GrafiteTypes.Command_error "bad source pattern"))
+ | NCicUnification.UnificationFailure msg
+ | NCicUnification.Uncertain msg ->
+ raise (GrafiteTypes.Command_error ("bad source pattern: " ^
+Lazy.force msg))
+ | MultiPassDisambiguator.DisambiguationError _ ->
+ raise (GrafiteTypes.Command_error ("bad source pattern: disambiguation error")))
| _ -> assert false
in
aux 0 [] ty
in
let status, tgt, arity =
- let metasenv,subst,status,tgt =
+ let _metasenv,subst,status,tgt =
GrafiteDisambiguate.disambiguate_nterm
- status None [] [] [] ("",0,tgt) in
- let tgt = NCicUntrusted.apply_subst subst [] tgt in
+ status `XTSort [] [] [] ("",0,tgt) in
+ let tgt = NCicUntrusted.apply_subst status subst [] tgt in
(* CHECK che sia unificabile mancante *)
let rec count_prod = function
| NCic.Prod (_,_,x) -> 1 + count_prod x
let arity = count_prod tgt in
let tgt=
if arity > 0 then cleanup_funclass_skel tgt
- else cleanup_skel () tgt
+ else cleanup_skel status () tgt
in
status, tgt, arity
in
exception Stop;;
-let close_graph name t s d to_s from_d p a status =
+let close_graph _name t s d to_s from_d _p a status =
let c =
List.find
(function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
NCicUnification.unify status metasenv subst [] a b)
(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 bo = NCicUntrusted.apply_subst status subst [] bo in
+ let p = NCicUntrusted.apply_subst status subst [] p in
+ let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
+ let metasenv = toposort status metasenv in
+ let bo = close_in_context status bo metasenv in
let pos =
match p with
| NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
- | t -> raise Stop
+ | _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 ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
+ let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
let src = only_head src in
let tgt = only_head tgt in
debug (lazy(
"composite " ^ name ^ ": "^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
+ status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
" cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
let uri = fresh_uri status name ".con" in
let obj_kind = NCic.Constant
([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity))
in
- let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
+ let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
let obj = uri,height,[],[],obj_kind in
let c =
NCic.Const
;;
(* idempotent *)
-let basic_index_ncoercion (name,t,s,d,position,arity) status =
+let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
NCicCoercion.index_coercion status name t s d arity position
;;
-let basic_eval_ncoercion (name,t,s,d,p,a) status =
+let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
let to_s =
NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
in
NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
in
let status = NCicCoercion.index_coercion status name t s d a p in
- let composites = close_graph name t s d to_s from_d p a status in
+ let composites =
+ if compose then close_graph name t s d to_s from_d p a status else [] in
List.fold_left
(fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
- let info = name,t,s,d,p,a in
+ let info = name,compose,t,s,d,p,a in
let st = NCicLibrary.add_obj st obj in
let st = basic_index_ncoercion info st in
uri::uris, info::infos, st)
;;
let record_ncoercion =
- let aux (name,t,s,d,p,a) ~refresh_uri_in_term =
+ let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
let t = refresh_uri_in_term t in
let s = refresh_uri_in_term s in
let d = refresh_uri_in_term d in
- basic_index_ncoercion (name,t,s,d,p,a)
+ basic_index_ncoercion (name,compose,t,s,d,p,a)
in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
- ~refresh_uri_in_reference
+ let aux_l l ~refresh_uri_in_universe:_ ~refresh_uri_in_term
+ ~refresh_uri_in_reference:_ ~alias_only status
=
- List.fold_right (aux ~refresh_uri_in_term) l
+ if not alias_only then
+ List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
+ else
+ status
in
- GrafiteTypes.Serializer.register#run "ncoercion" aux_l
+ GrafiteTypes.Serializer.register#run "ncoercion" aux_l
;;
let basic_eval_and_record_ncoercion infos status =
let uris, cinfos, status = basic_eval_ncoercion infos status in
- let dump = record_ncoercion (infos::cinfos) :: status#dump in
- status#set_dump dump, uris
+ NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
;;
let basic_eval_and_record_ncoercion_from_t_cpos_arity
- status (name,t,cpos,arity)
+ status (name,compose,t,cpos,arity)
=
- let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
- let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
+ let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
+ let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
let status, uris =
- basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+ basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
in
status,uris
;;
-let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
+let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt =
let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
+ GrafiteDisambiguate.disambiguate_nterm status `XTSort [] [] [] ("",0,ty) in
assert (metasenv=[]);
- let ty = NCicUntrusted.apply_subst subst [] ty in
+ let ty = NCicUntrusted.apply_subst status subst [] ty in
let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
+ GrafiteDisambiguate.disambiguate_nterm status (`XTSome ty) [] [] [] ("",0,t) in
assert (metasenv=[]);
- let t = NCicUntrusted.apply_subst subst [] t in
+ let t = NCicUntrusted.apply_subst status subst [] t in
let status, src, tgt, cpos, arity =
src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
let status, uris =
- basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
+ basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
in
status,uris
;;
projects / helm.git / blobdiff