helm/ocaml/cic_unification/cicMetaSubst.ml

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