--- /dev/null
+(* 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/.
+ *)
+
+(* $Id$ *)
+
+open Printf;;
+
+type coercion_search_result =
+ (* metasenv, last coercion argument, fully saturated coercion *)
+ (* to apply the coercion it is sufficient to unify the last coercion
+ argument (that is a Meta) with the term to be coerced *)
+ | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string Lazy.t
+
+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 (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in
+ let funclass_arityl =
+ 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,saturations) ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' ~subst metasenv context c
+ CicUniv.empty_ugraph in
+ let _,metasenv,args,lastmeta =
+ TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ metasenv, Cic.Meta (lastmeta - saturations - 1,irl),
+ match args with
+ [] -> c
+ | _ -> Cic.Appl (c::args)
+ ) funclass_arityl cl
+;;
+
+(* searches a coercion fron src to tgt in the !coercions list *)
+let look_for_coercion' metasenv subst context src tgt =
+ let pp_l s l =
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata[%s] da %s a %s" s
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ | _::_ ->
+ debug_print (lazy (
+ sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ in
+ try
+ let l =
+ CoercDb.find_coercion
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ in
+ pp_l "precise" l;
+ (match l with
+ | [] ->
+ let l =
+ CoercDb.find_coercion
+ (fun (_,t) -> CoercDb.eq_carr t tgt)
+ in
+ pp_l "approx" l;
+ (match l with
+ | [] -> NoCoercion
+ | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context))
+ | ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
+ with
+ | CoercDb.EqCarrNotImplemented s -> NotHandled s
+ | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
+;;
+
+let look_for_coercion metasenv subst context src tgt =
+ let src_uri = CoercDb.coerc_carr_of_term src in
+ let tgt_uri = CoercDb.coerc_carr_of_term tgt in
+ look_for_coercion' metasenv subst context src_uri tgt_uri
+
+let source_of t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
+ with Invalid_argument _ -> assert false (* t must be a coercion *)
+
+let generate_dot_file () =
+ let module Pp = GraphvizPp.Dot in
+ let buf = Buffer.create 10240 in
+ let fmt = Format.formatter_of_buffer buf in
+ Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+ ~edge_attrs:["fontsize", "10"] fmt;
+ let l = CoercDb.to_list () in
+ let pp_description carr =
+ match CoercDb.uri_of_carr carr with
+ | None -> ()
+ | Some uri ->
+ Pp.node (CoercDb.name_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ List.iter
+ (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 (u,saturations) ->
+ Pp.edge src_name tgt_name
+ ~attrs:[ "label",
+ (UriManager.name_of_uri u ^
+ if saturations = 0 then
+ ""
+ else
+ "(" ^ string_of_int saturations ^ ")");
+ "href", UriManager.string_of_uri u ]
+ fmt)
+ ul)
+ l;
+ Pp.trailer fmt;
+ Buffer.contents buf
+;;
+
+let is_composite t =
+ try
+ let uri =
+ match t with
+ | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+ | _ -> CicUtil.uri_of_term t
+ in
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | Cic.Constant (_,_, _, _, attrs),_ ->
+ List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+ | _ -> false
+ with Invalid_argument _ -> false
+;;
+
+let coerced_arg l =
+ match l with
+ | [] | [_] -> assert false
+ | c::_ when not (CoercDb.is_a_coercion' c) -> assert false
+ | c::tl ->
+ let arity =
+ match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a
+ in
+ (* decide a decent structure for coercion carriers so that all this stuff is
+ * useless *)
+ let pi =
+ (* this calculation is not complete, since we have strange carriers *)
+ let rec count_pi = function
+ | Cic.Prod(_,_,t) -> 1+ (count_pi t)
+ | _ -> 0
+ in
+ let uri = CicUtil.uri_of_term c in
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ | Cic.Constant (_, _, ty, _, _) -> count_pi ty
+ | _ -> assert false
+ in
+ try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None
+;;
+
+(************************* meet calculation stuff ********************)
+let eq_uri_opt u1 u2 =
+ match u1,u2 with
+ | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2
+ | None,Some _ | Some _, None -> false
+ | None, None -> true
+;;
+
+let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;;
+
+let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) =
+ CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22
+;;
+
+let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;;
+
+let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;;
+
+let splat e l = List.map (fun x -> e, Some x) l;;
+
+(* : carr -> (carr * uri option) where the option is always Some *)
+let get_coercions_to carr =
+ let l = CoercDb.to_list () in
+ let splat_coercion_to carr (src,tgt,cl) =
+ if CoercDb.eq_carr tgt carr then Some (splat src cl) else None
+ in
+ let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in
+ l
+;;
+
+(* : carr -> (carr * uri option) where the option is always Some *)
+let get_coercions_from carr =
+ let l = CoercDb.to_list () in
+ let splat_coercion_from carr (src,tgt,cl) =
+ if CoercDb.eq_carr src carr then Some (splat tgt cl) else None
+ in
+ List.flatten (HExtlib.filter_map (splat_coercion_from carr) l)
+;;
+
+(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 }
+ * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *)
+let intersect l1 l2 =
+ let is_in_l1 (x,u2) =
+ HExtlib.filter_map
+ (fun (src,u1) ->
+ if CoercDb.eq_carr x src then Some (src,u1,u2) else None)
+ l1
+ in
+ uniq2 (List.flatten (List.map is_in_l1 l2))
+;;
+
+(* grow tgt gives all the (src,u) such that u:tgt->src *)
+let grow tgt =
+ uniq ((tgt,None)::(get_coercions_to tgt))
+;;
+
+let lb (c,_,_) =
+ let l = get_coercions_from c in
+ fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+;;
+
+(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements
+ * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *)
+let rec min acc = function
+ | c::tl ->
+ if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
+ | [] -> acc
+;;
+
+let meets metasenv subst context left right =
+ let saturate metasenv uo =
+ match uo with
+ | None -> metasenv, None
+ | Some u ->
+ match saturate_coercion [u] metasenv subst context with
+ | [metasenv, sat, last] -> metasenv, Some (sat, last)
+ | _ -> assert false
+ in
+ List.map
+ (fun (c,uo1,uo2) ->
+ let metasenv, uo1 = saturate metasenv uo1 in
+ let metasenv, uo2 = saturate metasenv uo2 in
+ c,metasenv, uo1, uo2)
+ (min [] (intersect (grow left) (grow right)))
+;;
+
+(* EOF *)
projects / helm.git / blobdiff