helm/software/components/ng_refiner/nCicMetaSubst.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 (* $Id$ *)
  13
  14 exception MetaSubstFailure of string Lazy.t
  15 exception Uncertain of string Lazy.t
  16
  17 (*
  18 (*** Functions to apply a substitution ***)
  19
  20 let apply_subst_gen ~appl_fun subst term =
  21  let rec um_aux =
  22   let module C = Cic in
  23   let module S = CicSubstitution in
  24    function
  25       C.Rel _ as t -> t
  26     | C.Var (uri,exp_named_subst) ->
  27        let exp_named_subst' =
  28          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  29        in
  30        C.Var (uri, exp_named_subst')
  31     | C.Meta (i, l) ->
  32         (try
  33           let (_, t,_) = lookup_subst i subst in
  34           um_aux (S.subst_meta l t)
  35         with CicUtil.Subst_not_found _ ->
  36           (* unconstrained variable, i.e. free in subst*)
  37           let l' =
  38             List.map (function None -> None | Some t -> Some (um_aux t)) l
  39           in
  40            C.Meta (i,l'))
  41     | C.Sort _
  42     | C.Implicit _ as t -> t
  43     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
  44     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
  45     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
  46     | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
  47     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
  48     | C.Appl _ -> assert false
  49     | C.Const (uri,exp_named_subst) ->
  50        let exp_named_subst' =
  51          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  52        in
  53        C.Const (uri, exp_named_subst')
  54     | C.MutInd (uri,typeno,exp_named_subst) ->
  55        let exp_named_subst' =
  56          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  57        in
  58        C.MutInd (uri,typeno,exp_named_subst')
  59     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
  60        let exp_named_subst' =
  61          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  62        in
  63        C.MutConstruct (uri,typeno,consno,exp_named_subst')
  64     | C.MutCase (sp,i,outty,t,pl) ->
  65        let pl' = List.map um_aux pl in
  66        C.MutCase (sp, i, um_aux outty, um_aux t, pl')
  67     | C.Fix (i, fl) ->
  68        let fl' =
  69          List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
  70        in
  71        C.Fix (i, fl')
  72     | C.CoFix (i, fl) ->
  73        let fl' =
  74          List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
  75        in
  76        C.CoFix (i, fl')
  77  in
  78   um_aux term
  79 ;;
  80
  81 let apply_subst =
  82   let appl_fun um_aux he tl =
  83     let tl' = List.map um_aux tl in
  84     let t' =
  85      match um_aux he with
  86         Cic.Appl l -> Cic.Appl (l@tl')
  87       | he' -> Cic.Appl (he'::tl')
  88     in
  89      begin
  90       match he with
  91          Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
  92        | _ -> t'
  93      end
  94   in
  95   fun subst t ->
  96 (*     incr apply_subst_counter; *)
  97 match subst with
  98    [] -> t
  99  | _ -> apply_subst_gen ~appl_fun subst t
 100 ;;
 101
 102 let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
 103 let apply_subst s t =
 104   profiler.HExtlib.profile (apply_subst s) t
 105
 106
 107 let apply_subst_context subst context =
 108  match subst with
 109     [] -> context
 110   | _ ->
 111 (*
 112   incr apply_subst_context_counter;
 113   context_length := !context_length + List.length context;
 114 *)
 115   List.fold_right
 116     (fun item context ->
 117       match item with
 118       | Some (n, Cic.Decl t) ->
 119           let t' = apply_subst subst t in
 120           Some (n, Cic.Decl t') :: context
 121       | Some (n, Cic.Def (t, ty)) ->
 122           let ty' = apply_subst subst ty in
 123           let t' = apply_subst subst t in
 124           Some (n, Cic.Def (t', ty')) :: context
 125       | None -> None :: context)
 126     context []
 127
 128 let apply_subst_metasenv subst metasenv =
 129 (*
 130   incr apply_subst_metasenv_counter;
 131   metasenv_length := !metasenv_length + List.length metasenv;
 132 *)
 133 match subst with
 134    [] -> metasenv
 135  | _ ->
 136   List.map
 137     (fun (n, context, ty) ->
 138       (n, apply_subst_context subst context, apply_subst subst ty))
 139     (List.filter
 140       (fun (i, _, _) -> not (List.mem_assoc i subst))
 141       metasenv)
 142
 143 let tempi_type_of_aux_subst = ref 0.0;;
 144 let tempi_subst = ref 0.0;;
 145 let tempi_type_of_aux = ref 0.0;;
 146 *)
 147
 148 let newmeta =
 149   let maxmeta = ref 0 in
 150   fun () -> incr maxmeta; !maxmeta
 151 ;;
 152
 153 exception NotInTheList;;
 154
 155 let position n (shift, lc) =
 156   match lc with
 157   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
 158   | NCic.Itl len -> n - shift
 159   | NCic.Ctx tl ->
 160       let rec aux k = function
 161          | [] -> raise NotInTheList
 162          | (Cic.Rel m)::_ when m + shift = n -> k
 163          | _::tl -> aux (k+1) tl
 164       in
 165        aux 1 tl
 166 ;;
 167
 168 exception Occur;;
 169
 170 let rec force_does_not_occur metasenv subst restrictions t =
 171  let rec aux k = function
 172     | C.Rel r when List.mem (r - k) restrictions -> raise Occur
 173     | C.Meta (n, l) as t ->
 174        (* we ignore the subst since restrict will take care of already
 175         * instantiated/restricted metavariabels *)
 176        let more_to_be_restricted = ref [] in
 177        let l' =
 178          let i = ref 0 in
 179          HExtlib.map_option
 180            (fun t ->
 181              incr i ;
 182              try
 183                let (*subst, metasenv,*) t = aux k t in Some t
 184              with Occur ->
 185                more_to_be_restricted := !i :: !more_to_be_restricted; None)
 186            l
 187        in
 188        if !more_to_be_restricted = [] then
 189          if l = l' then t else NCic.Meta (n, l')
 190        else
 191          let metasenv, subst, newmeta =
 192            restrict metasenv subst n !more_to_be_restricted
 193          in
 194            (*metasenv, subst,*) NCic.Meta (newmeta, l')
 195     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 196  in
 197    aux 0 t
 198
 199 and force_does_not_occur_in_context metasenv subst restrictions = function
 200   | name, NCic.Decl t as orig ->
 201       let metasenv, subst, t' =
 202         force_does_not_occur metasenv subst restrictions t
 203       in
 204       metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
 205   | name, NCic.Def (bo, ty) as orig ->
 206       let metasenv, subst, bo' =
 207         force_does_not_occur metasenv subst restrictions bo in
 208       let metasenv, subst, ty' =
 209         force_does_not_occur metasenv subst restrictions ty in
 210       metasenv, subst,
 211        (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))
 212
 213 and erase_in_context metasenv subst pos restrictions = function
 214   | [] -> metasenv, subst, restrictions, []
 215   | hd::tl as orig ->
 216       let metasenv, subst, restricted, tl' =
 217         erase_in_context metasenv subst (i+1) restrictions tl in
 218       if List.mem i restricted then
 219         metasenv, subst, restricted, tl'
 220       else
 221         try
 222           let metasenv, subst, hd' =
 223             let delifted_restricted = List.map ((+) ~-i) restricted in
 224              force_does_not_occur_in_context
 225               metasenv susbst delifted_restricted hd
 226           in
 227            metasenv, subst, restricted,
 228             (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
 229         with Occur ->
 230             metasenv, subst, (i :: restricted), tl'
 231
 232 and restrict metasenv subst i restrictions =
 233   assert (restrictions <> []);
 234   try
 235     let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
 236       try
 237         let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
 238         let metasenv, subst, restrictions, newctx =
 239           erase_in_context metasenv subst 1 restrictions in
 240         let metasenv, subst, _ =
 241           force_does_not_occur metasenv subst restrictions ty in
 242         let metasenv, subst, _ =
 243           force_does_not_occur metasenv subst restrictions bo in
 244         (* we don't care newly generated bo/tys since up to subst they are
 245          * convertible (only metas are substituted for metas *)
 246         metasenv, subst, ?
 247       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
 248             ("Cannot restrict the context of the metavariable ?%d over "^^
 249             "the hypotheses %s since ?%d is already instantiated "^^
 250             "with %s and at least one of the hypotheses occurs in "^^
 251             "the substituted term" i  (String.concat ", "
 252             (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
 253             (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo)))))
 254   with NCicUtils.Subst_not_found _ ->
 255     try
 256       let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
 257       let metasenv, subst, restrictions, newctx =
 258         erase_in_context metasenv subst 1 restrictions in
 259       let metasenv, subst, newty =
 260         force_does_not_occur metasenv subst restrictions ty in
 261       let j = newmeta () in
 262       let metasenv_entry = j, (name, newctx, newty) in
 263       let subst_entry = i,(name,ctx, NCic.Meta (j, irl - restrictions), ty) in
 264       List.map
 265         (fun (n,x) as orig -> if i = n then metasenv_entry else orig) metasenv,
 266       subst_entry :: subst, j
 267     with
 268     | NCicUtils.Meta_not_found _ -> assert false
 269     | Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
 270         ("Cannot restrict the context of the metavariable ?%d "^^
 271         "over the hypotheses %s since metavariable's type depends "^^
 272         "on at least one of them" i (String.concat ", "
 273         (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions))))))
 274
 275 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
 276    otherwise the occur check does not make sense in case of unification
 277    of ?n with ?n *)
 278 let delift metasenv subst context n l t =
 279   let to_be_restricted = ref [] in
 280   let rec aux k = function
 281     | NCic.Rel n as t when n <= k -> t
 282     | NCic.Rel n ->
 283         (try
 284           match List.nth context (n-k-1) with
 285           | _,NCic.Def (bo,_) ->
 286                 (try C.Rel ((position (n-k) l) + k)
 287                  with NotInTheList ->
 288                 (* CSC: This bit of reduction hurts performances since it is
 289                  * possible to  have an exponential explosion of the size of the
 290                  * proof. required for nat/nth_prime.ma *)
 291                   aux k (NCicSubstitution.lift n bo))
 292           | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k)
 293         with Failure _ -> assert false) (*Unbound variable found in delift*)
 294     | NCic.Meta (i,l1) as orig ->
 295         (try
 296            let _,_,t,_ = NCicUtil.lookup_subst i subst in
 297            aux k (NCicSubstitution.subst_meta l1 t)
 298          with NCicUtil.Subst_not_found _ ->
 299            (* see the top level invariant *)
 300            if (i = n) then
 301             raise (MetaSubstFailure (lazy (Printf.sprintf (
 302               "Cannot unify the metavariable ?%d with a term that has "^^
 303               "as subterm %s in which the same metavariable "^^
 304               "occurs (occur check)") i
 305                (NCicPp.ppterm ~context ~metasenv ~subst t))))
 306            else
 307               let shift1,lc1 = l1 in
 308               let shift,lc = l in
 309               match lc, lc1 with
 310               | NCic.Irl len, NCic.Irl len1
 311                 when shift1 < shift || len1 + shift1 > len + shift ->
 312                   let restrictions =
 313                      HExtlib.list_seq 1 (shift - shift1) @
 314                      HExtlib.list_seq (shift+len+1) (shift1+len1)
 315                   in
 316                   let subst, metasenv, newmeta =
 317                      restrict metasenv subst i restrictions
 318                   in
 319                   (* return that meta *)
 320                   assert false
 321               | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
 322               | NCic.Irl len, NCic.Irl len1 ->
 323                    NCic.Meta (i, (shift1 - shift, lc1))
 324               | _ ->
 325                   let lc1 = NCicUtils.expand_local_context lc1 in
 326                   let rec deliftl j = function
 327                     | [] -> []
 328                     | t::tl ->
 329                         let tl = deliftl (j+1) tl in
 330                         try (aux (k+shift1) t)::tl
 331                         with
 332                         | NotInTheList | MetaSubstFailure _ ->
 333                             to_be_restricted := (i,j)::!to_be_restricted;
 334                             tl
 335                   in
 336                   let l1 = deliftl 1 l1 in
 337                   C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
 338     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 339   in
 340   let t = aux 0 t in
 341   let metasenv, subst = restrict subst !to_be_restricted metasenv in
 342   metasenv, subst, t
 343 ;;
 344
 345 (*
 346   in
 347    let res =
 348     try
 349      deliftaux 0 t
 350     with
 351      NotInTheList ->
 352       (* This is the case where we fail even first order unification. *)
 353       (* The reason is that our delift function is weaker than first  *)
 354       (* order (in the sense of alpha-conversion). See comment above  *)
 355       (* related to the delift function.                              *)
 356 (* debug_print (lazy "First Order UnificationFailure during delift") ;
 357 debug_print(lazy (sprintf
 358         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 359         (ppterm subst t)
 360         (String.concat "; "
 361           (List.map
 362             (function Some t -> ppterm subst t | None -> "_") l
 363           )))); *)
 364       let msg = (lazy (sprintf
 365         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 366         (ppterm ~metasenv subst t)
 367         (String.concat "; "
 368           (List.map
 369             (function Some t -> ppterm ~metasenv subst t | None -> "_")
 370             l))))
 371       in
 372        if
 373          List.exists
 374           (function
 375               Some t -> CicUtil.is_meta_closed (apply_subst subst t)
 376             | None -> true) l
 377        then
 378         raise (Uncertain msg)
 379        else
 380         raise (MetaSubstFailure msg)
 381    in
 382    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
 383     res, metasenv, subst
 384 ;;
 385 *)
 386
 387 (*
 388 (* delifts a term t of n levels strating from k, that is changes (Rel m)
 389  * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
 390  *)
 391 let delift_rels_from subst metasenv k n =
 392  let rec liftaux subst metasenv k =
 393   let module C = Cic in
 394    function
 395       C.Rel m as t ->
 396        if m < k then
 397         t, subst, metasenv
 398        else if m < k + n then
 399          raise DeliftingARelWouldCaptureAFreeVariable
 400        else
 401         C.Rel (m - n), subst, metasenv
 402     | C.Var (uri,exp_named_subst) ->
 403        let exp_named_subst',subst,metasenv =
 404         List.fold_right
 405          (fun (uri,t) (l,subst,metasenv) ->
 406            let t',subst,metasenv = liftaux subst metasenv k t in
 407             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 408        in
 409         C.Var (uri,exp_named_subst'),subst,metasenv
 410     | C.Meta (i,l) ->
 411         (try
 412           let (_, t,_) = lookup_subst i subst in
 413            liftaux subst metasenv k (CicSubstitution.subst_meta l t)
 414          with CicUtil.Subst_not_found _ ->
 415           let l',to_be_restricted,subst,metasenv =
 416            let rec aux con l subst metasenv =
 417             match l with
 418                [] -> [],[],subst,metasenv
 419              | he::tl ->
 420                 let tl',to_be_restricted,subst,metasenv =
 421                  aux (con + 1) tl subst metasenv in
 422                 let he',more_to_be_restricted,subst,metasenv =
 423                  match he with
 424                     None -> None,[],subst,metasenv
 425                   | Some t ->
 426                      try
 427                       let t',subst,metasenv = liftaux subst metasenv k t in
 428                        Some t',[],subst,metasenv
 429                      with
 430                       DeliftingARelWouldCaptureAFreeVariable ->
 431                        None,[i,con],subst,metasenv
 432                 in
 433                  he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
 434            in
 435             aux 1 l subst metasenv in
 436           let metasenv,subst = restrict subst to_be_restricted metasenv in
 437            C.Meta(i,l'),subst,metasenv)
 438     | C.Sort _ as t -> t,subst,metasenv
 439     | C.Implicit _ as t -> t,subst,metasenv
 440     | C.Cast (te,ty) ->
 441        let te',subst,metasenv = liftaux subst metasenv k te in
 442        let ty',subst,metasenv = liftaux subst metasenv k ty in
 443         C.Cast (te',ty'),subst,metasenv
 444     | C.Prod (n,s,t) ->
 445        let s',subst,metasenv = liftaux subst metasenv k s in
 446        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 447         C.Prod (n,s',t'),subst,metasenv
 448     | C.Lambda (n,s,t) ->
 449        let s',subst,metasenv = liftaux subst metasenv k s in
 450        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 451         C.Lambda (n,s',t'),subst,metasenv
 452     | C.LetIn (n,s,ty,t) ->
 453        let s',subst,metasenv = liftaux subst metasenv k s in
 454        let ty',subst,metasenv = liftaux subst metasenv k ty in
 455        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 456         C.LetIn (n,s',ty',t'),subst,metasenv
 457     | C.Appl l ->
 458        let l',subst,metasenv =
 459         List.fold_right
 460          (fun t (l,subst,metasenv) ->
 461            let t',subst,metasenv = liftaux subst metasenv k t in
 462             t'::l,subst,metasenv) l ([],subst,metasenv) in
 463        C.Appl l',subst,metasenv
 464     | C.Const (uri,exp_named_subst) ->
 465        let exp_named_subst',subst,metasenv =
 466         List.fold_right
 467          (fun (uri,t) (l,subst,metasenv) ->
 468            let t',subst,metasenv = liftaux subst metasenv k t in
 469             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 470        in
 471         C.Const (uri,exp_named_subst'),subst,metasenv
 472     | C.MutInd (uri,tyno,exp_named_subst) ->
 473        let exp_named_subst',subst,metasenv =
 474         List.fold_right
 475          (fun (uri,t) (l,subst,metasenv) ->
 476            let t',subst,metasenv = liftaux subst metasenv k t in
 477             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 478        in
 479         C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
 480     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 481        let exp_named_subst',subst,metasenv =
 482         List.fold_right
 483          (fun (uri,t) (l,subst,metasenv) ->
 484            let t',subst,metasenv = liftaux subst metasenv k t in
 485             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 486        in
 487         C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
 488     | C.MutCase (sp,i,outty,t,pl) ->
 489        let outty',subst,metasenv = liftaux subst metasenv k outty in
 490        let t',subst,metasenv = liftaux subst metasenv k t in
 491        let pl',subst,metasenv =
 492         List.fold_right
 493          (fun t (l,subst,metasenv) ->
 494            let t',subst,metasenv = liftaux subst metasenv k t in
 495             t'::l,subst,metasenv) pl ([],subst,metasenv)
 496        in
 497         C.MutCase (sp,i,outty',t',pl'),subst,metasenv
 498     | C.Fix (i, fl) ->
 499        let len = List.length fl in
 500        let liftedfl,subst,metasenv =
 501         List.fold_right
 502          (fun (name, i, ty, bo) (l,subst,metasenv) ->
 503            let ty',subst,metasenv = liftaux subst metasenv k ty in
 504            let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
 505             (name,i,ty',bo')::l,subst,metasenv
 506          ) fl ([],subst,metasenv)
 507        in
 508         C.Fix (i, liftedfl),subst,metasenv
 509     | C.CoFix (i, fl) ->
 510        let len = List.length fl in
 511        let liftedfl,subst,metasenv =
 512         List.fold_right
 513          (fun (name, ty, bo) (l,subst,metasenv) ->
 514            let ty',subst,metasenv = liftaux subst metasenv k ty in
 515            let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
 516             (name,ty',bo')::l,subst,metasenv
 517          ) fl ([],subst,metasenv)
 518        in
 519         C.CoFix (i, liftedfl),subst,metasenv
 520  in
 521   liftaux subst metasenv k
 522
 523 let delift_rels subst metasenv n t =
 524   delift_rels_from subst metasenv 1 n t
 525 *)
 526