X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=64911e198337ef472e010f2324dec30180fa7ab8;hb=156b87c397a8b5cf9b7381def41e070e235941ee;hp=68a1b2cbe983f0746a33e2fc9fe54b02de009ea7;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 68a1b2cbe..64911e198 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -250,7 +250,7 @@ let rec typeof hdb let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in let metasenv, subst, term, _ = typeof_aux metasenv subst context (Some ind) term in - let parameters, arguments = HExtlib.split_nth "NR 1" leftno args in + let parameters, arguments = HExtlib.split_nth leftno args in let outtype = match outtype with | C.Implicit _ as ot -> @@ -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 @@ -424,6 +424,20 @@ and sort_of_prod (NCicPp.ppterm ~subst ~metasenv ~context y) (NCicPp.ppterm ~subst ~metasenv ~context x)))) +and guess_name subst ctx ty = + let aux initial = "#" ^ String.make 1 initial in + match ty with + | C.Const (NReference.Ref (u,_)) + | C.Appl (C.Const (NReference.Ref (u,_)) :: _) -> + aux (String.sub (NUri.name_of_uri u) 0 1).[0] + | C.Prod _ -> aux 'f' + | C.Meta (n,lc) -> + (try + let _,_,t,_ = NCicUtils.lookup_subst n subst in + guess_name subst ctx (NCicSubstitution.subst_meta lc t) + with NCicUtils.Subst_not_found _ -> aux 'M') + | _ -> aux 'H' + and eat_prods hdb ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args = @@ -443,11 +457,12 @@ and eat_prods hdb let metasenv, subst, arg, ty_arg = typeof hdb ~look_for_coercion ~localise metasenv subst context arg None in + let name = guess_name subst context ty_arg in let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv - (("_",C.Decl ty_arg) :: context) `Type + ((name,C.Decl ty_arg) :: context) `Type in - let flex_prod = C.Prod ("_", ty_arg, meta) in + let flex_prod = C.Prod (name, ty_arg, meta) in (* next line grants that ty_args is a type *) let metasenv,subst, flex_prod, _ = typeof hdb ~look_for_coercion ~localise metasenv subst @@ -490,7 +505,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 ;; @@ -614,20 +637,20 @@ prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj List.fold_left (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) -> let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in - let sx_context_ty_rev,_= HExtlib.split_nth "NR 2" leftno (List.rev context) in + let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in let metasenv,subst,cl = List.fold_right (fun (k_relev,n,te) (metasenv,subst,res) -> let k_relev = - try snd (HExtlib.split_nth "NR 3" leftno 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 "NR 4" (List.length tys) (List.rev context) in + HExtlib.split_nth (List.length tys) (List.rev context) in let sx_context_te_rev,_ = - HExtlib.split_nth "NR 5" leftno chopped_context_rev in + HExtlib.split_nth leftno chopped_context_rev in let metasenv,subst,_ = try List.fold_left2