From 889815067d64e081eb90ea1a792890c2ad4e511c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Sep 2009 11:51:00 +0000 Subject: [PATCH] some more work for ng-coercions --- .../components/cic_unification/coercGraph.ml | 8 +- .../components/cic_unification/coercGraph.mli | 2 +- .../components/grafite_engine/.depend | 9 +- .../components/grafite_engine/Makefile | 1 + .../grafite_engine/grafiteEngine.ml | 255 +-------------- .../grafite_engine/nCicCoercDeclaration.ml | 297 ++++++++++++++++++ .../grafite_engine/nCicCoercDeclaration.mli | 28 ++ helm/software/components/ng_kernel/nCicPp.ml | 1 - .../components/ng_paramodulation/.depend | 14 +- helm/software/components/ng_refiner/.depend | 6 +- .../components/ng_refiner/nCicCoercion.ml | 50 ++- .../components/ng_refiner/nCicCoercion.mli | 8 +- .../components/ng_refiner/nCicRefiner.ml | 2 +- .../components/ng_refiner/nCicUnifHint.ml | 70 +++-- helm/software/matita/matitaMathView.ml | 24 +- 15 files changed, 436 insertions(+), 339 deletions(-) create mode 100644 helm/software/components/grafite_engine/nCicCoercDeclaration.ml create mode 100644 helm/software/components/grafite_engine/nCicCoercDeclaration.mli diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 9dfd6613d..9f953ccf8 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -135,13 +135,9 @@ let source_of t = | 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" @@ -227,8 +223,6 @@ let generate_dot_file () = fmt) ul) l; - Pp.trailer fmt; - Buffer.contents buf ;; let coerced_arg l = diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index 3bc6273c3..44f30d278 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -42,7 +42,7 @@ val look_for_coercion : 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 diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend index 2dca47091..10236823a 100644 --- a/helm/software/components/grafite_engine/.depend +++ b/helm/software/components/grafite_engine/.depend @@ -1,9 +1,14 @@ 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 diff --git a/helm/software/components/grafite_engine/Makefile b/helm/software/components/grafite_engine/Makefile index b6eed1e88..b6eb8fc63 100644 --- a/helm/software/components/grafite_engine/Makefile +++ b/helm/software/components/grafite_engine/Makefile @@ -4,6 +4,7 @@ PREDICATES = INTERFACE_FILES = \ grafiteTypes.mli \ grafiteSync.mli \ + nCicCoercDeclaration.mli \ grafiteEngine.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 0904cf331..597f29e10 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -495,253 +495,6 @@ let eval_unification_hint status t n = 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 ;; @@ -948,7 +701,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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") @@ -1033,10 +786,8 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = 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 diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml new file mode 100644 index 000000000..141ae369e --- /dev/null +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml @@ -0,0 +1,297 @@ +(* + ||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 [] +;; + diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.mli b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli new file mode 100644 index 000000000..666981568 --- /dev/null +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.mli @@ -0,0 +1,28 @@ +(* + ||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 + diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 006a8a7a5..2f4b694de 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -51,7 +51,6 @@ let r2s pp_fix_name r = | NCicEnvironment.ObjectNotFound _ | Failure "nth" | Invalid_argument "List.nth" -> R.string_of_reference r - ;; let string_of_implicit_annotation = function diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index 6dc4150c1..369ed6b69 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,31 +1,31 @@ +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 \ diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 35146bcc8..dc9a46fb3 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -2,7 +2,7 @@ nDiscriminationTree.cmi: 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 @@ -15,8 +15,8 @@ nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.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 \ diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 18540dcda..d168ba548 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -14,11 +14,12 @@ 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) @@ -42,11 +43,10 @@ class status = = 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 ^ " := " ^ @@ -88,7 +88,7 @@ let index_old_db odb (status : #status) = 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) @@ -125,12 +125,12 @@ let look_for_coercion status metasenv subst context infty expty = 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 -> @@ -148,7 +148,7 @@ let look_for_coercion status metasenv subst context infty expty = (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) ;; @@ -159,7 +159,7 @@ let match_coercion status ~metasenv ~subst ~context t = 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 @@ -183,23 +183,19 @@ let match_coercion status ~metasenv ~subst ~context t = ) 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); ); @@ -233,12 +229,8 @@ let generate_dot_file status = 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 ;; diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index dc62cb86d..dd5820eb9 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -28,7 +28,7 @@ val empty_db: db 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) *) @@ -39,13 +39,13 @@ val look_for_coercion: 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 diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 48d1eeb1c..a33162947 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -348,7 +348,7 @@ and try_coercions rdb (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 diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index abca189d9..9f349ba6b 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -11,6 +11,9 @@ (* $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 @@ -31,6 +34,8 @@ type db = exception HintNotValid +let skel_dummy = NCic.Implicit `Type;; + class status = object val db = HDB.empty, EQDB.empty @@ -52,6 +57,8 @@ let index_hint hdb context t1 t2 precedence = (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 @@ -59,6 +66,12 @@ let index_hint hdb context t1 t2 precedence = 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 @@ -71,11 +84,11 @@ let index_hint hdb context t1 t2 precedence = 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 @@ -138,11 +151,6 @@ let db () = | 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 @@ -201,6 +209,7 @@ let saturate ?(delta=0) metasenv subst context ty goal_arity = ;; let eq_class_of hdb t1 = + let eq_class = if NDiscriminationTree.NCicIndexable.path_string_of t1 = [Discrimination_tree.Variable] then @@ -209,13 +218,19 @@ let eq_class_of hdb t1 = 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: " ^ @@ -263,21 +278,20 @@ let look_for_hint hdb metasenv subst context t1 t2 = 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 ;; diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 255998c4f..7ab9299fb 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1035,14 +1035,30 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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) -- 2.39.2