X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=a724ae1cb6770c09559fa5a26bdfae55637d441c;hb=f68f477d76866de24ebdb5351912754a7dccbda5;hp=e38842ac82c57c6c454582438a5726f6f89ba86a;hpb=1bd6b7d2637d765f11ddbd1218d63474e9d0c63b;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index e38842ac8..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,8 +384,8 @@ 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 []))) -> - metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) + | 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 let metasenv, subst, newmeta = @@ -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 ;; @@ -524,12 +532,12 @@ let relocalise old_localise dt t add = let undebruijnate inductive ref t rev_fl = NCicSubstitution.psubst (fun x -> x) - (HExtlib.list_mapi + (List.rev (HExtlib.list_mapi (fun (_,_,rno,_,_,_) i -> NCic.Const (if inductive then NReference.mk_fix i rno ref else NReference.mk_cofix i ref)) - rev_fl) + rev_fl)) t ;; @@ -538,6 +546,7 @@ let typeof_obj hdb ?(localise=fun _ -> Stdpp.dummy_loc) ~look_for_coercion (uri,height,metasenv,subst,obj) = +prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj)); let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *) let metasenv, subst, ty, sort = typeof hdb ~localise ~look_for_coercion metasenv subst context ty None @@ -617,8 +626,11 @@ let typeof_obj hdb let metasenv,subst,cl = List.fold_right (fun (k_relev,n,te) (metasenv,subst,res) -> - let _,k_relev = HExtlib.split_nth leftno k_relev in + let k_relev = + try snd (HExtlib.split_nth leftno k_relev) + with Failure _ -> k_relev in let te = NCicTypeChecker.debruijn uri len [] te in + let metasenv, subst, te, _ = check_type metasenv subst tys te in let context,te = NCicReduction.split_prods ~subst tys leftno te in let _,chopped_context_rev = HExtlib.split_nth (List.length tys) (List.rev context) in @@ -664,11 +676,8 @@ let typeof_obj hdb else metasenv,subst,item1::context ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev - with Invalid_argument "List.fold_left2" -> assert false - in - let metasenv, subst, te, con_sort = - check_type metasenv subst context te - in + with Invalid_argument "List.fold_left2" -> assert false in + let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in (match NCicReduction.whd ~subst context con_sort, NCicReduction.whd ~subst [] ty_sort @@ -700,14 +709,26 @@ let typeof_obj hdb (lazy (localise te, "Non positive occurence in " ^ NUri.string_of_uri uri))) else + let relsno = List.length itl + leftno in let te = NCicSubstitution.psubst - (fun i -> NCic.Const (NReference.reference_of_spec uri - (NReference.Ind (ind,i,leftno)))) - (List.rev (HExtlib.list_seq 0 (List.length itl))) - te - in - metasenv,subst,(k_relev,n,te)::res + (fun i -> + if i <= leftno then + NCic.Rel i + else + NCic.Const (NReference.reference_of_spec uri + (NReference.Ind (ind,relsno - i,leftno)))) + (HExtlib.list_seq 1 (relsno+1)) + te in + let te = + List.fold_right + (fun (name,decl) te -> + match decl with + NCic.Decl ty -> NCic.Prod (name,ty,te) + | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te) + ) sx_context_te_rev te + in + metasenv,subst,(k_relev,n,te)::res ) cl (metasenv,subst,[]) in metasenv,subst,(it_relev,n,ty,cl)::res,i+1