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=8a6e8a1c818f5f19a99ff816531a19eb9f3561fc;hpb=5d492df3e2715395a554f64dc3f040e13f892974;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 8a6e8a1c8..04fddee83 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -14,10 +14,15 @@ let debug s = prerr_endline (Lazy.force s);; let debug _ = ();; -module COT : Set.OrderedType with type t = NCic.term * int * int = +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) @@ -29,26 +34,31 @@ type db = DB.t * DB.t 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. < coerc_db : db; .. > as 'status -> 'self - = fun o -> {< db = o#coerc_db >} + : 'status. #g_status as 'status -> 'self + = 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) 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 status#set_coerc_db (db_src, db_tgt) @@ -60,7 +70,7 @@ let index_old_db odb (status : #status) = List.fold_left (fun status (uri,_,arg) -> try - let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in + 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 @@ -84,7 +94,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) @@ -94,26 +104,52 @@ let index_old_db odb (status : #status) = let look_for_coercion status metasenv subst context infty expty = let db_src,db_tgt = status#coerc_db in - match infty, expty with + 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 set_src = DB.retrieve_unifiables db_src infty in - let set_tgt = DB.retrieve_unifiables db_tgt expty in + 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 (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 -> @@ -131,6 +167,89 @@ 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) ;; + +(* 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 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; +;;