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