helm/software/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 module COT : Set.OrderedType with type t = NCic.term * int * int =
  15   struct
  16         type t = NCic.term * int * int
  17         let compare = Pervasives.compare
  18   end
  19
  20 module CoercionSet = Set.Make(COT)
  21
  22 module DB =
  23   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
  24
  25 type db = DB.t * DB.t
  26
  27 let index_coercion (db_src,db_tgt) c src tgt arity arg =
  28   let data = (c,arity,arg) in
  29   let db_src = DB.index db_src src data in
  30   let db_tgt = DB.index db_tgt tgt data in
  31   db_src, db_tgt
  32 ;;
  33
  34 let db () =
  35   List.fold_left
  36     (fun db (_,tgt,clist) ->
  37        List.fold_left
  38          (fun db (uri,_,arg) ->
  39             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
  40             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
  41             let src, tgt =
  42               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
  43               match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1)
  44               with
  45               | NCic.Prod (_, src, tgt),_,_ ->
  46                 src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
  47               | t,metasenv,_ ->
  48                   prerr_endline (
  49                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
  50                   assert false
  51             in
  52 (*
  53             prerr_endline (Printf.sprintf "indicizzo %s %d %d"
  54               (UriManager.string_of_uri uri) arity arg);
  55 *)
  56             index_coercion db c src tgt arity arg)
  57          db clist)
  58     (DB.empty,DB.empty) (CoercDb.to_list ())
  59 ;;
  60
  61 (* XXX saturate takes no subst!!!! *)
  62 let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
  63   let set_src = DB.retrieve_unifiables db_src infty in
  64   let set_tgt = DB.retrieve_unifiables db_tgt expty in
  65   let candidates = CoercionSet.inter set_src set_tgt in
  66   prerr_endline "aaaaaaaaaaaaa";
  67   List.map
  68     (fun (t,arity,arg) ->
  69         let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
  70         let ty, metasenv, args =
  71           NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity
  72         in
  73         prerr_endline (
  74           NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
  75           NCicPp.ppterm ~metasenv ~subst:_subst ~context
  76           (NCicUntrusted.mk_appl t args) ^ " --- " ^
  77             string_of_int (List.length args) ^ " == " ^ string_of_int arg);
  78         metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
  79     (CoercionSet.elements candidates)
  80 ;;