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