X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=04fddee83fdee339546a4bf42484bdf3e23d8f73;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=5c79aa95c30a975fc9b333ba2065591c4648cb0b;hpb=ee641910c2496cd531c90cad25ffbe08591ca5df;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 5c79aa95c..04fddee83 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -11,10 +11,18 @@ (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *) -module COT : Set.OrderedType with type t = NCic.term * int * int = +let debug s = prerr_endline (Lazy.force s);; +let debug _ = ();; + +let convert_term = ref (fun _ _ -> assert false);; +let set_convert_term f = convert_term := f;; + +module COT : Set.OrderedType +with type t = string * NCic.term * int * int * NCic.term * +NCic.term = struct - type t = NCic.term * int * int - 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) @@ -24,56 +32,224 @@ module DB = type db = DB.t * DB.t -let index_coercion (db_src,db_tgt) c src tgt arity arg = - let data = (c,arity,arg) in +let empty_db = DB.empty,DB.empty + +class type g_status = + object + inherit NCicUnifHint.g_status + method coerc_db: db + end + +class status = + object + inherit NCicUnifHint.status + val db = empty_db + method coerc_db = db + method set_coerc_db v = {< db = v >} + method set_coercion_status + : 'status. #g_status as 'status -> 'self + = fun o -> {< db = o#coerc_db >}#set_unifhint_status o + end + +let index_coercion status name c src tgt arity arg = + let db_src,db_tgt = status#coerc_db in + let data = (name,c,arity,arg,src,tgt) in + debug (lazy ("INDEX:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ + string_of_int arg ^ " " ^ string_of_int arity)); let db_src = DB.index db_src src data in let db_tgt = DB.index db_tgt tgt data in - db_src, db_tgt + status#set_coerc_db (db_src, db_tgt) ;; -let db () = +let index_old_db odb (status : #status) = List.fold_left - (fun db (_,tgt,clist) -> + (fun status (_,tgt,clist) -> List.fold_left - (fun db (uri,_,arg) -> - let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in + (fun status (uri,_,arg) -> + try + let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in let src, tgt = let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in - match - NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) - with - | NCic.Prod (_, src, tgt),_,_ -> - src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt - | t,metasenv,_ -> - prerr_endline ( - NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); - assert false - in + let scty, metasenv,_ = + NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) + in + match scty with + | NCic.Prod (_, src, tgt) -> + let tgt = + NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt + in (* - prerr_endline (Printf.sprintf "indicizzo %s %d %d" - (UriManager.string_of_uri uri) arity arg); + debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s" + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1) + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src) + (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt)); *) - index_coercion db c src tgt arity arg) - db clist) - (DB.empty,DB.empty) (CoercDb.to_list ()) + src, tgt + | t -> + debug (lazy ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t)); + assert false + in + index_coercion status "foo" c src tgt arity arg + with + | NCicEnvironment.BadDependency _ + | NCicTypeChecker.TypeCheckerFailure _ -> status) + status clist) + status (CoercDb.to_list odb) +;; + +let look_for_coercion status metasenv subst context infty expty = + let db_src,db_tgt = status#coerc_db in + match + NCicUntrusted.apply_subst subst context infty, + NCicUntrusted.apply_subst subst context expty + with + | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), + (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] + | infty, expty -> + + debug (lazy ("LOOK FOR COERCIONS: " ^ + NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^ + NCicPp.ppterm ~metasenv ~subst ~context expty)); + + let src_class = infty :: NCicUnifHint.eq_class_of status infty in + let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in + + let set_src = + List.fold_left + (fun set infty -> + CoercionSet.union (DB.retrieve_unifiables db_src infty) set) + CoercionSet.empty src_class + in + let set_tgt = + List.fold_left + (fun set expty -> + CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set) + CoercionSet.empty tgt_class + in + + debug (lazy ("CANDIDATES SRC: " ^ + String.concat "," (List.map (fun (name,t,_,_,_,_) -> + name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) + (CoercionSet.elements set_src)))); + debug (lazy ("CANDIDATES TGT: " ^ + String.concat "," (List.map (fun (name,t,_,_,_,_) -> + name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) + (CoercionSet.elements set_tgt)))); + + let candidates = CoercionSet.inter set_src set_tgt in + + debug (lazy ("CANDIDATES: " ^ + String.concat "," (List.map (fun (name,t,_,_,_,_) -> + name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t) + (CoercionSet.elements candidates)))); + + List.map + (fun (name,t,arity,arg,_,_) -> + let ty = + try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t + with NCicTypeChecker.TypeCheckerFailure s -> + prerr_endline ("illtyped coercion: "^Lazy.force s); + prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + assert false + in + let ty, metasenv, args = + NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity + in + + debug (lazy ( + NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ + NCicPp.ppterm ~metasenv ~subst ~context + (NCicUntrusted.mk_appl t args) ^ " --- " ^ + string_of_int (List.length args) ^ " == " ^ string_of_int arg)); + + name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) + (CoercionSet.elements candidates) +;; + +(* CSC: very inefficient implementation! + Enrico, can we use a discrimination tree here? *) +let match_coercion status ~metasenv ~subst ~context t = + let db = + DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) [] + in + (HExtlib.list_findopt + (fun (_,p,arity,cpos,_,_) _ -> + try + let t = + match p,t with + NCic.Appl lp, NCic.Appl lt -> + (match fst (HExtlib.split_nth (List.length lp) lt) with + [t] -> t + | l -> NCic.Appl l) + | _,NCic.Appl (he::_) -> he + | _,_ -> t + in + let b = NCicReduction.alpha_eq metasenv subst context p t in + if not b then None else + let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in + let pis = + let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in + aux ty + in + Some (p,pis - arity - cpos - 1,cpos) + with + Failure _ -> None (* raised by split_nth *) + ) db) ;; -let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty = - let set_src = DB.retrieve_unifiables db_src infty in - let set_tgt = DB.retrieve_unifiables db_tgt expty in - let candidates = CoercionSet.inter set_src set_tgt in - List.map - (fun (t,arity,arg) -> - let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in - let ty, metasenv, args = - NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity - in -(* prerr_endline ( - NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ - NCicPp.ppterm ~metasenv ~subst ~context - (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) - (CoercionSet.elements candidates) +let generate_dot_file status fmt = + let module Pp = GraphvizPp.Dot in + let src_db, _ = status#coerc_db in + let edges = ref [] in + DB.iter src_db (fun _ dataset -> + edges := !edges @ + List.map + (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); + ); + let nodes = + HExtlib.list_uniq + (List.sort compare + (List.flatten + (List.map + (fun (_,a,b) -> + [a;b] + ) + !edges))) + in + let names = ref [] in + let id = ref 0 in + let mangle l = + try List.assoc l !names + with Not_found -> + incr id; + names := (l,"node"^string_of_int!id) :: !names; + List.assoc l !names + in + List.iter + (fun cl -> + Pp.node (mangle cl) + ~attrs:["label",String.concat "\\n" + (List.map (fun t-> + NCicPp.ppterm ~metasenv:[] ~subst:[] + ~context:[] t ~margin:max_int + ) cl)] + fmt) + nodes; + List.iter + (fun ((name,_,_,_),src,tgt) -> + Pp.edge (mangle src) (mangle tgt) + ~attrs:["label", name] fmt) + !edges; ;;