X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=813a589d603d7c2025d9cfb97686d10573e5064c;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=55ffb8edb99787b69b77fa2218caf8f96b0b21dd;hpb=5530db2f72548a8c579ae5f9868cbd38290eb065;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 55ffb8edb..813a589d6 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -33,7 +33,9 @@ exception ReferenceToVariable;; 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 = @@ -43,7 +45,7 @@ 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 = @@ -349,15 +351,15 @@ module Reduction(RS : 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 @@ -387,9 +389,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> | 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 @@ -403,9 +405,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> 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 @@ -419,9 +421,9 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> 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 @@ -495,11 +497,11 @@ debug_print ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -> | _::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 @@ -509,9 +511,15 @@ if List.mem uri params then debug_print "---- OK2" ; 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 @@ -546,8 +554,8 @@ if List.mem uri params then debug_print "---- OK2" ; 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 @@ -562,9 +570,9 @@ if List.mem uri params then debug_print "---- OK2" ; ) | (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 *) @@ -607,9 +615,9 @@ if List.mem uri params then debug_print "---- OK2" ; 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 *) @@ -664,13 +672,13 @@ if List.mem uri params then debug_print "---- OK2" ; 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 = @@ -685,7 +693,7 @@ if List.mem uri params then debug_print "---- OK2" ; 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 @@ -721,7 +729,7 @@ if List.mem uri params then debug_print "---- OK2" ; (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 @@ -760,7 +768,7 @@ if List.mem uri params then debug_print "---- OK2" ; try reduce context (0, [], [], t, []) with Not_found -> - debug_print (CicPp.ppterm t) ; + debug_print (lazy (CicPp.ppterm t)) ; raise Not_found ;; *) @@ -770,54 +778,45 @@ if List.mem uri params then debug_print "---- OK2" ; ;; -(* 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 = @@ -841,142 +840,142 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -985,17 +984,17 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -1003,21 +1002,20 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -1025,14 +1023,14 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -1040,6 +1038,39 @@ let are_convertible ?(subst=[]) ?(metasenv=[]) = 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 @@ -1063,9 +1094,10 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = 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) -> @@ -1075,13 +1107,30 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = 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