helm/ocaml/cic_unification/cicMetaSubst.ml

   1
   2 open Printf
   3
   4 exception AssertFailure of string
   5 exception MetaSubstFailure of string
   6
   7 exception RelToHiddenHypothesis (* TODO remove this exception *)
   8
   9 let debug_print = prerr_endline
  10
  11 type substitution = (int * Cic.term) list
  12
  13 let ppsubst subst =
  14   String.concat "\n"
  15     (List.map
  16       (fun (idx, term) -> Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
  17       subst)
  18
  19 (**** DELIFT ****)
  20 (* the delift function takes in input a metavariable index, an ordered list of
  21  * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
  22  * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
  23  * substitution that is applied to a metavariable occurrence and the result of
  24  * the delift function is a term the implicit variable can be substituted with
  25  * to make the term [t] unifiable with the metavariable occurrence.  In general,
  26  * the problem is undecidable if we consider equivalence in place of alpha
  27  * convertibility. Our implementation, though, is even weaker than alpha
  28  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
  29  * (missing all the other cases). Does this matter in practice?
  30  * The metavariable index is the index of the metavariable that must not occur
  31  * in the term (for occur check).
  32  *)
  33
  34 exception NotInTheList;;
  35
  36 let position n =
  37   let rec aux k =
  38    function
  39        [] -> raise NotInTheList
  40      | (Some (Cic.Rel m))::_ when m=n -> k
  41      | _::tl -> aux (k+1) tl in
  42   aux 1
  43 ;;
  44
  45 (*CSC: this restriction function is utterly wrong, since it does not check  *)
  46 (*CSC: that the variable that is going to be restricted does not occur free *)
  47 (*CSC: in a part of the sequent that is not going to be restricted.         *)
  48 (*CSC: In particular, the whole approach is wrong; if restriction can fail  *)
  49 (*CSC: (as indeed it is the case), we can not collect all the restrictions  *)
  50 (*CSC: and restrict everything at the end ;-(                               *)
  51 let restrict to_be_restricted =
  52   let rec erase i n =
  53     function
  54         [] -> []
  55       |        _::tl when List.mem (n,i) to_be_restricted ->
  56           None::(erase (i+1) n tl)
  57       | he::tl -> he::(erase (i+1) n tl) in
  58   let rec aux =
  59     function
  60         [] -> []
  61       |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
  62   aux
  63 ;;
  64
  65 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
  66 let delift n subst context metasenv l t =
  67  let module S = CicSubstitution in
  68   let to_be_restricted = ref [] in
  69   let rec deliftaux k =
  70    let module C = Cic in
  71     function
  72        C.Rel m ->
  73          if m <=k then
  74           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
  75                     (*CSC: deliftato la regola per il LetIn                 *)
  76                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
  77          else
  78           (match List.nth context (m-k-1) with
  79             Some (_,C.Def (t,_)) ->
  80              (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
  81              (*CSC: first order unification. Does it help or does it harm? *)
  82              deliftaux k (S.lift m t)
  83           | Some (_,C.Decl t) ->
  84              (*CSC: The following check seems to be wrong!             *)
  85              (*CSC: B:Set |- ?2 : Set                                  *)
  86              (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x                 *)
  87              (*CSC: Why should I restrict ?2 over B? The instantiation *)
  88              (*CSC: ?1 := A is perfectly reasonable and well-typed.    *)
  89              (*CSC: Thus I comment out the following two lines that    *)
  90              (*CSC: are the incriminated ones.                         *)
  91              (*(* It may augment to_be_restricted *)
  92                ignore (deliftaux k (S.lift m t)) ;*)
  93              (*CSC: end of bug commented out                           *)
  94              C.Rel ((position (m-k) l) + k)
  95           | None -> raise RelToHiddenHypothesis)
  96      | C.Var (uri,exp_named_subst) ->
  97         let exp_named_subst' =
  98          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
  99         in
 100          C.Var (uri,exp_named_subst')
 101      | C.Meta (i, l1) as t ->
 102         if i = n then
 103           raise (MetaSubstFailure (sprintf
 104             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
 105             i (CicPp.ppterm t)))
 106         else
 107           (try
 108             deliftaux k (S.lift_meta l (List.assoc i subst))
 109           with Not_found ->
 110             let rec deliftl j =
 111              function
 112                 [] -> []
 113               | None::tl -> None::(deliftl (j+1) tl)
 114               | (Some t)::tl ->
 115                  let l1' = (deliftl (j+1) tl) in
 116                   try
 117                    Some (deliftaux k t)::l1'
 118                   with
 119                      RelToHiddenHypothesis
 120                    | NotInTheList
 121                    | MetaSubstFailure _ ->
 122                       to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
 123             in
 124              let l' = deliftl 1 l1 in
 125               C.Meta(i,l'))
 126      | C.Sort _ as t -> t
 127      | C.Implicit as t -> t
 128      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 129      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 130      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 131      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
 132      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 133      | C.Const (uri,exp_named_subst) ->
 134         let exp_named_subst' =
 135          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 136         in
 137          C.Const (uri,exp_named_subst')
 138      | C.MutInd (uri,typeno,exp_named_subst) ->
 139         let exp_named_subst' =
 140          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 141         in
 142          C.MutInd (uri,typeno,exp_named_subst')
 143      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 144         let exp_named_subst' =
 145          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 146         in
 147          C.MutConstruct (uri,typeno,consno,exp_named_subst')
 148      | C.MutCase (sp,i,outty,t,pl) ->
 149         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
 150          List.map (deliftaux k) pl)
 151      | C.Fix (i, fl) ->
 152         let len = List.length fl in
 153         let liftedfl =
 154          List.map
 155           (fun (name, i, ty, bo) ->
 156            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 157            fl
 158         in
 159          C.Fix (i, liftedfl)
 160      | C.CoFix (i, fl) ->
 161         let len = List.length fl in
 162         let liftedfl =
 163          List.map
 164           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 165            fl
 166         in
 167          C.CoFix (i, liftedfl)
 168   in
 169    let res =
 170     try
 171      deliftaux 0 t
 172     with
 173      NotInTheList ->
 174       (* This is the case where we fail even first order unification. *)
 175       (* The reason is that our delift function is weaker than first  *)
 176       (* order (in the sense of alpha-conversion). See comment above  *)
 177       (* related to the delift function.                              *)
 178 debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
 179       raise (MetaSubstFailure (sprintf
 180         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 181         (CicPp.ppterm t)
 182         (String.concat "; "
 183           (List.map
 184             (function Some t -> CicPp.ppterm t | None -> "_")
 185             l))))
 186    in
 187     res, restrict !to_be_restricted metasenv
 188 ;;
 189
 190 (**** END OF DELIFT ****)
 191
 192 let rec unwind metasenv subst unwinded t =
 193  let unwinded = ref unwinded in
 194  let frozen = ref [] in
 195  let rec um_aux metasenv =
 196   let module C = Cic in
 197   let module S = CicSubstitution in
 198    function
 199       C.Rel _ as t -> t,metasenv
 200     | C.Var _  as t -> t,metasenv
 201     | C.Meta (i,l) ->
 202         (try
 203           S.lift_meta l (List.assoc i !unwinded), metasenv
 204          with Not_found ->
 205            if List.mem i !frozen then
 206              raise (MetaSubstFailure
 207               "Failed to unify due to cyclic constraints (occur check)")
 208            else
 209             let saved_frozen = !frozen in
 210             frozen := i::!frozen ;
 211             let res =
 212              try
 213               let t = List.assoc i subst in
 214               let t',metasenv' = um_aux metasenv t in
 215               let _,metasenv'' =
 216                let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
 217                 delift i subst canonical_context metasenv' l t'
 218               in
 219                unwinded := (i,t')::!unwinded ;
 220                S.lift_meta l t', metasenv'
 221              with Not_found ->
 222                (* not constrained variable, i.e. free in subst*)
 223                let l',metasenv' =
 224                 List.fold_right
 225                  (fun t (tl,metasenv) ->
 226                    match t with
 227                       None -> None::tl,metasenv
 228                     | Some t ->
 229                        let t',metasenv' = um_aux metasenv t in
 230                         (Some t')::tl, metasenv'
 231                  ) l ([],metasenv)
 232                in
 233                 C.Meta (i,l'), metasenv'
 234             in
 235             frozen := saved_frozen ;
 236             res
 237         )
 238     | C.Sort _
 239     | C.Implicit as t -> t,metasenv
 240     | C.Cast (te,ty) ->
 241        let te',metasenv' = um_aux metasenv te in
 242        let ty',metasenv'' = um_aux metasenv' ty in
 243        C.Cast (te',ty'),metasenv''
 244     | C.Prod (n,s,t) ->
 245        let s',metasenv' = um_aux metasenv s in
 246        let t',metasenv'' = um_aux metasenv' t in
 247        C.Prod (n, s', t'), metasenv''
 248     | C.Lambda (n,s,t) ->
 249        let s',metasenv' = um_aux metasenv s in
 250        let t',metasenv'' = um_aux metasenv' t in
 251        C.Lambda (n, s', t'), metasenv''
 252     | C.LetIn (n,s,t) ->
 253        let s',metasenv' = um_aux metasenv s in
 254        let t',metasenv'' = um_aux metasenv' t in
 255        C.LetIn (n, s', t'), metasenv''
 256     | C.Appl (he::tl) ->
 257        let tl',metasenv' =
 258         List.fold_right
 259          (fun t (tl,metasenv) ->
 260            let t',metasenv' = um_aux metasenv t in
 261             t'::tl, metasenv'
 262          ) tl ([],metasenv)
 263        in
 264         begin
 265          match um_aux metasenv' he with
 266             (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
 267           | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
 268         end
 269     | C.Appl _ -> assert false
 270     | C.Const (uri,exp_named_subst) ->
 271        let exp_named_subst', metasenv' =
 272         List.fold_right
 273          (fun (uri,t) (tl,metasenv) ->
 274            let t',metasenv' = um_aux metasenv t in
 275             (uri,t')::tl, metasenv'
 276          ) exp_named_subst ([],metasenv)
 277        in
 278         C.Const (uri,exp_named_subst'),metasenv'
 279     | C.MutInd (uri,typeno,exp_named_subst) ->
 280        let exp_named_subst', metasenv' =
 281         List.fold_right
 282          (fun (uri,t) (tl,metasenv) ->
 283            let t',metasenv' = um_aux metasenv t in
 284             (uri,t')::tl, metasenv'
 285          ) exp_named_subst ([],metasenv)
 286        in
 287         C.MutInd (uri,typeno,exp_named_subst'),metasenv'
 288     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 289        let exp_named_subst', metasenv' =
 290         List.fold_right
 291          (fun (uri,t) (tl,metasenv) ->
 292            let t',metasenv' = um_aux metasenv t in
 293             (uri,t')::tl, metasenv'
 294          ) exp_named_subst ([],metasenv)
 295        in
 296         C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
 297     | C.MutCase (sp,i,outty,t,pl) ->
 298        let outty',metasenv' = um_aux metasenv outty in
 299        let t',metasenv'' = um_aux metasenv' t in
 300        let pl',metasenv''' =
 301         List.fold_right
 302          (fun p (pl,metasenv) ->
 303            let p',metasenv' = um_aux metasenv p in
 304             p'::pl, metasenv'
 305          ) pl ([],metasenv'')
 306        in
 307         C.MutCase (sp, i, outty', t', pl'),metasenv'''
 308     | C.Fix (i, fl) ->
 309        let len = List.length fl in
 310        let liftedfl,metasenv' =
 311         List.fold_right
 312          (fun (name, i, ty, bo) (fl,metasenv) ->
 313            let ty',metasenv' = um_aux metasenv ty in
 314            let bo',metasenv'' = um_aux metasenv' bo in
 315             (name, i, ty', bo')::fl,metasenv''
 316          ) fl ([],metasenv)
 317        in
 318         C.Fix (i, liftedfl),metasenv'
 319     | C.CoFix (i, fl) ->
 320        let len = List.length fl in
 321        let liftedfl,metasenv' =
 322         List.fold_right
 323          (fun (name, ty, bo) (fl,metasenv) ->
 324            let ty',metasenv' = um_aux metasenv ty in
 325            let bo',metasenv'' = um_aux metasenv' bo in
 326             (name, ty', bo')::fl,metasenv''
 327          ) fl ([],metasenv)
 328        in
 329         C.CoFix (i, liftedfl),metasenv'
 330  in
 331   let t',metasenv' = um_aux metasenv t in
 332    t',metasenv',!unwinded
 333
 334 let apply_subst subst t =
 335  (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
 336  let metasenv = [] in
 337   let (t',_,_) = unwind metasenv [] subst t in
 338    t'
 339
 340 (* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
 341 (* performs as (apply_subst subst t) until it finds an application of   *)
 342 (* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
 343 (* a new beta-redex; in this case up to [reductions_no] consecutive     *)
 344 (* beta-reductions are performed.                                       *)
 345 (* Hint: this function is usually called when [reductions_no]           *)
 346 (*  eta-expansions have been performed and the head of the new          *)
 347 (*  application has been unified with (META [meta_to_reduce]):          *)
 348 (*  during the unwinding the eta-expansions are undone.                 *)
 349
 350 let rec apply_subst_context subst =
 351     List.map (function
 352       | Some (n, Cic.Decl t) -> Some (n, Cic.Decl (apply_subst subst t))
 353       | Some (n, Cic.Def (t, ty)) ->
 354           let ty' =
 355             match ty with
 356             | None -> None
 357             | Some ty -> Some (apply_subst subst ty)
 358           in
 359           Some (n, Cic.Def (apply_subst subst t, ty'))
 360       | None -> None)
 361
 362 let rec apply_subst_reducing subst meta_to_reduce t =
 363  let rec um_aux =
 364   let module C = Cic in
 365   let module S = CicSubstitution in
 366    function
 367       C.Rel _
 368     | C.Var _  as t -> t
 369     | C.Meta (i,l) as t ->
 370        (try
 371          S.lift_meta l (List.assoc i subst)
 372         with Not_found ->
 373           C.Meta (i,l))
 374     | C.Sort _ as t -> t
 375     | C.Implicit as t -> t
 376     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
 377     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
 378     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
 379     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
 380     | C.Appl (he::tl) ->
 381        let tl' = List.map um_aux tl in
 382         let t' =
 383          match um_aux he with
 384             C.Appl l -> C.Appl (l@tl')
 385           | _ as he' -> C.Appl (he'::tl')
 386         in
 387          begin
 388           match meta_to_reduce,he with
 389              Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
 390               let rec beta_reduce =
 391                function
 392                   (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
 393                     let he'' = CicSubstitution.subst he' t in
 394                      if tl' = [] then
 395                       he''
 396                      else
 397                       beta_reduce (n-1,C.Appl(he''::tl'))
 398                 | (_,t) -> t
 399               in
 400                beta_reduce (reductions_no,t')
 401            | _,_ -> t'
 402          end
 403     | C.Appl _ -> assert false
 404     | C.Const (uri,exp_named_subst) ->
 405        let exp_named_subst' =
 406         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 407        in
 408         C.Const (uri,exp_named_subst')
 409     | C.MutInd (uri,typeno,exp_named_subst) ->
 410        let exp_named_subst' =
 411         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 412        in
 413         C.MutInd (uri,typeno,exp_named_subst')
 414     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 415        let exp_named_subst' =
 416         List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
 417        in
 418         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 419     | C.MutCase (sp,i,outty,t,pl) ->
 420        C.MutCase (sp, i, um_aux outty, um_aux t,
 421         List.map um_aux pl)
 422     | C.Fix (i, fl) ->
 423        let len = List.length fl in
 424        let liftedfl =
 425         List.map
 426          (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
 427           fl
 428        in
 429         C.Fix (i, liftedfl)
 430     | C.CoFix (i, fl) ->
 431        let len = List.length fl in
 432        let liftedfl =
 433         List.map
 434          (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
 435           fl
 436        in
 437         C.CoFix (i, liftedfl)
 438  in
 439    um_aux t
 440
 441 let ppcontext ?(sep = "\n") subst context =
 442   String.concat sep
 443     (List.rev_map (function
 444       | Some (n, Cic.Decl t) ->
 445           sprintf "%s : %s"
 446             (CicPp.ppname n) (CicPp.ppterm (apply_subst subst t))
 447       | Some (n, Cic.Def (t, ty)) ->
 448           sprintf "%s : %s := %s"
 449             (CicPp.ppname n)
 450             (match ty with
 451             | None -> "_"
 452             | Some ty -> CicPp.ppterm (apply_subst subst ty))
 453             (CicPp.ppterm (apply_subst subst t))
 454       | None -> "_")
 455       context)
 456
 457 let ppmetasenv ?(sep = "\n") subst metasenv =
 458   String.concat sep
 459     (List.map
 460       (fun (i, c, t) ->
 461         sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i
 462           (CicPp.ppterm (apply_subst subst t)))
 463       (List.filter
 464         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
 465         metasenv))
 466
 467 (* UNWIND THE MGU INSIDE THE MGU *)
 468 let unwind_subst metasenv subst =
 469   List.fold_left
 470    (fun (unwinded,metasenv) (i,_) ->
 471      let (_,canonical_context,_) = CicUtil.lookup_meta i metasenv in
 472      let identity_relocation_list =
 473       CicMkImplicit.identity_relocation_list_for_metavariable canonical_context
 474      in
 475       let (_,metasenv',subst') =
 476        unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
 477       in
 478        subst',metasenv'
 479    ) ([],metasenv) subst
 480
 481 (* From now on we recreate a kernel abstraction where substitutions are part of
 482  * the calculus *)
 483
 484 let lift metasenv subst n term =
 485   (* TODO unwind's result is thrown away :-( *)
 486   let (subst, _) = unwind_subst metasenv subst in
 487   let term = apply_subst subst term in
 488   try
 489     CicSubstitution.lift n term
 490   with e ->
 491     raise (MetaSubstFailure ("Lift failure: " ^
 492       Printexc.to_string e))
 493
 494 let whd metasenv subst context term =
 495   (* TODO unwind's result is thrown away :-( *)
 496   let (subst, _) = unwind_subst metasenv subst in
 497   let term = apply_subst subst term in
 498   let context = apply_subst_context subst context in
 499   try
 500     CicReduction.whd context term
 501   with e ->
 502     raise (MetaSubstFailure ("Weak head reduction failure: " ^
 503       Printexc.to_string e))
 504
 505 let are_convertible metasenv subst context t1 t2 =
 506   (* TODO unwind's result is thrown away :-( *)
 507   let (subst, _) = unwind_subst metasenv subst in
 508   let context = apply_subst_context subst context in
 509   let (t1, t2) = (apply_subst subst t1, apply_subst subst t2) in
 510   CicReduction.are_convertible context t1 t2
 511
 512 let type_of_aux' metasenv subst context term =
 513   (* TODO unwind's result is thrown away :-( *)
 514   let (subst, _) = unwind_subst metasenv subst in
 515   let term = apply_subst subst term in
 516   let context = apply_subst_context subst context in
 517   let metasenv =
 518     List.map
 519       (fun (i, c, t) -> (i, apply_subst_context subst c, apply_subst subst t))
 520       (List.filter
 521         (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
 522         metasenv)
 523   in
 524   try
 525     CicTypeChecker.type_of_aux' metasenv context term
 526   with CicTypeChecker.TypeCheckerFailure msg ->
 527     raise (MetaSubstFailure ("Type checker failure: " ^ msg))
 528