exception ReferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;
-let debug_print = fun _ -> ()
+let debug = false
+let profile = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
let fdebug = ref 1;;
let debug t env s =
CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
- debug_print (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
+ debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
;;
module type Strategy =
)
| C.Var (uri,exp_named_subst) ->
(*
-debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens)) ;
+debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> UriManager.string_of_uri uri ^ " := " ^ CicPp.ppterm t) ens))) ;
*)
if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then
CicSubstitution.lift m (RS.from_ens (List.assq uri ens))
else
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable (_,_,_,params,_) -> params
| C.Appl l -> C.Appl (List.map (unwind_aux m) l)
| C.Const (uri,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant (_,_,_,params,_) -> params
| C.Variable _ -> raise ReferenceToVariable
C.Const (uri,exp_named_subst')
| C.MutInd (uri,i,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
C.MutInd (uri,i,exp_named_subst')
| C.MutConstruct (uri,i,j,exp_named_subst) ->
let params =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
(match o with
C.Constant _ -> raise ReferenceToConstant
| C.Variable _ -> raise ReferenceToVariable
| _::tl -> filter_and_lift already_instantiated tl
(*
| (uri,_)::tl ->
-debug_print ("---- SKIPPO " ^ UriManager.string_of_uri uri) ;
+debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ;
if List.for_all (function (uri',_) -> not (UriManager.eq uri uri'))
-exp_named_subst' then debug_print "---- OK1" ;
-debug_print ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params)) ;
-if List.mem uri params then debug_print "---- OK2" ;
+exp_named_subst' then debug_print (lazy "---- OK1") ;
+debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ;
+if List.mem uri params then debug_print (lazy "---- OK2") ;
filter_and_lift tl
*)
in
unwind_aux m t
;;
+ let unwind = unwind' 0;;
+
+(*
let unwind =
- unwind' 0
+ let profiler_unwind = HExtlib.profile ~enable:profile "are_convertible.unwind" in
+ fun k e ens t ->
+ profiler_unwind.HExtlib.profile (unwind k e ens) t
;;
+*)
let reduce ~delta ?(subst = []) context : config -> Cic.term =
let module C = Cic in
reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
else
( let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
)
| (k, e, ens, (C.Meta (n,l) as t), s) ->
(try
- let (_, term,_) = CicUtil.lookup_subst n subst in
+ let (_, term,_) = CicUtil.lookup_subst n subst in
reduce (k, e, ens,CicSubstitution.subst_meta l term,s)
- with CicUtil.Subst_not_found _ ->
+ with CicUtil.Subst_not_found _ ->
let t' = unwind k e ens t in
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
| (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
| (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
(let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
- in
- match o with
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ in
+ match o with
C.Constant (_,Some body,_,_,_) ->
let ens' = push_exp_named_subst k e ens exp_named_subst in
(* constants are closed *)
reduce (k, e, ens, (List.nth pl (j-1)), s)
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
- in
- match o with
+ let o,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind
+ in
+ match o with
C.InductiveDefinition (tl,ingredients,r,_) ->
- let (_,_,arity,_) = List.nth tl i in
- (arity,r)
+ let (_,_,arity,_) = List.nth tl i in
+ (arity,r)
| _ -> raise WrongUriToInductiveDefinition
in
let ts =
in
(* ts are already unwinded because they are a sublist of tl *)
reduce (k, e, ens, (List.nth pl (j-1)), (RS.to_stack_list ts)@s)
- | C.Cast _ | C.Implicit _ ->
+ | C.Cast _ | C.Implicit _ ->
raise (Impossible 2) (* we don't trust our whd ;-) *)
| _ ->
let t' = unwind k e ens t in
(name,recindex,unwind k e ens typ,
unwind' leng k e ens body)
in
- List.map unwind_fl fl
+ List.map unwind_fl fl
in
let new_env =
let counter = ref 0 in
try
reduce context (0, [], [], t, [])
with Not_found ->
- debug_print (CicPp.ppterm t) ;
+ debug_print (lazy (CicPp.ppterm t)) ;
raise Not_found
;;
*)
;;
-(* DEBUGGING ONLY
-let whd context t =
- let res = whd context t in
- let rescsc = CicReductionNaif.whd context t in
- if not (CicReductionNaif.are_convertible context res rescsc) then
- begin
- debug_print ("PRIMA: " ^ CicPp.ppterm t) ;
- flush stderr ;
- debug_print ("DOPO: " ^ CicPp.ppterm res) ;
- flush stderr ;
- debug_print ("CSC: " ^ CicPp.ppterm rescsc) ;
- flush stderr ;
-CicReductionNaif.fdebug := 0 ;
-let _ = CicReductionNaif.are_convertible context res rescsc in
- assert false ;
- end
- else
- res
-;;
-*)
end
;;
-(*
-module R = Reduction CallByNameStrategy;;
-module R = Reduction CallByValueStrategy;;
-module R = Reduction CallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByValueStrategy;;
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;;
-module R = Reduction LazyCallByNameStrategy;;
+(* ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
+ senza ridurre la testa
+module R = Reduction CallByNameStrategy;; OK 56.368s
+module R = Reduction CallByValueStrategy;; ROTTO
+module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByValueStrategy;; ROTTO
+module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
+module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
module R = Reduction
LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;;
+ OK 59.058s
+module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;;
+ ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
+module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
*)
module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
module U = UriManager;;
-let whd = R.whd;;
+let whd = R.whd
+
+(*
+let whd =
+ let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
+ fun ?(delta=true) ?(subst=[]) context t ->
+ profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
+*)
(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
* fallbacks to structural equality *)
-let (===) x y = (Pervasives.compare x y = 0)
+let (===) x y =
+ Pervasives.compare x y = 0
(* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) ?(metasenv=[]) =
+let are_convertible whd ?(subst=[]) ?(metasenv=[]) =
let rec aux test_equality_only context t1 t2 ugraph =
let aux2 test_equality_only t1 t2 ugraph =
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.Meta (n1,l1), C.Meta (n2,l2)) ->
- if n1 = n2 then
- let b2, ugraph1 =
- let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
- let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
- List.fold_left2
- (fun (b,ugraph) t1 t2 ->
- if b then
- match t1,t2 with
- None,_
- | _,None -> true,ugraph
- | Some t1',Some t2' ->
- aux test_equality_only context t1' t2' ugraph
- else
- false,ugraph
- ) (true,ugraph) l1 l2
- in
- if b2 then true,ugraph1 else false,ugraph
- else
- false,ugraph
+ if n1 = n2 then
+ let b2, ugraph1 =
+ let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+ let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
+ List.fold_left2
+ (fun (b,ugraph) t1 t2 ->
+ if b then
+ match t1,t2 with
+ None,_
+ | _,None -> true,ugraph
+ | Some t1',Some t2' ->
+ aux test_equality_only context t1' t2' ugraph
+ else
+ false,ugraph
+ ) (true,ugraph) l1 l2
+ in
+ if b2 then true,ugraph1 else false,ugraph
+ else
+ false,ugraph
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+ true,(CicUniv.add_eq t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ true,(CicUniv.add_ge t2 t1 ugraph)
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
(* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
- true,(CicUniv.add_eq t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- true,(CicUniv.add_ge t2 t1 ugraph)
- (* TASSI: CONSTRAINTS *)
- | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
- (* TASSI: CONSTRAINTS *)
| (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let b',ugraph' = aux true context s1 s2 ugraph in
- if b' then
+ let b',ugraph' = aux true context s1 s2 ugraph in
+ if b' then
aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
+ t1 t2 ugraph'
+ else
+ false,ugraph
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
if b' then
- aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
- t1 t2 ugraph'
- else
- false,ugraph
+ aux test_equality_only ((Some (name1, (C.Decl s1)))::context)
+ t1 t2 ugraph'
+ else
+ false,ugraph
| (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
let b',ugraph' = aux test_equality_only context s1 s2 ugraph in
- if b' then
+ if b' then
aux test_equality_only
((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph'
- else
- false,ugraph
+ else
+ false,ugraph
| (C.Appl l1, C.Appl l2) ->
(try
List.fold_right2
(fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph) l1 l2 (true,ugraph)
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph) l1 l2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
| (C.Const (uri1,exp_named_subst1), C.Const (uri2,exp_named_subst2)) ->
let b' = U.eq uri1 uri2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutInd (uri1,i1,exp_named_subst1),
C.MutInd (uri2,i2,exp_named_subst2)
) ->
let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutConstruct (uri1,i1,j1,exp_named_subst1),
C.MutConstruct (uri2,i2,j2,exp_named_subst2)
) ->
let b' = U.eq uri1 uri2 && i1 = i2 && j1 = j2 in
- if b' then
+ if b' then
(try
List.fold_right2
(fun (uri1,x) (uri2,y) (b,ugraph) ->
- if b && U.eq uri1 uri2 then
- aux test_equality_only context x y ugraph
- else
- false,ugraph
+ if b && U.eq uri1 uri2 then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph
) exp_named_subst1 exp_named_subst2 (true,ugraph)
with
Invalid_argument _ -> false,ugraph
)
- else
- false,ugraph
+ else
+ false,ugraph
| (C.MutCase (uri1,i1,outtype1,term1,pl1),
C.MutCase (uri2,i2,outtype2,term2,pl2)) ->
let b' = U.eq uri1 uri2 && i1 = i2 in
- if b' then
+ if b' then
let b'',ugraph''=aux test_equality_only context
- outtype1 outtype2 ugraph in
- if b'' then
- let b''',ugraph'''= aux test_equality_only context
- term1 term2 ugraph'' in
- List.fold_right2
- (fun x y (b,ugraph) ->
- if b then
- aux test_equality_only context x y ugraph
- else
- false,ugraph)
- pl1 pl2 (true,ugraph''')
- else
- false,ugraph
- else
- false,ugraph
+ outtype1 outtype2 ugraph in
+ if b'' then
+ let b''',ugraph'''= aux test_equality_only context
+ term1 term2 ugraph'' in
+ List.fold_right2
+ (fun x y (b,ugraph) ->
+ if b then
+ aux test_equality_only context x y ugraph
+ else
+ false,ugraph)
+ pl1 pl2 (b''',ugraph''')
+ else
+ false,ugraph
+ else
+ false,ugraph
| (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
let tys =
List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
List.fold_right2
(fun (_,recindex1,ty1,bo1) (_,recindex2,ty2,bo2) (b,ugraph) ->
if b && recindex1 = recindex2 then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
| (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
let tys =
List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
if i1 = i2 then
List.fold_right2
(fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
- if b then
- let b',ugraph' = aux test_equality_only context ty1 ty2
- ugraph in
- if b' then
- aux test_equality_only (tys@context) bo1 bo2 ugraph'
- else
- false,ugraph
- else
- false,ugraph)
- fl1 fl2 (true,ugraph)
- else
- false,ugraph
+ if b then
+ let b',ugraph' = aux test_equality_only context ty1 ty2
+ ugraph in
+ if b' then
+ aux test_equality_only (tys@context) bo1 bo2 ugraph'
+ else
+ false,ugraph
+ else
+ false,ugraph)
+ fl1 fl2 (true,ugraph)
+ else
+ false,ugraph
| (C.Cast _, _) | (_, C.Cast _)
- | (C.Implicit _, _) | (_, C.Implicit _) ->
- assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (_,_) -> false,ugraph
end
in
debug t1 [t2] "PREWHD";
(*
(match t1 with
- Cic.Meta _ ->
- debug_print (CicPp.ppterm t1);
- debug_print (CicPp.ppterm (whd ~subst context t1));
- debug_print (CicPp.ppterm t2);
- debug_print (CicPp.ppterm (whd ~subst context t2))
+ Cic.Meta _ ->
+ debug_print (lazy (CicPp.ppterm t1));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t1)));
+ debug_print (lazy (CicPp.ppterm t2));
+ debug_print (lazy (CicPp.ppterm (whd ~subst context t2)))
| _ -> ()); *)
- let t1' = whd ~subst context t1 in
- let t2' = whd ~subst context t2 in
+ let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+ let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
debug t1' [t2'] "POSTWHD";
aux2 test_equality_only t1' t2' ugraph
end
aux false (*c t1 t2 ugraph *)
;;
+(* DEBUGGING ONLY
+let whd ?(delta=true) ?(subst=[]) context t =
+ let res = whd ~delta ~subst context t in
+ let rescsc = CicReductionNaif.whd ~delta ~subst context t in
+ if not (fst (are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph)) then
+ begin
+ debug_print (lazy ("PRIMA: " ^ CicPp.ppterm t)) ;
+ flush stderr ;
+ debug_print (lazy ("DOPO: " ^ CicPp.ppterm res)) ;
+ flush stderr ;
+ debug_print (lazy ("CSC: " ^ CicPp.ppterm rescsc)) ;
+ flush stderr ;
+fdebug := 0 ;
+let _ = are_convertible CicReductionNaif.whd ~subst context res rescsc CicUniv.empty_ugraph in
+ assert false ;
+ end
+ else
+ res
+;;
+*)
+
+let are_convertible = are_convertible whd
+
+let whd = R.whd
+
+(*
+let profiler_other_whd = HExtlib.profile ~enable:profile "~are_convertible.whd"
+let whd ?(delta=true) ?(subst=[]) context t =
+ let foo () =
+ whd ~delta ~subst context t
+ in
+ profiler_other_whd.HExtlib.profile foo ()
+*)
let rec normalize ?(delta=true) ?(subst=[]) ctx term =
let module C = Cic in
let s' = aux ctx s in
C.Lambda (n, s', aux ((decl n s')::ctx) t)
| C.LetIn (n,s,t) ->
- let s' = aux ctx s in
- C.LetIn (n, s, aux ((def n s')::ctx) t)
+ (* the term is already in weak head normal form *)
+ assert false
| C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l))
+ | C.Appl [] -> assert false
| C.Const (uri,exp_named_subst) ->
C.Const (uri, List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
| C.MutInd (uri,typeno,exp_named_subst) ->
List.map (fun (n,t) -> n,aux ctx t) exp_named_subst)
| C.MutCase (sp,i,outt,t,pl) ->
C.MutCase (sp,i, aux ctx outt, aux ctx t, List.map (aux ctx) pl)
+(*CSC: to be completed, I suppose *)
| C.Fix _ -> t
| C.CoFix _ -> t
let normalize ?delta ?subst ctx term =
- prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term);
+(* prerr_endline ("NORMALIZE:" ^ CicPp.ppterm term); *)
let t = normalize ?delta ?subst ctx term in
- prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t);
+(* prerr_endline ("NORMALIZED:" ^ CicPp.ppterm t); *)
t
+(* performs an head beta/cast reduction *)
+let rec head_beta_reduce =
+ function
+ (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+ let he'' = CicSubstitution.subst he' t in
+ if tl' = [] then
+ he''
+ else
+ let he''' =
+ match he'' with
+ Cic.Appl l -> Cic.Appl (l@tl')
+ | _ -> Cic.Appl (he''::tl')
+ in
+ head_beta_reduce he'''
+ | Cic.Cast (te,_) -> head_beta_reduce te
+ | t -> t
projects / helm.git / blobdiff