matita/components/ng_refiner/nCicCoercion.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)
  13
  14 let debug s = prerr_endline (Lazy.force s);;
  15 let debug _ = ();;
  16
  17 let convert_term = ref (fun _ _ -> assert false);;
  18 let set_convert_term f = convert_term := f;;
  19
  20 module COT : Set.OrderedType
  21 with type t = string * NCic.term * int * int  * NCic.term *
  22 NCic.term =
  23   struct
  24      type t = string * NCic.term * int * int * NCic.term * NCic.term
  25      let compare = Pervasives.compare
  26   end
  27
  28 module CoercionSet = Set.Make(COT)
  29
  30 module DB =
  31   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
  32
  33 type db = DB.t * DB.t
  34
  35 let empty_db = DB.empty,DB.empty
  36
  37 class type g_status =
  38  object
  39   inherit NCicUnifHint.g_status
  40   method coerc_db: db
  41  end
  42
  43 class status =
  44  object
  45   inherit NCicUnifHint.status
  46   val db = empty_db
  47   method coerc_db = db
  48   method set_coerc_db v = {< db = v >}
  49   method set_coercion_status
  50    : 'status. #g_status as 'status -> 'self
  51    = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  52  end
  53
  54 let index_coercion status name c src tgt arity arg =
  55   let db_src,db_tgt = status#coerc_db in
  56   let data = (name,c,arity,arg,src,tgt) in
  57   debug (lazy ("INDEX:" ^
  58     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
  59     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
  60     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
  61     string_of_int arg ^ " " ^ string_of_int arity));
  62   let db_src = DB.index db_src src data in
  63   let db_tgt = DB.index db_tgt tgt data in
  64   status#set_coerc_db (db_src, db_tgt)
  65 ;;
  66
  67 let look_for_coercion status metasenv subst context infty expty =
  68  let db_src,db_tgt = status#coerc_db in
  69   match
  70     NCicUntrusted.apply_subst subst context infty,
  71     NCicUntrusted.apply_subst subst context expty
  72   with
  73   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
  74     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
  75   | infty, expty ->
  76
  77     debug (lazy ("LOOK FOR COERCIONS: " ^
  78       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
  79       NCicPp.ppterm ~metasenv ~subst ~context expty));
  80
  81     let src_class = infty :: NCicUnifHint.eq_class_of status infty in
  82     let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
  83
  84     let set_src =
  85       List.fold_left
  86         (fun set infty ->
  87           CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
  88         CoercionSet.empty src_class
  89     in
  90     let set_tgt =
  91       List.fold_left
  92         (fun set expty ->
  93           CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
  94         CoercionSet.empty tgt_class
  95     in
  96
  97     debug (lazy ("CANDIDATES SRC: " ^
  98       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
  99         name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
 100       (CoercionSet.elements set_src))));
 101     debug (lazy ("CANDIDATES TGT: " ^
 102       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
 103         name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
 104       (CoercionSet.elements set_tgt))));
 105
 106     let candidates = CoercionSet.inter set_src set_tgt in
 107
 108     debug (lazy ("CANDIDATES: " ^
 109       String.concat "," (List.map (fun (name,t,_,_,_,_) ->
 110         name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
 111       (CoercionSet.elements candidates))));
 112
 113     List.map
 114       (fun (name,t,arity,arg,_,_) ->
 115           let ty =
 116             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
 117             with NCicTypeChecker.TypeCheckerFailure s ->
 118              prerr_endline ("illtyped coercion: "^Lazy.force s);
 119              prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
 120              assert false
 121           in
 122           let ty, metasenv, args =
 123            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
 124           in
 125
 126           debug (lazy (
 127             NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
 128             NCicPp.ppterm ~metasenv ~subst ~context
 129             (NCicUntrusted.mk_appl t args) ^ " --- " ^
 130               string_of_int (List.length args) ^ " == " ^ string_of_int arg));
 131
 132           name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
 133       (CoercionSet.elements candidates)
 134 ;;
 135
 136 (* CSC: very inefficient implementation!
 137    Enrico, can we use a discrimination tree here? *)
 138 let match_coercion status ~metasenv ~subst ~context t =
 139  let db =
 140   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
 141  in
 142     (HExtlib.list_findopt
 143       (fun (_,p,arity,cpos,_,_) _ ->
 144         try
 145          let t =
 146           match p,t with
 147              NCic.Appl lp, NCic.Appl lt ->
 148               (match fst (HExtlib.split_nth (List.length lp) lt) with
 149                   [t] -> t
 150                 | l -> NCic.Appl l)
 151            | _,NCic.Appl (he::_) -> he
 152            | _,_ -> t
 153          in
 154          let b = NCicReduction.alpha_eq metasenv subst context p t in
 155          if not b then None else
 156          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
 157          let pis =
 158            let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
 159            aux ty
 160          in
 161          Some (p,pis - arity - cpos - 1,cpos)
 162         with
 163          Failure _ -> None (* raised by split_nth *)
 164       ) db)
 165 ;;
 166
 167 let generate_dot_file status fmt =
 168   let module Pp = GraphvizPp.Dot in
 169   let src_db, _ = status#coerc_db in
 170   let edges = ref [] in
 171   DB.iter src_db (fun _ dataset ->
 172      edges := !edges @
 173       List.map
 174         (fun (name,t,a,g,sk,dk) ->
 175           debug(lazy (let p = NCicPp.ppterm ~metasenv:[] ~context:[]
 176                 ~subst:[] in p t ^ " ::: " ^ p sk ^ " |--> " ^ p dk));
 177           let eq_s= sk::NCicUnifHint.eq_class_of status sk in
 178           let eq_t= dk::NCicUnifHint.eq_class_of status dk in
 179           (name,t,a,g),eq_s,eq_t
 180           )
 181         (CoercionSet.elements dataset);
 182     );
 183   let nodes =
 184     HExtlib.list_uniq
 185      (List.sort compare
 186        (List.flatten
 187          (List.map
 188            (fun (_,a,b) ->
 189              [a;b]
 190             )
 191            !edges)))
 192   in
 193   let names = ref [] in
 194   let id = ref 0 in
 195   let mangle l =
 196     try List.assoc l !names
 197     with Not_found ->
 198       incr id;
 199       names := (l,"node"^string_of_int!id) :: !names;
 200       List.assoc l !names
 201   in
 202   List.iter
 203     (fun cl ->
 204       Pp.node (mangle cl)
 205       ~attrs:["label",String.concat "\\n"
 206         (List.map (fun t->
 207           NCicPp.ppterm ~metasenv:[] ~subst:[]
 208            ~context:[] t ~margin:max_int
 209         ) cl)]
 210       fmt)
 211     nodes;
 212   List.iter
 213     (fun ((name,_,_,_),src,tgt) ->
 214        Pp.edge (mangle src) (mangle tgt)
 215        ~attrs:["label", name] fmt)
 216     !edges;
 217 ;;