From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 18 Jun 2009 17:26:27 +0000 (+0000)
Subject: better exception handling
X-Git-Tag: make_still_working~3844
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=421056da7b3e1d6b9d91d72092b4f3c3232a00ce;p=helm.git

better exception handling
---

diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index dc3816dab..52a45bbd4 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -11,8 +11,18 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-exception Error of string lazy_t
-let fail msg = raise (Error msg)
+exception Error of string lazy_t * exn option
+let fail ?exn msg = raise (Error (msg,exn))
+
+let wrap f x = 
+  try f x 
+  with 
+  | MultiPassDisambiguator.DisambiguationError _ 
+  | NCicRefiner.RefineFailure _ 
+  | NCicUnification.UnificationFailure _ 
+  | NCicTypeChecker.TypeCheckerFailure _ 
+  | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy "")
+;;
 
 class pstatus =
  fun (o: NCic.obj) ->
@@ -26,12 +36,7 @@ class pstatus =
 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
 type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
-let pp_tac_status status = 
-  prerr_endline (NCicPp.ppobj status#obj)
-;;
-
-let pp_lowtac_status status = 
-  prerr_endline "--------------------------------------------";
+let pp_status status = 
   prerr_endline (NCicPp.ppobj status#obj)
 ;;
 
@@ -87,6 +92,7 @@ let relocate status destination (name,source,t as orig) =
   let status = status#set_obj (u, d, metasenv, subst, o) in
   status, (name, destination, t)
 ;;
+let relocate a b c = wrap (relocate a b) c;;
 
 let term_of_cic_term s t c = 
   let s, (_,_,t) = relocate s c t in
@@ -113,6 +119,7 @@ let disambiguate status t ty context =
  let new_pstatus = uri,height,metasenv,subst,obj in
   status#set_obj new_pstatus, (None, context, t) 
 ;;
+let disambiguate a b c d = wrap (disambiguate a b c) d;;
 
 let typeof status ctx t =
   let status, (_,_,t) = relocate status ctx t in
@@ -120,6 +127,7 @@ let typeof status ctx t =
   let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
   status, (None, ctx, ty)
 ;;
+let typeof a b c = wrap (typeof a b) c;;
   
 let whd status ?delta ctx t =
   let status, (name,_,t) = relocate status ctx t in
@@ -142,6 +150,7 @@ let unify status ctx a b =
   let metasenv, subst = NCicUnification.unify status metasenv subst ctx a b in
    status#set_obj (n,h,metasenv,subst,o)
 ;;
+let unify a b c d = wrap (unify a b c) d;;
 
 let refine status ctx term expty =
   let status, (nt,_,term) = relocate status ctx term in
@@ -156,6 +165,7 @@ let refine status ctx term expty =
   in
    status#set_obj (name,height,metasenv,subst,obj), (nt,ctx,t), (ne,ctx,ty)
 ;;
+let refine a b c d = wrap (refine a b c) d;;
 
 let get_goalty status g =
  let _,_,metasenv,_,_ = status#obj in
@@ -330,6 +340,8 @@ let apply_subst status ctx t =
   status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)
 ;;
 
+(* ============= move this elsewhere ====================*)
+
 class ['stack] status =
  fun (o: NCic.obj) (s: 'stack) ->
   object
@@ -346,3 +358,4 @@ type 'status lowtactic = #lowtac_status as 'status -> int -> 'status
 class type tac_status = [Continuationals.Stack.t] status
 
 type 'status tactic = #tac_status as 'status -> 'status
+
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index f32511265..3fdc0330d 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -11,8 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-exception Error of string lazy_t
-val fail: string lazy_t -> 'a
+exception Error of string lazy_t * exn option
+val fail: ?exn:exn -> string lazy_t -> 'a
 
 class pstatus :
  NCic.obj ->
@@ -74,7 +74,7 @@ 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_tac_status: #pstatus -> unit
+val pp_status: #pstatus -> unit
 
 class ['stack] status :
  NCic.obj -> 'stack ->
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index fe7f176a0..dab608e8a 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 open Continuationals.Stack
@@ -22,7 +22,7 @@ module Ast = CicNotationPt
 
 let id_tac status = status ;;
 let print_tac print_status message status = 
-  if print_status then pp_tac_status status;
+  if print_status then pp_status status;
   prerr_endline message; 
   status
 ;;
@@ -244,7 +244,7 @@ let first_tac tacl status =
     (fun tac _ -> try Some (tac status) with NTacStatus.Error _ -> None) tacl
   in
     match res with
-      | None -> raise (NTacStatus.Error (lazy("No tactic left")))
+      | None -> fail (lazy "No tactics left")
       | Some x -> x
 ;;
 
diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index a2da0c3e0..126b78b89 100644
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -169,8 +169,10 @@ let rec to_string =
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
   | MatitaEngine.EnrichedWithStatus (exn,_) ->
      None, "EnrichedWithStatus "^snd(to_string exn)
-  | NTacStatus.Error msg ->
-     None, "NTactic error: " ^ Lazy.force msg
+  | NTacStatus.Error (msg,None) ->
+     None, "NTactic error: " ^ Lazy.force msg 
+  | NTacStatus.Error (msg,Some exn) ->
+     None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
   | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
      let loc =
       match errorll with