From f43df7eebd322709f8c92fd94d9c5225ae3c61db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 10:14:07 +0000 Subject: [PATCH] debug + relocate uses Prop instead of (Prop Prop)... we should think a better solution --- .../components/ng_tactics/nTacStatus.ml | 137 +++++++++++------- .../components/ng_tactics/nTacStatus.mli | 2 + 2 files changed, 85 insertions(+), 54 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index ce7ca8216..f5a7c65ba 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -11,6 +11,11 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +let debug = ref false;; +let pp x = + if !debug then prerr_endline (Lazy.force x) else () +;; + exception Error of string lazy_t * exn option let fail ?exn msg = raise (Error (msg,exn)) @@ -39,74 +44,94 @@ type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input let pp_status status = - prerr_endline (NCicPp.ppobj status#obj) + pp (lazy (NCicPp.ppobj status#obj)) ;; type cic_term = NCic.context * NCic.term let ctx_of (c,_) = c ;; -let relocate status destination (source,t as orig) = - if source == destination then status, orig else - let u, d, metasenv, subst, o = status#obj in - let rec lcp ctx j i = function - | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 -> - if n1 = n2 && - NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then - NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) - else - HExtlib.mk_list (NCic.Appl - [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j - | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 -> - if n1 = n2 && - NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 && - NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then - NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) - else - HExtlib.mk_list (NCic.Appl - [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j - | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 -> - if n1 = n2 && - NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then - NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) - else - HExtlib.mk_list (NCic.Appl - [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j - | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false - | _::_, [] -> - HExtlib.mk_list (NCic.Appl - [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j - | _ -> [] - in - let lc = - lcp [] (List.length destination) (List.length source) - (List.rev destination, List.rev source) - in - let lc = (0,NCic.Ctx (List.rev lc)) in - let (metasenv, subst), t = - NCicMetaSubst.delift - ~unify:(fun m s c t1 t2 -> - try Some (NCicUnification.unify status m s c t1 t2) - with - | NCicUnification.UnificationFailure _ - | NCicUnification.Uncertain _ -> None) - metasenv subst source 0 lc t - in - let status = status#set_obj (u, d, metasenv, subst, o) in - status, (destination, t) +let ppterm status t = + let uri,height,metasenv,subst,obj = status#obj in + let context,t = t in + NCicPp.ppterm ~metasenv ~subst ~context t ;; -let relocate a b c = wrap "relocate" (relocate a b) c;; -let term_of_cic_term s t c = - let s, (_,t) = relocate s c t in - s, t +let ppcontext status c = + let uri,height,metasenv,subst,obj = status#obj in + NCicPp.ppcontext ~metasenv ~subst c ;; -let ppterm status t = +let ppterm_and_context status t = let uri,height,metasenv,subst,obj = status#obj in let context,t = t in + NCicPp.ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ NCicPp.ppterm ~metasenv ~subst ~context t ;; +let relocate status destination (source,t as orig) = + pp(lazy("relocate:\n" ^ ppterm_and_context status orig)); + pp(lazy("relocate in:\n" ^ ppcontext status destination)); + let rc = + if source == destination then status, orig else + let u, d, metasenv, subst, o = status#obj in + let hole = NCic.Sort NCic.Prop in + (* XXX (Prop Prop) is so illtyped that + even the trie used for hints lookup complains. We say Prop. + *) + let rec lcp ctx j i = function + | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) + else + HExtlib.mk_list hole j + | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 && + NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) + else + HExtlib.mk_list hole j + | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + if n1 = n2 && + NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then + NCic.Rel i :: lcp (e::ctx)(j-1) (i-1) (cl1,cl2) + else + HExtlib.mk_list hole j + | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false + | _::_, [] -> HExtlib.mk_list hole j + | _ -> [] + in + let lc = + lcp [] (List.length destination) (List.length source) + (List.rev destination, List.rev source) + in + let lc = (0,NCic.Ctx (List.rev lc)) in + pp(lazy("delifting as " ^ + NCicPp.ppterm ~metasenv ~subst ~context:source + (NCic.Meta (0,lc)))); + let (metasenv, subst), t = + NCicMetaSubst.delift + ~unify:(fun m s c t1 t2 -> + try Some (NCicUnification.unify status m s c t1 t2) + with + | NCicUnification.UnificationFailure _ + | NCicUnification.Uncertain _ -> None) + metasenv subst source 0 lc t + in + let status = status#set_obj (u, d, metasenv, subst, o) in + status, (destination, t) + in + pp(lazy("relocated: " ^ ppterm (fst rc) (snd rc))); + rc +;; +let relocate a b c = wrap "relocate" (relocate a b) c;; + +let term_of_cic_term s t c = + let s, (_,t) = relocate s c t in + s, t +;; + let disambiguate status t ty context = let status, expty = match ty with @@ -252,6 +277,7 @@ let select_term = let is_found status ctx t wanted = (* we could lift wanted step-by-step *) + pp(lazy("is_found: "^ppterm status (ctx,t))); try true, unify status ctx (ctx, t) wanted with | Error (_, Some (NCicUnification.UnificationFailure _)) @@ -325,6 +351,7 @@ let select_term (match wanted with | Some wanted -> let status', wanted = disambiguate status wanted None ctx in + pp(lazy("wanted: "^ppterm status' wanted)); let (status',found), t' = match_term status' ctx wanted t in if found then status',t' else status,t | None -> @@ -336,8 +363,10 @@ let select_term ~context:[] ~subst:[] pat ^ " against " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)) in + pp(lazy ("select in: "^ppterm low_status (context,term))); let status, term = select low_status context path term in let term = (context, term) in + pp(lazy ("postprocess: "^ppterm low_status term)); postprocess status term ;; diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 0dd5acdc0..2c1ad3b1e 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -107,4 +107,6 @@ with type constant_name = NCicInverseRelIndexable.constant_name and type input = NCicInverseRelIndexable.input and type data = Ncic_termSet.elt and type dataset = Ncic_termSet.t +val debug : bool ref + (* end *) -- 2.39.2