]> matita.cs.unibo.it Git - helm.git/commitdiff
improved coercions support:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
- multiple coercions from the same carrier are allowed
- coercions are hidden from the proof too
- a new function to print proof in text mode added

19 files changed:
helm/software/components/acic_content/acic2content.ml
helm/software/components/acic_content/acic2content.mli
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/acic_content/termAcicContent.mli
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/content_pres/.depend
helm/software/components/content_pres/Makefile
helm/software/components/content_pres/boxPp.ml
helm/software/components/content_pres/boxPp.mli
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/content_pres/objPp.ml [new file with mode: 0644]
helm/software/components/content_pres/objPp.mli [new file with mode: 0644]
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/library/cicCoercion.ml
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/coercGraph.ml
helm/software/components/library/coercGraph.mli
helm/software/components/library/librarySync.ml

index e72d466d537fb7724dd91daadbe99f0886dee46f..23d6447863a9f9335f101d240e1edfa51ca885dd 100644 (file)
@@ -44,6 +44,8 @@ let conclude_prefix = "concl:";;
 let premise_prefix = "prem:";;
 let lemma_prefix = "lemma:";;
 
+let hide_coercions = ref true;;
+
 (* e se mettessi la conversione di BY nell'apply_context ? *)
 (* sarebbe carino avere l'invariante che la proof2pres
 generasse sempre prove con contesto vuoto *)
@@ -500,13 +502,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
         else raise Not_a_proof 
     | C.AAppl (id,li) ->
-        (try rewrite 
+        (try coercion 
+           seed li ~ids_to_inner_types ~ids_to_inner_sorts
+         with NotApplicable ->
+         try rewrite 
            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try inductive 
           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
-        try transitivity 
+         try transitivity 
            seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
           let subproofs, args =
@@ -795,6 +800,22 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
   | _ -> raise NotApplicable
 
+and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+  match li with
+    | ((Cic.AConst _) as he)::tl
+    | ((Cic.AMutInd _) as he)::tl
+    | ((Cic.AMutConstruct _) as he)::tl when 
+       CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+       !hide_coercions ->
+        let rec last =
+         function
+            [] -> assert false
+          | [t] -> t
+          | _::tl -> last tl
+        in
+          acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+    | _ -> raise NotApplicable
+
 and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
   let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
   let module C2A = Cic2acic in
index e1dfb82de1e118e8ecda4d89bb06dde1a97abc26..32ce688590559dc94e2e19139d18872122a96f10 100644 (file)
@@ -31,3 +31,6 @@ val annobj2content :
 
 val map_sequent :
   Cic.annconjecture -> Cic.annterm Content.conjecture
+
+val hide_coercions: bool ref
+
index a25730e4d1fa0aed8e2279694d2d60d3a7d7deb7..7948f2654ac51aa29cc79d13f12bbb3dd6a71534 100644 (file)
@@ -66,7 +66,6 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
-let hide_coercions = ref true;;
 
 let ast_of_acic0 term_info acic k =
   let k = k term_info in
@@ -123,7 +122,7 @@ let ast_of_acic0 term_info acic k =
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
        if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
-          !hide_coercions
+          !Acic2content.hide_coercions
        then
         let rec last =
          function
index 214d7f5d2e9f228dc677c50100ca6a3b8aa0fb78..49358bfce00a8b546e71c787b1afc1c68fbaa4b6 100644 (file)
@@ -23,7 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-val hide_coercions: bool ref
 
   (** {2 Persistant state handling} *)
 
index 90643164d576bf14b5f309fc4011104bfa1d8b1b..48ae522f4c9b4b170111a2dabff110e93388d863 100644 (file)
@@ -261,6 +261,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
      ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
+    let try_coercion t subst metasenv context ugraph coercion_tgt c =
+      let coerced = Cic.Appl[c;t] in
+      try
+        let newt,_,subst,metasenv,ugraph = 
+          type_of_aux subst metasenv context coerced ugraph 
+        in
+        let newt, tty, subst, metasenv, ugraph = 
+          avoid_double_coercion context subst metasenv ugraph newt coercion_tgt
+        in
+          Some (newt, tty, subst, metasenv, ugraph)
+      with 
+      | RefineFailure _ | Uncertain _ -> None
+    in
     let module C = Cic in
     let module S = CicSubstitution in
     let module U = UriManager in
@@ -392,15 +405,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context 
                            subst coercion_src context ^ " that is not a sort")))
-                    | CoercGraph.SomeCoercion c -> 
-                       let newt,_,subst,metasenv,ugraph = 
-                         type_of_aux subst metasenv context (Cic.Appl[c;t])
-                          ugraph in
-                       let newt, tty, subst, metasenv, ugraph = 
-                         avoid_double_coercion context subst metasenv ugraph
-                          newt coercion_tgt
-                       in
-                        newt, tty, subst, metasenv, ugraph)
+                    | CoercGraph.SomeCoercion candidates -> 
+                        let selected = 
+                          HExtlib.list_findopt
+                            (try_coercion 
+                              t subst metasenv context ugraph coercion_tgt)
+                            candidates
+                        in
+                        match selected with
+                        | Some x -> x
+                        | None -> 
+                            enrich localization_tbl t
+                              (RefineFailure 
+                                (lazy ("The term " ^ 
+                                CicMetaSubst.ppterm_in_context 
+                                  subst t context ^ 
+                                  " is not a type since it has type " ^ 
+                                  CicMetaSubst.ppterm_in_context
+                                  subst coercion_src context ^ 
+                                  " that is not a sort")))) 
             in
             let s',sort1,subst',metasenv',ugraph1 = 
               type_of_aux subst metasenv context s ugraph 
@@ -439,15 +462,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                       CoercGraph.look_for_coercion coercion_src coercion_tgt
                      in
                       match boh with
-                      | CoercGraph.SomeCoercion c -> 
-                        let newt,_,subst',metasenv',ugraph1 = 
-                         type_of_aux subst' metasenv' context (Cic.Appl[c;s'])
-                          ugraph1 in
-                        let newt, tty, subst', metasenv', ugraph1 = 
-                          avoid_double_coercion context subst' metasenv'
-                           ugraph1 newt coercion_tgt 
-                        in
-                         newt, tty, subst', metasenv', ugraph1
                       | CoercGraph.NoCoercion
                       |  CoercGraph.NotHandled _ ->
                         enrich localization_tbl s'
@@ -465,6 +479,24 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           " is not a type since it has type " ^ 
                           CicMetaSubst.ppterm_in_context 
                            subst coercion_src context ^ " that is not a sort")))
+                      | CoercGraph.SomeCoercion candidates -> 
+                        let selected = 
+                          HExtlib.list_findopt
+                            (try_coercion 
+                              s' subst' metasenv' context ugraph1 coercion_tgt)
+                            candidates
+                        in
+                        match selected with
+                        | Some x -> x
+                        | None -> 
+                           enrich localization_tbl s'
+                            (RefineFailure 
+                             (lazy ("The term " ^ 
+                              CicMetaSubst.ppterm_in_context subst s' context ^ 
+                              " is not a type since it has type " ^ 
+                              CicMetaSubst.ppterm_in_context 
+                              subst coercion_src context ^ 
+                              " that is not a sort")))
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
             let t',type2,subst'',metasenv'',ugraph2 =
@@ -1100,31 +1132,33 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
       let tgt_carr = CicMetaSubst.apply_subst subst ty in
       (match CoercGraph.look_for_coercion source_carr tgt_carr 
       with
-      | CoercGraph.SomeCoercion c -> 
-         let newt =
-          match c with
-             Cic.Appl l -> Cic.Appl (l @ [head])
-           | _ -> Cic.Appl [c;head]
+      | CoercGraph.SomeCoercion candidates -> 
+         let selected =  
+           HExtlib.list_findopt
+             (fun c ->
+               let newt =
+                match c with
+                | Cic.Appl l -> Cic.Appl (l @ [head])
+                | _ -> Cic.Appl [c;head]
+               in
+               (try
+                 let newt,_,subst,metasenv,ugraph = 
+                   type_of_aux subst metasenv context newt ugraph in
+                 let subst, metasenv, ugraph = 
+                  fo_unif_subst subst context metasenv newt t ugraph
+                 in
+                 debug_print 
+                   (lazy 
+                     ("packing: " ^ 
+                       CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+                 Some (newt, ty, subst, metasenv, ugraph)
+               with RefineFailure _ | Uncertain _ -> None))
+             candidates
          in
-          (try
-            let newt,_,subst,metasenv,ugraph = 
-              type_of_aux subst metasenv context newt ugraph in
-            let subst, metasenv, ugraph = 
-             fo_unif_subst subst context metasenv newt t ugraph
-            in
-            debug_print 
-              (lazy 
-                ("packing: " ^ 
-                  CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
-            newt, ty, subst, metasenv, ugraph
-           with
-              RefineFailure _ ->
-               prerr_endline ("#### Coercion not packed (Refine_failure): " ^
-                CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
-               assert false
-            | Uncertain _ ->
-               prerr_endline ("#### Coercion not packed (Uncerctain case): " ^
-                CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt);
+         (match selected with
+         | Some x -> x
+         | None -> 
+              prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
                assert false)
       | _ -> assert false) (* the composite coercion must exist *)
     else
@@ -1238,29 +1272,40 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                                  context ^ " but is here used with type " ^
                                 CicMetaSubst.ppterm_in_context subst s context
                                  (* "\nReason: " ^ Lazy.force e*))))
-                       | CoercGraph.SomeCoercion c -> 
-                          try
-                           let newt,newhety,subst,metasenv,ugraph = 
-                            type_of_aux subst metasenv context
-                             (Cic.Appl[c;hete]) ugraph in
-                           let newt, _, subst, metasenv, ugraph = 
-                            avoid_double_coercion context subst metasenv
-                             ugraph newt tgt_carr in
-                            let subst,metasenv,ugraph1 = 
-                             fo_unif_subst subst context metasenv 
-                                newhety s ugraph
-                            in
-                             newt, subst, metasenv, ugraph
-                          with _ ->
-                           enrich localization_tbl hete
-                             ~f:(fun _ ->
-                               (lazy ("The term " ^
+                       | CoercGraph.SomeCoercion candidates -> 
+                           let selected = 
+                             HExtlib.list_findopt
+                               (fun c -> 
+                                try
+                                 let t = Cic.Appl[c;hete] in
+                                 let newt,newhety,subst,metasenv,ugraph = 
+                                  type_of_aux subst metasenv context
+                                   t ugraph 
+                                 in
+                                 let newt, _, subst, metasenv, ugraph = 
+                                  avoid_double_coercion context subst metasenv
+                                   ugraph newt tgt_carr 
+                                 in
+                                 let subst,metasenv,ugraph1 = 
+                                   fo_unif_subst subst context metasenv 
+                                      newhety s ugraph
+                                 in
+                                  Some (newt, subst, metasenv, ugraph)
+                                with Uncertain _ | RefineFailure _ -> None)
+                               candidates
+                           in
+                           (match selected with
+                           | Some x -> x
+                           | None ->  
+                              enrich localization_tbl hete
+                               ~f:(fun _ ->
+                                (lazy ("The term " ^
                                  CicMetaSubst.ppterm_in_context subst hete
                                   context ^ " has type " ^
                                  CicMetaSubst.ppterm_in_context subst hety
                                   context ^ " but is here used with type " ^
                                  CicMetaSubst.ppterm_in_context subst s context
-                                  (* "\nReason: " ^ Lazy.force e*)))) exn)
+                                  (* "\nReason: " ^ Lazy.force e*)))) exn))
                      | exn ->
                         enrich localization_tbl hete
                          ~f:(fun _ ->
index 60e25ecd80fab06b1973720ef9bbd3068f8a9876..d16c75a761cd70b9bb06ddbdbf9e171cb0029079 100644 (file)
@@ -30,6 +30,8 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
     cicNotationPres.cmi box.cmi content2pres.cmi 
 content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
     cicNotationPres.cmx box.cmx content2pres.cmi 
+objPp.cmo: content2pres.cmi boxPp.cmi objPp.cmi 
+objPp.cmx: content2pres.cmx boxPp.cmx objPp.cmi 
 sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
     box.cmi sequent2pres.cmi 
 sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
index 980e8c25a2c9a9841cf41770fa8880ab57c733c2..5613ff9ffc59abad275425c3ff72368cb0fd6ff9 100644 (file)
@@ -12,6 +12,7 @@ INTERFACE_FILES =             \
        cicNotationPres.mli     \
        boxPp.mli               \
        content2pres.mli        \
+       objPp.mli               \
        sequent2pres.mli        \
        $(NULL)
 IMPLEMENTATION_FILES =         \
index 7a2fa9912f31144cb135e72441fe03f7b1bfd6fc..2957a3975446f48c3c0c69e763d3ba45eccd43cc 100644 (file)
@@ -93,7 +93,7 @@ let fixed_rendering s =
   let s_len = String.length s in
   (fun _ -> s_len, [s])
 
-let render_to_strings size markup =
+let render_to_strings choose_action size markup =
   let max_size = max_int in
   let rec aux_box =
     function
@@ -101,7 +101,7 @@ let render_to_strings size markup =
     | Box.Space _ -> fixed_rendering string_space
     | Box.Ink _ -> fixed_rendering string_ink
     | Box.Action (_, []) -> assert false
-    | Box.Action (_, hd :: _) -> aux_box hd
+    | Box.Action (_, l) -> aux_box (choose_action l)
     | Box.Object (_, o) -> aux_mpres o
     | Box.H (attrs, children) ->
         let spacing = want_spacing attrs in
@@ -236,6 +236,6 @@ let render_to_strings size markup =
   in
   snd (aux_mpres markup size)
 
-let render_to_string size markup =
-  String.concat "\n" (render_to_strings size markup)
+let render_to_string choose_action size markup =
+  String.concat "\n" (render_to_strings choose_action size markup)
 
index 6b7c3cec833a9bd4da3db1fd1ab563421d27f2ac..fe05e24d9e8af9da1bc5a22f14c82cb62d4e43ab 100644 (file)
  *)
 
   (** @return rows list of rows *)
-val render_to_strings:  int -> CicNotationPres.markup -> string list
+val render_to_strings: 
+  (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
+  int -> CicNotationPres.markup -> string list
 
   (** helper function
    * @return s, concatenation of the return value of render_to_strings above
    * with newlines as separators *)
-val render_to_string:   int -> CicNotationPres.markup -> string
+val render_to_string:
+  (CicNotationPres.boxml_markup Mpresentation.mpres Box.box list -> CicNotationPres.boxml_markup) -> 
+  int -> CicNotationPres.markup -> string
 
index 67340d37a255662b1270a26ce757c18d82768de7..fb459a94e36bada765133844b82235626573770b 100644 (file)
@@ -125,7 +125,7 @@ let _ =
       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
     ]
 
-let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ]+
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
 
 let regexp uri =
   ("cic:/" | "theory:/")              (* schema *)
diff --git a/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml
new file mode 100644 (file)
index 0000000..1eb47db
--- /dev/null
@@ -0,0 +1,30 @@
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+let obj_to_string n obj =
+  let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in
+  let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
+  let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
+  BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
diff --git a/helm/software/components/content_pres/objPp.mli b/helm/software/components/content_pres/objPp.mli
new file mode 100644 (file)
index 0000000..e007c6e
--- /dev/null
@@ -0,0 +1,27 @@
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+val obj_to_string:   int -> Cic.obj -> string
+
index ad5423b3e77097bbf9f603d2bcf05bcad15b94af..ebe7df36977901b7b8351f3af62db67f45a30306 100644 (file)
@@ -423,8 +423,10 @@ let refinement_toolkit = {
 let eval_coercion status ~add_composites uri =
  let status,compounds =
   GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
- let moo_content = coercion_moo_statement_of uri in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
+ let moo_content = 
+   List.map coercion_moo_statement_of (uri::compounds)
+ in
+ let status = GrafiteTypes.add_moo_content moo_content status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
    compounds
 
@@ -517,7 +519,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
           let obj,_ = 
             CicEnvironment.get_cooked_obj  CicUniv.empty_ugraph uri in
           let attrs = CicUtil.attributes_of_obj obj in
-          List.mem (`Class `Projection) attrs
+          List.mem (`Class `Coercion) attrs
         with Not_found -> assert false
       in
       (* looking at the fields we can know the 'wanted' coercions, but not the 
@@ -534,8 +536,7 @@ let add_coercions_of_record_to_moo obj lemmas status =
             | _ -> None) 
           fields
       in
-      (*
-      prerr_endline "wanted coercions:";
+      (*prerr_endline "wanted coercions:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
         wanted_coercions; *)
@@ -544,17 +545,22 @@ let add_coercions_of_record_to_moo obj lemmas status =
           (HExtlib.filter_map 
             (fun uri ->
               let is_a_wanted_coercion = 
-                List.exists (UriManager.eq uri) wanted_coercions in
-              if is_a_coercion uri && is_a_wanted_coercion then
+                List.exists (UriManager.eq uri) wanted_coercions 
+              in
+              if is_a_coercion uri || is_a_wanted_coercion then
                 Some (uri, coercion_moo_statement_of uri)
               else
                 None) 
             lemmas)
       in
-      (* prerr_endline "actual coercions:";
+      (*prerr_endline "actual coercions:";
+      List.iter 
+        (fun u -> prerr_endline (UriManager.string_of_uri u)) 
+        coercions; 
+      prerr_endline "lemmas was:";
       List.iter 
         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
-        coercions; *)
+        lemmas; *)
       let status = GrafiteTypes.add_moo_content moo_content status in 
       {status with 
         GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, 
index 7e36ac1aa5000d5c7ff2bb7dbc7627aa3d496e70..9a9ddb62bd6e797a89eed53de5e96997a5b76a8a 100644 (file)
@@ -42,19 +42,31 @@ let get_closure_coercions src tgt uri coercions =
   match src,tgt with
   | CoercDb.Uri _, CoercDb.Uri _ ->
       let c_from_tgt = 
-        List.filter (fun (f,_,_) -> eq_carr f tgt) coercions 
+        List.filter 
+          (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) 
+          coercions 
       in
       let c_to_src = 
-        List.filter (fun (_,t,_) -> eq_carr t src) coercions 
+        List.filter 
+          (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt)) 
+          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)
+        (HExtlib.flatten_map 
+          (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+        (HExtlib.flatten_map 
+          (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+        (HExtlib.flatten_map 
+          (fun (s,_,u1l) ->
+            HExtlib.flatten_map 
+              (fun (_,t,u2l) ->
+                HExtlib.flatten_map
+                  (fun u1 ->
+                    List.map 
+                      (fun u2 -> (s,[u1;uri;u2],t)) 
+                      u2l)
+                  u1l) 
+              c_from_tgt) 
+          c_to_src)
   | _ -> [] (* do not close in case source or target is not an indty ?? *)
 ;;
 
@@ -169,13 +181,50 @@ let generate_composite_closure rt c1 c2 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) -> 
+      fun (src,l1,tgt) ->
+        not (List.exists (fun (s,t,l2) -> 
           CoercDb.eq_carr s src && 
-          CoercDb.eq_carr t tgt)
+          CoercDb.eq_carr t tgt &&
+          try 
+            List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+          with
+          | Invalid_argument "List.for_all2" -> false)
         coercions))
   l
 
+let mangle s t l = 
+  (*List.fold_left
+    (fun s x -> s ^ "_" ^ x)
+    (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*)
+  s ^ "_OF_" ^ t
+;;
+
+exception ManglingFailed of string 
+
+let number_if_already_defined buri name =
+  let rec aux n =
+    let suffix = if n > 0 then string_of_int n else "" in
+    let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in
+    try
+      let _  = Http_getter.resolve ~writable:true uri in
+      if Http_getter.exists uri then
+        begin
+          HLog.warn ("Uri " ^ uri ^ " already exists.");
+          if n < 10 then aux (n+1) else 
+            raise 
+              (ManglingFailed 
+                ("Unable to give an altenative name to " ^ 
+                  buri ^ "/" ^ name ^ ".con"))
+        end
+      else
+        UriManager.uri_of_string uri
+    with 
+    | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri
+    | Http_getter_types.Unresolvable_URI _ -> assert false
+  in
+  aux 0
+;;
+  
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
@@ -184,44 +233,45 @@ let close_coercion_graph rt src tgt uri =
   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 = 
-    HExtlib.filter_map (
-      fun (src, l , tgt) ->
-        try 
-          (match l with
-          | [] -> assert false 
-          | he :: tl ->
-              let first_step = 
-                Cic.Constant ("", 
-                  Some (CoercDb.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 rt c 
-                          (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+  try
+    let new_coercions = 
+      HExtlib.filter_map (
+        fun (src, l , tgt) ->
+          try 
+            (match l with
+            | [] -> assert false 
+            | he :: tl ->
+                let first_step = 
+                  Cic.Constant ("", 
+                    Some (CoercDb.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 rt c 
+                            (CoercDb.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 by = List.map UriManager.name_of_uri l in
+                let name = mangle name_tgt name_src by in
+                let buri = UriManager.buri_of_uri uri in
+                let c_uri = number_if_already_defined buri name in
+                let named_obj = 
+                  match o with
+                  | Cic.Constant (_,bo,ty,vl,attrs) ->
+                      Cic.Constant (name,bo,ty,vl,attrs)
                   | _ -> 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
-                Some ((src,tgt,c_uri,named_obj)))
-        with UnableToCompose -> None
-    ) todo_list
-  in
-  new_coercions
+                in
+                  Some ((src,tgt,c_uri,named_obj)))
+          with UnableToCompose -> None
+      ) todo_list
+    in
+    new_coercions
+  with ManglingFailed s -> HLog.error s; []
 ;;
 
index 8b7982ea0576645c531fc82e5c599633ffcf39b2..25bdab18005033147bc31287db0fbfb8ba571f83 100644 (file)
@@ -72,28 +72,51 @@ let eq_carr src tgt =
 let to_list () =
   !db
 
-let add_coercion c =
-  db := c :: !db
-
-let remove_coercion p = 
-  db := List.filter (fun u -> not(p u)) !db
+let rec myfilter p = function
+  | [] -> []
+  | (s,t,l)::tl ->
+      let l = List.filter (fun u -> not (p (s,t,u))) l in
+      if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
+;;
+  
+let remove_coercion p = db := myfilter p !db;;
 
 let find_coercion f =
-  List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+  List.flatten 
+    (List.map 
+      (fun (_,_,x) -> x) 
+      (List.filter (fun (s,t,_) -> f (s,t)) !db))
+;;
 
-let is_a_coercion u =
-  List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+let is_a_coercion u = 
+  List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
+;;
 
 let get_carr uri =
   try
-    let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+    let src, tgt, _ = 
+      List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db 
+    in
     src, tgt
   with Not_found -> assert false (* uri must be a coercion *)
+;;
 
 let term_of_carr = function
   | Uri u -> CicUtil.term_of_uri u
   | Sort s -> Cic.Sort s
   | Term _ -> assert false
+;;
   
+let add_coercion (src,tgt,u) =
+  let f s t = eq_carr s src && eq_carr t tgt in
+  let where = List.filter (fun (s,t,_) -> f s t) !db in
+  let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
+  match where with
+  | [] -> db := (src,tgt,[u]) :: !db
+  | (src,tgt,l)::tl ->
+      assert (tl = []); (* not sure, this may be a feature *)
+      db := (src,tgt,u::l)::tl @ rest
+;;
+
 
 
index 1f5df89334352f3a299d5ee83ec8f044005c68a3..95dd96c0b18a2fd9a3849a8b707b74b1e1a7e38a 100644 (file)
@@ -45,7 +45,7 @@ val name_of_carr: coerc_carr -> string
 
 val to_list:
   unit -> 
-    (coerc_carr * coerc_carr * UriManager.uri) list
+    (coerc_carr * coerc_carr * UriManager.uri list) list
 
 val add_coercion:
   coerc_carr * coerc_carr * UriManager.uri -> unit
index 06d7a12d3ea3a5e250ae595dc747d906e75b0857..6d7a670efc688d641f2927ce62e03af1600f6076 100644 (file)
@@ -28,7 +28,7 @@
 open Printf;;
 
 type coercion_search_result = 
-  | SomeCoercion of Cic.term
+  | SomeCoercion of Cic.term list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
@@ -65,34 +65,29 @@ let look_for_coercion src tgt =
                (CoercDb.name_of_carr src) 
                (CoercDb.name_of_carr tgt)));
          None
-     | [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)));
-         Some u
-     | u::_ -> 
-         debug_print (lazy (
-           sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
              (List.length l)
              (CoercDb.name_of_carr src) 
-             (CoercDb.name_of_carr tgt)
-             (UriManager.name_of_uri u)));
-         Some u
+             (CoercDb.name_of_carr tgt)));
+         Some l
     in
      (match uri with
          None -> NoCoercion
-       | Some u ->
-          let c = CicUtil.term_of_uri u in
-          let arity = arity_of c in
-          let args = mk_implicits (arity - 1) in
-          let newt =
-           match args with
-              [] -> c
-            | _ -> Cic.Appl (c::args)
+       | Some ul ->
+          let cl = List.map CicUtil.term_of_uri ul in
+          let arityl = List.map arity_of cl in
+          let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+          let newtl =
+            List.map2 
+              (fun args c -> 
+                match args with
+                |  [] -> c
+                | _ -> Cic.Appl (c::args))
+              argsl cl
           in
-           SomeCoercion newt)
+           SomeCoercion newtl)
   with
     | CoercDb.EqCarrNotImplemented s -> NotHandled s
     | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
@@ -131,10 +126,14 @@ let generate_dot_file () =
   in
   let conclusion = " } \n" in
   let data = List.fold_left 
-    (fun acc (src,tgt,c) -> 
-      acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
-      CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
-      "\"];\n") "" l 
+    (fun acc (src,tgt,cl) -> 
+      List.fold_left 
+        (fun acc c ->
+          acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
+          CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
+          "\"];\n")
+        acc cl)
+      "" l 
   in
   preamble ^ data ^ conclusion
   
index 283d8a4844f3d26198bb80e3fee1e65d555a792f..691bafd4c9c404ce7b259f152eb710eff4813ee0 100644 (file)
@@ -26,7 +26,7 @@
 (* This module implements the Query interface to the Coercion Graph *)
 
 type coercion_search_result = 
-  | SomeCoercion of Cic.term
+  | SomeCoercion of Cic.term list
   | NoCoercion
   | NotMetaClosed
   | NotHandled of string Lazy.t
index 413cc986cbbc6188994a2e13f0c10e407e046b31..a59294aaa73f7eb3173b1d6047809f27061fee76 100644 (file)
@@ -217,60 +217,75 @@ let add_coercion ~add_composites refinement_toolkit uri =
     in
     aux ty
   in
+  let already_in = 
+     List.exists 
+      (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+      (CoercDb.to_list ())
+  in
   let ty_src, ty_tgt = extract_last_two_p coer_ty in
   let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
   let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
-  let new_coercions = 
-    CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in
-  let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
-  (* update the DB *)
-  List.iter 
-    (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
-      new_coercions;
-  if 
-    List.exists 
-      (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr)
-      (CoercDb.to_list ())
-  then
-    begin
-      assert (new_coercions = []);
-      []
-    end
+  if not add_composites then
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
-    begin
-      CoercDb.add_coercion (src_carr, tgt_carr, uri);
-      (* add the composites obj and they eventual lemmas *)
-      let lemmas = 
-        if add_composites then
-          List.fold_left
-            (fun acc (_,_,uri,obj) -> 
-              add_single_obj uri obj refinement_toolkit;
-              uri::acc) 
-            composite_uris new_coercions
-        else
-          []
-      in
-      (* store that composite_uris are related to uri. the first component is
-       * the stuff in the DB while the second is stuff for remove_obj *)
-      (* 
-         prerr_endline ("adding: " ^ 
-           string_of_bool add_composites ^ UriManager.string_of_uri uri);
-         List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-          composite_uris; 
-      *)
-      UriManager.UriHashtbl.add coercion_hashtbl uri 
-        (composite_uris,if add_composites then composite_uris else []);
-      lemmas
-    end
+    let new_coercions = 
+      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+    in
+    let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+    if already_in then
+      (* this if starts here just to be sure the closure function works fine *)
+      begin 
+        assert (new_coercions = []); 
+        HLog.warn
+          (UriManager.string_of_uri uri ^ 
+            " is already declared as a coercion! skipping...");
+        [] 
+      end
+    else
+      begin
+        (* update the DB *)
+        List.iter 
+          (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
+          new_coercions;
+        CoercDb.add_coercion (src_carr, tgt_carr, uri);
+        (* add the composites obj and they eventual lemmas *)
+        let lemmas = 
+          if add_composites then
+            List.fold_left
+              (fun acc (_,_,uri,obj) -> 
+                add_single_obj uri obj refinement_toolkit;
+                uri::acc) 
+              [] new_coercions
+          else
+            []
+        in
+        (* store that composite_uris are related to uri. the first component is
+         * the stuff in the DB while the second is stuff for remove_obj *)
+        (* 
+           prerr_endline ("adding: " ^ 
+             string_of_bool add_composites ^ UriManager.string_of_uri uri);
+           List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+            composite_uris; 
+        *)
+        UriManager.UriHashtbl.add coercion_hashtbl uri 
+          (composite_uris,if add_composites then composite_uris else []);
+        (*
+        prerr_endline ("lemmas:");
+          List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+          lemmas;
+        prerr_endline ("lemmas END");*)
+        lemmas
+      end
+;;
 
 let remove_coercion uri =
   try
     let (composites_in_db, composites_in_lib) = 
       UriManager.UriHashtbl.find coercion_hashtbl uri 
     in
-    prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+    (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-      composites_in_db;
+      composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
     CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
     (* remove from the DB *) 
@@ -297,7 +312,15 @@ let generate_projections refinement_toolkit uri fields =
         add_single_obj uri obj refinement_toolkit;
         let composites = 
          if coercion then
-            add_coercion ~add_composites:true refinement_toolkit uri
+            begin
+              prerr_endline ("composite for " ^ UriManager.string_of_uri uri);
+              let x = add_coercion ~add_composites:true refinement_toolkit uri
+              in
+              prerr_endline ("are: ");
+              List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
+              prerr_endline "---";
+              x
+            end
           else  
             []
         in
@@ -336,7 +359,7 @@ let add_obj refinement_toolkit uri obj =
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @ 
           generate_elimination_principles uri refinement_toolkit;
-       uris := !uris @ generate_inversion refinement_toolkit uri obj;
+        uris := !uris @ generate_inversion refinement_toolkit uri obj;
         let rec get_record_attrs =
           function
           | [] -> None