matita/components/grafite_engine/nCicCoercDeclaration.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 (* let debug s = prerr_endline (Lazy.force s) ;;*)
  13 let debug _ = ();;
  14
  15 let skel_dummy = NCic.Implicit `Type;;
  16
  17 let product f l1 l2 =
  18   List.fold_left
  19     (fun acc x ->
  20       List.fold_left
  21         (fun acc y ->
  22            f x y :: acc)
  23         acc l2)
  24     [] l1
  25 ;;
  26
  27 let pos_in_list x l =
  28       match
  29         HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
  30       with
  31       | Some i -> i
  32       | None -> assert false
  33 ;;
  34
  35 let rec count_prod = function
  36   | NCic.Prod (_,_,x) -> 1 + count_prod x
  37   | _ -> 0
  38 ;;
  39
  40 let term_at i t =
  41   match t with
  42   | NCic.Appl l ->
  43       (match
  44         HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
  45       with
  46       | Some i -> i
  47       | None -> assert false)
  48   | _ -> assert false
  49 ;;
  50
  51 let rec cleanup_funclass_skel = function
  52     | NCic.Prod (_,_,t) ->
  53         NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
  54     | _ -> skel_dummy
  55 ;;
  56
  57 let src_tgt_of_ty_cpos_arity status ty cpos arity =
  58   let pis = count_prod ty in
  59   let tpos = pis - arity in
  60   let rec pi_nth i j = function
  61     | NCic.Prod (_,s,_) when i = j -> s
  62     | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
  63     | t -> assert (i = j); t
  64   in
  65   let rec pi_tail i j = function
  66     | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
  67     | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
  68     | t -> assert (i = j); t
  69   in
  70   let mask t =
  71     let rec aux () = function
  72       | NCic.Meta _
  73       | NCic.Implicit _ as x -> x
  74       | NCic.Rel _ -> skel_dummy
  75       | t -> NCicUtils.map status (fun _ () -> ()) () aux t
  76     in
  77      aux () t
  78   in
  79   mask (pi_nth 0 cpos ty),
  80   mask (pi_tail 0 tpos ty)
  81 ;;
  82
  83 let rec cleanup_skel status () = function
  84   | NCic.Meta _ -> skel_dummy
  85   | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
  86 ;;
  87
  88 let close_in_context status t metasenv =
  89   let rec aux m_subst subst ctx = function
  90    | (i,(tag,[],ty)) :: tl ->
  91         let name = "x" ^ string_of_int (List.length ctx) in
  92         let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
  93         let ty = NCicUntrusted.apply_subst status (m_subst (List.length ctx)) ctx ty in
  94         let m_subst m =
  95           (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
  96         in
  97         NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
  98    | [] ->
  99            (* STRONG ASSUMPTION:
 100                 since metas occurring in t have an empty context,
 101                 the substitution i build makes sense (i.e, the Rel
 102                 I pun in the subst will not be lifted by subst_meta *)
 103            NCicUntrusted.apply_subst status subst ctx
 104              (NCicSubstitution.lift status (List.length ctx) t)
 105    | _ -> assert false
 106   in
 107   aux (fun _ -> []) [] [] metasenv
 108 ;;
 109
 110 let toposort status metasenv =
 111   let module T = HTopoSort.Make(
 112     struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
 113   in
 114   let deps (_,(_,_,t)) =
 115     List.filter (fun (j,_) ->
 116       List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
 117   in
 118   T.topological_sort metasenv deps
 119 ;;
 120
 121 let only_head = function
 122   | NCic.Appl (h::tl) ->
 123       NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
 124   | t -> t
 125 ;;
 126
 127 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 128   let status, src, cpos =
 129     let rec aux cpos ctx = function
 130       | NCic.Prod (name,ty,bo) ->
 131          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
 132          else
 133            (try
 134             let metasenv,subst,status,src =
 135               GrafiteDisambiguate.disambiguate_nterm
 136                 status None ctx [] [] ("",0,src) in
 137             let src = NCicUntrusted.apply_subst status subst [] src in
 138             (* CHECK that the declared pattern matches the abstraction *)
 139             let _ = NCicUnification.unify status metasenv subst ctx ty src in
 140             let src = cleanup_skel status () src in
 141             status, src, cpos
 142            with
 143            | NCicUnification.UnificationFailure msg
 144            | NCicUnification.Uncertain msg ->
 145                raise (GrafiteTypes.Command_error ("bad source pattern: " ^
 146 Lazy.force msg))
 147             | MultiPassDisambiguator.DisambiguationError _ ->
 148                raise (GrafiteTypes.Command_error ("bad source pattern:
 149 disambiguation error")))
 150       | _ -> assert false
 151     in
 152       aux 0 [] ty
 153   in
 154   let status, tgt, arity =
 155     let metasenv,subst,status,tgt =
 156       GrafiteDisambiguate.disambiguate_nterm
 157         status None [] [] [] ("",0,tgt) in
 158     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
 159     (* CHECK che sia unificabile mancante *)
 160     let rec count_prod = function
 161       | NCic.Prod (_,_,x) -> 1 + count_prod x
 162       | _ -> 0
 163     in
 164     let arity = count_prod tgt in
 165     let tgt=
 166       if arity > 0 then cleanup_funclass_skel tgt
 167       else cleanup_skel status () tgt
 168     in
 169      status, tgt, arity
 170   in
 171   status, src, tgt, cpos, arity
 172 ;;
 173
 174 let fresh_uri status prefix suffix =
 175   let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
 176   let rec diverge u i =
 177     if NCicLibrary.aliases_of u = [] then u
 178     else diverge (mk ("__" ^ string_of_int i)) (i+1)
 179   in
 180    diverge (mk "") 0
 181 ;;
 182
 183 exception Stop;;
 184
 185 let close_graph name t s d to_s from_d p a status =
 186   let c =
 187     List.find
 188      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
 189       (NCicCoercion.look_for_coercion status [] [] [] s d)
 190   in
 191   let compose_names a b = a ^ "__o__" ^ b in
 192   let composites =
 193     let to_s_o_c =
 194       product
 195         (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
 196           compose_names n1 n,m1@mc,c,[i,t1],j,a)
 197         to_s [c]
 198     in
 199     let c_o_from_d =
 200       product
 201         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
 202           compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty)
 203         [c] from_d
 204     in
 205     let to_s_o_c_o_from_d =
 206       product
 207         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
 208           compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
 209         to_s c_o_from_d
 210     in
 211     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
 212   in
 213   let composites =
 214     HExtlib.filter_map
 215      (fun (name,metasenv, bo, upl, p, arity) ->
 216         try
 217          let metasenv, subst =
 218            List.fold_left
 219             (fun (metasenv,subst) (a,b) ->
 220                 NCicUnification.unify status metasenv subst [] a b)
 221             (metasenv,[]) upl
 222          in
 223          let bo = NCicUntrusted.apply_subst status subst [] bo in
 224          let p = NCicUntrusted.apply_subst status subst [] p in
 225          let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
 226          let metasenv = toposort status metasenv in
 227          let bo = close_in_context status bo metasenv in
 228          let pos =
 229            match p with
 230            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
 231            | t -> raise Stop
 232          in
 233          let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
 234          let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
 235          let src = only_head src in
 236          let tgt = only_head tgt in
 237          debug (lazy(
 238            "composite " ^ name ^ ": "^
 239            status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
 240            status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
 241            status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
 242            status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
 243            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
 244          let uri = fresh_uri status name ".con" in
 245          let obj_kind = NCic.Constant
 246            ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity))
 247          in
 248          let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
 249          let obj = uri,height,[],[],obj_kind in
 250          let c =
 251            NCic.Const
 252              (NReference.reference_of_spec uri (NReference.Def height))
 253          in
 254          Some (obj,name,c,src,tgt,pos,arity)
 255        with
 256        | NCicTypeChecker.TypeCheckerFailure _
 257        | NCicUnification.UnificationFailure _
 258        | NCicUnification.Uncertain _ | Stop -> None
 259      ) composites
 260   in
 261     composites
 262 ;;
 263
 264 (* idempotent *)
 265 let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
 266   NCicCoercion.index_coercion status name t s d arity position
 267 ;;
 268
 269 let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
 270   let to_s =
 271     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
 272   in
 273   let from_d =
 274     NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
 275   in
 276   let status = NCicCoercion.index_coercion status name t s d a p in
 277   let composites =
 278    if compose then close_graph name t s d to_s from_d p a status else [] in
 279   List.fold_left
 280     (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
 281       let info = name,compose,t,s,d,p,a in
 282       let st = NCicLibrary.add_obj st obj in
 283       let st = basic_index_ncoercion info st in
 284       uri::uris, info::infos, st)
 285     ([],[],status) composites
 286 ;;
 287
 288 let record_ncoercion =
 289  let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
 290   let t = refresh_uri_in_term t in
 291   let s = refresh_uri_in_term s in
 292   let d = refresh_uri_in_term d in
 293    basic_index_ncoercion (name,compose,t,s,d,p,a)
 294  in
 295  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
 296   ~refresh_uri_in_reference ~alias_only status
 297  =
 298   if not alias_only then
 299    List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
 300   else
 301    status
 302  in
 303   GrafiteTypes.Serializer.register#run "ncoercion" aux_l
 304 ;;
 305
 306 let basic_eval_and_record_ncoercion infos status =
 307  let uris, cinfos, status = basic_eval_ncoercion infos status in
 308   NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 309 ;;
 310
 311 let basic_eval_and_record_ncoercion_from_t_cpos_arity
 312       status (name,compose,t,cpos,arity)
 313 =
 314   let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
 315   let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
 316   let status, uris =
 317    basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
 318   in
 319    status,uris
 320 ;;
 321
 322 let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt =
 323  let metasenv,subst,status,ty =
 324   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
 325  assert (metasenv=[]);
 326  let ty = NCicUntrusted.apply_subst status subst [] ty in
 327  let metasenv,subst,status,t =
 328   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
 329  assert (metasenv=[]);
 330  let t = NCicUntrusted.apply_subst status subst [] t in
 331  let status, src, tgt, cpos, arity =
 332    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
 333  let status, uris =
 334   basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
 335  in
 336   status,uris
 337 ;;
 338