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 _
 144            | NCicUnification.Uncertain _
 145            | MultiPassDisambiguator.DisambiguationError _ ->
 146                raise (GrafiteTypes.Command_error "bad source pattern"))
 147       | _ -> assert false
 148     in
 149       aux 0 [] ty
 150   in
 151   let status, tgt, arity =
 152     let metasenv,subst,status,tgt =
 153       GrafiteDisambiguate.disambiguate_nterm
 154         status None [] [] [] ("",0,tgt) in
 155     let tgt = NCicUntrusted.apply_subst status subst [] tgt in
 156     (* CHECK che sia unificabile mancante *)
 157     let rec count_prod = function
 158       | NCic.Prod (_,_,x) -> 1 + count_prod x
 159       | _ -> 0
 160     in
 161     let arity = count_prod tgt in
 162     let tgt=
 163       if arity > 0 then cleanup_funclass_skel tgt
 164       else cleanup_skel status () tgt
 165     in
 166      status, tgt, arity
 167   in
 168   status, src, tgt, cpos, arity
 169 ;;
 170
 171 let fresh_uri status prefix suffix =
 172   let mk x = NUri.uri_of_string (status#baseuri ^ "/" ^ prefix ^ x ^ suffix) in
 173   let rec diverge u i =
 174     if NCicLibrary.aliases_of u = [] then u
 175     else diverge (mk ("__" ^ string_of_int i)) (i+1)
 176   in
 177    diverge (mk "") 0
 178 ;;
 179
 180 exception Stop;;
 181
 182 let close_graph name t s d to_s from_d p a status =
 183   let c =
 184     List.find
 185      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
 186       (NCicCoercion.look_for_coercion status [] [] [] s d)
 187   in
 188   let compose_names a b = a ^ "__o__" ^ b in
 189   let composites =
 190     let to_s_o_c =
 191       product
 192         (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
 193           compose_names n1 n,m1@mc,c,[i,t1],j,a)
 194         to_s [c]
 195     in
 196     let c_o_from_d =
 197       product
 198         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
 199           compose_names n n1,m1@mc,t1,[i,c],j,count_prod ty)
 200         [c] from_d
 201     in
 202     let to_s_o_c_o_from_d =
 203       product
 204         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
 205           compose_names n1 n,m@m1,t,(i,t1)::upl,j,a)
 206         to_s c_o_from_d
 207     in
 208     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
 209   in
 210   let composites =
 211     HExtlib.filter_map
 212      (fun (name,metasenv, bo, upl, p, arity) ->
 213         try
 214          let metasenv, subst =
 215            List.fold_left
 216             (fun (metasenv,subst) (a,b) ->
 217                 NCicUnification.unify status metasenv subst [] a b)
 218             (metasenv,[]) upl
 219          in
 220          let bo = NCicUntrusted.apply_subst status subst [] bo in
 221          let p = NCicUntrusted.apply_subst status subst [] p in
 222          let metasenv = NCicUntrusted.apply_subst_metasenv status subst metasenv in
 223          let metasenv = toposort status metasenv in
 224          let bo = close_in_context status bo metasenv in
 225          let pos =
 226            match p with
 227            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
 228            | t -> raise Stop
 229          in
 230          let ty = NCicTypeChecker.typeof status ~metasenv:[] ~subst:[] [] bo in
 231          let src,tgt = src_tgt_of_ty_cpos_arity status ty pos arity in
 232          let src = only_head src in
 233          let tgt = only_head tgt in
 234          debug (lazy(
 235            "composite " ^ name ^ ": "^
 236            status#ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
 237            status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
 238            status#ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
 239            status#ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
 240            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
 241          let uri = fresh_uri status name ".con" in
 242          let obj_kind = NCic.Constant
 243            ([],name,Some bo,ty,(`Generated,`Definition,`Coercion arity))
 244          in
 245          let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
 246          let obj = uri,height,[],[],obj_kind in
 247          let c =
 248            NCic.Const
 249              (NReference.reference_of_spec uri (NReference.Def height))
 250          in
 251          Some (obj,name,c,src,tgt,pos,arity)
 252        with
 253        | NCicTypeChecker.TypeCheckerFailure _
 254        | NCicUnification.UnificationFailure _
 255        | NCicUnification.Uncertain _ | Stop -> None
 256      ) composites
 257   in
 258     composites
 259 ;;
 260
 261 (* idempotent *)
 262 let basic_index_ncoercion (name,_compose,t,s,d,position,arity) status =
 263   NCicCoercion.index_coercion status name t s d arity position
 264 ;;
 265
 266 let basic_eval_ncoercion (name,compose,t,s,d,p,a) status =
 267   let to_s =
 268     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
 269   in
 270   let from_d =
 271     NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
 272   in
 273   let status = NCicCoercion.index_coercion status name t s d a p in
 274   let composites =
 275    if compose then close_graph name t s d to_s from_d p a status else [] in
 276   List.fold_left
 277     (fun (uris,infos,st) ((uri,_,_,_,_ as obj),name,t,s,d,p,a) ->
 278       let info = name,compose,t,s,d,p,a in
 279       let st = NCicLibrary.add_obj st obj in
 280       let st = basic_index_ncoercion info st in
 281       uri::uris, info::infos, st)
 282     ([],[],status) composites
 283 ;;
 284
 285 let record_ncoercion =
 286  let aux (name,compose,t,s,d,p,a) ~refresh_uri_in_term =
 287   let t = refresh_uri_in_term t in
 288   let s = refresh_uri_in_term s in
 289   let d = refresh_uri_in_term d in
 290    basic_index_ncoercion (name,compose,t,s,d,p,a)
 291  in
 292  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
 293   ~refresh_uri_in_reference ~alias_only status
 294  =
 295   if not alias_only then
 296    List.fold_right (aux ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))) l status
 297   else
 298    status
 299  in
 300   GrafiteTypes.Serializer.register#run "ncoercion" aux_l
 301 ;;
 302
 303 let basic_eval_and_record_ncoercion infos status =
 304  let uris, cinfos, status = basic_eval_ncoercion infos status in
 305   NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 306 ;;
 307
 308 let basic_eval_and_record_ncoercion_from_t_cpos_arity
 309       status (name,compose,t,cpos,arity)
 310 =
 311   let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
 312   let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
 313   let status, uris =
 314    basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
 315   in
 316    status,uris
 317 ;;
 318
 319 let eval_ncoercion (status: #GrafiteTypes.status) name compose t ty (id,src) tgt =
 320  let metasenv,subst,status,ty =
 321   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
 322  assert (metasenv=[]);
 323  let ty = NCicUntrusted.apply_subst status subst [] ty in
 324  let metasenv,subst,status,t =
 325   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
 326  assert (metasenv=[]);
 327  let t = NCicUntrusted.apply_subst status subst [] t in
 328  let status, src, tgt, cpos, arity =
 329    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
 330  let status, uris =
 331   basic_eval_and_record_ncoercion (name,compose,t,src,tgt,cpos,arity) status
 332  in
 333   status,uris
 334 ;;
 335