From 7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Sep 2009 20:19:38 +0000 Subject: [PATCH] rewritten instantiate code --- .../components/ng_refiner/nCicMetaSubst.ml | 2 +- .../components/ng_refiner/nCicUnifHint.ml | 42 ++++- .../components/ng_refiner/nCicUnification.ml | 167 ++++++++++-------- 3 files changed, 132 insertions(+), 79 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index bdd0adfe0..496648f55 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -463,7 +463,7 @@ let mk_meta ?(attrs=[]) metasenv context ty = menv_entry :: metasenv, n, NCic.Meta (n, (0,NCic.Irl len)), ty | `Sort -> let ty = NCic.Implicit (`Typeof n) in - mk_meta (tyof attrs) n metasenv [] (`WithType ty) + mk_meta (`IsSort::tyof attrs) n metasenv [] (`WithType ty) | `Type -> let metasenv, _, ty, _ = mk_meta (tyof attrs) (newmeta ()) metasenv context `Sort in diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index a84ce0f4f..e3112f3f2 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -316,6 +316,40 @@ let look_for_hint hdb metasenv subst context t1 t2 = rc ;; +let pp_hint t p = + let context, t = + let rec aux ctx = function + | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest + | t -> ctx, t + in + aux [] t + in + let recproblems, concl = + let rec aux ctx = function + | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest + | t -> ctx, t + in + aux [] t + in + let buff = Buffer.create 100 in + let fmt = Format.formatter_of_buffer buff in +(* + F.fprintf "@[" + F.fprintf "@[" +(* pp_ctx [] context *) + F.fprintf "@]" + F.fprintf "@;" + F.fprintf "@[" +(* pp_ctx context recproblems *) + F.fprintf "@]" + F.fprintf "\vdash@;"; + NCicPp.ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[]; + F.fprintf "@]" + F.fprintf formatter "@?"; + prerr_endline (Buffer.contents buff); +*) +() +;; let generate_dot_file status fmt = let module Pp = GraphvizPp.Dot in @@ -344,18 +378,20 @@ let generate_dot_file status fmt = (NCicPp.ppterm ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r) in - let hint = "???" (* + let shint = "???" (* string_of_int precedence ^ "..." ^ Str.global_substitute (Str.regexp "\n") (fun _ -> "") (NCicPp.ppterm ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*) in nodes := (mangle l,l) :: (mangle r,r) :: !nodes; - edges := (mangle l, mangle r, hint) :: !edges) + edges := (mangle l, mangle r, shint, precedence, hint) :: !edges) (HintSet.elements dataset); ); List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes; - List.iter (fun x, y, l -> + List.iter (fun x, y, l, _, _ -> Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt) !edges; + edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges; + List.iter (fun x, y, _, p, l -> pp_hint l p) !edges; ;; diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 09b1f3d2e..8e3cf216e 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -200,98 +200,115 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = if swap then unify rdb test_eq_only m s c t2 t1 else unify rdb test_eq_only m s c t1 t2 in - let name, ctx, ty = NCicUtils.lookup_meta n metasenv in + let has_tag = List.exists in + let tags, _, ty = NCicUtils.lookup_meta n metasenv in + (* on the types *) let metasenv, subst, t = match ty with - | NCic.Implicit (`Typeof _) -> - (match NCicReduction.whd ~subst context t with - NCic.Sort _ -> metasenv,subst,t - | NCic.Meta (i,_) when - let _,_,ty = NCicUtils.lookup_meta i metasenv in - (match ty with - NCic.Implicit (`Typeof _) -> true - | _ -> false) - -> metasenv,subst,t - | NCic.Meta (i,_) -> - let rec remove_and_hope i = - let _,ctx,ty = NCicUtils.lookup_meta i metasenv in - match ty with - NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv - | _ -> - match NCicReduction.whd ~subst ctx ty with - NCic.Meta (j,_) -> - let metasenv = remove_and_hope j in - List.filter (fun i',_ -> i <> i') metasenv - | _ -> assert false (* NON POSSO RESTRINGERE *) - in - let metasenv = remove_and_hope i in - let metasenv = - (i,([],[],NCic.Implicit (`Typeof i))):: - List.filter (fun i',_ -> i <> i') metasenv - in - metasenv,subst,t - | NCic.Appl (NCic.Meta _::_) -> - raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")) - | t when could_reduce t -> - raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")) - | _ -> - raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term"))) + | NCic.Implicit (`Typeof _) -> + pp(lazy("meta with no type")); + assert(has_tag ((=)`IsSort) tags); + metasenv, subst, t | _ -> - pp (lazy ( - "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ - ppcontext ~metasenv ~subst context ^ - ppmetasenv ~subst metasenv)); let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with | NCicTypeChecker.AssertFailure msg -> - (pp (lazy "fine typeof (fallimento)"); - let ft = fix_sorts swap exc_to_be t in - if ft == t then - (prerr_endline ( ("ILLTYPED: " ^ - NCicPp.ppterm ~metasenv ~subst ~context t - ^ "\nBECAUSE:" ^ Lazy.force msg ^ - ppcontext ~metasenv ~subst context ^ - 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.AssertFailure _ -> - assert false) + pp(lazy("we try to fix the sort\n"^Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst + metasenv)); + let ft = fix_sorts swap exc_to_be t in + pp(lazy("unable to fix the sort")); + if ft == t then begin + raise (UnificationFailure (lazy ("unable to fix sorts of: "^ + NCicPp.ppterm ~metasenv ~subst ~context t))) + end; + (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.AssertFailure _ -> + raise (UnificationFailure (lazy + ("fix sorts generated an ill-typed: "^ + NCicPp.ppterm ~metasenv ~subst ~context t)))) | NCicTypeChecker.TypeCheckerFailure msg -> prerr_endline (Lazy.force msg); - prerr_endline ( - "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ - ppcontext ~metasenv ~subst context ^ - ppmetasenv ~subst metasenv); - pp msg; assert false + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); + prerr_endline (ppcontext ~metasenv ~subst context); + prerr_endline (ppmetasenv ~subst metasenv); + assert false in - let lty = NCicSubstitution.subst_meta lc ty in match ty_t with - | NCic.Implicit _ -> - raise (UnificationFailure - (lazy "trying to unify a term with a type")) - | ty_t -> + | NCic.Implicit (`Typeof _) -> + raise (UnificationFailure(lazy "trying to unify a term with a type")) + | _ -> + 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)); + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context ty_t)); let metasenv,subst = - try - unify test_eq_only metasenv subst context lty ty_t + try unify test_eq_only metasenv subst context lty ty_t with NCicEnvironment.BadConstraint _ as exc -> let ty_t = fix_sorts swap exc_to_be ty_t in try unify test_eq_only metasenv subst context lty ty_t - with _ -> raise exc in - metasenv, subst, t + with + | NCicEnvironment.BadConstraint _ + | UnificationFailure _ -> raise exc + in + metasenv, subst, t + in + (* viral sortification *) + let is_sort metasenv subst context t = + match NCicReduction.whd ~subst context t with + | NCic.Meta (i,_) -> + let tags, _, _ = NCicUtils.lookup_meta i metasenv in + has_tag ((=) `IsSort) tags + | NCic.Sort _ -> true + | _ -> false in - pp (lazy(string_of_int n ^ " := 111 = "^ - NCicPp.ppterm ~metasenv ~subst ~context t)); + let rec sortify metasenv subst = function + | NCic.Implicit (`Typeof _) + | NCic.Sort _ as t -> metasenv, subst, t, 0 + | NCic.Meta (i,_) as t -> + let tags, context, ty = NCicUtils.lookup_meta i metasenv in + if has_tag ((=) `IsSort) tags then metasenv, subst, t, i + else + let ty = NCicReduction.whd ~subst context ty in + let metasenv, subst, ty, _ = sortify metasenv subst ty in + let metasenv, j, m, _ = + NCicMetaSubst.mk_meta metasenv [] (`WithType ty) + in + pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j)); + let metasenv,subst = unify test_eq_only metasenv subst context t m in + let j = if swap then i else j in + let tags, context, ty = NCicUtils.lookup_meta j metasenv in + let tags = `IsSort :: tags in + let metasenv = List.filter (fun x,_ -> x <> j) metasenv in + let metasenv = (j,(tags,context,ty)) ::metasenv in + metasenv, subst, m, j + | t -> + if could_reduce t then raise (Uncertain(lazy "not a sort")) + else raise (UnificationFailure(lazy "not a sort")) + in + let metasenv, subst, _, n = + if has_tag ((=) `IsSort) tags then + let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t) + in m,s,x,n + else if is_sort metasenv subst context t then + sortify metasenv subst (NCic.Meta (n,lc)) + else + metasenv, subst, NCic.Rel ~-1,n + in + let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in + (* instantiation *) + + (* sortification: + - Meta sort === t -> check t is sort or sortify + - add tag `IsSort and set cc=[] to n and its pile + - se gli ancestor non sono sorte o meta... bum... + - cambiare in-place menv + - geneare meta fresh sorta e dall'alto al basso + - Meta _ === Meta sort -> sortify n (i.e. add `IsSort) + *) + pp (lazy(string_of_int n ^ " := 111 = "^ + NCicPp.ppterm ~metasenv ~subst ~context t)); let (metasenv, subst), t = try NCicMetaSubst.delift @@ -323,7 +340,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = with NCicUtils.Subst_not_found _ -> (* by cumulativity when unify(?,Type_i) * we could ? := Type_j with j <= i... *) - let subst = (n, (name, ctx, t, ty)) :: subst in + let subst = (n, (tags, ctx, t, ty)) :: subst in pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); let metasenv = -- 2.39.2