From 53be448c4f8ca0b60be92e24f355662a0ea7567f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 Oct 2008 20:17:39 +0000 Subject: [PATCH] many bugs fixed --- helm/software/components/ng_refiner/check.ml | 9 +- .../components/ng_refiner/nCicMetaSubst.ml | 153 +----------------- .../components/ng_refiner/nCicRefiner.ml | 28 ++-- .../components/ng_refiner/nCicUnification.ml | 57 +++++-- 4 files changed, 75 insertions(+), 172 deletions(-) diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index bb423690b..7d13b9a35 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -282,7 +282,7 @@ let _ = metasenv, subst | Sys.Break -> metasenv, subst in - if (NCicReduction.are_convertible ~subst [] infty ty) + if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty) then prerr_endline ("OK: " ^ NUri.string_of_uri u) else @@ -308,11 +308,16 @@ let _ = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo in*) with + | Sys.Break -> () | NCicRefiner.RefineFailure msg | NCicRefiner.Uncertain msg -> let _, msg = Lazy.force msg in prerr_endline msg; - prerr_endline ("FAIL: " ^ NUri.string_of_uri u)) + prerr_endline ("FAIL: " ^ NUri.string_of_uri u) + | e -> + prerr_endline (Printexc.to_string e); + prerr_endline ("FAIL: " ^ NUri.string_of_uri u) + ) | _ -> ()) alluris; ;; diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 12fe97708..6abe62e80 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -204,6 +204,7 @@ let rec force_does_not_occur metasenv subst restrictions t = * instantiated/restricted metavariabels *) let (metasenv,subst as ms), restrictions_for_n, l' = let l = NCicUtils.expand_local_context lc in + let ms, _, restrictions_for_n, l = List.fold_right (fun t (ms, i, restrictions_for_n, l) -> @@ -214,6 +215,7 @@ let rec force_does_not_occur metasenv subst restrictions t = ms, i-1, i::restrictions_for_n, l) l (ms, List.length l, [], []) in + ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l) in if restrictions_for_n = [] then @@ -374,8 +376,8 @@ let delift metasenv subst context n l t = let low_gap = max 0 (shift - shift1) in let high_gap = max 0 (stop1 - stop) in let restrictions = - HExtlib.list_seq (k+1-shift1) (low_gap + 1) @ - HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) + HExtlib.list_seq (*max 1 (k+1-shift1)*) (k+1) (low_gap + 1) @ + HExtlib.list_seq (len1 - high_gap + 1) (len1 + 1) in let metasenv, subst, newmeta = restrict metasenv subst i restrictions @@ -402,9 +404,9 @@ let delift metasenv subst context n l t = assert (List.length cctx = newlc_len); (metasenv, subst), meta - | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig + | NCic.Irl _, NCic.Irl _ when shift = k -> ms, orig | NCic.Irl _, NCic.Irl _ -> - ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1)) + ms, NCic.Meta (i, (max 0 (shift1 - shift + k), lc1)) | _ -> let lc1 = NCicUtils.expand_local_context lc1 in let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in @@ -456,7 +458,8 @@ let delift metasenv subst context n l t = let l = List.map (NCicSubstitution.lift shift) lc in if List.exists - (fun t -> NCicUntrusted.metas_of_term subst context t = []) + (fun t -> + NCicUntrusted.metas_of_term subst context t = []) l then raise (Uncertain msg) @@ -464,146 +467,6 @@ let delift metasenv subst context n l t = raise (MetaSubstFailure msg) ;; -(* -(* delifts a term t of n levels strating from k, that is changes (Rel m) - * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails - *) -let delift_rels_from subst metasenv k n = - let rec liftaux subst metasenv k = - let module C = Cic in - function - C.Rel m as t -> - if m < k then - t, subst, metasenv - else if m < k + n then - raise DeliftingARelWouldCaptureAFreeVariable - else - C.Rel (m - n), subst, metasenv - | C.Var (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Var (uri,exp_named_subst'),subst,metasenv - | C.Meta (i,l) -> - (try - let (_, t,_) = lookup_subst i subst in - liftaux subst metasenv k (CicSubstitution.subst_meta l t) - with CicUtil.Subst_not_found _ -> - let l',to_be_restricted,subst,metasenv = - let rec aux con l subst metasenv = - match l with - [] -> [],[],subst,metasenv - | he::tl -> - let tl',to_be_restricted,subst,metasenv = - aux (con + 1) tl subst metasenv in - let he',more_to_be_restricted,subst,metasenv = - match he with - None -> None,[],subst,metasenv - | Some t -> - try - let t',subst,metasenv = liftaux subst metasenv k t in - Some t',[],subst,metasenv - with - DeliftingARelWouldCaptureAFreeVariable -> - None,[i,con],subst,metasenv - in - he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv - in - aux 1 l subst metasenv in - let metasenv,subst = restrict subst to_be_restricted metasenv in - C.Meta(i,l'),subst,metasenv) - | C.Sort _ as t -> t,subst,metasenv - | C.Implicit _ as t -> t,subst,metasenv - | C.Cast (te,ty) -> - let te',subst,metasenv = liftaux subst metasenv k te in - let ty',subst,metasenv = liftaux subst metasenv k ty in - C.Cast (te',ty'),subst,metasenv - | C.Prod (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Prod (n,s',t'),subst,metasenv - | C.Lambda (n,s,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.Lambda (n,s',t'),subst,metasenv - | C.LetIn (n,s,ty,t) -> - let s',subst,metasenv = liftaux subst metasenv k s in - let ty',subst,metasenv = liftaux subst metasenv k ty in - let t',subst,metasenv = liftaux subst metasenv (k+1) t in - C.LetIn (n,s',ty',t'),subst,metasenv - | C.Appl l -> - let l',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) l ([],subst,metasenv) in - C.Appl l',subst,metasenv - | C.Const (uri,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.Const (uri,exp_named_subst'),subst,metasenv - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst',subst,metasenv = - List.fold_right - (fun (uri,t) (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv) - in - C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv - | C.MutCase (sp,i,outty,t,pl) -> - let outty',subst,metasenv = liftaux subst metasenv k outty in - let t',subst,metasenv = liftaux subst metasenv k t in - let pl',subst,metasenv = - List.fold_right - (fun t (l,subst,metasenv) -> - let t',subst,metasenv = liftaux subst metasenv k t in - t'::l,subst,metasenv) pl ([],subst,metasenv) - in - C.MutCase (sp,i,outty',t',pl'),subst,metasenv - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, i, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,i,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.Fix (i, liftedfl),subst,metasenv - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl,subst,metasenv = - List.fold_right - (fun (name, ty, bo) (l,subst,metasenv) -> - let ty',subst,metasenv = liftaux subst metasenv k ty in - let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in - (name,ty',bo')::l,subst,metasenv - ) fl ([],subst,metasenv) - in - C.CoFix (i, liftedfl),subst,metasenv - in - liftaux subst metasenv k - -let delift_rels subst metasenv n t = - delift_rels_from subst metasenv 1 n t -*) - let mk_meta ?name metasenv context ty = match ty with | `Typeless -> diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index eb7b136c2..2dce2a4a7 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -48,16 +48,18 @@ let exp_implicit metasenv context expty = let force_to_sort metasenv subst context t = match NCicReduction.whd ~subst context t with - | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t -> + | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as t -> metasenv, subst, t - | C.Meta (i,(_,lc)) as t -> + | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> + metasenv, subst, 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, _ = + let metasenv, subst, newmeta = if len > 0 then NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) - else metasenv, subst, 0 + else metasenv, subst, i in - metasenv, subst, t + metasenv, subst, C.Meta (newmeta,(0,C.Irl 0)) | C.Sort _ -> metasenv, subst, t | _ -> assert false ;; @@ -73,9 +75,9 @@ let sort_of_prod | C.Sort (C.Type u1), C.Sort (C.Type u2) -> metasenv, subst, C.Sort (C.Type (u1@u2)) | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, t2 - | C.Meta _, C.Sort _ - | C.Meta _, C.Meta _ - | C.Sort _, C.Meta _ -> metasenv, subst, t2 + | C.Meta _, C.Sort _ + | C.Meta _, C.Meta (_,(_,_)) + | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, t2 | x, (C.Sort _ | C.Meta _) | _, x -> let y, context, orig = if x == t1 then s, context, orig_s @@ -96,10 +98,9 @@ let check_allowed_sort_elimination localise r orig = let rec aux metasenv subst context ind arity1 arity2 = (*D*)inside 'S'; try let rc = let arity1 = NCicReduction.whd ~subst context arity1 in - pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " ... " ^ - NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nNEV:"^ -NCicPp.ppmetasenv ~subst metasenv -)); + pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " elimsto " ^ + NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^ + NCicPp.ppmetasenv ~subst metasenv)); match arity1 with | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) -> let metasenv, meta, _ = @@ -166,6 +167,7 @@ let rec typeof fun t as orig -> (*D*)inside 'R'; try let rc = pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t)); + pp (lazy (NCicPp.ppmetasenv ~subst metasenv)); let metasenv, subst, t, infty = match t with | C.Rel n -> @@ -307,6 +309,8 @@ let rec typeof NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term])) | C.Match _ -> assert false in + pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ + NCicPp.ppterm ~metasenv ~subst ~context infty )); force_ty metasenv subst context orig t infty expty (*D*)in outside(); rc with exc -> outside (); raise exc in diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 202e68e4c..d5cf38922 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -85,7 +85,8 @@ let fix_sorts swap metasenv subst context meta t = | NCic.Sort (NCic.Type u) as orig -> if swap then match NCicEnvironment.sup u with - | None -> raise (fail_exc metasenv subst context meta t) + | None -> prerr_endline "no sup for" ; + raise (fail_exc metasenv subst context meta t) | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1) else NCic.Sort (NCic.Type ( @@ -161,6 +162,8 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = and instantiate test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = + pp (lazy(string_of_int n ^ " :=?= "^ + NCicPp.ppterm ~metasenv ~subst ~context t)); let unify test_eq_only m s c t1 t2 = if swap then unify test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 @@ -169,23 +172,38 @@ and instantiate test_eq_only metasenv subst context n lc t swap = let metasenv, subst, t = match ty with | NCic.Implicit (`Typeof _) -> - metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t + metasenv,subst, t + (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *) | _ -> - pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + pp (lazy ( + "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^ + NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ + NCicPp.ppmetasenv ~subst metasenv)); let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure _ -> + with + | NCicTypeChecker.AssertFailure msg -> + (pp (lazy "fine typeof (fallimento)"); let ft = fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in - if ft == t then assert false + if ft == t then + (prerr_endline ( ("ILLTYPED: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t + ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^ + NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv + )); + assert false) else try pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context ft)); ft, NCicTypeChecker.typeof ~subst ~metasenv context ft - with NCicTypeChecker.TypeCheckerFailure _ -> - assert false + with NCicTypeChecker.AssertFailure _ -> + assert false) + | NCicTypeChecker.TypeCheckerFailure msg -> + pp msg; assert false in let lty = NCicSubstitution.subst_meta lc ty in pp (lazy("On the types: " ^ @@ -195,11 +213,22 @@ and instantiate test_eq_only metasenv subst context n lc t swap = let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in metasenv, subst, t in + pp (lazy(string_of_int n ^ " := 111 = "^ + NCicPp.ppterm ~metasenv ~subst ~context t)); let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t - with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) - | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) + with NCicMetaSubst.Uncertain msg -> + pp (lazy ("delift fails: " ^ Lazy.force msg)); + raise (Uncertain msg) + | NCicMetaSubst.MetaSubstFailure msg -> + pp (lazy ("delift fails: " ^ Lazy.force msg)); + raise (UnificationFailure msg) in + pp (lazy(string_of_int n ^ " := 222 = "^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx t + ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv + + )); (* Unifying the types may have already instantiated n. *) try let _, _,oldt,_ = NCicUtils.lookup_subst n subst in @@ -266,10 +295,12 @@ and unify test_eq_only metasenv subst context t1 t2 = metasenv, subst, i::to_restrict, i-1) l1 l2 (metasenv, subst, [], List.length l1) in - let metasenv, subst, _ = - NCicMetaSubst.restrict metasenv subst n1 to_restrict - in - metasenv, subst + if to_restrict <> [] then + let metasenv, subst, _ = + NCicMetaSubst.restrict metasenv subst n1 to_restrict + in + metasenv, subst + else metasenv, subst with | Invalid_argument _ -> assert false | NCicMetaSubst.MetaSubstFailure msg -> -- 2.39.2