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