]> matita.cs.unibo.it Git - helm.git/commitdiff
Coercions are now generalized to the general form
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Aug 2007 13:36:44 +0000 (13:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Aug 2007 13:36:44 +0000 (13:36 +0000)
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax

   coercion uri arity saturations

where:
 1. arity and saturations are optional with default 0
 2. the saturations option is the number of ys

Useful example: it is now possible to declare a coercion from
 nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.

TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)

18 files changed:
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteMarshal.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteSync.mli
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/library/cicCoercion.ml
helm/software/components/library/cicCoercion.mli
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/librarySync.ml
helm/software/components/library/librarySync.mli
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/closeCoercionGraph.mli
helm/software/matita/matita.ml

index 93bd922ef3f0294631cbbfa35cff6f8385941559..e88406b5801bcddde3f43923a867ee534cb23a5d 100644 (file)
@@ -79,7 +79,7 @@ let require value =
    command_of_obj (G.Include (floc, value ^ ".ma"))
 
 let coercion value =
-   command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0))
+   command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
 
 let inline (uri, prefix) =
     command_of_macro (G.Inline (floc, G.Declarative, uri, prefix))
index cb33d9e324f0b41851668c37c1f237770b33342a..43e342e708f710ff27fcdb3f0aa41d00e6c4be5f 100644 (file)
@@ -41,14 +41,15 @@ let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 let saturate_coercion ul metasenv subst context =
-  let cl = List.map CicUtil.term_of_uri ul in
+  let cl =
+   List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
   let funclass_arityl = 
-    let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+    let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in
     List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
   in
   let freshmeta = CicMkImplicit.new_meta metasenv subst in
    List.map2
-    (fun arity c -> 
+    (fun arity (c,saturations) -> 
       let ty,_ =
        CicTypeChecker.type_of_aux' ~subst metasenv context c
         CicUniv.empty_ugraph in
@@ -57,7 +58,7 @@ let saturate_coercion ul metasenv subst context =
       let irl =
        CicMkImplicit.identity_relocation_list_for_metavariable context
       in
-       metasenv, Cic.Meta (lastmeta-1,irl),
+       metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
         match args with
            [] -> c
          | _ -> Cic.Appl (c::args)
@@ -128,18 +129,23 @@ let generate_dot_file () =
         Pp.node (CoercDb.name_of_carr carr)
           ~attrs:["href", UriManager.string_of_uri uri] fmt in
   List.iter
-    (fun (src, tgt, cl) ->
+    (fun (src, tgt, ul) ->
       let src_name = CoercDb.name_of_carr src in
       let tgt_name = CoercDb.name_of_carr tgt in
       pp_description src;
       pp_description tgt;
       List.iter
-        (fun c ->
+        (fun (u,saturations) ->
           Pp.edge src_name tgt_name
-            ~attrs:[ "label", UriManager.name_of_uri c;
-              "href", UriManager.string_of_uri c ]
+            ~attrs:[ "label",
+                     (UriManager.name_of_uri u ^
+                      if saturations = 0 then
+                       ""
+                      else
+                       "(" ^ string_of_int saturations ^ ")");
+              "href", UriManager.string_of_uri u ]
             fmt)
-        cl)
+        ul)
     l;
   Pp.trailer fmt;
   Buffer.contents buf
@@ -186,7 +192,7 @@ let coerced_arg l =
 (************************* meet calculation stuff ********************)
 let eq_uri_opt u1 u2 = 
   match u1,u2 with
-  | Some u1, Some u2 -> UriManager.eq u1 u2
+  | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
   | None,Some _ | Some _, None -> false
   | None, None -> true
 ;;
index d5eb9c241259efcb7fc1ff0e24d328b92f68bad8..b0c25bc1e361f2a8ea892bd3686c9b8fa80cbd96 100644 (file)
@@ -140,11 +140,12 @@ type 'term macro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 11
+let magic = 12
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
-  | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
+  | Coercion of loc * UriManager.uri * bool (* add_obj *) *
+     int (* arity *) * int (* saturations *)
   | Default of loc * string * UriManager.uri list
   | Drop of loc
   | Include of loc * string
index 14b7d180ca15ef61a41e86f969a527b2945731e1..de7af826370d8c87acd36762cf9ac19c4475130c 100644 (file)
@@ -263,13 +263,15 @@ let pp_default what uris =
   Printf.sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_coercion uri do_composites arity =
-   Printf.sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
-     (if do_composites then "compounds" else "no compounds")
+let pp_coercion uri do_composites arity saturations=
+   Printf.sprintf "coercion %s %d %d (* %s *)"
+    (UriManager.string_of_uri uri) arity saturations
+    (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~term_pp ~obj_pp = function
   | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
-  | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
+  | Coercion (_, uri, do_composites, i, j) ->
+     pp_coercion uri do_composites i j
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"
   | Include (_,path) -> "include \"" ^ path ^ "\""
index 056b1225d1c2c14cf3de6343fab6472f7598f875..7731902b4adbf73b4c02566deafa9c6693e8c9c2 100644 (file)
@@ -44,8 +44,8 @@ let rehash_cmd_uris =
   | GrafiteAst.Default (loc, name, uris) ->
       let uris = List.map rehash_uri uris in
       GrafiteAst.Default (loc, name, uris)
-  | GrafiteAst.Coercion (loc, uri, close, arity) ->
-      GrafiteAst.Coercion (loc, rehash_uri uri, close, arity)
+  | GrafiteAst.Coercion (loc, uri, close, arity, saturations) ->
+      GrafiteAst.Coercion (loc, rehash_uri uri, close, arity, saturations)
   | GrafiteAst.Index (loc, key, uri) ->
       GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri)
   | cmd ->
index a31f3990e2c3e5acfb19441ba968ab4a4431eb56..7cf1520ab549c661bb7b3060c2716bcc6d615034 100644 (file)
@@ -456,8 +456,8 @@ type 'a eval_executable =
 type 'a eval_from_moo =
  { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
       
-let coercion_moo_statement_of (uri,arity) =
-  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
+let coercion_moo_statement_of (uri,arity, saturations) =
+  GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations)
 
 let refinement_toolkit = {
   RefinementTool.type_of_aux' = 
@@ -482,17 +482,17 @@ let refinement_toolkit = {
   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
  }
   
-let eval_coercion status ~add_composites uri arity baseuri =
+let eval_coercion status ~add_composites uri arity saturations baseuri =
  let status,compounds =
-  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity 
-   baseuri
+  GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
+   saturations baseuri
  in
  let moo_content = 
-   List.map coercion_moo_statement_of ((uri,arity)::compounds)
+   List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds)
  in
  let status = GrafiteTypes.add_moo_content moo_content status in
   {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
-   List.map fst compounds
+   List.map (fun u,_,_ -> u) compounds
 
 module MatitaStatus =
  struct
@@ -603,9 +603,9 @@ let add_coercions_of_record_to_moo obj lemmas status =
               in
               let is_a_coercion, arity_coercion = is_a_coercion uri in
               if is_a_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_coercion))
+                Some (uri, coercion_moo_statement_of (uri,arity_coercion,0))
               else if is_a_wanted_coercion then
-                Some (uri, coercion_moo_statement_of (uri,arity_wanted))
+                Some (uri, coercion_moo_statement_of (uri,arity_wanted,0))
               else
                 None)
             lemmas)
@@ -648,8 +648,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
 *)
       let status = GrafiteTypes.add_moo_content [cmd] status in
       status,[] 
-  | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
-     eval_coercion status ~add_composites uri arity
+  | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
+     eval_coercion status ~add_composites uri arity saturations
       (GrafiteTypes.get_string_option status "baseuri")
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
index fecdde3c6a8321edcadec528908ff138222e611f..067fe9b59dc3c5acd5afda051fff0e3bf405e028 100644 (file)
@@ -99,9 +99,12 @@ let add_obj refinement_toolkit uri obj status =
      GrafiteTypes.universe = universe},
    lemmas
 
-let add_coercion refinement_toolkit ~add_composites status uri arity baseuri =
+let add_coercion refinement_toolkit ~add_composites status uri arity
+ saturations baseuri
+=
  let compounds = 
-   LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in
+   LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity
+    saturations baseuri in
   {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
    compounds
  
index 42b29a9fa3432990c4654f27e9c34a08e9f84814..0a2595430462e88341e9cfeb3c458165fb695fcf 100644 (file)
@@ -31,9 +31,10 @@ val add_obj:
 val add_coercion:
   RefinementTool.kit ->
   add_composites:bool -> GrafiteTypes.status ->
-  UriManager.uri -> int ->
+  UriManager.uri -> int -> int ->
   string (* baseuri *) ->
-    GrafiteTypes.status * (UriManager.uri * int) list (* URI and arity *)
+    GrafiteTypes.status * (UriManager.uri * int * int) list
+     (* URI, arity, saturations *)
 
 val time_travel: 
   present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
index e2108381200b82ae16626d0a61fd11bafc419ac3..081055ce84d64ffea17c354bc635e4e091100775 100644 (file)
@@ -639,9 +639,11 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
         let arity = match arity with None -> 0 | Some x -> x in
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
+        let saturations = match saturations with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion
+         (loc, UriManager.uri_of_string suri, true, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
index 42a19bcf92fcea3cbcab72129101c62ea0a87b27..85dc9f65b83d8951022dc510a770b392e78043f7 100644 (file)
 (* $Id$ *)
 
 let close_coercion_graph_ref = ref
- (fun _ _ _ _ -> [] : 
-   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ (fun _ _ _ _ -> [] : 
+   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
    string (* baseuri *) ->
-     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
+     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
 ;;
 
 let set_close_coercion_graph f = close_coercion_graph_ref := f;;
 
-let close_coercion_graph c1 c2 u s = 
-  !close_coercion_graph_ref c1 c2 u s
+let close_coercion_graph c1 c2 u sat s = 
+  !close_coercion_graph_ref c1 c2 u sat s
 ;;
index 5dc086ec44cf2a9668355f550a8a430be3390715..d862297261eecf8a37801db95d2a707e178cc0e8 100644 (file)
 (* This module implements the Coercions transitive closure *)
 
 val set_close_coercion_graph : 
-  (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list)
   -> unit
 
 val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list
 
index 1f3874912b93ff231ca48563a1c9ad04d6f9e23c..e0dc18d05f7146e9bf0125265eb9ef4aaa41e660 100644 (file)
@@ -99,7 +99,7 @@ let eq_carr ?(exact=false) src tgt =
 ;;
 
 let to_list () =
-  List.map (fun (s,t,l) -> s,t,List.map fst l) !db
+  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db
 ;;
 
 let rec myfilter p = function
@@ -107,14 +107,14 @@ let rec myfilter p = function
   | (s,t,l)::tl ->
       let l = 
         HExtlib.filter_map 
-          (fun (u,n) -> 
-            if p (s,t,u) then
+          (fun (u,n,saturations) -> 
+            if p (s,t,u,saturations) then
               if n = 1 then
                 None
               else
-                Some (u,n-1)
+                Some (u,n-1,saturations)
             else
-              Some (u,n)) 
+              Some (u,n,saturations)) 
           l 
       in
       if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
@@ -124,7 +124,7 @@ let remove_coercion p = db := myfilter p !db;;
 
 let find_coercion f =
     List.map
-    fst
+    (fun uri,_,saturations -> uri,saturations)
     (List.flatten
     (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
 ;;
@@ -133,7 +133,7 @@ let get_carr uri =
   try
     let src, tgt, _ = 
       List.find 
-        (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl) 
+        (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl) 
         !db 
     in
     src, tgt
@@ -142,7 +142,7 @@ let get_carr uri =
 
 let is_a_coercion u = 
   List.exists 
-    (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) 
+    (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl) 
     !db
 ;;
 
@@ -169,24 +169,26 @@ let term_of_carr = function
   | Term _ -> assert false
 ;;
   
-let add_coercion (src,tgt,u) =
+let add_coercion (src,tgt,u,saturations) =
   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,1]) :: !db
+  | [] -> db := (src,tgt,[u,1,saturations]) :: !db
   | (src,tgt,l)::tl ->
       assert (tl = []); (* not sure, this may be a feature *)
-      if List.exists (fun (x,_) -> UriManager.eq u x) l then
-        let l' = List.map 
-          (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n))
+      if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
+        let l' = List.map
+          (fun (x,n,saturations') ->
+            assert (saturations=saturations');
+            if UriManager.eq u x then
+             (x,n+1,saturations)
+            else
+             (x,n,saturations))
           l
         in
         db := (src,tgt,l')::tl @ rest
       else
-        db := (src,tgt,(u,1)::l)::tl @ rest
+        db := (src,tgt,(u,1,saturations)::l)::tl @ rest
       
 ;;
-
-
-
index e6d7e46b30042778b6b3889970c56dac329741bd..e1afd61aa0eb2cd3272da19819b9eefbc2bc9c24 100644 (file)
@@ -48,16 +48,16 @@ val uri_of_carr: coerc_carr -> UriManager.uri option
 
 val to_list:
   unit -> 
-    (coerc_carr * coerc_carr * UriManager.uri list) list
+    (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
 
 val add_coercion:
-  coerc_carr * coerc_carr * UriManager.uri -> unit
+  coerc_carr * coerc_carr * UriManager.uri * int -> unit
 
 val remove_coercion:
-  (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
+  (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
 
 val find_coercion: 
-  (coerc_carr * coerc_carr -> bool) -> UriManager.uri list 
+  (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list 
     
 val is_a_coercion: UriManager.uri -> bool
 val is_a_coercion': Cic.term -> bool
index 64f037922554e7ccb439ad10afd7cff174d92729..cbc45e6a933bba38e57efa8623ce050f7caf9e14 100644 (file)
@@ -230,9 +230,11 @@ let generate_elimination_principles uri refinement_toolkit =
   
 let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
-  CoercDb.remove_coercion (fun (_,_,u1) -> true)
+  CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
+let add_coercion ~add_composites refinement_toolkit uri arity saturations
+ baseuri
+=
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -248,7 +250,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let spline2list ty =
+  let spine2list ty =
     let rec aux = function
       | Cic.Prod( _, src, tgt) -> src::aux tgt
       | t -> [t]
@@ -256,30 +258,34 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     aux ty
   in
   let src_carr, tgt_carr = 
-    let list_remove_from_tail n l = 
-      let rec aux n = function
-        | hd::tl when n > 0 -> aux (n-1) tl
-        | l when n = 0 -> l
-        | _ -> assert false
+    let get_classes arity saturations l = 
+      let rec aux target = function
+         0,0,tgt::src::_ when target = None -> src,Some (`Class tgt)
+       | 0,0,src::_ when target <> None -> src,target
+       | 0,saturations,tgt::tl when target = None ->
+          aux (Some (`Class tgt)) (0,saturations,tl)
+       | 0,saturations,_::tl ->
+          aux target (0,saturations - 1,tl)
+       | arity,saturations,_::tl ->
+          aux (Some `Funclass) (arity - 1, saturations, tl)
+       | _,_,_ -> assert false
       in
-      aux n (List.rev l)
+       aux None (arity,saturations,List.rev l)
     in
-    let types = spline2list coer_ty in
-    match arity, list_remove_from_tail arity types with
-    | 0,tgt::src::_ -> 
-        (* if ~delta is true, it is impossible to define an identity coercion *)
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
-    | n,_::src::_ -> 
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-        CoercDb.Fun arity
-    | _ -> assert false    
+    let types = spine2list coer_ty in
+    let src,tgt = get_classes arity saturations types in
+     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+     match tgt with
+        None -> assert false
+      | Some `Funclass -> CoercDb.Fun arity
+      | Some (`Class tgt) ->
+         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
   in
   let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
-         (fun u -> 
+         (fun u,_ -> 
            let bo = 
             match obj with 
             | Cic.Constant (_, Some bo, _, _, _) -> bo
@@ -294,36 +300,37 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
               ("Coercions " ^ 
                 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
                 uri^" are not convertible, but are between the same nodes.\n"^
-                "From now on nification can fail randomly.");
+                "From now on unification can fail randomly.");
              false))
          ul)
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj))
+      List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj))
       new_coercions 
     in
-    let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions 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)) 
+      (fun (src,tgt,uri,saturations,_) ->
+        CoercDb.add_coercion (src,tgt,uri,saturations)) 
       new_coercions;
-    CoercDb.add_coercion (src_carr, tgt_carr, uri);
+    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
       if add_composites then
         List.fold_left
-          (fun acc (_,tgt,uri,obj) -> 
+          (fun acc (_,tgt,uri,saturations,obj) -> 
             add_single_obj uri obj refinement_toolkit;
             let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
-             (uri,arity)::acc) 
+             (uri,arity,saturations)::acc) 
           [] new_coercions
       else
         []
@@ -355,10 +362,10 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
-      (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
+      (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
       composites_in_db;
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
@@ -375,6 +382,7 @@ let generate_projections refinement_toolkit uri fields =
   try
    List.iter2 
     (fun (uri, name, bo) (_name, coercion, arity) ->
+      let saturations = 0 in
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -390,14 +398,14 @@ let generate_projections refinement_toolkit uri fields =
                 every time. Right? *)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
-                (UriManager.buri_of_uri uri)
+                 saturations (UriManager.buri_of_uri uri)
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
   prerr_endline "---";
 *)
               (*CSC: I throw the arity away. See comment above *)
-              List.map fst x
+              List.map (fun u,_,_ -> u) x
             end
           else  
             []
index 96e9231009b58cb4b7df425d6eee90db73f073fa..980e4724a990de49ba049a97c7b6bcf3ca2c3f5c 100644 (file)
@@ -48,8 +48,8 @@ val remove_obj: UriManager.uri -> unit
 val add_coercion: 
   add_composites:bool -> 
   RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
-   string (* baseuri *) ->
-    (UriManager.uri * int) list (* URI and arity *)
+   int (* saturations *) -> string (* baseuri *) ->
+    (UriManager.uri * int * int) list (* URI, arity, saturations *)
 
 (* inverse of add_coercion, removes both the eventually created composite   *)
 (* coercions and the information that [uri] and the composites are coercion *)
index 6c253df9f73c9274ec1087b122415f9312374962..0ab937ace0a89b6643034a21936cdc9242d31af4 100644 (file)
@@ -81,20 +81,25 @@ exception UnableToCompose
 
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * both living in the same context and metasenv *)
-let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
+let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity
+ last_lam_with_inn_arg
+=
+assert (sat1 = 0);
+assert (sat2 = 0);
+let saturationsres = 0 in
   let original_metasenv = metasenv in 
   let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
   let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
   let rec mk_implicits = function
     | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
   in
-  let rec mk_lambda_spline c namer = function
+  let rec mk_lambda_spine c namer = function
     | 0 -> c
     | n -> 
         Cic.Lambda 
           (namer n,
            (Cic.Implicit None), 
-           mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1))
+           mk_lambda_spine (CicSubstitution.lift 1 c) namer (n-1))
   in 
   let count_saturations_needed t arity = 
     let rec aux acc n = function
@@ -177,7 +182,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
       | Cic.Appl l -> List.tl l
       | _ -> assert false
     in
-    (* i should cut off the laet elem of l_c2 *)
+    (* i should cut off the last elem of l_c2 *)
     let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
     List.sort 
       (fun (i,ctx1,ty1) (j,ctx1,ty1) -> 
@@ -204,8 +209,8 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
   let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
   let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
-  let spline_len = saturations_for_c1 + saturations_for_c2 in
-  let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in
+  let spine_len = saturations_for_c1 + saturations_for_c2 in
+  let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
   let old_insert_coercions = !CicRefine.insert_coercions in
   let c, metasenv, univ = 
@@ -218,13 +223,13 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
 (*       let metasenv = order_metasenv metasenv in *)
 (*       debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *)
       let body_metasenv, lambdas_metasenv = 
-        split_metasenv metasenv (spline_len + List.length context)
+        split_metasenv metasenv (spine_len + List.length context)
       in
       debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
       debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
       let body_metasenv = order_body_menv term body_metasenv in
       debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
-      let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+      let subst = create_subst_from_metas_to_rels spine_len body_metasenv in
       debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
       let term = CicMetaSubst.apply_subst subst term in
       let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
@@ -233,7 +238,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
         CicRefine.type_of_aux' metasenv context term ugraph
       in
       let body_metasenv, lambdas_metasenv = 
-        split_metasenv metasenv (spline_len + List.length context)
+        split_metasenv metasenv (spine_len + List.length context)
       in
       let lambdas_metasenv = 
         List.filter 
@@ -264,7 +269,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
         CicRefine.insert_coercions := old_insert_coercions;
         raise exn
   in  
-  c, metasenv, univ 
+  c, metasenv, univ, saturationsres
 ;;
 
 let build_obj c univ arity =
@@ -291,7 +296,7 @@ let filter_duplicates l coercions =
           CoercDb.eq_carr s src && 
           CoercDb.eq_carr t tgt &&
           try 
-            List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2
+            List.for_all2 (fun (u1,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
           with
           | Invalid_argument "List.for_all2" -> false)
         coercions))
@@ -340,10 +345,10 @@ let number_if_already_defined buri name 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 baseuri =
+let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
-  let todo_list = get_closure_coercions src tgt uri coercions in
+  let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
   let todo_list = filter_duplicates todo_list coercions in
   try
     let new_coercions = 
@@ -352,43 +357,45 @@ let close_coercion_graph src tgt uri baseuri =
           try 
             (match l with
             | [] -> assert false 
-            | he :: tl ->
+            | (he,saturations1) :: tl ->
                 let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
                 let first_step = 
                   Cic.Constant ("", 
                     Some (CoercDb.term_of_carr (CoercDb.Uri he)),
-                    Cic.Sort Cic.Prop, [], obj_attrs arity)
+                    Cic.Sort Cic.Prop, [], obj_attrs arity), saturations1
                 in
                 let o,_ = 
-                  List.fold_left (fun (o,univ) coer ->
+                  List.fold_left (fun (o,univ) (coer,saturations) ->
                     match o with 
-                    | Cic.Constant (_,Some c,_,[],_) ->
-                        let t, menv, univ = 
-                          generate_composite c 
-                            (CoercDb.term_of_carr (CoercDb.Uri coer)) 
+                    | Cic.Constant (_,Some u,_,[],_),saturations1 ->
+                        let t, menv, univ, saturationsres = 
+                          generate_composite' (u,saturations1) 
+                            (CoercDb.term_of_carr (CoercDb.Uri coer),
+                             saturations) 
                             [] [] univ arity true
                         in
                         if (menv = []) then
                           HLog.warn "MENV non empty after composing coercions";
-                        build_obj t univ arity
+                        let o,univ = build_obj t univ arity in
+                         (o,saturationsres),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 by = List.map (fun u,_ -> UriManager.name_of_uri u) l in
                 let name = mangle name_tgt name_src by in
                 let c_uri = 
                   number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_) -> u) acc) 
+                    (List.map (fun (_,_,u,_,_) -> u) acc) 
                 in
-                let named_obj = 
+                let named_obj,saturations = 
                   match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs) ->
-                      Cic.Constant (name,bo,ty,vl,attrs)
+                  | Cic.Constant (_,bo,ty,vl,attrs),saturations ->
+                      Cic.Constant (name,bo,ty,vl,attrs),saturations
                   | _ -> assert false 
                 in
-                  (src,tgt,c_uri,named_obj))::acc
+                  (src,tgt,c_uri,saturations,named_obj))::acc
           with UnableToCompose -> acc
       ) [] todo_list
     in
@@ -397,3 +404,12 @@ let close_coercion_graph src tgt uri baseuri =
 ;;
 
 CicCoercion.set_close_coercion_graph close_coercion_graph;;
+
+(* generate_composite (c2 (c1 s)) in the universe graph univ
+ * both living in the same context and metasenv *)
+let generate_composite c1 c2 context metasenv univ arity b =
+ let a,b,c,_ =
+  generate_composite' (c1,0) (c2,0) context metasenv univ arity b
+ in
+  a,b,c
+;;
index 8750ce0f7888f2bb359b5624aef88404d58bb376..1acea0eebda80bf37a24585ea78933b47dcb6a9f 100644 (file)
 (* This module implements the Coercions transitive closure *)
 
 val close_coercion_graph:
-  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
   string (* baseuri *) ->
-    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+    (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
+      list
 
 exception UnableToCompose
 
index 58d404888d7bde1e178185eaf21833651518689b..a326754dc40a39ac65ad30df18e795f4d64eae95 100644 (file)
@@ -250,7 +250,12 @@ let _ =
       List.iter
       (fun (s,t,ul) -> 
           HLog.debug
-           ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":"
+           ((String.concat ","
+              (List.map
+                (fun u,saturations ->
+                  UriManager.name_of_uri u ^
+                   "(" ^ string_of_int saturations ^ ")")
+                ul)) ^ ":"
              ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
         (CoercDb.to_list ()));
     addDebugSeparator ();