From c4ea5fdf898b6bbeff10e44046620e8b5bdefbb7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 May 2009 11:54:20 +0000 Subject: [PATCH] 1) order of processing of case branches reverted (to generate metas in left-to-right order) 2) metas generated by eat_prods are now re-ordered so that they occur in left-to-right order --- .../components/ng_refiner/nCicRefiner.ml | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index ed14180aa..a724ae1cb 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -301,9 +301,9 @@ let rec typeof hdb NCicUnification.unify hdb metasenv subst context resty expty in *) - let _, metasenv, subst, pl_rev = - List.fold_left - (fun (j, metasenv, subst, branches) p -> + let _, metasenv, subst, pl = + List.fold_right + (fun p (j, metasenv, subst, branches) -> let cons = let cons = Ref.mk_constructor j r in if parameters = [] then C.Const cons @@ -319,12 +319,12 @@ let rec typeof hdb NCicPp.ppterm ~metasenv ~subst ~context ty_branch )); let metasenv, subst, p, _ = typeof_aux metasenv subst context (Some ty_branch) p in - j+1, metasenv, subst, p :: branches) - (1, metasenv, subst, []) pl + j-1, metasenv, subst, p :: branches) + pl (List.length pl, metasenv, subst, []) in let resty = C.Appl (outtype::arguments@[term]) in let resty = NCicReduction.head_beta_reduce ~subst resty in - metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty + metasenv, subst, C.Match (r, outtype, term, pl),resty | C.Match _ -> assert false in pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ @@ -384,7 +384,7 @@ and force_to_sort hdb match NCicReduction.whd ~subst context ty with | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> metasenv, subst, t, ty - | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ??? + | C.Meta (_i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ??? metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *) | C.Meta (i,(_,lc)) -> let len = match lc with C.Irl len->len | C.Ctx l->List.length l in @@ -490,7 +490,15 @@ and eat_prods hdb in aux metasenv subst [] newhead newheadty (arg :: tl) in - aux metasenv subst [] he ty_he args + (* We need to reverse the order of the new created metas since they + are pushed on top of the metasenv in the wrong order *) + let highest_meta = NCicMetaSubst.maxmeta () in + let metasenv, subst, newhead, newheadty = + aux metasenv subst [] he ty_he args in + let metasenv_old,metasenv_new = + List.partition (fun (i,_) -> i <= highest_meta) metasenv + in + (List.rev metasenv_new) @ metasenv_old, subst, newhead, newheadty (*D*)in outside(); rc with exc -> outside (); raise exc ;; -- 2.39.2