X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=d99fc6f798f67f72ccbee796adc50b8bd0db1474;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e256a19b82545562e990493c72429c7c85b3effc;hpb=1e18535e2671bd62d2ad82ab8d5c5201545d0bdb;p=helm.git diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index e256a19b8..d99fc6f79 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,73 +25,84 @@ 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] @@ -122,8 +133,8 @@ 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 = @@ -134,22 +145,28 @@ let generate_composite_closure c1 c2 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,23 +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, [], - obj_attrs) + 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 + 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 = @@ -188,29 +203,8 @@ let close_coercion_graph src tgt uri = ((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 *)