Added coercion handling module

diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile
index 9762f59363f62e062c13d8e18a66e38a3a911212..0002887aa3a37895a5cd0e39a4a3e1d9dd37077b 100644 (file)
--- a/helm/ocaml/cic_unification/Makefile
+++ b/helm/ocaml/cic_unification/Makefile
@@ -7,6 +7,7 @@ INTERFACE_FILES = \
        cicMkImplicit.mli \
        freshNamesGenerator.mli \
        cicUnification.mli \
+       coercGraph.mli \
        cicRefine.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
new file mode 100644 (file)
index 0000000..4dd0507
--- /dev/null
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -0,0 +1,214 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+open Printf;;
+
+ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
+
+(* 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"
+  
+    );
+
+]
+;;
+
+(* 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));
+      None
+;;
+
+(* 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
+  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)
+;;
+
+      
+
+(* 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 ->
+      prerr_endline (sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) 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 
+    obj,univ
+;;
+
+(* removes from l the coercions that are in !coercions *)
+let filter_duplicates l =
+  List.filter (
+      fun (src,_,tgt) ->
+        not (List.exists (fun (s,t,u) -> 
+          UriManager.eq s src && 
+          UriManager.eq t tgt)
+        !coercions))
+  l
+
+(* 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 new_coercions, new_coercions_obj = 
+    List.split (
+      List.map (
+        fun (src, l , tgt) ->
+          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,[]))
+              in
+              let o,u = 
+                List.fold_left (fun (o,u) coer ->
+                  match o with 
+                  |  Cic.Constant (_,Some c,_,[]) ->
+                    generate_composite_closure c (term_of_uri' coer) u
+                  | _ -> 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 = 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) -> Cic.Constant (name,bo,ty,vl)
+                | _ -> assert false 
+              in
+                ((src,tgt,c_uri),(c_uri,named_obj,u))
+      ) todo_list)
+  in
+  coercions := !coercions @ new_coercions;
+  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 *)

diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli
new file mode 100644 (file)
index 0000000..3c03312
--- /dev/null
+++ b/helm/ocaml/cic_unification/coercGraph.mli
@@ -0,0 +1,31 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val look_for_coercion :
+  UriManager.uri -> UriManager.uri -> Cic.term option
+
+val close_coercion_graph:
+  UriManager.uri -> UriManager.uri -> UriManager.uri ->
+    (UriManager.uri * Cic.obj * CicUniv.universe_graph) list