helm/ocaml/cic_proof_checking/cicReduction.ml

   1 (* Copyright (C) 2000, 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 (* TODO unify exceptions *)
  27
  28 exception CicReductionInternalError;;
  29 exception WrongUriToInductiveDefinition;;
  30 exception Impossible of int;;
  31 exception ReferenceToConstant;;
  32 exception ReferenceToVariable;;
  33 exception ReferenceToCurrentProof;;
  34 exception ReferenceToInductiveDefinition;;
  35
  36 let debug = false
  37 let profile = false
  38 let debug_print s = if debug then prerr_endline (Lazy.force s)
  39
  40 let fdebug = ref 1;;
  41 let debug t env s =
  42  let rec debug_aux t i =
  43   let module C = Cic in
  44   let module U = UriManager in
  45    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  46  in
  47   if !fdebug = 0 then
  48    debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
  49 ;;
  50
  51 module type Strategy =
  52  sig
  53   type stack_term
  54   type env_term
  55   type ens_term
  56   val to_stack : Cic.term -> stack_term
  57   val to_stack_list : Cic.term list -> stack_term list
  58   val to_env : Cic.term -> env_term
  59   val to_ens : Cic.term -> ens_term
  60   val from_stack :
  61    unwind:
  62     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  63       Cic.term -> Cic.term) ->
  64    stack_term -> Cic.term
  65   val from_stack_list :
  66    unwind:
  67     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  68       Cic.term -> Cic.term) ->
  69    stack_term list -> Cic.term list
  70   val from_env : env_term -> Cic.term
  71   val from_ens : ens_term -> Cic.term
  72   val stack_to_env :
  73    reduce:
  74     (int * env_term list * ens_term Cic.explicit_named_substitution *
  75       Cic.term * stack_term list -> Cic.term) ->
  76    unwind:
  77     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  78       Cic.term -> Cic.term) ->
  79    stack_term -> env_term
  80   val compute_to_env :
  81    reduce:
  82     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
  83       stack_term list -> Cic.term) ->
  84    unwind:
  85     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  86       Cic.term -> Cic.term) ->
  87    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  88     Cic.term -> env_term
  89   val compute_to_stack :
  90    reduce:
  91     (int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term *
  92       stack_term list -> Cic.term) ->
  93    unwind:
  94     (int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  95       Cic.term -> Cic.term) ->
  96    int -> env_term list -> ens_term Cic.explicit_named_substitution ->
  97     Cic.term -> stack_term
  98  end
  99 ;;
 100
 101 module CallByNameStrategy =
 102  struct
 103   type stack_term = Cic.term
 104   type env_term = Cic.term
 105   type ens_term = Cic.term
 106   let to_stack v = v
 107   let to_stack_list l = l
 108   let to_env v = v
 109   let to_ens v = v
 110   let from_stack ~unwind v = v
 111   let from_stack_list ~unwind l = l
 112   let from_env v = v
 113   let from_ens v = v
 114   let stack_to_env ~reduce ~unwind v = v
 115   let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
 116   let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
 117  end
 118 ;;
 119
 120 module CallByValueStrategy =
 121  struct
 122   type stack_term = Cic.term
 123   type env_term = Cic.term
 124   type ens_term = Cic.term
 125   let to_stack v = v
 126   let to_stack_list l = l
 127   let to_env v = v
 128   let to_ens v = v
 129   let from_stack ~unwind v = v
 130   let from_stack_list ~unwind l = l
 131   let from_env v = v
 132   let from_ens v = v
 133   let stack_to_env ~reduce ~unwind v = v
 134   let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 135   let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
 136  end
 137 ;;
 138
 139 module CallByValueStrategyByNameOnConstants =
 140  struct
 141   type stack_term = Cic.term
 142   type env_term = Cic.term
 143   type ens_term = Cic.term
 144   let to_stack v = v
 145   let to_stack_list l = l
 146   let to_env v = v
 147   let to_ens v = v
 148   let from_stack ~unwind v = v
 149   let from_stack_list ~unwind l = l
 150   let from_env v = v
 151   let from_ens v = v
 152   let stack_to_env ~reduce ~unwind v = v
 153   let compute_to_stack ~reduce ~unwind k e ens =
 154    function
 155       Cic.Const _ as t -> unwind k e ens t
 156     | t -> reduce (k,e,ens,t,[])
 157   let compute_to_env ~reduce ~unwind k e ens =
 158    function
 159       Cic.Const _ as t -> unwind k e ens t
 160     | t -> reduce (k,e,ens,t,[])
 161  end
 162 ;;
 163
 164 module LazyCallByValueStrategy =
 165  struct
 166   type stack_term = Cic.term lazy_t
 167   type env_term = Cic.term lazy_t
 168   type ens_term = Cic.term lazy_t
 169   let to_stack v = lazy v
 170   let to_stack_list l = List.map to_stack l
 171   let to_env v = lazy v
 172   let to_ens v = lazy v
 173   let from_stack ~unwind v = Lazy.force v
 174   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 175   let from_env v = Lazy.force v
 176   let from_ens v = Lazy.force v
 177   let stack_to_env ~reduce ~unwind v = v
 178   let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 179   let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
 180  end
 181 ;;
 182
 183 module LazyCallByValueStrategyByNameOnConstants =
 184  struct
 185   type stack_term = Cic.term lazy_t
 186   type env_term = Cic.term lazy_t
 187   type ens_term = Cic.term lazy_t
 188   let to_stack v = lazy v
 189   let to_stack_list l = List.map to_stack l
 190   let to_env v = lazy v
 191   let to_ens v = lazy v
 192   let from_stack ~unwind v = Lazy.force v
 193   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 194   let from_env v = Lazy.force v
 195   let from_ens v = Lazy.force v
 196   let stack_to_env ~reduce ~unwind v = v
 197   let compute_to_stack ~reduce ~unwind k e ens t =
 198    lazy (
 199     match t with
 200        Cic.Const _ as t -> unwind k e ens t
 201      | t -> reduce (k,e,ens,t,[]))
 202   let compute_to_env ~reduce ~unwind k e ens t =
 203    lazy (
 204     match t with
 205        Cic.Const _ as t -> unwind k e ens t
 206      | t -> reduce (k,e,ens,t,[]))
 207  end
 208 ;;
 209
 210 module LazyCallByNameStrategy =
 211  struct
 212   type stack_term = Cic.term lazy_t
 213   type env_term = Cic.term lazy_t
 214   type ens_term = Cic.term lazy_t
 215   let to_stack v = lazy v
 216   let to_stack_list l = List.map to_stack l
 217   let to_env v = lazy v
 218   let to_ens v = lazy v
 219   let from_stack ~unwind v = Lazy.force v
 220   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 221   let from_env v = Lazy.force v
 222   let from_ens v = Lazy.force v
 223   let stack_to_env ~reduce ~unwind v = v
 224   let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 225   let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
 226  end
 227 ;;
 228
 229 module
 230  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
 231 =
 232  struct
 233   type stack_term = reduce:bool -> Cic.term
 234   type env_term = reduce:bool -> Cic.term
 235   type ens_term = reduce:bool -> Cic.term
 236   let to_stack v =
 237    let value = lazy v in
 238     fun ~reduce -> Lazy.force value
 239   let to_stack_list l = List.map to_stack l
 240   let to_env v =
 241    let value = lazy v in
 242     fun ~reduce -> Lazy.force value
 243   let to_ens v =
 244    let value = lazy v in
 245     fun ~reduce -> Lazy.force value
 246   let from_stack ~unwind v = (v ~reduce:false)
 247   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 248   let from_env v = (v ~reduce:true)
 249   let from_ens v = (v ~reduce:true)
 250   let stack_to_env ~reduce ~unwind v = v
 251   let compute_to_stack ~reduce ~unwind k e ens t =
 252    let svalue =
 253      lazy (
 254       match t with
 255          Cic.Const _ as t -> unwind k e ens t
 256        | t -> reduce (k,e,ens,t,[])
 257      ) in
 258    let lvalue =
 259     lazy (unwind k e ens t)
 260    in
 261     fun ~reduce ->
 262      if reduce then Lazy.force svalue else Lazy.force lvalue
 263   let compute_to_env ~reduce ~unwind k e ens t =
 264    let svalue =
 265      lazy (
 266       match t with
 267          Cic.Const _ as t -> unwind k e ens t
 268        | t -> reduce (k,e,ens,t,[])
 269      ) in
 270    let lvalue =
 271     lazy (unwind k e ens t)
 272    in
 273     fun ~reduce ->
 274      if reduce then Lazy.force svalue else Lazy.force lvalue
 275  end
 276 ;;
 277
 278 module ClosuresOnStackByValueFromEnvOrEnsStrategy =
 279  struct
 280   type stack_term =
 281    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 282   type env_term = Cic.term
 283   type ens_term = Cic.term
 284   let to_stack v = (0,[],[],v)
 285   let to_stack_list l = List.map to_stack l
 286   let to_env v = v
 287   let to_ens v = v
 288   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 289   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 290   let from_env v = v
 291   let from_ens v = v
 292   let stack_to_env ~reduce ~unwind (k,e,ens,t) = reduce (k,e,ens,t,[])
 293   let compute_to_env ~reduce ~unwind k e ens t =
 294    unwind k e ens t
 295   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 296  end
 297 ;;
 298
 299 module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
 300  struct
 301   type stack_term =
 302    int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
 303   type env_term = Cic.term
 304   type ens_term = Cic.term
 305   let to_stack v = (0,[],[],v)
 306   let to_stack_list l = List.map to_stack l
 307   let to_env v = v
 308   let to_ens v = v
 309   let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
 310   let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
 311   let from_env v = v
 312   let from_ens v = v
 313   let stack_to_env ~reduce ~unwind (k,e,ens,t) =
 314    match t with
 315       Cic.Const _ as t -> unwind k e ens t
 316     | t -> reduce (k,e,ens,t,[])
 317   let compute_to_env ~reduce ~unwind k e ens t =
 318    unwind k e ens t
 319   let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
 320  end
 321 ;;
 322
 323 module Reduction(RS : Strategy) =
 324  struct
 325   type env = RS.env_term list
 326   type ens = RS.ens_term Cic.explicit_named_substitution
 327   type stack = RS.stack_term list
 328   type config = int * env * ens * Cic.term * stack
 329
 330   (* k is the length of the environment e *)
 331   (* m is the current depth inside the term *)
 332   let unwind' m k e ens t =
 333    let module C = Cic in
 334    let module S = CicSubstitution in
 335     if k = 0 && ens = [] then
 336      t
 337     else
 338      let rec unwind_aux m =
 339       function
 340          C.Rel n as t ->
 341           if n <= m then t else
 342            let d =
 343             try
 344              Some (RS.from_env (List.nth e (n-m-1)))
 345             with _ -> None
 346            in
 347             (match d with
 348                 Some t' ->
 349                  if m = 0 then t' else S.lift m t'
 350               | None -> C.Rel (n-k)
 351             )
 352        | C.Var (uri,exp_named_subst) ->
 353 (*
 354 debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
 355 *)
 356          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 357           CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
 358          else
 359           let params =
 360             let o,_ =
 361               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 362             in
 363            (match o with
 364                C.Constant _ -> raise ReferenceToConstant
 365              | C.Variable (_,_,_,params,_) -> params
 366              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 367              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 368            )
 369           in
 370            let exp_named_subst' =
 371             substaux_in_exp_named_subst params exp_named_subst m
 372            in
 373             C.Var (uri,exp_named_subst')
 374        | C.Meta (i,l) ->
 375           let l' =
 376            List.map
 377             (function
 378                 None -> None
 379               | Some t -> Some (unwind_aux m t)
 380             ) l
 381           in
 382            C.Meta (i, l')
 383        | C.Sort _ as t -> t
 384        | C.Implicit _ as t -> t
 385        | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*)
 386        | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t)
 387        | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t)
 388        | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
 389        | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
 390        | C.Const (uri,exp_named_subst) ->
 391           let params =
 392             let o,_ =
 393               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 394             in
 395            (match o with
 396                C.Constant (_,_,_,params,_) -> params
 397              | C.Variable _ -> raise ReferenceToVariable
 398              | C.CurrentProof (_,_,_,_,params,_) -> params
 399              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 400            )
 401           in
 402            let exp_named_subst' =
 403             substaux_in_exp_named_subst params exp_named_subst m
 404            in
 405             C.Const (uri,exp_named_subst')
 406        | C.MutInd (uri,i,exp_named_subst) ->
 407           let params =
 408             let o,_ =
 409               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 410             in
 411            (match o with
 412                C.Constant _ -> raise ReferenceToConstant
 413              | C.Variable _ -> raise ReferenceToVariable
 414              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 415              | C.InductiveDefinition (_,params,_,_) -> params
 416            )
 417           in
 418            let exp_named_subst' =
 419             substaux_in_exp_named_subst params exp_named_subst m
 420            in
 421             C.MutInd (uri,i,exp_named_subst')
 422        | C.MutConstruct (uri,i,j,exp_named_subst) ->
 423           let params =
 424             let o,_ =
 425               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 426             in
 427            (match o with
 428                C.Constant _ -> raise ReferenceToConstant
 429              | C.Variable _ -> raise ReferenceToVariable
 430              | C.CurrentProof _ -> raise ReferenceToCurrentProof
 431              | C.InductiveDefinition (_,params,_,_) -> params
 432            )
 433           in
 434            let exp_named_subst' =
 435             substaux_in_exp_named_subst params exp_named_subst m
 436            in
 437             C.MutConstruct (uri,i,j,exp_named_subst')
 438        | C.MutCase (sp,i,outt,t,pl) ->
 439           C.MutCase (sp,i,unwind_aux m outt, unwind_aux m t,
 440            List.map (unwind_aux m) pl)
 441        | C.Fix (i,fl) ->
 442           let len = List.length fl in
 443           let substitutedfl =
 444            List.map
 445             (fun (name,i,ty,bo) ->
 446               (name, i, unwind_aux m ty, unwind_aux (m+len) bo))
 447              fl
 448           in
 449            C.Fix (i, substitutedfl)
 450        | C.CoFix (i,fl) ->
 451           let len = List.length fl in
 452           let substitutedfl =
 453            List.map
 454             (fun (name,ty,bo) -> (name, unwind_aux m ty, unwind_aux (m+len) bo))
 455              fl
 456           in
 457            C.CoFix (i, substitutedfl)
 458      and substaux_in_exp_named_subst params exp_named_subst' m  =
 459   (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params
 460       let ens' =
 461        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 462   (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *)
 463         List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens
 464       in
 465       let rec filter_and_lift =
 466        function
 467           [] -> []
 468         | uri::tl ->
 469            let r = filter_and_lift tl in
 470             (try
 471               (uri,(List.assq uri ens'))::r
 472              with
 473               Not_found -> r
 474             )
 475       in
 476        filter_and_lift params
 477   *)
 478
 479   (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *)
 480   (*CSC: e' vero???? una veloce prova non sembra confermare la teoria        *)
 481
 482   (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *)
 483   (*CSC: codice altamente inefficiente *)
 484       let rec filter_and_lift already_instantiated =
 485        function
 486           [] -> []
 487         | (uri,t)::tl when
 488             List.for_all
 489              (function (uri',_)-> not (UriManager.eq uri uri')) exp_named_subst'
 490             &&
 491              not (List.mem uri already_instantiated)
 492             &&
 493              List.mem uri params
 494            ->
 495             (uri,CicSubstitution.lift m (RS.from_ens t)) ::
 496              (filter_and_lift (uri::already_instantiated) tl)
 497         | _::tl -> filter_and_lift already_instantiated tl
 498 (*
 499         | (uri,_)::tl ->
 500 debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
 501 if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
 502 exp_named_subst' then debug_print (lazy "---- OK1") ;
 503 debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
 504 if List.mem uri params then debug_print (lazy "---- OK2") ;
 505         filter_and_lift tl
 506 *)
 507       in
 508        List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @
 509         (filter_and_lift [] (List.rev ens))
 510      in
 511       unwind_aux m t
 512   ;;
 513
 514   let unwind = unwind' 0;;
 515
 516 (*
 517   let unwind =
 518    let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in
 519     fun k e ens t ->
 520      profiler_unwind.HExtlib.profile (unwind k e ens) t
 521   ;;
 522 *)
 523
 524   let reduce ~delta ?(subst = []) context : config -> Cic.term =
 525    let module C = Cic in
 526    let module S = CicSubstitution in
 527    let rec reduce =
 528     function
 529        (k, e, _, (C.Rel n as t), s) ->
 530         let d =
 531          try
 532           Some (RS.from_env (List.nth e (n-1)))
 533          with
 534           _ ->
 535            try
 536             begin
 537              match List.nth context (n - 1 - k) with
 538                 None -> assert false
 539               | Some (_,C.Decl _) -> None
 540               | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
 541             end
 542            with
 543             _ -> None
 544         in
 545          (match d with
 546              Some t' -> reduce (0,[],[],t',s)
 547            | None ->
 548               if s = [] then
 549                C.Rel (n-k)
 550               else C.Appl (C.Rel (n-k)::(RS.from_stack_list ~unwind s))
 551          )
 552      | (k, e, ens, (C.Var (uri,exp_named_subst) as t), s) ->
 553          if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
 554           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
 555          else
 556           ( let o,_ =
 557               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 558             in
 559             match o with
 560               C.Constant _ -> raise ReferenceToConstant
 561             | C.CurrentProof _ -> raise ReferenceToCurrentProof
 562             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 563             | C.Variable (_,None,_,_,_) ->
 564                let t' = unwind k e ens t in
 565                 if s = [] then t' else
 566                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 567             | C.Variable (_,Some body,_,_,_) ->
 568                let ens' = push_exp_named_subst k e ens exp_named_subst in
 569                 reduce (0, [], ens', body, s)
 570           )
 571      | (k, e, ens, (C.Meta (n,l) as t), s) ->
 572         (try
 573            let (_, term,_) = CicUtil.lookup_subst n subst in
 574            reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
 575          with  CicUtil.Subst_not_found _ ->
 576            let t' = unwind k e ens t in
 577            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
 578      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
 579      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
 580      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
 581         reduce (k, e, ens, te, s) (* s should be empty *)
 582      | (k, e, ens, (C.Prod _ as t), s) ->
 583          unwind k e ens t (* s should be empty *)
 584      | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
 585      | (k, e, ens, C.Lambda (_,_,t), p::s) ->
 586          reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
 587      | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
 588         let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
 589          reduce (k+1, m'::e, ens, t, s)
 590      | (_, _, _, C.Appl [], _) -> assert false
 591      | (k, e, ens, C.Appl (he::tl), s) ->
 592         let tl' =
 593          List.map
 594           (function t -> RS.compute_to_stack ~reduce ~unwind k e ens t) tl
 595         in
 596          reduce (k, e, ens, he, (List.append tl') s)
 597   (* CSC: Old Dead Code
 598      | (k, e, ens, C.Appl ((C.Lambda _ as he)::tl), s)
 599      | (k, e, ens, C.Appl ((C.Const _ as he)::tl), s)
 600      | (k, e, ens, C.Appl ((C.MutCase _ as he)::tl), s)
 601      | (k, e, ens, C.Appl ((C.Fix _ as he)::tl), s) ->
 602   (* strict evaluation, but constants are NOT unfolded *)
 603         let red =
 604          function
 605             C.Const _ as t -> unwind k e ens t
 606           | t -> reduce (k,e,ens,t,[])
 607         in
 608          let tl' = List.map red tl in
 609           reduce (k, e, ens, he , List.append tl' s)
 610      | (k, e, ens, C.Appl l, s) ->
 611          C.Appl (List.append (List.map (unwind k e ens) l) s)
 612   *)
 613      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) when delta=false->
 614            let t' = unwind k e ens t in
 615            if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 616      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
 617         (let o,_ =
 618            CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 619          in
 620           match o with
 621             C.Constant (_,Some body,_,_,_) ->
 622              let ens' = push_exp_named_subst k e ens exp_named_subst in
 623               (* constants are closed *)
 624               reduce (0, [], ens', body, s)
 625           | C.Constant (_,None,_,_,_) ->
 626              let t' = unwind k e ens t in
 627               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 628           | C.Variable _ -> raise ReferenceToVariable
 629           | C.CurrentProof (_,_,body,_,_,_) ->
 630              let ens' = push_exp_named_subst k e ens exp_named_subst in
 631               (* constants are closed *)
 632               reduce (0, [], ens', body, s)
 633           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
 634         )
 635      | (k, e, ens, (C.MutInd _ as t),s) ->
 636         let t' = unwind k e ens t in
 637          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 638      | (k, e, ens, (C.MutConstruct _ as t),s) ->
 639          let t' = unwind k e ens t in
 640           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 641      | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
 642         let decofix =
 643          function
 644             C.CoFix (i,fl) as t ->
 645              let (_,_,body) = List.nth fl i in
 646               let body' =
 647                let counter = ref (List.length fl) in
 648                 List.fold_right
 649                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 650                  fl
 651                  body
 652               in
 653                (* the term is the result of a reduction; *)
 654                (* so it is already unwinded.             *)
 655                reduce (0,[],[],body',[])
 656           | C.Appl (C.CoFix (i,fl) :: tl) ->
 657              let (_,_,body) = List.nth fl i in
 658               let body' =
 659                let counter = ref (List.length fl) in
 660                 List.fold_right
 661                  (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
 662                  fl
 663                  body
 664               in
 665                (* the term is the result of a reduction; *)
 666                (* so it is already unwinded.             *)
 667                reduce (0,[],[],body',RS.to_stack_list tl)
 668           | t -> t
 669         in
 670          (match decofix (reduce (k,e,ens,term,[])) with
 671              C.MutConstruct (_,_,j,_) ->
 672               reduce (k, e, ens, (List.nth pl (j-1)), s)
 673            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
 674               let (arity, r) =
 675                 let o,_ =
 676                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
 677                 in
 678                   match o with
 679                       C.InductiveDefinition (tl,ingredients,r,_) ->
 680                         let (_,_,arity,_) = List.nth tl i in
 681                           (arity,r)
 682                     | _ -> raise WrongUriToInductiveDefinition
 683               in
 684                let ts =
 685                 let num_to_eat = r in
 686                  let rec eat_first =
 687                   function
 688                      (0,l) -> l
 689                    | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
 690                    | _ -> raise (Impossible 5)
 691                  in
 692                   eat_first (num_to_eat,tl)
 693                in
 694                 (* ts are already unwinded because they are a sublist of tl *)
 695                 reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
 696            | C.Cast _ | C.Implicit _ ->
 697               raise (Impossible 2) (* we don't trust our whd ;-) *)
 698            | _ ->
 699              let t' = unwind k e ens t in
 700               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 701          )
 702      | (k, e, ens, (C.Fix (i,fl) as t), s) ->
 703         let (_,recindex,_,body) = List.nth fl i in
 704          let recparam =
 705           try
 706            Some (RS.from_stack ~unwind (List.nth s recindex))
 707           with
 708            _ -> None
 709          in
 710           (match recparam with
 711               Some recparam ->
 712                (match reduce (0,[],[],recparam,[]) with
 713                    (* match recparam with *)
 714                    C.MutConstruct _
 715                  | C.Appl ((C.MutConstruct _)::_) ->
 716                     (* OLD
 717                     let body' =
 718                      let counter = ref (List.length fl) in
 719                       List.fold_right
 720                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
 721                        fl
 722                        body
 723                     in
 724                      reduce (k, e, ens, body', s) *)
 725                     (* NEW *)
 726                     let leng = List.length fl in
 727                     let fl' =
 728                      let unwind_fl (name,recindex,typ,body) =
 729                       (name,recindex,unwind k e ens typ,
 730                         unwind' leng k e ens body)
 731                      in
 732                       List.map unwind_fl fl
 733                     in
 734                      let new_env =
 735                       let counter = ref 0 in
 736                       let rec build_env e =
 737                        if !counter = leng then e
 738                        else
 739                         (incr counter ;
 740                          build_env ((RS.to_env (C.Fix (!counter -1, fl')))::e))
 741                       in
 742                        build_env e
 743                      in
 744                       reduce (k+leng, new_env, ens, body, s)
 745                  | _ ->
 746                    let t' = unwind k e ens t in
 747                     if s = [] then t' else
 748                      C.Appl (t'::(RS.from_stack_list ~unwind s))
 749                )
 750             | None ->
 751                let t' = unwind k e ens t in
 752                 if s = [] then t' else
 753                  C.Appl (t'::(RS.from_stack_list ~unwind s))
 754           )
 755      | (k, e, ens, (C.CoFix (i,fl) as t),s) ->
 756         let t' = unwind k e ens t in
 757          if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
 758    and push_exp_named_subst k e ens =
 759     function
 760        [] -> ens
 761      | (uri,t)::tl ->
 762          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
 763    in
 764      reduce
 765   ;;
 766   (*
 767   let rec whd context t =
 768     try
 769       reduce context (0, [], [], t, [])
 770     with Not_found ->
 771       debug_print (lazy (CicPp.ppterm t)) ;
 772       raise Not_found
 773   ;;
 774   *)
 775
 776   let rec whd ?(delta=true) ?(subst=[]) context t =
 777     reduce ~delta ~subst context (0, [], [], t, [])
 778   ;;
 779
 780
 781  end
 782 ;;
 783
 784
 785 (* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
 786            senza ridurre la testa
 787 module R = Reduction CallByNameStrategy;; OK 56.368s
 788 module R = Reduction CallByValueStrategy;; ROTTO
 789 module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
 790 module R = Reduction LazyCallByValueStrategy;; ROTTO
 791 module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
 792 module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
 793 module R = Reduction
 794  LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
 795  OK 59.058s
 796 module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
 797 module R = Reduction
 798  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 799 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 800 *)
 801 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 802 module U = UriManager;;
 803
 804 let whd = R.whd
 805
 806 (*
 807 let whd =
 808  let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
 809   fun ?(delta=true) ?(subst=[]) context t ->
 810    profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
 811 *)
 812
 813   (* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
 814     * fallbacks to structural equality *)
 815 let (===) x y =
 816   Pervasives.compare x y = 0
 817
 818 (* t1, t2 must be well-typed *)
 819 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
 820  let rec aux test_equality_only context t1 t2 ugraph =
 821   let aux2 test_equality_only t1 t2 ugraph =
 822
 823    (* this trivial euristic cuts down the total time of about five times ;-) *)
 824    (* this because most of the time t1 and t2 are "sintactically" the same   *)
 825    if t1 === t2 then
 826      true,ugraph
 827    else
 828     begin
 829      let module C = Cic in
 830        match (t1,t2) with
 831           (C.Rel n1, C.Rel n2) -> (n1 = n2),ugraph
 832         | (C.Var (uri1,exp_named_subst1), C.Var (uri2,exp_named_subst2)) ->
 833             if U.eq uri1 uri2 then
 834              (try
 835                List.fold_right2
 836                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 837                   let b',ugraph' = aux test_equality_only context x y ugraph in
 838                   (U.eq uri1 uri2 && b' && b),ugraph'
 839                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 840               with
 841                Invalid_argument _ -> false,ugraph
 842              )
 843             else
 844               false,ugraph
 845         | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
 846             if n1 = n2 then
 847               let b2, ugraph1 =
 848                 let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
 849                 let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
 850                   List.fold_left2
 851                     (fun (b,ugraph) t1 t2 ->
 852                        if b then
 853                          match t1,t2 with
 854                              None,_
 855                            | _,None  -> true,ugraph
 856                            | Some t1',Some t2' ->
 857                                aux test_equality_only context t1' t2' ugraph
 858                        else
 859                          false,ugraph
 860                     ) (true,ugraph) l1 l2
 861               in
 862                 if b2 then true,ugraph1 else false,ugraph
 863             else
 864               false,ugraph
 865           (* TASSI: CONSTRAINTS *)
 866         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
 867             true,(CicUniv.add_eq t2 t1 ugraph)
 868           (* TASSI: CONSTRAINTS *)
 869         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 870             true,(CicUniv.add_ge t2 t1 ugraph)
 871           (* TASSI: CONSTRAINTS *)
 872         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
 873           (* TASSI: CONSTRAINTS *)
 874         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
 875         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 876             let b',ugraph' = aux true context s1 s2 ugraph in
 877             if b' then
 878               aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 879                 t1 t2 ugraph'
 880             else
 881               false,ugraph
 882         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
 883            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 884            if b' then
 885              aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
 886                t1 t2 ugraph'
 887            else
 888              false,ugraph
 889         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
 890            let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
 891            if b' then
 892             aux test_equality_only
 893              ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
 894            else
 895              false,ugraph
 896         | (C.Appl l1, C.Appl l2) ->
 897            (try
 898              List.fold_right2
 899                (fun  x y (b,ugraph) ->
 900                  if b then
 901                    aux test_equality_only context x y ugraph
 902                  else
 903                    false,ugraph) l1 l2 (true,ugraph)
 904             with
 905              Invalid_argument _ -> false,ugraph
 906            )
 907         | (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
 908             let b' = U.eq uri1 uri2 in
 909             if b' then
 910              (try
 911                List.fold_right2
 912                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 913                   if b && U.eq uri1 uri2 then
 914                     aux test_equality_only context x y ugraph
 915                   else
 916                     false,ugraph
 917                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 918               with
 919                Invalid_argument _ -> false,ugraph
 920              )
 921             else
 922               false,ugraph
 923         | (C.MutInd (uri1,i1,exp_named_subst1),
 924            C.MutInd (uri2,i2,exp_named_subst2)
 925           ) ->
 926             let b' = U.eq uri1 uri2 && i1 = i2 in
 927             if b' then
 928              (try
 929                List.fold_right2
 930                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 931                   if b && U.eq uri1 uri2 then
 932                     aux test_equality_only context x y ugraph
 933                   else
 934                    false,ugraph
 935                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 936               with
 937                Invalid_argument _ -> false,ugraph
 938              )
 939             else
 940               false,ugraph
 941         | (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 942            C.MutConstruct (uri2,i2,j2,exp_named_subst2)
 943           ) ->
 944             let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
 945             if b' then
 946              (try
 947                List.fold_right2
 948                 (fun (uri1,x) (uri2,y) (b,ugraph) ->
 949                   if b && U.eq uri1 uri2 then
 950                     aux test_equality_only context x y ugraph
 951                   else
 952                     false,ugraph
 953                 ) exp_named_subst1 exp_named_subst2 (true,ugraph)
 954               with
 955                Invalid_argument _ -> false,ugraph
 956              )
 957             else
 958               false,ugraph
 959         | (C.MutCase (uri1,i1,outtype1,term1,pl1),
 960            C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
 961             let b' = U.eq uri1 uri2 && i1 = i2 in
 962             if b' then
 963              let b'',ugraph''=aux test_equality_only context
 964                  outtype1 outtype2 ugraph in
 965              if b'' then
 966                let b''',ugraph'''= aux test_equality_only context
 967                    term1 term2 ugraph'' in
 968                List.fold_right2
 969                  (fun x y (b,ugraph) ->
 970                    if b then
 971                      aux test_equality_only context x y ugraph
 972                    else
 973                      false,ugraph)
 974                  pl1 pl2 (b''',ugraph''')
 975              else
 976                false,ugraph
 977             else
 978               false,ugraph
 979         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
 980             let tys =
 981               List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
 982             in
 983             if i1 = i2 then
 984              List.fold_right2
 985               (fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
 986                 if b && recindex1 = recindex2 then
 987                   let b',ugraph' = aux test_equality_only context ty1 ty2
 988                       ugraph in
 989                   if b' then
 990                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
 991                   else
 992                     false,ugraph
 993                 else
 994                   false,ugraph)
 995              fl1 fl2 (true,ugraph)
 996             else
 997               false,ugraph
 998         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
 999            let tys =
1000             List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
1001            in
1002             if i1 = i2 then
1003               List.fold_right2
1004               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
1005                 if b then
1006                   let b',ugraph' = aux test_equality_only context ty1 ty2
1007                       ugraph in
1008                   if b' then
1009                     aux test_equality_only (tys@context) bo1 bo2 ugraph'
1010                   else
1011                     false,ugraph
1012                 else
1013                   false,ugraph)
1014              fl1 fl2 (true,ugraph)
1015             else
1016               false,ugraph
1017         | (C.Cast _, _) | (_, C.Cast _)
1018         | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
1019         | (_,_) -> false,ugraph
1020     end
1021   in
1022      begin
1023      debug t1 [t2] "PREWHD";
1024      (*
1025      (match t1 with
1026          Cic.Meta _ ->
1027            debug_print (lazy (CicPp.ppterm t1));
1028            debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
1029            debug_print (lazy (CicPp.ppterm t2));
1030            debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
1031        | _ -> ()); *)
1032      let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
1033      let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
1034       debug t1' [t2'] "POSTWHD";
1035       aux2 test_equality_only t1' t2' ugraph
1036     end
1037  in
1038   aux false (*c t1 t2 ugraph *)
1039 ;;
1040
1041 (* DEBUGGING ONLY
1042 let whd ?(delta=true) ?(subst=[]) context t =
1043  let res = whd ~delta ~subst context t in
1044  let rescsc = CicReductionNaif.whd ~delta ~subst context t in
1045   if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
1046    begin
1047     debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
1048     flush stderr ;
1049     debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
1050     flush stderr ;
1051     debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
1052     flush stderr ;
1053 fdebug := 0 ;
1054 let _ =  are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
1055     assert false ;
1056    end
1057   else
1058    res
1059 ;;
1060 *)
1061
1062 let are_convertible = are_convertible whd
1063
1064 let whd = R.whd
1065
1066 (*
1067 let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
1068 let whd ?(delta=true) ?(subst=[]) context t =
1069  let foo () =
1070   whd ~delta ~subst context t
1071  in
1072   profiler_other_whd.HExtlib.profile foo ()
1073 *)
1074
1075 let rec normalize ?(delta=true) ?(subst=[]) ctx term =
1076   let module C = Cic in
1077   let t = whd ~delta ~subst ctx term in
1078   let aux = normalize ~delta ~subst in
1079   let decl name t = Some (name, C.Decl t) in
1080   let def  name t = Some (name, C.Def (t,None)) in
1081   match t with
1082   | C.Rel n -> t
1083   | C.Var (uri,exp_named_subst) ->
1084       C.Var (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1085   | C.Meta (i,l) ->
1086       C.Meta (i,List.map (function Some t -> Some (aux ctx t) | None -> None) l)
1087   | C.Sort _ -> t
1088   | C.Implicit _ -> t
1089   | C.Cast (te,ty) -> C.Cast (aux ctx te, aux ctx ty)
1090   | C.Prod (n,s,t) ->
1091       let s' = aux ctx s in
1092       C.Prod (n, s', aux ((decl n s')::ctx) t)
1093   | C.Lambda (n,s,t) ->
1094       let s' = aux ctx s in
1095       C.Lambda (n, s', aux ((decl n s')::ctx) t)
1096   | C.LetIn (n,s,t) ->
1097       (* the term is already in weak head normal form *)
1098       assert false
1099   | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
1100   | C.Appl [] -> assert false
1101   | C.Const (uri,exp_named_subst) ->
1102       C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1103   | C.MutInd (uri,typeno,exp_named_subst) ->
1104       C.MutInd (uri,typeno, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1105   | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
1106       C.MutConstruct (uri, typeno, consno,
1107         List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
1108   | C.MutCase (sp,i,outt,t,pl) ->
1109       C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
1110 (*CSC: to be completed, I suppose *)
1111   | C.Fix _ -> t
1112   | C.CoFix _ -> t
1113
1114 let normalize ?delta ?subst ctx term =
1115 (*  prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
1116   let t = normalize ?delta ?subst ctx term in
1117 (*  prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
1118   t
1119
1120
1121 (* performs an head beta/cast reduction *)
1122 let rec head_beta_reduce =
1123  function
1124     (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
1125       let he'' = CicSubstitution.subst he' t in
1126        if tl' = [] then
1127         he''
1128        else
1129         let he''' =
1130          match he'' with
1131             Cic.Appl l -> Cic.Appl (l@tl')
1132           | _ -> Cic.Appl (he''::tl')
1133         in
1134          head_beta_reduce he'''
1135   | Cic.Cast (te,_) -> head_beta_reduce te
1136   | t -> t