blob: 7f3e5932445604ea11236ac217e231b775dda3f1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** * Interface of calls to Coq by CoqIde *)
type 'a menu = 'a * (string * string) list
type goals =
| Message of string
| Goals of ((string menu) list * string menu) list
(** We use phantom types and GADT to protect ourselves against wild casts *)
type 'a call =
| In_loadpath of string
| Raw_interp of string
| Interp of bool * string
| Rewind of int
| Read_stdout
| Cur_goals
| Cur_status
| Cases of string
let interp (b,s) : unit call = Interp (b,s)
let raw_interp s : unit call = Raw_interp s
let read_stdout : string call = Read_stdout
let rewind i : unit call = Rewind i
let is_in_loadpath s : bool call = In_loadpath s
let current_goals : goals call = Cur_goals
let current_status : string call = Cur_status
let make_cases s : string list list call = Cases s
(** * Coq answers to CoqIde *)
type location = (int * int) option (* start and end of the error *)
type 'a value =
| Good of 'a
| Fail of (location * string)
type handler = {
interp : bool * string -> unit;
raw_interp : string -> unit;
read_stdout : unit -> string;
rewind : int -> unit;
is_in_loadpath : string -> bool;
current_goals : unit -> goals;
current_status : unit -> string;
make_cases : string -> string list list;
}
let abstract_eval_call handler explain_exn c =
try
let res = match c with
| In_loadpath s -> Obj.magic (handler.is_in_loadpath s)
| Raw_interp s -> Obj.magic (handler.raw_interp s)
| Interp (b,s) -> Obj.magic (handler.interp (b,s))
| Rewind i -> Obj.magic (handler.rewind i)
| Read_stdout -> Obj.magic (handler.read_stdout ())
| Cur_goals -> Obj.magic (handler.current_goals ())
| Cur_status -> Obj.magic (handler.current_status ())
| Cases s -> Obj.magic (handler.make_cases s)
in Good res
with e ->
let (l,str) = explain_exn e in
Fail (l,str)
(** * Debug printing *)
let pr_call = function
| In_loadpath s -> "In_loadpath["^s^"]"
| Raw_interp s -> "Raw_interp["^s^"]"
| Interp (b,s) -> "Interp["^(if b then "true" else "false")^","^s^"]"
| Rewind i -> "Rewind["^(string_of_int i)^"]"
| Read_stdout -> "Read_stdout"
| Cur_goals -> "Cur_goals"
| Cur_status -> "Cur_status"
| Cases s -> "Cases["^s^"]"
let pr_value = function
| Good _ -> "Good"
| Fail (_,str) -> "Fail["^str^"]"
|
