helm/ocaml/cic_unification/cicMetaSubst.ml

   1 (* Copyright (C) 2003, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open Printf
  27
  28 (* PROFILING *)
  29 (*
  30 let deref_counter = ref 0
  31 let apply_subst_context_counter = ref 0
  32 let apply_subst_metasenv_counter = ref 0
  33 let lift_counter = ref 0
  34 let subst_counter = ref 0
  35 let whd_counter = ref 0
  36 let are_convertible_counter = ref 0
  37 let metasenv_length = ref 0
  38 let context_length = ref 0
  39 let reset_counters () =
  40  apply_subst_counter := 0;
  41  apply_subst_context_counter := 0;
  42  apply_subst_metasenv_counter := 0;
  43  lift_counter := 0;
  44  subst_counter := 0;
  45  whd_counter := 0;
  46  are_convertible_counter := 0;
  47  metasenv_length := 0;
  48  context_length := 0
  49 let print_counters () =
  50   prerr_endline (Printf.sprintf
  51 "apply_subst: %d
  52 apply_subst_context: %d
  53 apply_subst_metasenv: %d
  54 lift: %d
  55 subst: %d
  56 whd: %d
  57 are_convertible: %d
  58 metasenv length: %d (avg = %.2f)
  59 context length: %d (avg = %.2f)
  60 "
  61   !apply_subst_counter !apply_subst_context_counter
  62   !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter
  63   !are_convertible_counter !metasenv_length
  64   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
  65   !context_length
  66   ((float !context_length) /. (float !apply_subst_context_counter))
  67   )*)
  68
  69
  70
  71 exception MetaSubstFailure of string
  72 exception Uncertain of string
  73 exception AssertFailure of string
  74
  75 let debug_print = prerr_endline
  76
  77 type substitution = (int * (Cic.context * Cic.term)) list
  78
  79 (*
  80 let rec deref subst =
  81   let third _,_,a = a in
  82   function
  83       Cic.Meta(n,l) as t ->
  84         (try
  85            deref subst
  86              (CicSubstitution.lift_meta
  87                 l (third (CicUtil.lookup_subst n subst)))
  88          with
  89            CicUtil.Subst_not_found _ -> t)
  90     | t -> t
  91 ;;
  92 *)
  93
  94 let lookup_subst = CicUtil.lookup_subst
  95 ;;
  96
  97
  98 (* clean_up_meta take a metasenv and a term and make every local context
  99 of each occurrence of a metavariable consistent with its canonical context,
 100 with respect to the hidden hipothesis *)
 101
 102 (*
 103 let clean_up_meta subst metasenv t =
 104   let module C = Cic in
 105   let rec aux t =
 106   match t with
 107       C.Rel _
 108     | C.Sort _  -> t
 109     | C.Implicit _ -> assert false
 110     | C.Meta (n,l) as t ->
 111         let cc =
 112           (try
 113              let (cc,_) = lookup_subst n subst in cc
 114            with CicUtil.Subst_not_found _ ->
 115              try
 116                let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
 117              with CicUtil.Meta_not_found _ -> assert false) in
 118         let l' =
 119           (try
 120              List.map2
 121                (fun t1 t2 ->
 122                   match t1,t2 with
 123                       None , _ -> None
 124                     | _ , t -> t) cc l
 125            with
 126                Invalid_argument _ -> assert false) in
 127         C.Meta (n, l')
 128     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
 129     | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest)
 130     | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest)
 131     | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest)
 132     | C.Appl l -> C.Appl (List.map aux l)
 133     | C.Var (uri,exp_named_subst) ->
 134         let exp_named_subst' =
 135           List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
 136         in
 137         C.Var (uri, exp_named_subst')
 138     | C.Const (uri, exp_named_subst) ->
 139         let exp_named_subst' =
 140           List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
 141         in
 142         C.Const (uri, exp_named_subst')
 143     | C.MutInd (uri,tyno,exp_named_subst) ->
 144         let exp_named_subst' =
 145           List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
 146         in
 147         C.MutInd (uri, tyno, exp_named_subst')
 148     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 149         let exp_named_subst' =
 150           List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
 151         in
 152         C.MutConstruct (uri, tyno, consno, exp_named_subst')
 153     | C.MutCase (uri,tyno,out,te,pl) ->
 154         C.MutCase (uri, tyno, aux out, aux te, List.map aux pl)
 155     | C.Fix (i,fl) ->
 156        let fl' =
 157          List.map
 158           (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl
 159        in
 160        C.Fix (i, fl')
 161     | C.CoFix (i,fl) ->
 162        let fl' =
 163          List.map
 164           (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl
 165        in
 166        C.CoFix (i, fl')
 167  in
 168  aux t *)
 169
 170 (*** Functions to apply a substitution ***)
 171
 172 let apply_subst_gen ~appl_fun subst term =
 173  let rec um_aux =
 174   let module C = Cic in
 175   let module S = CicSubstitution in
 176    function
 177       C.Rel _ as t -> t
 178     | C.Var (uri,exp_named_subst) ->
 179        let exp_named_subst' =
 180          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 181        in
 182        C.Var (uri, exp_named_subst')
 183     | C.Meta (i, l) ->
 184         (try
 185           let (_, t,_) = lookup_subst i subst in
 186           um_aux (S.lift_meta l t)
 187         with CicUtil.Subst_not_found _ ->
 188           (* unconstrained variable, i.e. free in subst*)
 189           let l' =
 190             List.map (function None -> None | Some t -> Some (um_aux t)) l
 191           in
 192            C.Meta (i,l'))
 193     | C.Sort _ as t -> t
 194     | C.Implicit _ -> assert false
 195     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
 196     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
 197     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
 198     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
 199     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
 200     | C.Appl _ -> assert false
 201     | C.Const (uri,exp_named_subst) ->
 202        let exp_named_subst' =
 203          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 204        in
 205        C.Const (uri, exp_named_subst')
 206     | C.MutInd (uri,typeno,exp_named_subst) ->
 207        let exp_named_subst' =
 208          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 209        in
 210        C.MutInd (uri,typeno,exp_named_subst')
 211     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 212        let exp_named_subst' =
 213          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 214        in
 215        C.MutConstruct (uri,typeno,consno,exp_named_subst')
 216     | C.MutCase (sp,i,outty,t,pl) ->
 217        let pl' = List.map um_aux pl in
 218        C.MutCase (sp, i, um_aux outty, um_aux t, pl')
 219     | C.Fix (i, fl) ->
 220        let fl' =
 221          List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
 222        in
 223        C.Fix (i, fl')
 224     | C.CoFix (i, fl) ->
 225        let fl' =
 226          List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
 227        in
 228        C.CoFix (i, fl')
 229  in
 230  um_aux term
 231 ;;
 232
 233 let apply_subst =
 234 (* CSC: old code that never performs beta reduction
 235   let appl_fun um_aux he tl =
 236     let tl' = List.map um_aux tl in
 237       begin
 238        match um_aux he with
 239           Cic.Appl l -> Cic.Appl (l@tl')
 240         | he' -> Cic.Appl (he'::tl')
 241       end
 242   in
 243   apply_subst_gen ~appl_fun
 244 *)
 245   let appl_fun um_aux he tl =
 246     let tl' = List.map um_aux tl in
 247     let t' =
 248      match um_aux he with
 249         Cic.Appl l -> Cic.Appl (l@tl')
 250       | he' -> Cic.Appl (he'::tl')
 251     in
 252      begin
 253       match he with
 254          Cic.Meta (m,_) ->
 255           let rec beta_reduce =
 256            function
 257               (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
 258                 let he'' = CicSubstitution.subst he' t in
 259                  if tl' = [] then
 260                   he''
 261                  else
 262                   beta_reduce (Cic.Appl(he''::tl'))
 263             | t -> t
 264           in
 265            beta_reduce t'
 266        | _ -> t'
 267      end
 268   in
 269   fun s t ->
 270 (*     incr apply_subst_counter; *)
 271     apply_subst_gen ~appl_fun s t
 272 ;;
 273
 274 let rec apply_subst_context subst context =
 275 (*
 276   incr apply_subst_context_counter;
 277   context_length := !context_length + List.length context;
 278 *)
 279   List.fold_right
 280     (fun item context ->
 281       match item with
 282       | Some (n, Cic.Decl t) ->
 283           let t' = apply_subst subst t in
 284           Some (n, Cic.Decl t') :: context
 285       | Some (n, Cic.Def (t, ty)) ->
 286           let ty' =
 287             match ty with
 288             | None -> None
 289             | Some ty -> Some (apply_subst subst ty)
 290           in
 291           let t' = apply_subst subst t in
 292           Some (n, Cic.Def (t', ty')) :: context
 293       | None -> None :: context)
 294     context []
 295
 296 let apply_subst_metasenv subst metasenv =
 297 (*
 298   incr apply_subst_metasenv_counter;
 299   metasenv_length := !metasenv_length + List.length metasenv;
 300 *)
 301   List.map
 302     (fun (n, context, ty) ->
 303       (n, apply_subst_context subst context, apply_subst subst ty))
 304     (List.filter
 305       (fun (i, _, _) -> not (List.mem_assoc i subst))
 306       metasenv)
 307
 308 (***** Pretty printing functions ******)
 309
 310 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 311
 312 let ppterm_in_context subst term name_context =
 313  CicPp.pp (apply_subst subst term) name_context
 314
 315 let ppcontext' ?(sep = "\n") subst context =
 316  let separate s = if s = "" then "" else s ^ sep in
 317   List.fold_right
 318    (fun context_entry (i,name_context) ->
 319      match context_entry with
 320         Some (n,Cic.Decl t) ->
 321          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
 322           (ppterm_in_context subst t name_context), (Some n)::name_context
 323       | Some (n,Cic.Def (bo,ty)) ->
 324          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
 325           (match ty with
 326               None -> "_"
 327             | Some ty -> ppterm_in_context subst ty name_context)
 328           (ppterm_in_context subst bo name_context), (Some n)::name_context
 329        | None ->
 330           sprintf "%s_ :? _" (separate i), None::name_context
 331     ) context ("",[])
 332
 333 let ppsubst_unfolded subst =
 334   String.concat "\n"
 335     (List.map
 336       (fun (idx, (c, t,_)) ->
 337         let context,name_context = ppcontext' ~sep:"; " subst c in
 338          sprintf "%s |- ?%d:= %s" context idx
 339           (ppterm_in_context subst t name_context))
 340        subst)
 341 (*
 342         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
 343       subst) *)
 344 ;;
 345
 346 let ppsubst subst =
 347   String.concat "\n"
 348     (List.map
 349       (fun (idx, (c, t, _)) ->
 350         let context,name_context = ppcontext' ~sep:"; " [] c in
 351          sprintf "%s |- ?%d:= %s" context idx
 352           (ppterm_in_context [] t name_context))
 353        subst)
 354 ;;
 355
 356 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 357
 358 let ppmetasenv ?(sep = "\n") metasenv subst =
 359   String.concat sep
 360     (List.map
 361       (fun (i, c, t) ->
 362         let context,name_context = ppcontext' ~sep:"; " subst c in
 363          sprintf "%s |- ?%d: %s" context i
 364           (ppterm_in_context subst t name_context))
 365       (List.filter
 366         (fun (i, _, _) -> not (List.mem_assoc i subst))
 367         metasenv))
 368
 369 let tempi_type_of_aux_subst = ref 0.0;;
 370 let tempi_subst = ref 0.0;;
 371 let tempi_type_of_aux = ref 0.0;;
 372
 373 (**** DELIFT ****)
 374 (* the delift function takes in input a metavariable index, an ordered list of
 375  * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
 376  * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
 377  * substitution that is applied to a metavariable occurrence and the result of
 378  * the delift function is a term the implicit variable can be substituted with
 379  * to make the term [t] unifiable with the metavariable occurrence.  In general,
 380  * the problem is undecidable if we consider equivalence in place of alpha
 381  * convertibility. Our implementation, though, is even weaker than alpha
 382  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
 383  * (missing all the other cases). Does this matter in practice?
 384  * The metavariable index is the index of the metavariable that must not occur
 385  * in the term (for occur check).
 386  *)
 387
 388 exception NotInTheList;;
 389
 390 let position n =
 391   let rec aux k =
 392    function
 393        [] -> raise NotInTheList
 394      | (Some (Cic.Rel m))::_ when m=n -> k
 395      | _::tl -> aux (k+1) tl in
 396   aux 1
 397 ;;
 398
 399 exception Occur;;
 400
 401 let rec force_does_not_occur subst to_be_restricted t =
 402  let module C = Cic in
 403  let more_to_be_restricted = ref [] in
 404  let rec aux k = function
 405       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
 406     | C.Rel _
 407     | C.Sort _ as t -> t
 408     | C.Implicit _ -> assert false
 409     | C.Meta (n, l) ->
 410        (* we do not retrieve the term associated to ?n in subst since *)
 411        (* in this way we can restrict if something goes wrong         *)
 412        let l' =
 413          let i = ref 0 in
 414          List.map
 415            (function t ->
 416              incr i ;
 417              match t with
 418                 None -> None
 419               | Some t ->
 420                  try
 421                    Some (aux k t)
 422                  with Occur ->
 423                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
 424                    None)
 425            l
 426        in
 427         C.Meta (n, l')
 428     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
 429     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
 430     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
 431     | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
 432     | C.Appl l -> C.Appl (List.map (aux k) l)
 433     | C.Var (uri,exp_named_subst) ->
 434         let exp_named_subst' =
 435           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 436         in
 437         C.Var (uri, exp_named_subst')
 438     | C.Const (uri, exp_named_subst) ->
 439         let exp_named_subst' =
 440           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 441         in
 442         C.Const (uri, exp_named_subst')
 443     | C.MutInd (uri,tyno,exp_named_subst) ->
 444         let exp_named_subst' =
 445           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 446         in
 447         C.MutInd (uri, tyno, exp_named_subst')
 448     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 449         let exp_named_subst' =
 450           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 451         in
 452         C.MutConstruct (uri, tyno, consno, exp_named_subst')
 453     | C.MutCase (uri,tyno,out,te,pl) ->
 454         C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
 455     | C.Fix (i,fl) ->
 456        let len = List.length fl in
 457        let k_plus_len = k + len in
 458        let fl' =
 459          List.map
 460           (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
 461        in
 462        C.Fix (i, fl')
 463     | C.CoFix (i,fl) ->
 464        let len = List.length fl in
 465        let k_plus_len = k + len in
 466        let fl' =
 467          List.map
 468           (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
 469        in
 470        C.CoFix (i, fl')
 471  in
 472  let res = aux 0 t in
 473  (!more_to_be_restricted, res)
 474
 475 let rec restrict subst to_be_restricted metasenv =
 476   let names_of_context_indexes context indexes =
 477     String.concat ", "
 478       (List.map
 479         (fun i ->
 480           try
 481            match List.nth context (i-1) with
 482            | None -> assert false
 483            | Some (n, _) -> CicPp.ppname n
 484           with
 485            Failure _ -> assert false
 486         ) indexes)
 487   in
 488   let force_does_not_occur_in_context to_be_restricted = function
 489     | None -> [], None
 490     | Some (name, Cic.Decl t) ->
 491         let (more_to_be_restricted, t') =
 492           force_does_not_occur subst to_be_restricted t
 493         in
 494         more_to_be_restricted, Some (name, Cic.Decl t')
 495     | Some (name, Cic.Def (bo, ty)) ->
 496         let (more_to_be_restricted, bo') =
 497           force_does_not_occur subst to_be_restricted bo
 498         in
 499         let more_to_be_restricted, ty' =
 500           match ty with
 501           | None ->  more_to_be_restricted, None
 502           | Some ty ->
 503               let more_to_be_restricted', ty' =
 504                 force_does_not_occur subst to_be_restricted ty
 505               in
 506               more_to_be_restricted @ more_to_be_restricted',
 507               Some ty'
 508         in
 509         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
 510   in
 511   let rec erase i to_be_restricted n = function
 512     | [] -> [], to_be_restricted, []
 513     | hd::tl ->
 514         let more_to_be_restricted,restricted,tl' =
 515           erase (i+1) to_be_restricted n tl
 516         in
 517         let restrict_me = List.mem i restricted in
 518         if restrict_me then
 519           more_to_be_restricted, restricted, None:: tl'
 520         else
 521           (try
 522             let more_to_be_restricted', hd' =
 523               let delifted_restricted =
 524                let rec aux =
 525                 function
 526                    [] -> []
 527                  | j::tl when j > i -> (j - i)::aux tl
 528                  | _::tl -> aux tl
 529                in
 530                 aux restricted
 531               in
 532                force_does_not_occur_in_context delifted_restricted hd
 533             in
 534              more_to_be_restricted @ more_to_be_restricted',
 535              restricted, hd' :: tl'
 536           with Occur ->
 537             more_to_be_restricted, (i :: restricted), None :: tl')
 538   in
 539   let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
 540     List.fold_right
 541       (fun (n, context, t) (more, metasenv) ->
 542         let to_be_restricted =
 543           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 544         in
 545         let (more_to_be_restricted, restricted, context') =
 546          (* just an optimization *)
 547          if to_be_restricted = [] then
 548           [],[],context
 549          else
 550           erase 1 to_be_restricted n context
 551         in
 552         try
 553           let more_to_be_restricted', t' =
 554             force_does_not_occur subst restricted t
 555           in
 556           let metasenv' = (n, context', t') :: metasenv in
 557           (more @ more_to_be_restricted @ more_to_be_restricted',
 558           metasenv')
 559         with Occur ->
 560           raise (MetaSubstFailure (sprintf
 561             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
 562             n (names_of_context_indexes context to_be_restricted))))
 563       metasenv ([], [])
 564   in
 565   let (more_to_be_restricted', subst) = (* restrict subst *)
 566     List.fold_right
 567       (* TODO: cambiare dopo l'aggiunta del ty *)
 568       (fun (n, (context, term,ty)) (more, subst') ->
 569         let to_be_restricted =
 570           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 571         in
 572         (try
 573           let (more_to_be_restricted, restricted, context') =
 574            (* just an optimization *)
 575             if to_be_restricted = [] then
 576               [], [], context
 577             else
 578               erase 1 to_be_restricted n context
 579           in
 580           let more_to_be_restricted', term' =
 581             force_does_not_occur subst restricted term
 582           in
 583           let more_to_be_restricted'', ty' =
 584             force_does_not_occur subst restricted ty in
 585           let subst' = (n, (context', term',ty')) :: subst' in
 586           let more =
 587             more @ more_to_be_restricted
 588             @ more_to_be_restricted'@more_to_be_restricted'' in
 589           (more, subst')
 590         with Occur ->
 591           let error_msg = sprintf
 592             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
 593             n (names_of_context_indexes context to_be_restricted) n
 594             (ppterm subst term)
 595           in
 596           (* DEBUG
 597           prerr_endline error_msg;
 598           prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst));
 599           prerr_endline ("subst = \n" ^ (ppsubst subst));
 600           prerr_endline ("context = \n" ^ (ppcontext subst context)); *)
 601           raise (MetaSubstFailure error_msg)))
 602       subst ([], [])
 603   in
 604   match more_to_be_restricted @ more_to_be_restricted' with
 605   | [] -> (metasenv, subst)
 606   | l -> restrict subst l metasenv
 607 ;;
 608
 609 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
 610
 611 let delift n subst context metasenv l t =
 612 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
 613    otherwise the occur check does not make sense *)
 614
 615 (*
 616  prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
 617  al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))));
 618 *)
 619
 620  let module S = CicSubstitution in
 621   let l =
 622    let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
 623    List.map2 (fun ct lt ->
 624      match (ct, lt) with
 625      | None, _ -> None
 626      | Some _, _ -> lt)
 627      canonical_context l
 628   in
 629   let to_be_restricted = ref [] in
 630   let rec deliftaux k =
 631    let module C = Cic in
 632     function
 633        C.Rel m ->
 634          if m <=k then
 635           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
 636                     (*CSC: deliftato la regola per il LetIn                 *)
 637                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
 638          else
 639           (try
 640             match List.nth context (m-k-1) with
 641                Some (_,C.Def (t,_)) ->
 642                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
 643                 (*CSC: first order unification. Does it help or does it harm? *)
 644                 deliftaux k (S.lift m t)
 645              | Some (_,C.Decl t) ->
 646                 C.Rel ((position (m-k) l) + k)
 647              | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
 648            with
 649             Failure _ ->
 650              raise (MetaSubstFailure "Unbound variable found in deliftaux")
 651           )
 652      | C.Var (uri,exp_named_subst) ->
 653         let exp_named_subst' =
 654          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 655         in
 656          C.Var (uri,exp_named_subst')
 657      | C.Meta (i, l1) as t ->
 658          (try
 659            let (_,t,_) = CicUtil.lookup_subst i subst in
 660              deliftaux k (CicSubstitution.lift_meta l1 t)
 661          with CicUtil.Subst_not_found _ ->
 662            (* see the top level invariant *)
 663            if (i = n) then
 664             raise (MetaSubstFailure (sprintf
 665               "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
 666               i (ppterm subst t)))
 667           else
 668             begin
 669            (* I do not consider the term associated to ?i in subst since *)
 670            (* in this way I can restrict if something goes wrong.        *)
 671               let rec deliftl j =
 672                 function
 673                     [] -> []
 674                   | None::tl -> None::(deliftl (j+1) tl)
 675                   | (Some t)::tl ->
 676                       let l1' = (deliftl (j+1) tl) in
 677                         try
 678                           Some (deliftaux k t)::l1'
 679                         with
 680                             NotInTheList
 681                           | MetaSubstFailure _ ->
 682                               to_be_restricted :=
 683                               (i,j)::!to_be_restricted ; None::l1'
 684               in
 685               let l' = deliftl 1 l1 in
 686                 C.Meta(i,l')
 687             end)
 688      | C.Sort _ as t -> t
 689      | C.Implicit _ as t -> t
 690      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 691      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 692      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 693      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
 694      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 695      | C.Const (uri,exp_named_subst) ->
 696         let exp_named_subst' =
 697          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 698         in
 699          C.Const (uri,exp_named_subst')
 700      | C.MutInd (uri,typeno,exp_named_subst) ->
 701         let exp_named_subst' =
 702          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 703         in
 704          C.MutInd (uri,typeno,exp_named_subst')
 705      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 706         let exp_named_subst' =
 707          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 708         in
 709          C.MutConstruct (uri,typeno,consno,exp_named_subst')
 710      | C.MutCase (sp,i,outty,t,pl) ->
 711         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
 712          List.map (deliftaux k) pl)
 713      | C.Fix (i, fl) ->
 714         let len = List.length fl in
 715         let liftedfl =
 716          List.map
 717           (fun (name, i, ty, bo) ->
 718            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 719            fl
 720         in
 721          C.Fix (i, liftedfl)
 722      | C.CoFix (i, fl) ->
 723         let len = List.length fl in
 724         let liftedfl =
 725          List.map
 726           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 727            fl
 728         in
 729          C.CoFix (i, liftedfl)
 730   in
 731    let res =
 732     try
 733      deliftaux 0 t
 734     with
 735      NotInTheList ->
 736       (* This is the case where we fail even first order unification. *)
 737       (* The reason is that our delift function is weaker than first  *)
 738       (* order (in the sense of alpha-conversion). See comment above  *)
 739       (* related to the delift function.                              *)
 740 (* debug_print "First Order UnificationFailure during delift" ;
 741 prerr_endline(sprintf
 742         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 743         (ppterm subst t)
 744         (String.concat "; "
 745           (List.map
 746             (function Some t -> ppterm subst t | None -> "_") l
 747           ))); *)
 748       raise (Uncertain (sprintf
 749         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 750         (ppterm subst t)
 751         (String.concat "; "
 752           (List.map
 753             (function Some t -> ppterm subst t | None -> "_")
 754             l))))
 755    in
 756    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
 757     res, metasenv, subst
 758 ;;
 759
 760 (**** END OF DELIFT ****)
 761
 762
 763 (** {2 Format-like pretty printers} *)
 764
 765 let fpp_gen ppf s =
 766   Format.pp_print_string ppf s;
 767   Format.pp_print_newline ppf ();
 768   Format.pp_print_flush ppf ()
 769
 770 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
 771 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
 772 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
 773