1(****************************************************************************)
2(* Copyright (C) 2007-2009 Gacek                                            *)
3(* Copyright (C) 2013-2018 Inria (Institut National de Recherche            *)
4(*                         en Informatique et en Automatique)               *)
5(*                                                                          *)
6(* This file is part of Abella.                                             *)
7(*                                                                          *)
8(* Abella is free software: you can redistribute it and/or modify           *)
9(* it under the terms of the GNU General Public License as published by     *)
10(* the Free Software Foundation, either version 3 of the License, or        *)
11(* (at your option) any later version.                                      *)
12(*                                                                          *)
13(* Abella is distributed in the hope that it will be useful,                *)
14(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
15(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
16(* GNU General Public License for more details.                             *)
17(*                                                                          *)
18(* You should have received a copy of the GNU General Public License        *)
19(* along with Abella.  If not, see <http://www.gnu.org/licenses/>.          *)
20(****************************************************************************)
21
22open Metaterm
23open Term
24open Typing
25open Printf
26open Extensions
27
28type uclause = string option * uterm * uterm list
29type clause = string list * term
30
31type flavor = Inductive | CoInductive
32
33type udef_clause = umetaterm * umetaterm
34type def_clause = {
35  head : metaterm ;
36  body : metaterm ;
37}
38type def = {
39  flavor   : flavor ;
40  typarams : string list ;
41  mutual   : ty Itab.t ;
42  clauses  : def_clause list ;
43}
44type defs_table = (string, def) Hashtbl.t
45
46type id = string
47
48exception Reported_parse_error
49
50type set_value =
51  | Str of string
52  | Int of int
53  | QStr of string
54
55type clearable =
56  | Keep of id * ty list
57  | Remove of id * ty list
58
59type common_command =
60  | Back | Reset
61  | Set of string * set_value
62  | Show of string
63  | Quit
64
65type top_command =
66  | Theorem of id * string list * umetaterm
67  | Define of flavor * tyctx * udef_clause list
68  | Import of string * (string * string) list
69  | Specification of string
70  | Query of umetaterm
71  | Kind of id list * knd
72  | Type of id list * ty
73  | Close of aty list
74  | SSplit of id * id list
75  | TopCommon of common_command
76
77type compiled =
78  | CTheorem of id * string list * metaterm
79  | CDefine of flavor * string list * tyctx * def_clause list
80  | CImport of string * (string * string) list
81  | CKind of id list * knd
82  | CType of id list * ty
83  | CClose of (aty * aty list) list
84
85type witness =
86  | WTrue
87  | WHyp of id
88  | WLeft of witness
89  | WRight of witness
90  | WSplit of witness * witness
91  | WForall of id list * witness
92  | WIntros of id list * witness
93  | WExists of (id * term) list * witness
94  | WReflexive
95  | WUnfold of id * int * witness list
96  | WMagic
97
98let witness_to_string =
99  let bind_to_string (id, t) =
100    id ^ " = " ^ term_to_string t
101  in
102
103  let rec aux = function
104    | WTrue -> "true"
105    | WHyp id -> "apply " ^ id
106    | WLeft w -> "left " ^ aux w
107    | WRight w -> "right " ^ aux w
108    | WSplit(w1,w2) -> "split(" ^ aux w1 ^ ", " ^ aux w2 ^ ")"
109    | WForall(ids,w) ->
110        "forall[" ^ (String.concat ", " ids) ^ "] " ^ aux w
111    | WIntros(ids,w) ->
112        "intros[" ^ (String.concat ", " ids) ^ "] " ^ aux w
113    | WExists(binds,w) ->
114        "exists[" ^ (String.concat ", " (List.map bind_to_string binds)) ^
115        "] " ^ aux w
116    | WReflexive -> "="
117    | WUnfold(id,n,[]) ->
118        Printf.sprintf "unfold(%s, %d)" id n
119    | WUnfold(id,n,ws) ->
120        let ws = List.map aux ws |> String.concat ", " in
121        Printf.sprintf "unfold(%s, %d, %s)" id n ws
122    | WMagic -> "*"
123  in
124  aux
125
126type depth_bound = int
127
128type ewitness =
129  | ETerm of uterm
130  | ESub of id * uterm
131
132type clear_mode =
133  | Clear_delete
134  | Clear_extro
135
136type hhint = id option
137
138type command =
139  | Induction of int list * hhint
140  | CoInduction of id option
141  | Apply of depth_bound option * clearable * clearable list * (id * uterm) list * hhint
142  | Backchain of depth_bound option * clearable * (id * uterm) list
143  | CutFrom of clearable * clearable * uterm * hhint
144  | Cut of clearable * clearable * hhint
145  | SearchCut of clearable * hhint
146  | Inst of clearable * (id * uterm) list * hhint
147  | Case of clearable * hhint
148  | Assert of umetaterm * int option * hhint
149  | Monotone of clearable * uterm * hhint
150  | Exists of [`EXISTS | `WITNESS] * ewitness list
151  | Clear of clear_mode * id list
152  | Abbrev of id list * string
153  | Unabbrev of id list
154  | Rename of id * id
155  | Permute of id list * id option
156  | Search of [`nobounds | `depth of depth_bound | `witness of witness]
157  | Async_steps
158  | Split
159  | SplitStar
160  | Left
161  | Right
162  | Intros of id list
163  | Unfold of clause_selector * solution_selector
164  | Skip
165  | Abort
166  | Undo
167  | Common of common_command
168
169and clause_selector =
170  | Select_any
171  | Select_num of int
172  | Select_named of string
173
174and solution_selector =
175  | Solution_first
176  | Solution_all
177
178type any_command =
179  | ATopCommand of top_command
180  | ACommand of command
181  | ACommon of common_command
182
183type sig_decl =
184  | SKind of id list * knd
185  | SType of id list * ty
186
187type lpsig =
188  | Sig of string * string list * sig_decl list
189
190type lpmod =
191  | Mod of string * string list * uclause list
192
193let udef_to_string (head, body) =
194  if body = UTrue then
195    umetaterm_to_string head
196  else
197    sprintf "%s := %s" (umetaterm_to_string head)
198      (umetaterm_to_formatted_string body)
199
200let udef_clauses_to_string cls =
201  String.concat ";\n" (List.map udef_to_string cls)
202
203let flavor_to_string dtype =
204  match dtype with
205    | Inductive -> "inductive"
206    | CoInductive -> "coinductive"
207
208let set_value_to_string v =
209  match v with
210    | Str s -> s
211    | Int d -> string_of_int d
212    | QStr s -> sprintf "%S" s
213
214let id_list_to_string ids =
215  String.concat ", " ids
216
217let idtys_to_string idtys =
218  String.concat ",\t\n"
219    (List.map (fun (id, ty) -> id ^ " : " ^ (ty_to_string ty)) idtys)
220
221let inst_to_string tys =
222  match tys with
223  | [] -> ""
224  | _ -> "[" ^ (List.map ty_to_string tys |> String.concat ",") ^ "]"
225
226let clearable_to_string cl =
227  match cl with
228  | Keep (h, tys) -> h ^ inst_to_string tys
229  | Remove (h, tys) -> "*" ^ h ^ inst_to_string tys
230
231let common_command_to_string cc =
232  match cc with
233  | Back ->
234      sprintf "#<back>"
235  | Reset ->
236      sprintf "#<reset>"
237  | Set(k, v) ->
238      sprintf "Set %s %s" k (set_value_to_string v)
239  | Show nm ->
240      sprintf "Show %s" nm
241  | Quit ->
242      sprintf "Quit"
243
244let gen_to_string tys =
245  match tys with
246  | [] -> ""
247  | _ -> " [" ^ String.concat "," tys ^ "]"
248
249let aty_list_to_string atys =
250  String.concat "," (List.map aty_to_string atys)
251
252let top_command_to_string tc =
253  match tc with
254    | Theorem(name, tys, body) ->
255        sprintf "Theorem %s%s : \n%s" name (gen_to_string tys)
256          (umetaterm_to_formatted_string body)
257    | Define(flavor, idtys, cls) ->
258        sprintf "%s %s by \n%s"
259          (match flavor with Inductive -> "Define" | _ -> "CoDefine")
260          (idtys_to_string idtys) (udef_clauses_to_string cls) ;
261    | Import (filename, withs) ->
262        sprintf "Import \"%s\"%s%s" filename
263          (if withs = [] then "" else " with ")
264          (withs |>
265           List.map (fun (a, b) -> a ^ " := " ^ b) |>
266           String.concat ", ")
267    | Specification filename ->
268        sprintf "Specification \"%s\"" filename
269    | Query q ->
270        sprintf "Query %s" (umetaterm_to_formatted_string q)
271    | Kind (ids, knd) ->
272        sprintf "Kind %s %s" (id_list_to_string ids) (knd_to_string knd)
273    | Type(ids, ty) ->
274        sprintf "Type %s %s" (id_list_to_string ids) (ty_to_string ty)
275    | Close atys ->
276        sprintf "Close %s" (aty_list_to_string atys)
277    | SSplit(id, ids) ->
278        if ids <> [] then
279          sprintf "Split %s as %s" id (id_list_to_string ids)
280        else
281          sprintf "Split %s" id
282    | TopCommon(cc) ->
283        common_command_to_string cc
284
285let withs_to_string ws =
286  String.concat ", "
287    (List.map (fun (x,t) -> x ^ " = " ^ (uterm_to_string t)) ws)
288
289let hn_to_string = function
290  | None -> ""
291  | Some hn -> sprintf "%s : " hn
292
293let clearables_to_string cls =
294  List.map clearable_to_string cls |> String.concat " "
295
296let dbound_to_string = function
297  | None -> ""
298  | Some n -> " " ^ string_of_int n
299
300let ewitness_to_string = function
301  | ETerm t -> uterm_to_string t
302  | ESub (x, t) -> x ^ " = " ^ uterm_to_string t
303
304let command_to_string c =
305  match c with
306    | Induction(is, hn) ->
307        sprintf "%sinduction on %s" (hn_to_string hn)
308          (String.concat " " (List.map string_of_int is))
309    | CoInduction None -> "coinduction"
310    | CoInduction (Some hn) -> "coinduction " ^ hn
311    | Apply(dbound, h, hs, ws, hn) -> begin
312        let buf = Buffer.create 10 in
313        Buffer.add_string buf (hn_to_string hn) ;
314        Buffer.add_string buf "apply" ;
315        Buffer.add_string buf (dbound_to_string dbound) ;
316        Buffer.add_string buf (" " ^ clearable_to_string h) ;
317        if hs <> [] then
318          (Buffer.add_string buf " to " ;
319           Buffer.add_string buf (clearables_to_string hs)) ;
320        if ws <> [] then
321          (Buffer.add_string buf " with " ;
322           Buffer.add_string buf (withs_to_string ws)) ;
323        Buffer.contents buf
324      end
325    | Backchain(dbound, h, []) ->
326        sprintf "backchain%s %s"
327          (dbound_to_string dbound)
328          (clearable_to_string h)
329    | Backchain(dbound, h, ws) ->
330        sprintf "backchain%s %s with %s"
331          (dbound_to_string dbound)
332          (clearable_to_string h)
333          (withs_to_string ws)
334    | Cut(h1, h2, hn) ->
335        sprintf "%scut %s with %s"
336          (hn_to_string hn)
337          (clearable_to_string h1)
338          (clearable_to_string h2)
339    | CutFrom(h, arg, t, hn) ->
340        sprintf "%scut %s from %s with %s"
341          (hn_to_string hn) (uterm_to_string t)
342          (clearable_to_string h)
343          (clearable_to_string arg)
344    | SearchCut(h, hn) ->
345        sprintf "%s cut %s" (hn_to_string hn)
346          (clearable_to_string h)
347    | Inst(h, ws, hn) ->
348        sprintf "%s inst %s with %s" (hn_to_string hn)
349          (clearable_to_string h)
350          (withs_to_string ws)
351    | Case(Keep (h, _), hn) ->
352        sprintf "%scase %s (keep)" (hn_to_string hn) h
353    | Case(Remove (h, _), hn) ->
354        sprintf "%scase %s" (hn_to_string hn) h
355    | Assert(t, dp, hn) ->
356        sprintf "%sassert %s%s"
357          (hn_to_string hn)
358          (match dp with
359           | Some dp -> string_of_int dp ^ " "
360           | None -> "")
361          (umetaterm_to_formatted_string t)
362    | Monotone(h, t, hn) ->
363        sprintf "%smonotone %s with %s"
364          (hn_to_string hn)
365          (clearable_to_string h)
366          (uterm_to_string t)
367    | Exists (how, ews) ->
368        let hows = match how with
369          | `EXISTS -> "exists"
370          | `WITNESS -> "witness"
371        in
372        sprintf "%s %s" hows
373          (List.map ewitness_to_string ews |> String.concat ", ")
374    | Clear (cm, hs) ->
375        sprintf "clear %s%s"
376          (match cm with
377           | Clear_delete -> ""
378           | Clear_extro -> " -> ")
379          (String.concat " " hs)
380    | Abbrev(hs, s) ->
381        sprintf "abbrev %s \"%s\"" (String.concat " " hs) s
382    | Unabbrev hs ->
383        sprintf "unabbrev %s" (String.concat " " hs)
384    | Rename(hfrom, hto) ->
385        sprintf "rename %s to %s" hfrom hto
386    | Permute(ids, t) ->
387        sprintf "permute (%s)%s"
388          (String.concat " " ids)
389          (match t with None -> "" | Some h -> " " ^ h)
390    | Search(`nobounds) -> "search"
391    | Search(`depth d) -> sprintf "search %d" d
392    | Search(`witness w) -> sprintf "search with %s" (witness_to_string w)
393    | Async_steps -> "async"
394    | Split -> "split"
395    | SplitStar -> "split*"
396    | Left -> "left"
397    | Right -> "right"
398    | Unfold (clause_sel, sol_sel) ->
399        sprintf "unfold%s%s"
400          (match clause_sel with
401           | Select_any -> ""
402           | Select_num n -> " " ^ string_of_int n
403           | Select_named n -> " " ^ n)
404          (match sol_sel with
405           | Solution_first -> ""
406           | Solution_all -> " (all)")
407    | Intros [] -> "intros"
408    | Intros ids -> sprintf "intros %s" (String.concat " " ids)
409    | Skip -> "skip"
410    | Abort -> "abort"
411    | Undo -> "undo"
412    | Common(cc) -> common_command_to_string cc
413