| Some _ -> assert false (* t must be a coercion not to funclass *)
;;
-let generate_dot_file () =
+let generate_dot_file fmt =
let l = CoercDb.to_list (CoercDb.dump ()) in
let module Pp = GraphvizPp.Dot in
- let buf = Buffer.create 10240 in
- let fmt = Format.formatter_of_buffer buf in
- Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
- ~edge_attrs:["fontsize", "10"] fmt;
if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n"
fmt)
ul)
l;
- Pp.trailer fmt;
- Buffer.contents buf
;;
let coerced_arg l =
val source_of: Cic.term -> Cic.term
-val generate_dot_file: unit -> string
+val generate_dot_file: Format.formatter -> unit
(* given the Appl contents returns the argument of the head coercion *)
val coerced_arg: Cic.term list -> (Cic.term * int) option
grafiteTypes.cmi:
grafiteSync.cmi: grafiteTypes.cmi
+nCicCoercDeclaration.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
grafiteTypes.cmx: grafiteTypes.cmi
grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi
grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi
-grafiteEngine.cmo: grafiteTypes.cmi grafiteSync.cmi grafiteEngine.cmi
-grafiteEngine.cmx: grafiteTypes.cmx grafiteSync.cmx grafiteEngine.cmi
+nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
+nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
+grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi grafiteSync.cmi \
+ grafiteEngine.cmi
+grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx grafiteSync.cmx \
+ grafiteEngine.cmi
INTERFACE_FILES = \
grafiteTypes.mli \
grafiteSync.mli \
+ nCicCoercDeclaration.mli \
grafiteEngine.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
status,`New []
;;
-let product f l1 l2 =
- List.fold_left
- (fun acc x ->
- List.fold_left
- (fun acc y ->
- f x y :: acc)
- acc l2)
- [] l1
-;;
-
-let pos_in_list x l =
- match
- HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
- with
- | Some i -> i
- | 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 term_at i t =
- match t with
- | NCic.Appl l ->
- (match
- HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
- with
- | Some i -> i
- | None -> assert false)
- | _ -> assert false
-;;
-
-let src_tgt_of_ty_cpos_arity ty cpos arity =
- let pis = count_prod ty in
- let tpos = pis - arity in
- let rec pi_nth i j = function
- | NCic.Prod (_,s,_) when i = j -> s
- | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
- | t -> assert (i = j); t
- in
- let rec cleanup_prod = function
- | NCic.Prod (_,_,t) -> NCic.Prod ("_",NCic.Implicit `Type, cleanup_prod t)
- | _ -> NCic.Implicit `Type
- in
- let rec pi_tail i j = function
- | NCic.Prod (_,_,_) as t when i = j -> cleanup_prod t
- | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
- | t -> assert (i = j); t
- in
- let mask t =
- let rec aux () = function
- | NCic.Meta _
- | NCic.Implicit _ as x -> x
- | NCic.Rel _ -> NCic.Implicit `Type
- | t -> NCicUtils.map (fun _ () -> ()) () aux t
- in
- aux () t
- in
- mask (pi_nth 0 cpos ty),
- mask (pi_tail 0 tpos ty)
-;;
-
-let close_in_context 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 m_subst m =
- (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
- in
- NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
- | [] ->
- (* STRONG ASSUMPTION:
- 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)
- | _ -> assert false
- in
- aux (fun _ -> []) [] [] metasenv
-;;
-
-let toposort 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
- in
- T.topological_sort metasenv deps
-;;
-
-let basic_eval_ncoercion (name,t,s,d,p,a) status =
- let to_s =
- NCicCoercion.look_for_coercion status [] [] [] (NCic.Implicit `Type) s
- in
- let from_d =
- NCicCoercion.look_for_coercion status [] [] [] d (NCic.Implicit `Type)
- in
- let status = NCicCoercion.index_coercion status t s d a p in
- let c =
- List.find
- (function (_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
- (NCicCoercion.look_for_coercion status [] [] [] s d)
- in
- let composites =
- let to_s_o_c =
- product (fun (m1,t1,_,j) (mc,c,_,i) -> m1@mc,c,[i,t1],j,a)
- to_s [c]
- in
- let c_o_from_d =
- product (fun (mc,c,_,j) (m1,t1,ty,i) -> m1@mc,t1,[i,c],j,count_prod ty)
- [c] from_d
- in
- let to_s_o_c_o_from_d =
- product (fun (m1,t1,_,j) (m,t,upl,i,a)->
- 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
- in
- let composites =
- HExtlib.filter_map
- (fun (metasenv, bo, upl, p, arity) ->
- try
- let metasenv, subst =
- List.fold_left
- (fun (metasenv,subst) (a,b) ->
- NCicUnification.unify status metasenv subst [] a b)
- (metasenv,[]) upl
- in
- let bo = NCicUntrusted.apply_subst subst [] bo 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
- in
- let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
- let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
-(*
- prerr_endline (
- 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 ^
- " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity);
-*)
- Some (bo,src,tgt,arity,pos)
- with
- | NCicTypeChecker.TypeCheckerFailure _
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> None
- ) composites
- in
- List.fold_left
- (fun st (t,s,d,a,p) -> NCicCoercion.index_coercion st t s d a p)
- status composites
-;;
-
-let inject_ncoercion =
- let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
- ~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_eval_ncoercion (name,t,s,d,p,a)
- in
- 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
- 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
- status, tgt, count_prod tgt
- in
- status, src, tgt, cpos, arity
-;;
-
-let basic_eval_and_inject_ncoercion infos status =
- let status = basic_eval_ncoercion infos status in
- let dump = inject_ncoercion infos::status#dump in
- status#set_dump dump
-;;
-
-let eval_ncoercion status name t ty (id,src) tgt =
-
- let metasenv,subst,status,ty =
- GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
- assert (metasenv=[]);
- let ty = NCicUntrusted.apply_subst subst [] ty in
- let metasenv,subst,status,t =
- GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
- assert (metasenv=[]);
- let t = NCicUntrusted.apply_subst 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 =
- basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
- in
- status,`New []
-;;
-
let basic_eval_add_constraint (s,u1,u2) status =
NCicLibrary.add_constraint status s u1 u2
;;
match cmd with
| GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
| GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
- eval_ncoercion status name t ty source target
+ NCicCoercDeclaration.eval_ncoercion status name t ty source target
| GrafiteAst.NQed loc ->
if status#ng_mode <> `ProofMode then
raise (GrafiteTypes.Command_error "Not in proof mode")
GrafiteDisambiguate.disambiguate_nterm None status [] [] []
("",0,CicNotationPt.Ident (name,None)) in
assert (metasenv = [] && subst = []);
- let ty = NCicTypeChecker.typeof ~subst ~metasenv [] t in
- let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
- basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity)
- status
+ NCicCoercDeclaration.basic_eval_and_inject_ncoercion_from_t_cpos_arity
+ status (name,t,cpos,arity)
) status coercions
in
status,uris
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+let debug s = prerr_endline (Lazy.force s) ;;
+let debug _ = ();;
+
+let skel_dummy = NCic.Implicit `Type;;
+
+let product f l1 l2 =
+ List.fold_left
+ (fun acc x ->
+ List.fold_left
+ (fun acc y ->
+ f x y :: acc)
+ acc l2)
+ [] l1
+;;
+
+let pos_in_list x l =
+ match
+ HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
+ with
+ | Some i -> i
+ | 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 term_at i t =
+ match t with
+ | NCic.Appl l ->
+ (match
+ HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
+ with
+ | Some i -> i
+ | None -> assert false)
+ | _ -> assert false
+;;
+
+let rec cleanup_funclass_skel = function
+ | NCic.Prod (_,_,t) ->
+ NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
+ | _ -> skel_dummy
+;;
+
+let src_tgt_of_ty_cpos_arity ty cpos arity =
+ let pis = count_prod ty in
+ let tpos = pis - arity in
+ let rec pi_nth i j = function
+ | NCic.Prod (_,s,_) when i = j -> s
+ | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
+ | t -> assert (i = j); t
+ in
+ let rec pi_tail i j = function
+ | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
+ | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
+ | t -> assert (i = j); t
+ in
+ let mask t =
+ let rec aux () = function
+ | NCic.Meta _
+ | NCic.Implicit _ as x -> x
+ | NCic.Rel _ -> skel_dummy
+ | t -> NCicUtils.map (fun _ () -> ()) () aux t
+ in
+ aux () t
+ in
+ mask (pi_nth 0 cpos ty),
+ mask (pi_tail 0 tpos ty)
+;;
+
+let rec cleanup_skel () = function
+ | NCic.Meta _ -> skel_dummy
+ | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skel t
+;;
+
+let close_in_context 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 m_subst m =
+ (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
+ in
+ NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
+ | [] ->
+ (* STRONG ASSUMPTION:
+ 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)
+ | _ -> assert false
+ in
+ aux (fun _ -> []) [] [] metasenv
+;;
+
+let toposort 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
+ in
+ T.topological_sort metasenv deps
+;;
+
+let only_head = function
+ | NCic.Appl (h::tl) ->
+ NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
+ | t -> t
+;;
+
+let basic_eval_ncoercion (name,t,s,d,p,a) status =
+ let to_s =
+ NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
+ in
+ let from_d =
+ NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
+ in
+ let status = NCicCoercion.index_coercion status name t s d a p in
+ let c =
+ List.find
+ (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
+ (NCicCoercion.look_for_coercion status [] [] [] s d)
+ in
+ let compose_names a b = a ^ "__o__" ^ b in
+ let composites =
+ let to_s_o_c =
+ product
+ (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
+ compose_names n1 n,m1@mc,c,[i,t1],j,a)
+ to_s [c]
+ in
+ 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)
+ [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)
+ to_s c_o_from_d
+ in
+ to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
+ in
+ let composites =
+ HExtlib.filter_map
+ (fun (name,metasenv, bo, upl, p, arity) ->
+ try
+ let metasenv, subst =
+ List.fold_left
+ (fun (metasenv,subst) (a,b) ->
+ NCicUnification.unify status metasenv subst [] a b)
+ (metasenv,[]) upl
+ in
+ let bo = NCicUntrusted.apply_subst subst [] bo 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
+ 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: "^
+ 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 ^
+ " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
+ Some (name,bo,src,tgt,arity,pos)
+ with
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicUnification.UnificationFailure _
+ | NCicUnification.Uncertain _ -> None
+ ) composites
+ in
+ List.fold_left
+ (fun st (name,t,s,d,a,p) -> NCicCoercion.index_coercion st name t s d a p)
+ status composites
+;;
+
+let inject_ncoercion =
+ let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
+ ~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_eval_ncoercion (name,t,s,d,p,a)
+ in
+ 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
+;;
+
+let basic_eval_and_inject_ncoercion infos status =
+ let status = basic_eval_ncoercion infos status in
+ let dump = inject_ncoercion infos::status#dump in
+ status#set_dump dump
+;;
+
+let basic_eval_and_inject_ncoercion_from_t_cpos_arity
+ status (name,t,cpos,arity)
+=
+ let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
+ let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
+ basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
+;;
+
+let eval_ncoercion status name t ty (id,src) tgt =
+
+ let metasenv,subst,status,ty =
+ GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
+ assert (metasenv=[]);
+ let ty = NCicUntrusted.apply_subst subst [] ty in
+ let metasenv,subst,status,t =
+ GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
+ assert (metasenv=[]);
+ let t = NCicUntrusted.apply_subst 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 =
+ basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
+ in
+ status,`New []
+;;
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+
+(* evals a coercion declaration statement: name t ty (id,src) tgt *)
+val eval_ncoercion:
+ GrafiteTypes.status as 'status ->
+ string ->
+ CicNotationPt.term ->
+ CicNotationPt.term ->
+ string * CicNotationPt.term ->
+ CicNotationPt.term -> 'status * [> `New of 'c list ]
+
+(* for records, the term is the projection, already refined, while the
+ * first integer is the number of left params and the second integer is
+ * the arity in the `:arity>` syntax *)
+val basic_eval_and_inject_ncoercion_from_t_cpos_arity:
+ (GrafiteTypes.status as 'status) ->
+ string * NCic.term * int * int -> 'status
+
| NCicEnvironment.ObjectNotFound _
| Failure "nth"
| Invalid_argument "List.nth" -> R.string_of_reference r
-
;;
let string_of_implicit_annotation = function
+terms.cmi:
pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
orderings.cmi: terms.cmi
foUtils.cmi: terms.cmi orderings.cmi
-index.cmi: terms.cmi orderings.cmi
foUnif.cmi: terms.cmi orderings.cmi
+index.cmi: terms.cmi orderings.cmi
superposition.cmi: terms.cmi orderings.cmi index.cmi
stats.cmi: terms.cmi orderings.cmi
paramod.cmi: terms.cmi orderings.cmi
nCicBlob.cmi: terms.cmi
cicBlob.cmi: terms.cmi
nCicProof.cmi: terms.cmi
+nCicParamod.cmi:
terms.cmo: terms.cmi
terms.cmx: terms.cmi
pp.cmo: terms.cmi pp.cmi
pp.cmx: terms.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
-orderings.cmo: terms.cmi pp.cmi orderings.cmi
-orderings.cmx: terms.cmx pp.cmx orderings.cmi
+orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi
+orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi
foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
- index.cmi
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
- index.cmi
foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
foUnif.cmi foSubst.cmi superposition.cmi
superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
nCicMetaSubst.cmi:
nCicUnifHint.cmi:
nCicCoercion.cmi: nCicUnifHint.cmi
-nRstatus.cmi: nCicCoercion.cmi
+nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi
nCicUnification.cmi: nRstatus.cmi
nCicRefiner.cmi: nRstatus.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nCicCoercion.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
nCicCoercion.cmi
-nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi
-nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi
+nRstatus.cmo: nCicUnifHint.cmi nCicCoercion.cmi nRstatus.cmi
+nRstatus.cmx: nCicUnifHint.cmx nCicCoercion.cmx nRstatus.cmi
nCicUnification.cmo: nRstatus.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
nCicCoercion.cmi nCicUnification.cmi
nCicUnification.cmx: nRstatus.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;
-module COT : Set.OrderedType with type t = NCic.term * int * int * NCic.term *
+module COT : Set.OrderedType
+with type t = string * NCic.term * int * int * NCic.term *
NCic.term =
struct
- type t = NCic.term * int * int * NCic.term * NCic.term
- let compare = Pervasives.compare
+ type t = string * NCic.term * int * int * NCic.term * NCic.term
+ let compare = Pervasives.compare
end
module CoercionSet = Set.Make(COT)
= fun o -> {< db = o#coerc_db >}#set_unifhint_status o
end
-let index_coercion status c src tgt arity arg =
+let index_coercion status name c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
- let data = (c,arity,arg,src,tgt) in
+ let data = (name,c,arity,arg,src,tgt) in
- let debug s = prerr_endline (Lazy.force s) in
debug (lazy ("INDEX:" ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
assert false
in
- index_coercion status c src tgt arity arg
+ index_coercion status "foo" c src tgt arity arg
with
| NCicEnvironment.BadDependency _
| NCicTypeChecker.TypeCheckerFailure _ -> status)
let candidates = CoercionSet.inter set_src set_tgt in
debug (lazy ("CANDIDATES: " ^
- String.concat "," (List.map (fun (t,_,_,_,_) ->
- NCicPp.ppterm ~metasenv ~subst ~context t)
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
(CoercionSet.elements candidates))));
List.map
- (fun (t,arity,arg,_,_) ->
+ (fun (name,t,arity,arg,_,_) ->
let ty =
try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
with NCicTypeChecker.TypeCheckerFailure s ->
(NCicUntrusted.mk_appl t args) ^ " --- " ^
string_of_int (List.length args) ^ " == " ^ string_of_int arg));
- metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
+ name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
(CoercionSet.elements candidates)
;;
DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
in
(HExtlib.list_findopt
- (fun (p,arity,cpos,_,_) _ ->
+ (fun (_,p,arity,cpos,_,_) _ ->
try
let t =
match p,t with
) db)
;;
-let generate_dot_file status =
+let generate_dot_file status fmt =
let module Pp = GraphvizPp.Dot in
- let buf = Buffer.create 10240 in
- let fmt = Format.formatter_of_buffer buf in
- Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
- ~edge_attrs:["fontsize", "10"] fmt;
let src_db, _ = status#coerc_db in
let edges = ref [] in
DB.iter src_db (fun _ dataset ->
edges := !edges @
List.map
- (fun (t,a,g,sk,dk) ->
- prerr_endline (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
- ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk);
- let eq_s=List.sort compare (sk::NCicUnifHint.eq_class_of status sk) in
- let eq_t=List.sort compare (dk::NCicUnifHint.eq_class_of status dk) in
- (t,a,g),eq_s,eq_t
+ (fun (name,t,a,g,sk,dk) ->
+ debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
+ ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
+ let eq_s= sk::NCicUnifHint.eq_class_of status sk in
+ let eq_t= dk::NCicUnifHint.eq_class_of status dk in
+ (name,t,a,g),eq_s,eq_t
)
(CoercionSet.elements dataset);
);
fmt)
nodes;
List.iter
- (fun ((t,a,b),src,tgt) ->
+ (fun ((name,_,_,_),src,tgt) ->
Pp.edge (mangle src) (mangle tgt)
- ~attrs:["label",
- NCicPp.ppterm ~metasenv:[]
- ~subst:[] ~context:[] t] fmt)
+ ~attrs:["label", name] fmt)
!edges;
- Pp.trailer fmt;
- Buffer.contents buf
;;
index_coercion db c A B \arity_left(c ??x??) \position(x,??x??)
*)
val index_coercion:
- #status as 'status ->
+ #status as 'status -> string ->
NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
(* gets the old imperative coercion DB (list format) *)
NCic.metasenv -> NCic.substitution -> NCic.context ->
(* inferred type, expected type *)
NCic.term -> NCic.term ->
- (* enriched metasenv, new term, its type, metavriable to
+ (* name, enriched metasenv, new term, its type, metavriable to
* be unified with the old term *)
- (NCic.metasenv * NCic.term * NCic.term * NCic.term) list
+ (string * NCic.metasenv * NCic.term * NCic.term * NCic.term) list
(* returns (coercion,arity,arg) *)
val match_coercion:
#status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
context:NCic.context -> NCic.term -> (NCic.term * int * int) option
-val generate_dot_file: #status -> string
+val generate_dot_file: #status -> Format.formatter -> unit
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context infty)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
- | (metasenv, newterm, newtype, meta)::tl ->
+ | (_,metasenv, newterm, newtype, meta)::tl ->
try
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
+let debug s = prerr_endline (Lazy.force s);;
+let debug _ = ();;
+
module COT : Set.OrderedType with type t = int * NCic.term =
struct
type t = int * NCic.term
exception HintNotValid
+let skel_dummy = NCic.Implicit `Type;;
+
class status =
object
val db = HDB.empty, EQDB.empty
(match t2 with
| NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> false | _ -> true)
);
+ (* here we do not use skel_dummy since it could cause an assert false in
+ * the subst function that lives in the kernel *)
let hole = NCic.Meta (-1,(0,NCic.Irl 0)) in
let t1_skeleton =
List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t1 context
let t2_skeleton =
List.fold_left (fun t _ -> NCicSubstitution.subst hole t) t2 context
in
+ let rec cleanup_skeleton () = function
+ | NCic.Meta _ -> skel_dummy
+ | t -> NCicUtils.map (fun _ () -> ()) () cleanup_skeleton t
+ in
+ let t1_skeleton = cleanup_skeleton () t1_skeleton in
+ let t2_skeleton = cleanup_skeleton () t2_skeleton in
let src = pair t1_skeleton t2_skeleton in
let ctx2abstractions context t =
List.fold_left
let data_hint = ctx2abstractions context (pair t1 t2) in
let data_t1 = t2_skeleton in
let data_t2 = t1_skeleton in
-(*
- prerr_endline ("INDEXING: " ^
+
+ debug(lazy ("INDEXING: " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
-*)
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data_hint));
+
hdb#set_uhint_db (
HDB.index (fst (hdb#uhint_db)) src (precedence, data_hint),
EQDB.index
| b1,b2 ->
if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2
then begin
-(*
- prerr_endline ("hint: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[]
- ~context:ctx b1 ^ " === " ^ NCicPp.ppterm ~metasenv:[]
- ~subst:[] ~context:ctx b2);
-*)
let rec mk_rels =
function 0 -> [] | n -> NCic.Rel n :: mk_rels (n-1)
in
;;
let eq_class_of hdb t1 =
+ let eq_class =
if NDiscriminationTree.NCicIndexable.path_string_of t1 =
[Discrimination_tree.Variable]
then
else
let candidates = EQDB.retrieve_unifiables (snd hdb#uhint_db) t1 in
let candidates = HintSet.elements candidates in
- List.map snd (List.sort (fun (x,_) (y,_) -> compare x y) candidates)
+ let candidates = List.sort (fun (x,_) (y,_) -> compare x y) candidates in
+ List.map snd candidates
+ in
+ debug(lazy("eq_class of: " ^ NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[]
+ t1 ^ " is\n" ^ String.concat "\n"
+ (List.map (NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[]) eq_class)));
+ eq_class
;;
let look_for_hint hdb metasenv subst context t1 t2 =
+ debug(lazy ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context t1));
+ debug(lazy ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context t2));
(*
- prerr_endline ("KEY1: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t1 t2));
- prerr_endline ("KEY2: "^NCicPp.ppterm ~metasenv ~subst ~context (pair t2 t1));
HDB.iter hdb
(fun p ds ->
prerr_endline ("ENTRY: " ^
List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
in
let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
-(*
- prerr_endline "Hints:";
- List.iter
- (fun (metasenv, (t1, t2), premises) ->
- prerr_endline
- ("\t" ^ String.concat "; "
- (List.map (fun (a,b) ->
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
- " =?= "^
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
- premises) ^
- " ==> "^
- NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
- " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
- rc;
-*)
+
+ debug(lazy ("Hints:"^
+ String.concat "\n" (List.map
+ (fun (metasenv, (t1, t2), premises) ->
+ ("\t" ^ String.concat "; "
+ (List.map (fun (a,b) ->
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
+ " =?= "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
+ premises) ^
+ " ==> "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+ " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
+ rc)));
+
rc
;;
win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
in
let load_coerchgraph tred () =
- let str = CoercGraph.generate_dot_file () in
+ let module Pp = GraphvizPp.Dot in
let filename, oc = Filename.open_temp_file "matita" ".dot" in
- output_string oc str;
+ let fmt = Format.formatter_of_out_channel oc in
+ Pp.header
+ ~name:"Coercions"
+ ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ let status = (MatitaScript.current ())#grafite_status in
+ NCicCoercion.generate_dot_file status fmt;
+ Pp.trailer fmt;
+ Pp.header
+ ~name:"OLDCoercions"
+ ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ CoercGraph.generate_dot_file fmt;
+ Pp.trailer fmt;
+ Pp.raw "@." fmt;
close_out oc;
if tred then
- gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+ gviz#load_graph_from_file
+ ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename
else
- gviz#load_graph_from_file filename;
+ gviz#load_graph_from_file
+ ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;
HExtlib.safe_remove filename
in
object (self)
projects / helm.git / commitdiff