From e68d06002f901a6252bc0b6ad6b655c9acb72b0f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Nov 2007 09:20:34 +0000 Subject: [PATCH] added ~delta parameter to saturate_term and used it when saturating a coercion. it is always true that the user wants the type of its coercion no to be unfolded, since its arity was computed without unfolding. --- components/cic_unification/cicRefine.ml | 4 +++- components/cic_unification/coercGraph.ml | 2 +- components/cic_unification/termUtil.ml | 4 ++-- components/cic_unification/termUtil.mli | 1 + 4 files changed, 7 insertions(+), 4 deletions(-) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index e0f8fd1c7..f680b01f1 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1334,7 +1334,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ " <==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ + "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c + context)); debug_print (lazy ("FO_UNIF_SUBST: " ^ CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) let subst,metasenv,ugraph = diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml index 43e342e70..f12ea14b1 100644 --- a/components/cic_unification/coercGraph.ml +++ b/components/cic_unification/coercGraph.ml @@ -54,7 +54,7 @@ let saturate_coercion ul metasenv subst context = CicTypeChecker.type_of_aux' ~subst metasenv context c CicUniv.empty_ugraph in let _,metasenv,args,lastmeta = - TermUtil.saturate_term freshmeta metasenv context ty arity in + TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in diff --git a/components/cic_unification/termUtil.ml b/components/cic_unification/termUtil.ml index 8905830be..1886b25d7 100644 --- a/components/cic_unification/termUtil.ml +++ b/components/cic_unification/termUtil.ml @@ -31,7 +31,7 @@ (* hypothesis, a list of arguments for the new applications and the index of *) (* the last new META introduced. The nth argument in the list of arguments is *) (* just the nth new META. *) -let saturate_term newmeta metasenv context ty goal_arity = +let saturate_term ?(delta=true) newmeta metasenv context ty goal_arity = let module C = Cic in let module S = CicSubstitution in assert (goal_arity >= 0); @@ -79,7 +79,7 @@ let saturate_term newmeta metasenv context ty goal_arity = lastmeta,prod_no + 1 | t -> let head = CicReduction.normalize ~delta:false context t in - match CicReduction.whd context head with + match CicReduction.whd context head ~delta with C.Prod _ as head' -> aux newmeta head' | _ -> head,[],[],newmeta,0 in diff --git a/components/cic_unification/termUtil.mli b/components/cic_unification/termUtil.mli index 358b64616..c851bb588 100644 --- a/components/cic_unification/termUtil.mli +++ b/components/cic_unification/termUtil.mli @@ -32,5 +32,6 @@ (* the last new META introduced. The nth argument in the list of arguments is *) (* just the nth new META. *) val saturate_term: + ?delta: bool -> (* default true *) int -> Cic.metasenv -> Cic.context -> Cic.term -> int -> Cic.term * Cic.metasenv * Cic.term list * int -- 2.39.2