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 let debug s = prerr_endline (Lazy.force s);;
  15 let debug _ = ();;
  16
  17 module COT : Set.OrderedType with type t = NCic.term * int * int =
  18   struct
  19         type t = NCic.term * int * int
  20         let compare = Pervasives.compare
  21   end
  22
  23 module CoercionSet = Set.Make(COT)
  24
  25 module DB =
  26   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CoercionSet)
  27
  28 type db = DB.t * DB.t
  29
  30 let empty_db = DB.empty,DB.empty
  31
  32 class status =
  33  object
  34   val db = empty_db
  35   method coerc_db = db
  36   method set_coerc_db v = {< db = v >}
  37   method set_coercion_status
  38    : 'status. < coerc_db : db; .. > as 'status -> 'self
  39    = fun o -> {< db = o#coerc_db >}
  40  end
  41
  42 let index_coercion status c src tgt arity arg =
  43   let db_src,db_tgt = status#coerc_db in
  44   let data = (c,arity,arg) in
  45
  46   debug (lazy ("INDEX:" ^
  47     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
  48     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
  49     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
  50     string_of_int arg ^ " " ^ string_of_int arity));
  51
  52   let db_src = DB.index db_src src data in
  53   let db_tgt = DB.index db_tgt tgt data in
  54   status#set_coerc_db (db_src, db_tgt)
  55 ;;
  56
  57 let index_old_db odb (status : #status) =
  58   List.fold_left
  59     (fun status (_,tgt,clist) ->
  60        List.fold_left
  61          (fun status (uri,_,arg) ->
  62            try
  63             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
  64             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
  65             let src, tgt =
  66               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
  67               let scty, metasenv,_ =
  68                 NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1)
  69               in
  70               match scty with
  71               | NCic.Prod (_, src, tgt) ->
  72                  let tgt =
  73                    NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
  74                  in
  75 (*
  76             debug (lazy (Printf.sprintf "indicizzo %s (%d)) : %s ===> %s"
  77               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
  78               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
  79               (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
  80 *)
  81                 src, tgt
  82               | t ->
  83                   debug (lazy (
  84                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
  85                   assert false
  86             in
  87             index_coercion status c src tgt arity arg
  88            with
  89            | NCicEnvironment.BadDependency _
  90            | NCicTypeChecker.TypeCheckerFailure _ -> status)
  91          status clist)
  92     status (CoercDb.to_list odb)
  93 ;;
  94
  95 let look_for_coercion status metasenv subst context infty expty =
  96  let db_src,db_tgt = status#coerc_db in
  97   match infty, expty with
  98   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
  99     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
 100   | _ ->
 101
 102     debug (lazy ("LOOK FOR COERCIONS: " ^
 103       NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
 104       NCicPp.ppterm ~metasenv ~subst ~context expty));
 105
 106     let set_src = DB.retrieve_unifiables db_src infty in
 107     let set_tgt = DB.retrieve_unifiables db_tgt expty in
 108     let candidates = CoercionSet.inter set_src set_tgt in
 109
 110     debug (lazy ("CANDIDATES: " ^
 111       String.concat "," (List.map (fun (t,_,_) ->
 112         NCicPp.ppterm ~metasenv ~subst ~context t)
 113       (CoercionSet.elements candidates))));
 114
 115     List.map
 116       (fun (t,arity,arg) ->
 117           let ty =
 118             try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
 119             with NCicTypeChecker.TypeCheckerFailure s ->
 120              prerr_endline ("illtyped coercion: "^Lazy.force s);
 121              prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
 122              assert false
 123           in
 124           let ty, metasenv, args =
 125            NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
 126           in
 127
 128           debug (lazy (
 129             NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
 130             NCicPp.ppterm ~metasenv ~subst ~context
 131             (NCicUntrusted.mk_appl t args) ^ " --- " ^
 132               string_of_int (List.length args) ^ " == " ^ string_of_int arg));
 133
 134           metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
 135       (CoercionSet.elements candidates)
 136 ;;
 137
 138 (* CSC: very inefficient implementation!
 139    Enrico, can we use a discrimination tree here? *)
 140 let match_coercion status ~metasenv ~subst ~context t =
 141  let db =
 142   DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
 143  in
 144     (HExtlib.list_findopt
 145       (fun (p,arity,cpos) _ ->
 146         try
 147          let t =
 148           match p,t with
 149              NCic.Appl lp, NCic.Appl lt ->
 150               (match fst (HExtlib.split_nth (List.length lp) lt) with
 151                   [t] -> t
 152                 | l -> NCic.Appl l)
 153            | _,NCic.Appl (he::_) -> he
 154            | _,_ -> t
 155          in
 156          let b = NCicReduction.alpha_eq metasenv subst context p t in
 157          if not b then None else
 158          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
 159          let pis =
 160            let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
 161            aux ty
 162          in
 163          Some (p,pis - arity - cpos - 1,cpos)
 164         with
 165          Failure _ -> None (* raised by split_nth *)
 166       ) db)
 167 ;;