X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=d99fc6f798f67f72ccbee796adc50b8bd0db1474;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4dd05073b26b3ab2af09899254f7713a6a25a22c;hpb=93e7f6e653ae9e6e17d054ccd3b9aaf801e13bcf;p=helm.git diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 4dd05073b..d99fc6f79 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,76 +25,87 @@ open Printf;; -ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml") +type coercion_search_result = + | SomeCoercion of Cic.term + | NoCoercion + | NotMetaClosed + | NotHandled of string Lazy.t -(* the list of known coercions (MUST be transitively closed) *) -let coercions = ref [ - (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)", - UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con", - UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ; +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () - ( - UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)", - UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)", - UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con" - - ); - ( - UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)", - UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)", - UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con" - - ); - -] -;; (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion src tgt = - try - let s,t,u = - List.find (fun (s,t,_) -> - UriManager.eq s src && - UriManager.eq t tgt) - !coercions + try + let l = + CoercDb.find_coercion + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in - prerr_endline (sprintf ":) TROVATA la coercion %s %s" - (UriManager.name_of_uri src) - (UriManager.name_of_uri tgt)); - Some (CicUtil.term_of_uri (UriManager.string_of_uri u)) - with - Not_found -> - prerr_endline (sprintf ":( NON TROVATA la coercion %s %s" - (UriManager.name_of_uri src) (UriManager.name_of_uri tgt)); - None + match l with + | [] -> + debug_print + (lazy + (sprintf ":-( coercion non trovata da %s a %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + NoCoercion + | [u] -> + debug_print (lazy ( + sprintf ":-) TROVATA 1 coercion da %s a %s: %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt) + (UriManager.name_of_uri u))); + SomeCoercion (CicUtil.term_of_uri u) + | u::_ -> + debug_print (lazy ( + sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt) + (UriManager.name_of_uri u))); + SomeCoercion (CicUtil.term_of_uri u) + with + | CoercDb.EqCarrNotImplemented s -> NotHandled s + | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed ;; +let look_for_coercion src tgt = + let src_uri = CoercDb.coerc_carr_of_term src in + 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 = - let c_from_tgt = - List.filter (fun (f,_,_) -> - UriManager.eq f tgt) - !coercions - in - let c_to_src = - List.filter (fun (_,t,_) -> - UriManager.eq t src) - !coercions +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 - (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) + 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 = @@ -122,34 +133,40 @@ let generate_composite_closure c1 c2 univ = try CicTypeChecker.type_of_aux' [] [] c univ with CicTypeChecker.TypeCheckerFailure s as exn -> - prerr_endline (sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) s); + 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,[]) 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 = +let filter_duplicates l coercions = List.filter ( fun (src,_,tgt) -> not (List.exists (fun (s,t,u) -> - UriManager.eq s src && - UriManager.eq t tgt) - !coercions)) + 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 _ -> assert false + | 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 todo_list = get_closure_coercions src tgt uri in - let todo_list = filter_duplicates todo_list in + 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, new_coercions_obj = List.split ( List.map ( @@ -157,22 +174,21 @@ let close_coercion_graph src tgt uri = match l with | [] -> assert false | he :: tl -> - let term_of_uri' uri = - CicUtil.term_of_uri (UriManager.string_of_uri uri) - in let first_step = - (Cic.Constant ("",Some (term_of_uri' he),Cic.Sort Cic.Prop,[])) + Cic.Constant ("", + Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs) in let o,u = - List.fold_left (fun (o,u) coer -> + List.fold_left (fun (o,univ) coer -> match o with - | Cic.Constant (_,Some c,_,[]) -> - generate_composite_closure c (term_of_uri' coer) u + | 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 = UriManager.name_of_uri src in - let name_tgt = UriManager.name_of_uri tgt 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 = @@ -180,35 +196,15 @@ let close_coercion_graph src tgt uri = in let named_obj = match o with - | Cic.Constant (_,bo,ty,vl) -> Cic.Constant (name,bo,ty,vl) + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) | _ -> assert false in ((src,tgt,c_uri),(c_uri,named_obj,u)) ) todo_list) in - coercions := !coercions @ new_coercions; + List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); new_coercions_obj ;; - - - -(* stupid case *) - -let l = close_coercion_graph - (UriManager.uri_of_string - "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)") - (UriManager.uri_of_string - "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)") - (UriManager.uri_of_string - "cic:/CoRN/algebra/CRings/cr_crr.con") -in - List.iter (fun (u,o,g) -> - prerr_endline (CicPp.ppobj o); - prerr_endline (UriManager.string_of_uri u); - prerr_endline "") - l - - - (* EOF *)