X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcoercGraph.ml;h=cd958a8f62074aa5ba4ac76fb023043b2478587e;hb=2b2b90087f836c2f32291935216549e9370e68c3;hp=3862fcccc8904e206d6a47fc86bfca7eff68c35f;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml index 3862fcccc..cd958a8f6 100644 --- a/helm/ocaml/library/coercGraph.ml +++ b/helm/ocaml/library/coercGraph.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf;; type coercion_search_result = @@ -34,7 +36,6 @@ type coercion_search_result = let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () - (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion src tgt = try @@ -75,188 +76,6 @@ let look_for_coercion src tgt = let tgt_uri = CoercDb.coerc_carr_of_term tgt in look_for_coercion src_uri tgt_uri -(* given the new coercion uri from src to tgt returns the list - * of new coercions to create. hte list elements are - * (source, list of coercions to follow, target) - *) -let get_closure_coercions src tgt uri coercions = - let eq_carr s t = - try - CoercDb.eq_carr s t - with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false - in - match src,tgt with - | CoercDb.Uri _, CoercDb.Uri _ -> - let c_from_tgt = - List.filter (fun (f,_,_) -> eq_carr f tgt) coercions - in - let c_to_src = - List.filter (fun (_,t,_) -> eq_carr t src) coercions - in - (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @ - (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @ - (List.fold_left ( - fun l (s,_,u1) -> - ((List.map (fun (_,t,u2) -> - (s,[u1;uri;u2],t) - )c_from_tgt)@l) ) - [] c_to_src) - | _ -> [] (* do not close in case source or target is not an indty ?? *) -;; - -let obj_attrs = [`Class `Coercion; `Generated] - -(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure c1 c2 univ = - let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in - let rec mk_rels n = - match n with - | 0 -> [] - | _ -> (Cic.Rel n) :: (mk_rels (n-1)) - in - let rec compose k = - function - | Cic.Prod (name,src,tgt) -> - let name = - match name with - | Cic.Anonymous -> Cic.Name "x" - | _ -> name - in - Cic.Lambda (name,src,compose (k+1) tgt) - | Cic.Appl (he::tl) -> - Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) - | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) - in - let c = compose 0 c1_ty in - let c_ty,univ = - try - CicTypeChecker.type_of_aux' [] [] c univ - with CicTypeChecker.TypeCheckerFailure s as exn -> - debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) (Lazy.force s))); - raise exn - in - let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types c_ty - in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in - obj,univ -;; - -(* removes from l the coercions that are in !coercions *) -let filter_duplicates l coercions = - List.filter ( - fun (src,_,tgt) -> - not (List.exists (fun (s,t,u) -> - CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt) - coercions)) - l - -let term_of_carr = function - | CoercDb.Uri u -> CicUtil.term_of_uri u - | CoercDb.Sort s -> Cic.Sort s - | CoercDb.Term _ -> assert false - -(* given a new coercion uri from src to tgt returns - * a list of (new coercion uri, coercion obj, universe graph) - *) -let close_coercion_graph src tgt uri = - (* check if the coercion already exists *) - let coercions = CoercDb.to_list () in - let todo_list = get_closure_coercions src tgt uri coercions in - let todo_list = filter_duplicates todo_list coercions in - let new_coercions = - List.map ( - fun (src, l , tgt) -> - match l with - | [] -> assert false - | he :: tl -> - let first_step = - Cic.Constant ("", - Some (term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs) - in - let o,_ = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (term_of_carr (CoercDb.Uri - coer)) univ - | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl - in - let name_src = CoercDb.name_of_carr src in - let name_tgt = CoercDb.name_of_carr tgt in - let name = name_tgt ^ "_of_" ^ name_src in - let buri = UriManager.buri_of_uri uri in - let c_uri = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - let named_obj = - match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) - | _ -> assert false - in - ((src,tgt,c_uri,named_obj)) - ) todo_list - in - new_coercions -;; - -let coercion_hashtbl = UriManager.UriHashtbl.create 3 - -let add_coercion uri = - let coer_ty,_ = - CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri) - CicUniv.empty_ugraph - in - (* we have to get the source and the tgt type uri - * in Coq syntax we have already their names, but - * since we don't support Funclass and similar I think - * all the coercion should be of the form - * (A:?)(B:?)T1->T2 - * So we should be able to extract them from the coercion type - *) - let extract_last_two_p ty = - let rec aux = function - | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2)) - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false - in - aux ty - in - let ty_src,ty_tgt = extract_last_two_p coer_ty in - let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in - let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in - let new_coercions = close_coercion_graph src_uri tgt_uri uri in - UriManager.UriHashtbl.add coercion_hashtbl uri - (List.map (fun (_,_,uri,_) -> uri) new_coercions); - CoercDb.add_coercion (src_uri,tgt_uri,uri); - List.iter - (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) - new_coercions; - List.map (fun (_,_,uri,o) -> uri,o) new_coercions - - -let remove_coercion uri = - try - let res = UriManager.UriHashtbl.find coercion_hashtbl uri in - UriManager.UriHashtbl.remove coercion_hashtbl uri; - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); - List.iter - (fun u -> - CoercDb.remove_coercion - (fun (_,_,u1) -> UriManager.eq u u1)) - res; - with - Not_found -> () - -let remove_all () = - CoercDb.remove_coercion (fun (_,_,u1) -> true) - let is_a_coercion t = try let uri = CicUtil.uri_of_term t in @@ -266,13 +85,13 @@ let is_a_coercion t = let source_of t = try let uri = CicUtil.uri_of_term t in - term_of_carr (fst (CoercDb.get_carr uri)) + CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) let target_of t = try let uri = CicUtil.uri_of_term t in - term_of_carr (snd (CoercDb.get_carr uri)) + CoercDb.term_of_carr (snd (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) (* EOF *)