helm/ocaml/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 (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
  64 let generate_composite_closure c1 c2 univ =
  65   let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
  66   let rec mk_rels n =
  67     match n with
  68     | 0 -> []
  69     | _ -> (Cic.Rel n) :: (mk_rels (n-1))
  70   in
  71   let rec compose k =
  72     function
  73     | Cic.Prod (name,src,tgt) ->
  74         let name =
  75           match name with
  76           | Cic.Anonymous -> Cic.Name "x"
  77           | _ -> name
  78         in
  79           Cic.Lambda (name,src,compose (k+1) tgt)
  80     | Cic.Appl (he::tl) ->
  81         Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
  82     | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
  83   in
  84   let c = compose 0 c1_ty in
  85   let c_ty,univ =
  86     try
  87       CicTypeChecker.type_of_aux' [] [] c univ
  88     with CicTypeChecker.TypeCheckerFailure s as exn ->
  89       debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s"
  90         (CicPp.ppterm c) (Lazy.force s)));
  91       raise exn
  92   in
  93   let cleaned_ty =
  94     FreshNamesGenerator.clean_dummy_dependent_types c_ty
  95   in
  96   let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
  97     obj,univ
  98 ;;
  99
 100 (* removes from l the coercions that are in !coercions *)
 101 let filter_duplicates l coercions =
 102   List.filter (
 103       fun (src,_,tgt) ->
 104         not (List.exists (fun (s,t,u) ->
 105           CoercDb.eq_carr s src &&
 106           CoercDb.eq_carr t tgt)
 107         coercions))
 108   l
 109
 110 (* given a new coercion uri from src to tgt returns
 111  * a list of (new coercion uri, coercion obj, universe graph)
 112  *)
 113 let close_coercion_graph src tgt uri =
 114   (* check if the coercion already exists *)
 115   let coercions = CoercDb.to_list () in
 116   let todo_list = get_closure_coercions src tgt uri coercions in
 117   let todo_list = filter_duplicates todo_list coercions in
 118   let new_coercions =
 119     List.map (
 120       fun (src, l , tgt) ->
 121         match l with
 122         | [] -> assert false
 123         | he :: tl ->
 124             let first_step =
 125               Cic.Constant ("",
 126                 Some (CoercDb.term_of_carr (CoercDb.Uri he)),
 127                 Cic.Sort Cic.Prop, [], obj_attrs)
 128             in
 129             let o,_ =
 130               List.fold_left (fun (o,univ) coer ->
 131                 match o with
 132                 | Cic.Constant (_,Some c,_,[],_) ->
 133                     generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri
 134                     coer)) univ
 135                 | _ -> assert false
 136               ) (first_step, CicUniv.empty_ugraph) tl
 137             in
 138             let name_src = CoercDb.name_of_carr src in
 139             let name_tgt = CoercDb.name_of_carr tgt in
 140             let name = name_tgt ^ "_of_" ^ name_src in
 141             let buri = UriManager.buri_of_uri uri in
 142             let c_uri =
 143               UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
 144             in
 145             let named_obj =
 146               match o with
 147               | Cic.Constant (_,bo,ty,vl,attrs) ->
 148                   Cic.Constant (name,bo,ty,vl,attrs)
 149               | _ -> assert false
 150             in
 151               ((src,tgt,c_uri,named_obj))
 152     ) todo_list
 153   in
 154   new_coercions
 155 ;;
 156