matitaB/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 (* TODO: all newast's must be returned to the caller in some way
  13  * e.g. modifying the status? *)
  14
  15 (* let debug s = prerr_endline (Lazy.force s) ;;*)
  16 let debug _ = ();;
  17
  18 let skel_dummy = NCic.Implicit `Type;;
  19
  20 let product f l1 l2 =
  21   List.fold_left
  22     (fun acc x ->
  23       List.fold_left
  24         (fun acc y ->
  25            f x y :: acc)
  26         acc l2)
  27     [] l1
  28 ;;
  29
  30 let pos_in_list x l =
  31       match
  32         HExtlib.list_findopt (fun y i -> if y = x then Some i else None) l
  33       with
  34       | Some i -> i
  35       | None -> assert false
  36 ;;
  37
  38 let rec count_prod = function
  39   | NCic.Prod (_,_,x) -> 1 + count_prod x
  40   | _ -> 0
  41 ;;
  42
  43 let term_at i t =
  44   match t with
  45   | NCic.Appl l ->
  46       (match
  47         HExtlib.list_findopt (fun y j -> if i+1=j then Some y else None) l
  48       with
  49       | Some i -> i
  50       | None -> assert false)
  51   | _ -> assert false
  52 ;;
  53
  54 let rec cleanup_funclass_skel = function
  55     | NCic.Prod (_,_,t) ->
  56         NCic.Prod ("_",skel_dummy, cleanup_funclass_skel t)
  57     | _ -> skel_dummy
  58 ;;
  59
  60 let src_tgt_of_ty_cpos_arity status ty cpos arity =
  61   let pis = count_prod ty in
  62   let tpos = pis - arity in
  63   let rec pi_nth i j = function
  64     | NCic.Prod (_,s,_) when i = j -> s
  65     | NCic.Prod (_,_,t) -> pi_nth (i+1) j t
  66     | t -> assert (i = j); t
  67   in
  68   let rec pi_tail i j = function
  69     | NCic.Prod (_,_,_) as t when i = j -> cleanup_funclass_skel t
  70     | NCic.Prod (_,_,t) -> pi_tail (i+1) j t
  71     | t -> assert (i = j); t
  72   in
  73   let mask t =
  74     let rec aux () = function
  75       | NCic.Meta _
  76       | NCic.Implicit _ as x -> x
  77       | NCic.Rel _ -> skel_dummy
  78       | t -> NCicUtils.map status (fun _ () -> ()) () aux t
  79     in
  80      aux () t
  81   in
  82   mask (pi_nth 0 cpos ty),
  83   mask (pi_tail 0 tpos ty)
  84 ;;
  85
  86 let rec cleanup_skel status () = function
  87   | NCic.Meta _ -> skel_dummy
  88   | t -> NCicUtils.map status (fun _ () -> ()) () (cleanup_skel status) t
  89 ;;
  90
  91 let close_in_context status t metasenv =
  92   let rec aux m_subst subst ctx = function
  93    | (i,(tag,[],ty)) :: tl ->
  94         let name = "x" ^ string_of_int (List.length ctx) in
  95         let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
  96         let ty = NCicUntrusted.apply_subst status (m_subst (List.length ctx)) ctx ty in
  97         let m_subst m =
  98           (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m)
  99         in
 100         NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl)
 101    | [] ->
 102            (* STRONG ASSUMPTION:
 103                 since metas occurring in t have an empty context,
 104                 the substitution i build makes sense (i.e, the Rel
 105                 I pun in the subst will not be lifted by subst_meta *)
 106            NCicUntrusted.apply_subst status subst ctx
 107              (NCicSubstitution.lift status (List.length ctx) t)
 108    | _ -> assert false
 109   in
 110   aux (fun _ -> []) [] [] metasenv
 111 ;;
 112
 113 let toposort status metasenv =
 114   let module T = HTopoSort.Make(
 115     struct type t = int * NCic.conjecture let compare (i,_) (j,_) = i-j end)
 116   in
 117   let deps (_,(_,_,t)) =
 118     List.filter (fun (j,_) ->
 119       List.mem j (NCicUntrusted.metas_of_term status [] [] t)) metasenv
 120   in
 121   T.topological_sort metasenv deps
 122 ;;
 123
 124 let only_head = function
 125   | NCic.Appl (h::tl) ->
 126       NCic.Appl (h :: HExtlib.mk_list skel_dummy (List.length tl))
 127   | t -> t
 128 ;;
 129
 130 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 131   let status, src, cpos =
 132     let rec aux cpos ctx = function
 133       | NCic.Prod (name,ty,bo) ->
 134          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
 135          else
 136            (try
 137             let metasenv,subst,status,src =
 138               GrafiteDisambiguate.disambiguate_nterm
 139                 status None ctx [] [] ("",0,src) in
 140             let src = NCicUntrusted.apply_subst status subst [] src in
 141             (* CHECK that the declared pattern matches the abstraction *)
 142             let _ = NCicUnification.unify status metasenv subst ctx ty src in
 143             let src = cleanup_skel status () src in
 144             status, src, cpos
 145            with
 146            | NCicUnification.UnificationFailure _
 147            | NCicUnification.Uncertain _
 148            | MultiPassDisambiguator.DisambiguationError _ ->
 149                raise (GrafiteTypes.Command_error "bad source pattern"))
 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 status 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,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_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   ~refresh_uri_in_reference ~alias_only status
 296  =
 297   if not alias_only then
 298    List.fold_right
 299     (aux ~refresh_uri_in_term:(refresh_uri_in_term
 300      (status:>NCicEnvironment.status))) l status
 301   else
 302    status
 303  in
 304   GrafiteTypes.Serializer.register#run "ncoercion" aux_l
 305 ;;
 306
 307 let basic_eval_and_record_ncoercion infos status =
 308  let uris, cinfos, status = basic_eval_ncoercion infos status in
 309   NCicLibrary.dump_obj status (record_ncoercion (infos::cinfos)), uris
 310 ;;
 311
 312 let basic_eval_and_record_ncoercion_from_t_cpos_arity
 313       status (name,t,cpos,arity)
 314 =
 315   let ty = NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] [] t in
 316   let src,tgt = src_tgt_of_ty_cpos_arity status ty cpos arity in
 317   let status, uris =
 318    basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
 319   in
 320    status,uris
 321 ;;
 322
 323 let eval_ncoercion (status: #GrafiteTypes.status) name t ty (id,src) tgt =
 324  let metasenv,subst,status,ty =
 325   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,ty) in
 326  assert (metasenv=[]);
 327  let ty = NCicUntrusted.apply_subst status subst [] ty in
 328  let metasenv,subst,status,t =
 329   GrafiteDisambiguate.disambiguate_nterm status (Some ty) [] [] [] ("",0,t) in
 330  assert (metasenv=[]);
 331  let t = NCicUntrusted.apply_subst status subst [] t in
 332  let status, src, tgt, cpos, arity =
 333    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
 334  let status, uris =
 335   basic_eval_and_record_ncoercion (name,t,src,tgt,cpos,arity) status
 336  in
 337   status,uris
 338 ;;
 339