From e1ffde2ba67b8a2f7d4d97898ba28afd65d96ea7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 21 Oct 2008 11:33:33 +0000 Subject: [PATCH] - mk_restricted_irl removed, the non-optimized code was the same - delift fixed in case Meta (used to produce negative shift/irl-len) - fix-sorts takes into account the swap parameter to implement cumulativity --- .../components/ng_refiner/nCicMetaSubst.ml | 103 +++++++++--------- .../components/ng_refiner/nCicRefiner.ml | 11 +- .../components/ng_refiner/nCicUnification.ml | 40 ++++--- 3 files changed, 82 insertions(+), 72 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index aa49a84ee..12fe97708 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -179,15 +179,6 @@ let pack_lc orig = ;; -let mk_restricted_irl shift len restrictions = - let rec aux n = - if n = 0 then 0 else - if List.mem (n+shift) restrictions then aux (n-1) - else 1+aux (n-1) - in - pack_lc (shift, NCic.Irl (aux len)) -;; - let mk_perforated_irl shift len restrictions = let rec aux n = @@ -208,28 +199,22 @@ let rec force_does_not_occur metasenv subst restrictions t = List.length (List.filter (fun x -> x < r - k) restrictions) in if amount > 0 then ms, NCic.Rel (r - amount) else ms, orig - | NCic.Meta (n, l) as orig -> + | NCic.Meta (n, (shift,lc as l)) as orig -> (* we ignore the subst since restrict will take care of already * instantiated/restricted metavariabels *) let (metasenv,subst as ms), restrictions_for_n, l' = - match l with - | shift, NCic.Irl len -> - let restrictions = - List.filter - (fun i -> i > shift && i <= shift + len) restrictions in - ms, restrictions, mk_restricted_irl shift len restrictions - | shift, NCic.Ctx l -> - let ms, _, restrictions_for_n, l = - List.fold_right - (fun t (ms, i, restrictions_for_n, l) -> - try - let ms, t = aux (k-shift) ms t in - ms, i-1, restrictions_for_n, t::l - with Occur -> - ms, i-1, i::restrictions_for_n, l) - l (ms, List.length l, [], []) - in - ms, restrictions_for_n, pack_lc (shift, NCic.Ctx 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) -> + try + let ms, t = aux (k-shift) ms t in + ms, i-1, restrictions_for_n, t::l + with Occur -> + 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 ms, if l = l' then orig else NCic.Meta (n, l') @@ -287,13 +272,23 @@ and restrict metasenv subst i restrictions = let (metasenv, subst), newbo = force_does_not_occur metasenv subst restrictions bo in let j = newmeta () in - let subst_entry_j = j, (name, newctx, newty, newbo) in + let subst_entry_j = j, (name, newctx, newbo, newty) in let reloc_irl = mk_perforated_irl 0 (List.length ctx) restrictions in let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in - metasenv, - subst_entry_j :: List.map - (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst, - j + let new_subst = + subst_entry_j :: List.map + (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst + in +(* + prerr_endline ("restringo nella subst: " ^string_of_int i ^ " -> " ^ + string_of_int j ^ "\n" ^ + NCicPp.ppsubst ~metasenv [subst_entry_j] ^ "\n\n" ^ + NCicPp.ppsubst ~metasenv [subst_entry_i] ^ "\n" ^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx bo ^ " ---- " ^ + NCicPp.ppterm ~metasenv ~subst ~context:newctx newbo + ); +*) + metasenv, new_subst, j with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf ("Cannot restrict the context of the metavariable ?%d over "^^ "the hypotheses %s since ?%d is already instantiated "^^ @@ -362,11 +357,9 @@ let delift metasenv subst context n l t = let shift1,lc1 = l1 in let shift,lc = l in let shift = shift + k in - let _ = prerr_endline ("XXX restringo " ^ string_of_int i) in match lc, lc1 with | NCic.Irl len, NCic.Irl len1 when shift1 + len1 < shift || shift1 > shift + len -> - prerr_endline "WWW 1"; let restrictions = HExtlib.list_seq 1 (len1 + 1) in let metasenv, subst, newmeta = restrict metasenv subst i restrictions @@ -376,7 +369,6 @@ let delift metasenv subst context n l t = | NCic.Irl len, NCic.Irl len1 when shift1 < shift || len1 + shift1 > len + shift -> (* C. Hoare. Premature optimization is the root of all evil*) - prerr_endline ("WWW 2 : " ^ string_of_int i); let stop = shift + len in let stop1 = shift1 + len1 in let low_gap = max 0 (shift - shift1) in @@ -388,23 +380,26 @@ let delift metasenv subst context n l t = let metasenv, subst, newmeta = restrict metasenv subst i restrictions in +(* prerr_endline ("RESTRICTIONS FOR: " ^ - NCicPp.ppterm ~metasenv ~subst ~context:[] - (NCic.Meta (i,l1)) ^ - " that was part of a term unified with " ^ NCicPp.ppterm ~metasenv ~subst ~context:[] - (NCic.Meta (n,l)) ^ " ====> " ^ - String.concat "," (List.map string_of_int restrictions) - ^ "\nMENV:\n" ^ NCicPp.ppmetasenv ~subst metasenv - ^ "\nSUBST:\n" ^ NCicPp.ppsubst subst ~metasenv - ); - let newlc = - assert (if shift1 > k then shift1 + low_gap - shift = 0 else - true); - NCic.Irl (len1 - low_gap - high_gap + max 0 (k - shift1)) in + (NCic.Meta (i,l1))^" that was part of a term unified with " + ^ NCicPp.ppterm ~metasenv ~subst ~context:[] (NCic.Meta + (n,l)) ^ " ====> " ^ String.concat "," (List.map + string_of_int restrictions) ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv ^ "\nSUBST:\n" ^ + NCicPp.ppsubst subst ~metasenv); +*) + let newlc_len = + len1 - low_gap - high_gap + max 0 (k - shift1) in + assert (if shift1 > k then + shift1 + low_gap - shift = 0 else true); let meta = - NCic.Meta(newmeta,(shift1 + low_gap - shift, newlc)) + NCic.Meta(newmeta,(shift1 + low_gap - shift, + NCic.Irl newlc_len)) in + let _, cctx, _ = NCicUtils.lookup_meta newmeta metasenv in + assert (List.length cctx = newlc_len); (metasenv, subst), meta | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig @@ -412,12 +407,13 @@ let delift metasenv subst context n l t = ms, NCic.Meta (i, (max 0 (shift1 - shift), lc1)) | _ -> let lc1 = NCicUtils.expand_local_context lc1 in + let lc1 = List.map (NCicSubstitution.lift shift1) lc1 in let rec deliftl tbr j ms = function | [] -> ms, tbr, [] | t::tl -> let ms, tbr, tl = deliftl tbr (j+1) ms tl in try - let ms, t = aux (k-shift1) ms t in + let ms, t = aux k ms t in ms, tbr, t::tl with | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl @@ -427,7 +423,11 @@ let delift metasenv subst context n l t = prerr_endline ("TO BE RESTRICTED: " ^ (String.concat "," (List.map string_of_int to_be_r))); *) - let l1 = pack_lc (shift, NCic.Ctx lc1') in + let l1 = pack_lc (0, NCic.Ctx lc1') in +(* + prerr_endline ("newmeta:" ^ NCicPp.ppterm + ~metasenv ~subst ~context (NCic.Meta (999,l1))); +*) if to_be_r = [] then (metasenv, subst), (if lc1' = lc1 then orig else NCic.Meta (i,l1)) @@ -435,6 +435,7 @@ let delift metasenv subst context n l t = let metasenv, subst, newmeta = restrict metasenv subst i to_be_r in (metasenv, subst), NCic.Meta(newmeta,l1)) + | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t in try aux 0 (metasenv,subst) t diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 253af6f37..eb7b136c2 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -22,11 +22,13 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; +(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; +*) -(* let pp _ = ();; *) +let pp _ = ();; let wrap_exc msg = function | NCicUnification.Uncertain _ -> Uncertain msg @@ -292,6 +294,9 @@ let rec typeof let ty_branch = NCicTypeChecker.type_of_branch ~subst context leftno outtype cons ty_cons in + pp (lazy ("TYPEOFBRANCH: " ^ + NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^ + 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) @@ -327,8 +332,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args = in let flex_prod = C.Prod ("_", ty_arg, meta) in pp (lazy ( "UNIFICATION in CTX:\n"^ - NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^ - NCicPp.ppmetasenv ~subst metasenv ^ "\nOF: " ^ + NCicPp.ppcontext ~metasenv ~subst context + ^ "\nOF: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); let metasenv, subst = diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d3c86d281..202e68e4c 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -72,18 +72,26 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; +(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; +*) -(* let pp _ = ();; *) +let pp _ = ();; -let fix_sorts metasenv subst context meta t = +let fix_sorts swap metasenv subst context meta t = let rec aux () = function | NCic.Sort (NCic.Type u) as orig -> - (match NCicEnvironment.sup u with - | None -> raise (fail_exc metasenv subst context meta t) - | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)) + if swap then + match NCicEnvironment.sup u with + | None -> 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 ( + match NCicEnvironment.sup NCicEnvironment.type0 with + | Some x -> x + | _ -> assert false)) | NCic.Meta _ as orig -> orig | t -> NCicUtils.map (fun _ _ -> ()) () aux t in @@ -157,35 +165,31 @@ and instantiate test_eq_only metasenv subst context n lc t swap = if swap then unify test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 in - let fix_sorts t = - if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t - else - NCic.Sort (NCic.Type ( - match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ -> - assert false)) - in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let metasenv, subst, t = match ty with - | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t + | NCic.Implicit (`Typeof _) -> + metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t | _ -> pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with NCicTypeChecker.TypeCheckerFailure _ -> - let ft = fix_sorts t in - if ft == t then assert false else + let ft = + fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t + in + if ft == t then assert false + else try pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context ft)); ft, NCicTypeChecker.typeof ~subst ~metasenv context ft - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft); - prerr_endline (Lazy.force msg); + with NCicTypeChecker.TypeCheckerFailure _ -> assert false in let lty = NCicSubstitution.subst_meta lc ty in pp (lazy("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in -- 2.39.2