components/library/cicCoercion.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 let debug = false
  29 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  30
  31 (* given the new coercion uri from src to tgt returns the list
  32  * of new coercions to create. hte list elements are
  33  * (source, list of coercions to follow, target)
  34  *)
  35 let get_closure_coercions src tgt uri coercions =
  36   let eq_carr s t =
  37     try
  38       CoercDb.eq_carr s t
  39     with
  40     | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
  41   in
  42   match src,tgt with
  43   | CoercDb.Uri _, CoercDb.Uri _ ->
  44       let c_from_tgt =
  45         List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
  46       in
  47       let c_to_src =
  48         List.filter (fun (_,t,_) -> eq_carr t src) coercions
  49       in
  50         (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
  51         (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
  52         (List.fold_left (
  53           fun l (s,_,u1) ->
  54             ((List.map (fun (_,t,u2) ->
  55               (s,[u1;uri;u2],t)
  56             )c_from_tgt)@l) )
  57         [] c_to_src)
  58   | _ -> [] (* do not close in case source or target is not an indty ?? *)
  59 ;;
  60
  61 let obj_attrs = [`Class `Coercion; `Generated]
  62
  63 exception UnableToCompose
  64
  65 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
  66 let generate_composite_closure rt c1 c2 univ =
  67   let module RT = RefinementTool in
  68   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
  69   let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
  70   let rec mk_implicits n =
  71     match n with
  72     | 0 -> []
  73     | _ -> (Cic.Implicit None) :: mk_implicits (n-1)
  74   in
  75   let rec mk_lambda_spline c = function
  76     | 0 -> c
  77     | n ->
  78         Cic.Lambda
  79           (Cic.Name ("A" ^ string_of_int (n-1)),
  80            (Cic.Implicit None),
  81            mk_lambda_spline c (n-1))
  82   in
  83   let rec count_saturations_needed n = function
  84     | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t
  85     | _ -> n
  86   in
  87   let compose c1 nc1 c2 nc2 =
  88     Cic.Lambda
  89       (Cic.Name "x",
  90       (Cic.Implicit None),
  91       Cic.Appl ( c2 :: mk_implicits nc2 @
  92         [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
  93   in
  94   let order_metasenv metasenv =
  95     List.sort
  96       (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2)
  97       metasenv
  98   in
  99   let rec create_subst_from_metas_to_rels n = function
 100     | [] -> []
 101     | (metano, ctx, ty)::tl ->
 102         (metano,(ctx,Cic.Rel (n+1),ty)) ::
 103           create_subst_from_metas_to_rels (n-1) tl
 104   in
 105   let split_metasenv metasenv n =
 106     List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
 107   in
 108   let purge_unused_lambdas metasenv t =
 109     let rec aux = function
 110         | Cic.Lambda (_, Cic.Meta (i,_), t) when
 111           List.exists (fun (j,_,_) -> j = i) metasenv ->
 112             CicSubstitution.subst (Cic.Rel ~-100) t
 113         | Cic.Lambda (name, s, t) ->
 114             Cic.Lambda (name, s, aux t)
 115         | t -> t
 116     in
 117     aux t
 118   in
 119   debug_print (lazy ("\nCOMPOSING"));
 120   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
 121   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
 122   let saturations_for_c1 = count_saturations_needed 0 c1_ty in
 123   let saturations_for_c2 = count_saturations_needed 0 c2_ty in
 124   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
 125   let spline_len = saturations_for_c1 + saturations_for_c2 in
 126   let c = mk_lambda_spline c spline_len in
 127   (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *)
 128   let c, univ =
 129     match rt.RT.type_of_aux' [] [] c univ with
 130     | RT.Success (term, ty, metasenv, ugraph) ->
 131         debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
 132         let metasenv = order_metasenv metasenv in
 133         debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv));
 134         let body_metasenv, lambdas_metasenv =
 135           split_metasenv metasenv spline_len
 136         in
 137         debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
 138         debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
 139         let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
 140         debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
 141         let term = rt.RT.apply_subst subst term in
 142         debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
 143         (match rt.RT.type_of_aux' metasenv [] term ugraph with
 144         | RT.Success (term, ty, metasenv, ugraph) ->
 145             let body_metasenv, lambdas_metasenv =
 146               split_metasenv metasenv spline_len
 147             in
 148             let term = purge_unused_lambdas lambdas_metasenv term in
 149             debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
 150             term, ugraph
 151         | RT.Exception s -> debug_print s; raise UnableToCompose)
 152     | RT.Exception s -> debug_print s; raise UnableToCompose
 153   in
 154   let c_ty,univ =
 155     try
 156       CicTypeChecker.type_of_aux' [] [] c univ
 157     with CicTypeChecker.TypeCheckerFailure s ->
 158       debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s"
 159         (CicPp.ppterm c) (Lazy.force s)));
 160       raise UnableToCompose
 161   in
 162   let cleaned_ty =
 163     FreshNamesGenerator.clean_dummy_dependent_types c_ty
 164   in
 165   let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
 166     obj,univ
 167 ;;
 168
 169 (* removes from l the coercions that are in !coercions *)
 170 let filter_duplicates l coercions =
 171   List.filter (
 172       fun (src,_,tgt) ->
 173         not (List.exists (fun (s,t,u) ->
 174           CoercDb.eq_carr s src &&
 175           CoercDb.eq_carr t tgt)
 176         coercions))
 177   l
 178
 179 (* given a new coercion uri from src to tgt returns
 180  * a list of (new coercion uri, coercion obj, universe graph)
 181  *)
 182 let close_coercion_graph rt src tgt uri =
 183   (* check if the coercion already exists *)
 184   let coercions = CoercDb.to_list () in
 185   let todo_list = get_closure_coercions src tgt uri coercions in
 186   let todo_list = filter_duplicates todo_list coercions in
 187   let new_coercions =
 188     HExtlib.filter_map (
 189       fun (src, l , tgt) ->
 190         try
 191           (match l with
 192           | [] -> assert false
 193           | he :: tl ->
 194               let first_step =
 195                 Cic.Constant ("",
 196                   Some (CoercDb.term_of_carr (CoercDb.Uri he)),
 197                   Cic.Sort Cic.Prop, [], obj_attrs)
 198               in
 199               let o,_ =
 200                 List.fold_left (fun (o,univ) coer ->
 201                   match o with
 202                   | Cic.Constant (_,Some c,_,[],_) ->
 203                         generate_composite_closure rt c
 204                           (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
 205                   | _ -> assert false
 206                 ) (first_step, CicUniv.empty_ugraph) tl
 207               in
 208               let name_src = CoercDb.name_of_carr src in
 209               let name_tgt = CoercDb.name_of_carr tgt in
 210               let name = name_tgt ^ "_of_" ^ name_src in
 211               let buri = UriManager.buri_of_uri uri in
 212               let c_uri =
 213                 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
 214               in
 215               let named_obj =
 216                 match o with
 217                 | Cic.Constant (_,bo,ty,vl,attrs) ->
 218                     Cic.Constant (name,bo,ty,vl,attrs)
 219                 | _ -> assert false
 220               in
 221                 Some ((src,tgt,c_uri,named_obj)))
 222         with UnableToCompose -> None
 223     ) todo_list
 224   in
 225   new_coercions
 226 ;;
 227