From 8e4ffe5706cf010943d78cddea1c83d0bbb86ba3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 24 Aug 2007 10:46:20 +0000 Subject: Utilisation plus précise de la contrainte de type pour interpréter les points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/command.ml | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 05166b21f..b9716d4f5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -563,13 +563,18 @@ type fixpoint_expr = { fix_type : constr_expr } -let interp_fix_type isevars env fix = - interp_type_evars isevars env - (generalize_constr_expr fix.fix_type fix.fix_binders) +let interp_fix_context isevars env fix = + interp_context_evars isevars env fix.fix_binders -let interp_fix_body isevars env impls fix fixtype = - interp_casted_constr_evars isevars env ~impls - (abstract_constr_expr fix.fix_body fix.fix_binders) fixtype +let interp_fix_ccl isevars (env,_) fix = + interp_type_evars isevars env fix.fix_type + +let interp_fix_body isevars env_rec impls (_,ctx) fix ccl = + let env = push_rel_context ctx env_rec in + let body = interp_casted_constr_evars isevars env ~impls fix.fix_body ccl in + it_mkLambda_or_LetIn body ctx + +let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx let declare_fix boxed kind f def t = let ce = { @@ -607,7 +612,9 @@ let interp_recursive fixkind l boxed = (* Interp arities allowing for unresolved types *) let isevars = ref (Evd.create_evar_defs Evd.empty) in - let fixtypes = List.map (interp_fix_type isevars env) fixl in + let fixctxs = List.map (interp_fix_context isevars env) fixl in + let fixccls = List.map2 (interp_fix_ccl isevars) fixctxs fixl in + let fixtypes = List.map2 build_fix_type fixctxs fixccls in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) @@ -618,7 +625,7 @@ let interp_recursive fixkind l boxed = let fixdefs = States.with_heavy_rollback (fun () -> List.iter (declare_interning_data impls) notations; - List.map2 (interp_fix_body isevars env_rec impls) fixl fixtypes) + list_map3 (interp_fix_body isevars env_rec impls) fixctxs fixl fixccls) () in (* Instantiate evars and check all are resolved *) -- cgit v1.2.3