From 61d514611fc8434164c4275e7b59f81617104ef3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 31 Mar 2010 13:35:12 +0000 Subject: [PATCH] More debugging info from print_tac. From: sacerdot --- helm/software/components/ng_tactics/nTacStatus.ml | 7 ++++--- helm/software/components/ng_tactics/nTacStatus.mli | 4 ++-- helm/software/components/ng_tactics/nTactics.ml | 2 +- helm/software/components/ng_tactics/nTactics.mli | 2 ++ 4 files changed, 9 insertions(+), 6 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 6d5df3196..280634d30 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -51,8 +51,9 @@ class pstatus = type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input -let pp_status status = - pp (lazy (NCicPp.ppobj status#obj)) +let pp_tac_status status = + prerr_endline (NCicPp.ppobj status#obj); + prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack) ;; type cic_term = NCic.context * NCic.term @@ -409,7 +410,7 @@ let analyse_indty status ty = | _,NCic.Const ref -> ref, [] | _,NCic.Appl (NCic.Const (NRef.Ref (_,(NRef.Ind _)) as ref) :: args) -> ref, args - | _,_ -> fail (lazy ("not an inductive type")) in + | _,_ -> fail (lazy ("not an inductive type: " ^ ppterm status ty)) in let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in let _,_,_,cl = List.nth tl i in let consno = List.length cl in diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli index 6e4cc79dd..ad9df5256 100644 --- a/helm/software/components/ng_tactics/nTacStatus.mli +++ b/helm/software/components/ng_tactics/nTacStatus.mli @@ -88,8 +88,6 @@ val mk_in_scope: #pstatus as 'status -> cic_term -> 'status * cic_term val mk_out_scope: int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term -val pp_status: #pstatus -> unit - class type ['stack] g_status = object inherit g_pstatus @@ -111,6 +109,8 @@ type 'status lowtactic = #lowtac_status as 'status -> int -> 'status class type tac_status = [Continuationals.Stack.t] status +val pp_tac_status: #tac_status -> unit + type 'status tactic = #tac_status as 'status -> 'status (* indexing facilities over cic_term based on inverse De Bruijn indexes *) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 019aac2f1..f6d8bfaec 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -22,7 +22,7 @@ module Ast = CicNotationPt let id_tac status = status ;; let print_tac print_status message status = - if print_status then pp_status status; + if print_status then pp_tac_status status; prerr_endline message; status ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index a4b2bde68..a4c48e686 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -11,6 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +val print_tac: bool -> string -> 's NTacStatus.tactic + val dot_tac: 's NTacStatus.tactic val branch_tac: ?force:bool -> 's NTacStatus.tactic val shift_tac: 's NTacStatus.tactic -- 2.39.2