From 735ab0a7d2f7afaed0695e014034f4b2d6e287c8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Dec 2016 08:09:54 +0100
Subject: Stdlib functions now return Ltac2 exceptions.

---
 Init.v      | 14 ++++++++++++++
 Int.v       |  2 ++
 tac2core.ml | 55 ++++++++++++++++++++++++++++++++-----------------------
 3 files changed, 48 insertions(+), 23 deletions(-)

diff --git a/Init.v b/Init.v
index 322f275346..8ff5837bb4 100644
--- a/Init.v
+++ b/Init.v
@@ -30,3 +30,17 @@ Ltac2 Type 'a option := [ None | Some ('a) ].
 Ltac2 Type 'a ref := { mutable contents : 'a }.
 
 Ltac2 Type bool := [ true | false ].
+
+(** Pervasive exceptions *)
+
+Ltac2 Type exn ::= [ Out_of_bounds ].
+(** Used for bound checking, e.g. with String and Array. *)
+
+Ltac2 Type exn ::= [ Not_focussed ].
+(** In Ltac2, the notion of "current environment" only makes sense when there is
+    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
+    focussing when we need it, we raise this non-backtracking error when it does
+    not make sense. *)
+
+Ltac2 Type exn ::= [ Not_found ].
+(** Used when something is missing. *)
diff --git a/Int.v b/Int.v
index bb0287efc8..ab43eb27b0 100644
--- a/Int.v
+++ b/Int.v
@@ -8,6 +8,8 @@
 
 Require Import Coq.ltac2.Init.
 
+Ltac2 Type exn ::= [ Division_by_zero ].
+
 Ltac2 @ external equal : int -> int -> bool := "ltac2" "int_equal".
 Ltac2 @ external compare : int -> int -> int := "ltac2" "int_compare".
 Ltac2 @ external add : int -> int -> int := "ltac2" "int_add".
diff --git a/tac2core.ml b/tac2core.ml
index 227bea8ddd..3232fcba5b 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -20,6 +20,10 @@ open Proofview.Notations
 (** Standard values *)
 
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let stdlib_prefix md =
+  MPfile (DirPath.make (List.map Id.of_string [md; "ltac2"; "Coq"]))
+let coq_stdlib md n =
+  KerName.make2 (stdlib_prefix md) (Label.of_id (Id.of_string n))
 
 let val_tag t = match val_tag t with
 | Val.Base t -> t
@@ -125,9 +129,21 @@ end
 
 let val_valexpr = Val.create "ltac2:valexpr"
 
+(** Stdlib exceptions *)
+
+let err_notfocussed =
+  LtacError (coq_core "Not_focussed", [||])
+
+let err_outofbounds =
+  LtacError (coq_core "Out_of_bounds", [||])
+
+let err_notfound =
+  LtacError (coq_core "Not_found", [||])
+
 (** Helper functions *)
 
 let thaw f = interp_app f [v_unit]
+let throw e = Proofview.tclLIFT (Proofview.NonLogical.raise e)
 
 let return x = Proofview.tclUNIT x
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -138,16 +154,9 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
-(** In Ltac2, the notion of "current environment" only makes sense when there is
-    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
-    focussing when we need it, we raise a non-backtracking error when it does
-    not make sense. *)
-exception NonFocussedGoal
-
-let () = register_handler begin function
-| NonFocussedGoal -> str "Several goals under focus"
-| _ -> raise Unhandled
-end
+let wrap_exn f err =
+  return () >>= fun () ->
+    try return (f ()) with e when CErrors.noncritical e -> err
 
 let pf_apply f =
   Proofview.Goal.goals >>= function
@@ -159,7 +168,7 @@ let pf_apply f =
     gl >>= fun gl ->
     f (Proofview.Goal.env gl) (Tacmach.New.project gl)
   | _ :: _ :: _ ->
-    Proofview.tclLIFT (Proofview.NonLogical.raise NonFocussedGoal)
+    throw err_notfocussed
 
 (** Primitives *)
 
@@ -197,8 +206,8 @@ let prm_message_concat : ml_tactic = function
 
 let prm_array_make : ml_tactic = function
 | [ValInt n; x] ->
-  (** FIXME: wrap exception *)
-  wrap (fun () -> ValBlk (0, Array.make n x))
+  if n < 0 || n > Sys.max_array_length then throw err_outofbounds
+  else wrap (fun () -> ValBlk (0, Array.make n x))
 | _ -> assert false
 
 let prm_array_length : ml_tactic = function
@@ -207,14 +216,14 @@ let prm_array_length : ml_tactic = function
 
 let prm_array_set : ml_tactic = function
 | [ValBlk (_, v); ValInt n; x] ->
-  (** FIXME: wrap exception *)
-  wrap_unit (fun () -> v.(n) <- x)
+  if n < 0 || n >= Array.length v then throw err_outofbounds
+  else wrap_unit (fun () -> v.(n) <- x)
 | _ -> assert false
 
 let prm_array_get : ml_tactic = function
 | [ValBlk (_, v); ValInt n] ->
-  (** FIXME: wrap exception *)
-  wrap (fun () -> v.(n))
+  if n < 0 || n >= Array.length v then throw err_outofbounds
+  else wrap (fun () -> v.(n))
 | _ -> assert false
 
 (** Int *)
@@ -243,8 +252,8 @@ let prm_string_make : ml_tactic = function
 | [n; c] ->
   let n = Value.to_int n in
   let c = Value.to_char c in
-  (** FIXME: wrap exception *)
-  wrap (fun () -> Value.of_string (Bytes.make n c))
+  if n < 0 || n > Sys.max_string_length then throw err_outofbounds
+  else wrap (fun () -> Value.of_string (Bytes.make n c))
 | _ -> assert false
 
 let prm_string_length : ml_tactic = function
@@ -257,16 +266,16 @@ let prm_string_set : ml_tactic = function
   let s = Value.to_string s in
   let n = Value.to_int n in
   let c = Value.to_char c in
-  (** FIXME: wrap exception *)
-  wrap_unit (fun () -> Bytes.set s n c)
+  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  else wrap_unit (fun () -> Bytes.set s n c)
 | _ -> assert false
 
 let prm_string_get : ml_tactic = function
 | [s; n] ->
   let s = Value.to_string s in
   let n = Value.to_int n in
-  (** FIXME: wrap exception *)
-  wrap (fun () -> Value.of_char (Bytes.get s n))
+  if n < 0 || n >= Bytes.length s then throw err_outofbounds
+  else wrap (fun () -> Value.of_char (Bytes.get s n))
 | _ -> assert false
 
 (** Error *)
-- 
cgit v1.2.3