X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=57274e616446b3dab7b416c8db8f71f3aace8441;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=6aad3676d11176fa045cc26ebfed4df9190b92cb;hpb=0575a1cb077087970f311b48f2e45dc4a01a6867;p=helm.git diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 6aad3676d..57274e616 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,47 +25,30 @@ open Printf;; -type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list - -(* 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") ; - - ( - 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" - - ); - -] -;; +let debug = false +let debug_print = if debug then prerr_endline else ignore (* 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 - 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)); + try + let src = CicUtil.uri_of_term src in + let tgt = CicUtil.uri_of_term tgt in + let l = + CoercDb.find_coercion + (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) + in + match l with + | [] -> debug_print ":( coercion non trovata"; None + | u::_ -> + debug_print ( + sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + (List.length l) + (UriManager.name_of_uri src) + (UriManager.name_of_uri tgt) + (UriManager.name_of_uri u)); + Some (CicUtil.term_of_uri u) + with Invalid_argument s -> + debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s); None ;; @@ -73,17 +56,9 @@ let look_for_coercion src tgt = * 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 - in +let get_closure_coercions src tgt uri coercions = + 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 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 ( @@ -122,7 +97,7 @@ 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" + debug_print (sprintf "Generated composite coercion:\n%s\n%s" (CicPp.ppterm c) s); raise exn in @@ -134,13 +109,13 @@ 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)) + coercions)) l (* given a new coercion uri from src to tgt returns @@ -148,8 +123,9 @@ let filter_duplicates l = *) 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,9 +133,7 @@ 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 term_of_uri' uri = CicUtil.term_of_uri uri in let first_step = Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [], obj_attrs) @@ -188,30 +162,8 @@ let close_coercion_graph src tgt uri = ((src,tgt,c_uri),(c_uri,named_obj,u)) ) todo_list) in - coercions := !coercions @ new_coercions @ [src,tgt,uri]; + List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); new_coercions_obj ;; -let get_coercions_list () = - !coercions - - -(* 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 *)