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 basic_eval_ncoercion (name,t,s,d,p,a) status =
 134   let to_s =
 135     NCicCoercion.look_for_coercion status [] [] [] skel_dummy s
 136   in
 137   let from_d =
 138     NCicCoercion.look_for_coercion status [] [] [] d skel_dummy
 139   in
 140   let status = NCicCoercion.index_coercion status name t s d a p in
 141   let c =
 142     List.find
 143      (function (_,_,NCic.Appl (x::_),_,_) -> x = t | _ -> assert false)
 144       (NCicCoercion.look_for_coercion status [] [] [] s d)
 145   in
 146   let compose_names a b = a ^ "__o__" ^ b in
 147   let composites =
 148     let to_s_o_c =
 149       product
 150         (fun (n1,m1,t1,_,j) (n,mc,c,_,i) ->
 151           compose_names n1 n,m1@mc,c,[i,t1],j,a)
 152         to_s [c]
 153     in
 154     let c_o_from_d =
 155       product
 156         (fun (n,mc,c,_,j) (n1,m1,t1,ty,i) ->
 157           compose_names n1 n,m1@mc,t1,[i,c],j,count_prod ty)
 158         [c] from_d
 159     in
 160     let to_s_o_c_o_from_d =
 161       product
 162         (fun (n1,m1,t1,_,j) (n,m,t,upl,i,a)->
 163           compose_names n n1,m@m1,t,(i,t1)::upl,j,a)
 164         to_s c_o_from_d
 165     in
 166     to_s_o_c @ c_o_from_d @ to_s_o_c_o_from_d
 167   in
 168   let composites =
 169     HExtlib.filter_map
 170      (fun (name,metasenv, bo, upl, p, arity) ->
 171         try
 172          let metasenv, subst =
 173            List.fold_left
 174             (fun (metasenv,subst) (a,b) ->
 175                 NCicUnification.unify status metasenv subst [] a b)
 176             (metasenv,[]) upl
 177          in
 178          let bo = NCicUntrusted.apply_subst subst [] bo in
 179          let metasenv = toposort metasenv in
 180          let bo = close_in_context bo metasenv in
 181          let pos =
 182            match p with
 183            | NCic.Meta (p,_) -> pos_in_list p (List.map fst metasenv)
 184            | _ -> assert false
 185          in
 186          let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] bo in
 187          let src,tgt = src_tgt_of_ty_cpos_arity ty pos arity in
 188          let src = only_head src in
 189          let tgt = only_head tgt in
 190          debug (lazy(
 191            "composite: "^
 192            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] bo ^ " : " ^
 193            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty ^ " as " ^
 194            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
 195            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^
 196            " cpos=" ^ string_of_int pos ^ " arity=" ^ string_of_int arity));
 197          Some (name,bo,src,tgt,arity,pos)
 198        with
 199        | NCicTypeChecker.TypeCheckerFailure _
 200        | NCicUnification.UnificationFailure _
 201        | NCicUnification.Uncertain _ -> None
 202      ) composites
 203   in
 204   List.fold_left
 205     (fun st (name,t,s,d,a,p) -> NCicCoercion.index_coercion st name t s d a p)
 206     status composites
 207 ;;
 208
 209 let inject_ncoercion =
 210  let basic_eval_ncoercion (name,t,s,d,p,a) ~refresh_uri_in_universe
 211   ~refresh_uri_in_term
 212  =
 213   let t = refresh_uri_in_term t in
 214   let s = refresh_uri_in_term s in
 215   let d = refresh_uri_in_term d in
 216    basic_eval_ncoercion (name,t,s,d,p,a)
 217  in
 218   NRstatus.Serializer.register "ncoercion" basic_eval_ncoercion
 219 ;;
 220
 221 let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
 222   let status, src, cpos =
 223     let rec aux cpos ctx = function
 224       | NCic.Prod (name,ty,bo) ->
 225          if name <> id then aux (cpos+1) ((name,NCic.Decl ty)::ctx) bo
 226          else
 227            (try
 228             let metasenv,subst,status,src =
 229               GrafiteDisambiguate.disambiguate_nterm
 230                 None status ctx [] [] ("",0,src) in
 231             let src = NCicUntrusted.apply_subst subst [] src in
 232             (* CHECK that the declared pattern matches the abstraction *)
 233             let _ = NCicUnification.unify status metasenv subst ctx ty src in
 234             let src = cleanup_skel () src in
 235             status, src, cpos
 236            with
 237            | NCicUnification.UnificationFailure _
 238            | NCicUnification.Uncertain _
 239            | MultiPassDisambiguator.DisambiguationError _ ->
 240                raise (GrafiteTypes.Command_error "bad source pattern"))
 241       | _ -> assert false
 242     in
 243       aux 0 [] ty
 244   in
 245   let status, tgt, arity =
 246     let metasenv,subst,status,tgt =
 247       GrafiteDisambiguate.disambiguate_nterm
 248         None status [] [] [] ("",0,tgt) in
 249     let tgt = NCicUntrusted.apply_subst subst [] tgt in
 250     (* CHECK che sia unificabile mancante *)
 251     let rec count_prod = function
 252       | NCic.Prod (_,_,x) -> 1 + count_prod x
 253       | _ -> 0
 254     in
 255     let arity = count_prod tgt in
 256     let tgt=
 257       if arity > 0 then cleanup_funclass_skel tgt
 258       else cleanup_skel () tgt
 259     in
 260      status, tgt, arity
 261   in
 262   status, src, tgt, cpos, arity
 263 ;;
 264
 265 let basic_eval_and_inject_ncoercion infos status =
 266  let status = basic_eval_ncoercion infos status in
 267  let dump = inject_ncoercion infos::status#dump in
 268   status#set_dump dump
 269 ;;
 270
 271 let basic_eval_and_inject_ncoercion_from_t_cpos_arity
 272       status (name,t,cpos,arity)
 273 =
 274   let ty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] t in
 275   let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
 276   basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
 277 ;;
 278
 279 let eval_ncoercion status name t ty (id,src) tgt =
 280
 281  let metasenv,subst,status,ty =
 282   GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,ty) in
 283  assert (metasenv=[]);
 284  let ty = NCicUntrusted.apply_subst subst [] ty in
 285  let metasenv,subst,status,t =
 286   GrafiteDisambiguate.disambiguate_nterm (Some ty) status [] [] [] ("",0,t) in
 287  assert (metasenv=[]);
 288  let t = NCicUntrusted.apply_subst subst [] t in
 289
 290  let status, src, tgt, cpos, arity =
 291    src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
 292  let status =
 293   basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
 294  in
 295   status,`New []
 296 ;;
 297