1(*===========================================================================*) 2(* EmitML: mapping HOL expressions to ML. The basic HOL theory hierarchy has *) 3(* a loose analogue in the hierarchy of basic ML structures. Thus we have *) 4(* something like *) 5(* *) 6(* HOL Theory ML Structure *) 7(* ---------- ------------ *) 8(* boolTheory Bool *) 9(* numTheory Arbnum *) 10(* intTheory Arbint *) 11(* optionTheory Option *) 12(* listTheory List *) 13(* stringTheory Char,String *) 14(* *) 15(* Missing from this list are pairs (pairTheory in HOL, builtin to ML), *) 16(* which are flat tuples in ML and nested pairs in HOL. Also there is the *) 17(* unit type, which exists in both HOL and ML. Other structures where there *) 18(* is a close relationship arise from Anthony Fox's parameterized theory of *) 19(* n-bit words. *) 20(* *) 21(* The ideal, we assume, is to build formalizations in HOL and then "export" *) 22(* them to ML, with the idea that the executable aspects of a HOL *) 23(* formalization can be faithfully copied down to ML. If this can be *) 24(* supported, then ground HOL expressions should be able to be copied to ML *) 25(* and executed there, with huge speed-ups. This can be used to provide a *) 26(* code generation facility and a testing environment for HOL definitions. *) 27(* *) 28(* Exporting HOL definitions of types and functions consists of 2 things: *) 29(* installing those definitions in ML and mapping HOL expressions into *) 30(* syntactically acceptable ML expressions. The latter operation is "just" *) 31(* prettyprinting, where the prettyprinter uses a table mapping HOL types *) 32(* and constants to their ML counterparts. This table needs to be extensible *) 33(* as theories load. *) 34(* *) 35(*===========================================================================*) 36 37structure EmitML :> EmitML = 38struct 39 40open HolKernel boolSyntax Abbrev; 41 42val ERR = mk_HOL_ERR "EmitML"; 43val WARN = HOL_WARNING "EmitML"; 44val type_grammar = Parse.type_grammar 45 46(*---------------------------------------------------------------------------*) 47(* All ref cells. *) 48(*---------------------------------------------------------------------------*) 49 50val emitOcaml = ref false; 51val sigSuffix = ref "ML.sig"; 52val structSuffix = ref "ML.sml"; 53val sigCamlSuffix = ref "ML.mli"; 54val structCamlSuffix = ref "ML.ml"; 55 56val is_int_literal_hook = ref (fn _:term => false); 57val int_of_term_hook = ref 58 (fn _:term => (raise ERR "EmitML" "integers not loaded") : Arbint.int) 59 60(*---------------------------------------------------------------------------*) 61(* Misc. syntax operations *) 62(*---------------------------------------------------------------------------*) 63 64val is_pair_type = Lib.can pairSyntax.dest_prod; 65val is_num_literal = Lib.can Literal.relaxed_dest_numeral; 66fun nameOfC t = #Name (dest_thy_const t) 67 68(*---------------------------------------------------------------------------*) 69(* Version of dest_string that doesn't care if characters look like *) 70(* *) 71(* CHAR (NUMERAL n) or CHAR n *) 72(*---------------------------------------------------------------------------*) 73 74val is_string_literal = Lib.can Literal.relaxed_dest_string_lit; 75 76fun strip_cons M = 77 case total (listSyntax.dest_cons) M 78 of SOME (h,t) => h::strip_cons t 79 | NONE => [M]; 80 81fun is_fn_app tm = is_comb tm andalso not(pairSyntax.is_pair tm) 82fun is_infix_app tm = is_conj tm orelse is_disj tm orelse is_eq tm ; 83 84local 85 val a = mk_var("a",bool) 86 val b = mk_var("b",bool) 87in 88val andalso_tm = list_mk_abs([a,b],mk_conj(a,b)) 89val orelse_tm = list_mk_abs([a,b],mk_disj(a,b)) 90end 91 92(*---------------------------------------------------------------------------*) 93(* Peculiar names for fake record constructors. These help generate code for *) 94(* projection and access functions automatically defined for records. The *) 95(* need for this comes from the fact that large records declarations are *) 96(* modelled differently than small records; the difference in representation *) 97(* is vexatious when defining the ML projection and access functions, since *) 98(* we want the resulting ML to look the same, i.e., be readable, no matter *) 99(* how big the record is. *) 100(*---------------------------------------------------------------------------*) 101 102fun mk_record_vconstr (name,ty) = mk_var(name^"--Record Constr Var",ty) 103 104fun dest_record_vconstr v = 105 let open Substring 106 val (name,ty) = dest_var v 107 val (ss1,ss2) = position "--Record Constr Var" (full name) 108 in if string ss2 = "--Record Constr Var" 109 then (string ss1,ty) 110 else raise ERR "dest_record_vconstr" "" 111 end handle _ => raise ERR "dest_record_vconstr" ""; 112 113val is_fake_constructor = Lib.can dest_record_vconstr; 114 115local 116 val reserved_set = Redblackset.addList (Redblackset.empty String.compare, 117 ["abstype", "datatype", "do", "end", "eqtype", "exception", "fn", "fun", 118 "functor", "handle", "include", "infix", "infixr", "local", "nonfix", "op", 119 "open", "raise", "rec", "sharing", "sig", "signature", "struct", 120 "structure", "type", "val", "where", "withtype", "while"]) 121 fun is_reserved s = Redblackset.member (reserved_set, s) 122in 123 fun fix_reserved s = if is_reserved s then s ^ "_" else s 124end 125 126fun fix_symbol c = 127 case c of 128 #"#" => #"^" 129 | #"\\" => #"!" 130 | #":" => #"?" 131 | #"~" => #"$" 132 | #"|" => #"@" 133 | _ => c; 134 135fun capitalize s = 136 if !emitOcaml then 137 Char.toString (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE) 138 else 139 s; 140 141fun lowerize s = 142 if !emitOcaml then 143 Char.toString (Char.toLower (String.sub(s,0))) ^ String.extract(s,1,NONE) 144 else 145 s; 146 147fun fix_name (prefix,is_type_cons,s) = 148 let val c0 = String.sub(s,0) 149 val s1 = if not (prefix = "") andalso c0 = #" " then 150 String.extract(s,1,NONE) 151 else 152 s 153 in 154 if !emitOcaml then 155 if s = "andalso" then 156 "&&" 157 else if s = "orelse" then 158 "||" 159 else if s = "SOME" then 160 "Some" 161 else if s = "NONE" then 162 "None" 163 else let val s1 = String.map fix_symbol s in 164 if not (Char.isAlphaNum c0 orelse (s1 = "=")) then 165 prefix ^ "(" ^ s1 ^ ")" 166 else if is_type_cons then 167 prefix ^ capitalize s1 168 else 169 prefix ^ (if Char.isUpper c0 then "_" ^ s1 else fix_reserved s1) 170 end 171 else 172 prefix ^ (fix_reserved s1) 173 end; 174 175fun ML s = capitalize s ^ "ML"; 176 177fun full_name openthys (is_type_cons,s1,s2,_) = 178 let val prefix = if mem s1 openthys orelse (s1="") then 179 "" 180 else 181 ML s1 ^ "." 182 in 183 fix_name (prefix,is_type_cons,s2) 184 end; 185 186fun const_map openthys c = full_name openthys (ConstMapML.apply c); 187 188val COMMA_PREC = 50; 189val CONS_PREC = 450; 190 191fun prec_of c = 192 if same_const c boolSyntax.equality then 100 else 193 if same_const c boolSyntax.disjunction then 300 else 194 if same_const c boolSyntax.conjunction then 400 else 195 if same_const c pairSyntax.comma_tm then COMMA_PREC else 0; 196 197val minprec = ~1; 198val maxprec = 9999; 199 200datatype side = LEFT | RIGHT; 201 202fun pick_name slist n (s1,s2) = if mem n slist then s1 else s2; 203 204fun vars_of_types alist = 205 map (fn (i,ty) => mk_var("v"^Int.toString i,ty)) (Lib.enumerate 0 alist); 206 207(*---------------------------------------------------------------------------*) 208(* Convert a constructor application (C t1 ... tn) to C'(t1,...,tn) where *) 209(* C' is a variable with the same name as C. This code only deals with *) 210(* pseudo-constructors, like INSERT for sets and BAG_INSERT for bags. These *) 211(* are *not* constructors, but we will generate programs in which they are *) 212(* constructors for abstract datatypes. *) 213(* *) 214(* Real constructors are detected in the term prettyprinter by testing *) 215(* TypeBase.is_constructor. In contrast, pseudo-constructors are dealt with *) 216(* in a pre-processing pass over the theorems that code is being generated *) 217(* from. *) 218(*---------------------------------------------------------------------------*) 219 220local val emit_tag = "EmitML" 221 val pseudo_constr_defs = ref [] : thm list ref; 222in 223fun pseudo_constr_rws() = map concl (!pseudo_constr_defs) 224val reshape_thm_hook = ref (fn th => 225 pairLib.GEN_BETA_RULE (Rewrite.PURE_REWRITE_RULE (!pseudo_constr_defs) th)) 226 227fun new_pseudo_constr (c,a) = 228 let fun nstrip_fun 0 ty = ([],ty) 229 | nstrip_fun n ty = 230 let val (d,r) = dom_rng ty 231 val (f,b) = nstrip_fun (n-1) r 232 in (d::f,b) 233 end 234 val (argtys,target) = nstrip_fun a (type_of c) 235 val args = vars_of_types argtys 236 val pvar = mk_var("^" ^ fst(dest_const c), 237 pairSyntax.list_mk_prod argtys --> target) 238 val new = pairSyntax.list_mk_pabs 239 (args,mk_comb(pvar,pairSyntax.list_mk_pair args)) 240 val thm = mk_oracle_thm emit_tag ([],mk_eq(c,new)) 241 in 242 pseudo_constr_defs := thm :: !pseudo_constr_defs 243 end 244end; 245 246fun generic_type_of tm = 247 if is_const tm 248 then let val {Name,Thy,...} = dest_thy_const tm 249 in type_of (prim_mk_const{Name=Name,Thy=Thy}) 250 end 251 else type_of tm; 252 253 254fun is_supported_PMATCH tm = let 255 val pmi = patternMatchesLib.analyse_pmatch false tm 256in 257 if !emitOcaml then patternMatchesLib.is_ocaml_pmatch pmi 258 else patternMatchesLib.is_sml_pmatch pmi 259end 260 261fun strip_supported_PMATCH tm = let 262 val (i, rows) = patternMatchesSyntax.dest_PMATCH tm 263 fun dest_r r = let 264 val (_, p, g, r) = patternMatchesSyntax.dest_PMATCH_ROW_ABS r 265 in (p, r, g) end 266in 267 (i, List.map dest_r rows) 268end 269 270 271(*---------------------------------------------------------------------------*) 272(* A prettyprinter from HOL to very simple ML, dealing with basic paired *) 273(* lambda calculus terms, plus literals (strings, nums, ints), notation for *) 274(* lists, and case expressions. *) 275(*---------------------------------------------------------------------------*) 276val B = smpp.block PP.CONSISTENT 277fun term_to_ML openthys side = 278 let open Portable PP smpp 279 fun prec_paren p i j = if i >= j then add_string p else nothing 280 val lparen = prec_paren "(" 281 val rparen = prec_paren ")" 282 val const_map = const_map openthys 283 val numML = if !emitOcaml then "NumML." else "numML." 284 val intML = if !emitOcaml then "IntML." else "intML." 285 val fcpML = if !emitOcaml then "FcpML." else "fcpML." 286 fun fix s = fix_name("", false, s) 287 fun pp i tm = 288 if is_var tm then pp_var tm else 289 if is_cond tm then pp_cond i tm else 290 if is_arb tm then pp_arb i else 291 if is_num_literal tm then pp_num_literal i tm else 292 if !is_int_literal_hook tm then pp_int_literal tm else 293 if is_string_literal tm then pp_string tm else 294 if listSyntax.is_list tm then pp_list tm else 295 if listSyntax.is_cons tm then pp_cons i tm else 296 if listSyntax.is_mem tm then pp_mem i (listSyntax.dest_mem tm) else 297 if is_infix_app tm then pp_binop i tm else 298 if pairSyntax.is_pair tm then pp_pair i tm else 299 if boolSyntax.is_let tm then pp_lets i tm else 300 if pairSyntax.is_pabs tm then pp_abs i tm else 301 if combinSyntax.is_fail tm then pp_fail i tm else 302 if oneSyntax.is_one tm then pp_one tm else 303 if TypeBase.is_record tm then pp_record i (TypeBase.dest_record tm) else 304 if is_supported_PMATCH tm then 305 pp_case_with_guard i (strip_supported_PMATCH tm) else 306 if TypeBase.is_case tm then pp_case i (TypeBase.strip_case tm) else 307 if is_the_value tm then pp_itself tm else 308 if is_const tm then pp_const i tm else 309 if is_comb tm then pp_comb i tm 310 else raise ERR "term_to_ML" 311 ("Unknown syntax with term: "^Parse.term_to_string tm) 312 and pp_cond i tm = let 313 val (b,a1,a2) = dest_cond tm 314 val parens = i >= (if !emitOcaml then minprec else 70) 315 fun doparens p = if parens then B 1 (add_string "(" >> p >> add_string ")") 316 else p 317 in 318 doparens ( 319 B 0 ( 320 add_string"if" >> 321 add_break(1,2) >> 322 block PP.INCONSISTENT 0 (pp 70 b) >> 323 add_break(1,0) >> 324 add_string"then" 325 ) >> 326 add_break(1,2) >> 327 block INCONSISTENT 0 (pp 70 a1) >> 328 add_break(1,0) >> 329 B 0(add_string"else" >> add_break(1,2) >> pp minprec a2) 330 ) 331 end 332 and pp_num_from_string s = 333 if s="0" then 334 add_string (pick_name openthys "num" ("ZERO",numML ^ "ZERO")) 335 else if s="1" then 336 add_string (pick_name openthys "num" (fix "ONE",numML ^ fix "ONE")) 337 else if s="2" then 338 add_string (pick_name openthys "num" (fix "TWO",numML ^ fix "TWO")) 339 else 340 block INCONSISTENT 0 ( 341 add_string"(" >> 342 add_string (pick_name openthys "num" 343 ("fromString ", numML ^ "fromString ")) >> 344 add_break(0,0) >> 345 add_string (quote s) >> 346 add_string")" 347 ) 348 and pp_num_literal i tm = 349 (*------------------------------------------------------------*) 350 (* Numeric literals can be built from strings or constructors *) 351 (*------------------------------------------------------------*) 352 let val s = Arbnum.toString(Literal.relaxed_dest_numeral tm) 353 in if side = RIGHT (* use fromString *) 354 then 355 pp_num_from_string s 356 else (* side = LEFT, so use constructors *) 357 if s = "0" 358 then add_string (pick_name openthys "num" ("ZERO",numML ^ "ZERO")) 359 else pp_comb i tm 360 end 361 and pp_int_literal tm = 362 let val s = Arbint.toString(!int_of_term_hook tm) 363 in B 0 ( 364 add_string"(" >> add_break(0,0) >> 365 add_string (pick_name openthys "int" 366 ("fromString", intML ^ "fromString")) >> 367 add_break(0,0) >> 368 add_string (mlquote s) >> 369 add_break(0,0) >> 370 add_string")" 371 ) 372 end 373 and pp_string tm = add_string (mlquote (Literal.relaxed_dest_string_lit tm)) 374 and pp_list tm = 375 let val els = fst (listSyntax.dest_list tm) 376 in B 0 ( 377 add_string "[" >> 378 block INCONSISTENT 0 ( 379 pr_list (pp minprec) 380 (add_string (if !emitOcaml then ";" else ",") >> 381 add_break(0,0)) 382 els 383 ) >> 384 add_string "]" 385 ) 386 end 387 and pp_binop i tm = 388 let val (c,t1,t2) = case strip_comb tm 389 of (c,[t1,t2]) => (c,t1,t2) 390 | _ => raise ERR "term_to_ML" "" 391 val j = prec_of c 392 in B 0 ( 393 lparen i j >> 394 block INCONSISTENT 0 ( 395 pp (j+1) t1 >> add_break(1,0) >> 396 add_string (const_map c) >> add_break(1,0) >> 397 pp j t2 398 ) >> 399 rparen i j 400 ) 401 end 402 and pp_cons i tm = 403 let val alist = strip_cons tm 404 val j = CONS_PREC 405 in B 0 ( 406 lparen i j >> 407 block INCONSISTENT 0 ( 408 pr_list (pp j) 409 (add_string "::" >> add_break(0,0)) alist 410 ) >> 411 rparen i j 412 ) 413 end 414 and pp_mem i (t1, t2) = 415 block INCONSISTENT 0 ( 416 lparen i maxprec >> 417 add_string (full_name openthys (false,"list","MEM",bool)) >> 418 add_break(1,0) >> 419 pr_list (pp maxprec) (add_break(1,0)) [t1, t2] >> 420 rparen i maxprec 421 ) 422 and pp_pair i tm = 423 let val (t1,t2) = pairSyntax.dest_pair tm 424 val j = COMMA_PREC 425 in block INCONSISTENT 0 ( 426 lparen maxprec i >> 427 block INCONSISTENT 0 ( 428 pp (j+1) t1 >> 429 add_string "," >> add_break(0,0) >> 430 pp j t2 431 ) >> 432 rparen maxprec i 433 ) 434 end 435 and pp_lets i tm = (* a sequence of lets *) 436 let val (blists,body) = pairSyntax.strip_anylet tm 437 fun pp_binding (k,(l,r)) = 438 block INCONSISTENT 4 ( 439 add_string k >> add_break(1,0) >> 440 pp minprec l >>add_break(1,0) >> 441 add_string "=" >> add_break(1,0) >> 442 B 0 (pp minprec r) 443 ) 444 in B 0 ( 445 if !emitOcaml then 446 let 447 fun keyword [] = raise ERR "term_to_ML" "pp_lets" 448 | keyword l = ("let", hd l) :: (map (pair "and") (tl l)) 449 val blist' = map keyword blists 450 fun droplast [] = [] 451 | droplast l = List.take(l, length l - 1) 452 in 453 lparen i minprec >> 454 B 0 ( 455 mapp (fn l => 456 pr_list pp_binding add_newline l >> 457 add_break(1,0) >> add_string "in" >> add_break(1,0)) 458 (droplast blist') >> 459 pr_list pp_binding add_newline (last blist') >> 460 add_break(1,0) >> 461 add_string "in" >> add_break(1,3) >> 462 pp minprec body 463 ) >> 464 rparen i minprec 465 end 466 else 467 let 468 fun keyword1 (l,r) = (if is_fn_app l then "fun" else "val", (l,r)) 469 fun keyword [] = raise ERR "term_to_ML" "pp_lets" 470 | keyword l = map keyword1 l 471 val blist' = flatten (map keyword blists) 472 in 473 lparen i 5000 >> 474 B 0 ( 475 add_string "let " >> 476 B 0 (pr_list pp_binding add_newline blist') >> 477 add_break(1,0) >> add_string"in" >> 478 add_break(1,3) >> pp minprec body >> 479 add_break(1,0) >> add_string "end" 480 ) >> 481 rparen i 5000 482 end 483 ) 484 end 485 and pp_case i (a,cases) = 486 pp_case_with_guard i 487 (a, List.map (fn (pat, rhs) => (pat, rhs, T)) cases) 488 and pp_case_with_guard i (a,cases) = 489 B 1 ( 490 (* from HOL term grammar *) 491 lparen i (if !emitOcaml then minprec else 7) >> 492 block INCONSISTENT 2 ( 493 add_string (if !emitOcaml then "match" else "case") >> 494 add_break(1,0) >> 495 pp minprec a 496 ) >> add_break(1,0) >> 497 block CONSISTENT 1 ( 498 add_string (if !emitOcaml then "with " else "of ") >> 499 pp_case_clause (hd cases) >> 500 add_break(1,0) >> 501 pr_list (fn cl => (add_string "| " >> pp_case_clause cl)) 502 (add_break(1,0)) (tl cases) 503 ) >> 504 rparen i (if !emitOcaml then minprec else 7) 505 ) 506 and pp_case_clause (pat,rhs,guard) = 507 B 3 ( 508 pp minprec pat >> 509 (if (aconv guard T) then nothing 510 else 511 (* guards only occur for Ocaml *) 512 add_string (" when") >> add_break (1,0) >> pp 7 guard) >> 513 add_string (if !emitOcaml then " ->" else " =>") >> 514 add_break (1,0) >> 515 pp 7 rhs 516 ) 517 and pp_record i (ty,flds) = 518 pp_open_comb i (hd(TypeBase.constructors_of ty), map snd flds) 519 and pp_fail i tm = 520 let val (f,s,args) = combinSyntax.dest_fail tm 521 val fname = fst(dest_const f) 522 in 523 block CONSISTENT 3 ( 524 add_string "raise (" >> 525 add_string (if !emitOcaml then "Failure" else "Fail") >> 526 add_break (1,0) >> 527 add_string (Lib.quote (fname^": "^s)^")") 528 ) 529 end 530 and pp_arb i = 531 lparen i maxprec >> 532 B 3 ( 533 add_string 534 (if !emitOcaml then "raise (Failure \"ARB\")" 535 else "raise Fail \"ARB\"") 536 ) >> 537 rparen i maxprec 538 and pp_itself tm = 539 let fun skip1 s = String.extract(s, 1, NONE) 540 fun num_type typ = 541 let val pp_n = !type_pp.pp_num_types 542 val _ = type_pp.pp_num_types := true 543 in 544 skip1 (Hol_pp.type_to_string typ) before 545 type_pp.pp_num_types := pp_n 546 end 547 fun itself x = 548 block INCONSISTENT 2 ( 549 add_string "(" >> 550 add_string 551 (pick_name openthys "fcp" ("ITSELF", fcpML ^ "ITSELF")) >> 552 add_break (1,0) >> 553 pp_num_from_string x >> 554 add_string ")" 555 ) 556 fun pp_itself_type typ = 557 if is_vartype typ then 558 add_string (skip1 (dest_vartype typ)) 559 else 560 case (dest_type typ) of 561 ("one", []) => itself "1" 562 | ("num", []) => itself "1" 563 | ("int", []) => itself "1" 564 | ("list", [a]) => itself "1" 565 | ("bool", []) => itself "2" 566 | ("bit0", [a]) => itself (num_type typ) 567 | ("bit1", [a]) => itself (num_type typ) 568 | ("string", []) => itself "1" 569 | (tyop, [a, b]) => 570 block INCONSISTENT 0 ( 571 add_string ( 572 "(" ^ 573 pick_name openthys "fcp" 574 (case tyop of 575 "sum" => (fix "SUMi", fcpML ^ fix "SUMi") 576 | "prod" => (fix "MULi", fcpML ^ fix "MULi") 577 | "cart" => (fix "EXPi", fcpML ^ fix "EXPi") 578 | _ => raise ERR "term_to_ML" "pp_itself") ^ 579 "(") >> 580 block INCONSISTENT 0 ( 581 pp_itself_type a >> 582 add_string ", " >> 583 add_break (0,0) >> 584 pp_itself_type b 585 ) >> add_string "))" 586 ) 587 | _ => raise ERR "term_to_ML" "pp_itself" 588 in 589 (pp_itself_type o hd o snd o dest_type o type_of) tm 590 end 591 592 and pp_var tm = let val s = fst(dest_var tm) 593 val c = String.sub(s,0) 594 in 595 if c = #"^" then 596 add_string (fix_reserved (String.extract(s,1,NONE))) 597 else if c = #"_" then 598 add_string "_" 599 else if !emitOcaml andalso Char.isUpper c then 600 add_string ("_" ^ s) 601 else 602 add_string (fix_reserved s) 603 end 604 and pp_const i tm = 605 if same_const tm boolSyntax.conjunction 606 then pp_abs i andalso_tm else 607 if same_const tm boolSyntax.disjunction 608 then pp_abs i orelse_tm 609 else add_string (const_map tm) 610 and pp_one tm = add_string "()" 611 and pp_nil tm = add_string "[]" 612 and pp_open_comb i (f,args) = 613 let val constrname = 614 case Lib.total ConstMapML.apply f of 615 SOME (true,_,nm,_) => SOME nm 616 | _ => NONE 617 in B 0( 618 lparen i maxprec >> 619 (if TypeBase.is_constructor f andalso isSome constrname 620 orelse is_fake_constructor f 621 then 622 let 623 val fname = case constrname of 624 SOME s => s 625 | _ => fst(dest_record_vconstr f) 626 in 627 (* instead of: pp maxprec f; *) 628 add_string (fix_name ("", true, fname)) >> 629 add_string "(" >> 630 block INCONSISTENT 1 ( 631 pr_list (pp minprec) 632 (add_string "," >> add_break(0,0)) args 633 ) >> 634 add_string ")" 635 end 636 else 637 block INCONSISTENT 2 ( 638 pr_list (pp maxprec) (add_break(1,0)) (f::args) 639 )) >> 640 rparen i maxprec 641 ) 642 end 643 and pp_comb i tm = 644 let val (h,args) = strip_comb tm 645 val (argtys,target) = strip_fun(generic_type_of h) 646 in if length argtys < length args 647 then let val (app,rst) = split_after (length argtys) args 648 in 649 lparen i maxprec >> 650 pp maxprec (list_mk_comb(h,app)) >> 651 add_break (1,0) >> 652 pr_list (pp maxprec) (add_break(1,0)) rst >> 653 rparen i maxprec 654 end 655 else pp_open_comb i (h,args) 656 end 657 and pp_abs i tm = 658 let val (vstruct,body) = pairSyntax.dest_pabs tm 659 in lparen i (if !emitOcaml then minprec else 5000) 660 >> add_string (if !emitOcaml then "function" else "fn") 661 >> add_break (1,0) 662 >> pp 50 vstruct 663 >> add_break (1,0) 664 >> add_string (if !emitOcaml then "->" else "=>") 665 >> add_break (1,0) 666 >> pp minprec body 667 >> rparen i (if !emitOcaml then minprec else 5000) 668 end 669 670 in fn i => fn M => block INCONSISTENT 0 (pp i M) 671 end; 672 673fun pp_term_as_ML openthys side M = term_to_ML openthys side minprec M; 674 675fun same_fn eq1 eq2 = 676 same_const (fst(strip_comb(lhs eq1))) (fst(strip_comb(lhs eq2))); 677 678(*---------------------------------------------------------------------------*) 679(* Print a function definition as ML, i.e., fun f ... = ... *) 680(*---------------------------------------------------------------------------*) 681 682fun partitions P [] = [] 683 | partitions P (h::t) = 684 case partition (P h) t 685 of (L1,L2) => (h::L1) :: partitions P L2; 686 687fun pp_defn_as_ML openthys = 688 let open Portable PP smpp 689 val toML = term_to_ML openthys 690 fun pp_clause i eq = 691 let val (L,R) = dest_eq eq 692 in 693 block INCONSISTENT 2 ( 694 toML LEFT minprec L >> add_break(1,0) >> add_string "=" >> 695 add_break(1,0) >> 696 toML RIGHT i R 697 ) 698 end 699 fun pp_clauses (s,els) = 700 let val s' = if is_fn_app(lhs(hd els)) then s else "val" 701 in B 2 ( 702 add_string (s'^" ") >> 703 pp_clause (if length els = 1 then minprec else 100) (hd els) >> 704 add_newline >> 705 (case tl els of 706 [] => nothing 707 | els' => 708 pr_list (fn c => (add_string "| " >> pp_clause 100 c)) 709 add_newline els' >> 710 add_newline) 711 ) 712 end 713 fun pp tm = 714 let val eqns = map (snd o strip_forall) 715 (strip_conj (snd (strip_forall tm))) 716 val clauses = partitions same_fn eqns (* term list list *) 717 val clauses' = ("fun",hd clauses)::map (pair "and") (tl clauses) 718 in 719 B 0 (pr_list pp_clauses add_newline clauses') 720 end 721 in 722 pp 723 end; 724 725fun pp_defn_as_OCAML openthys = 726 let open Portable PP smpp 727 val const_map = const_map openthys 728 val toML = term_to_ML openthys 729 fun pp_clause i eq = 730 let val (L,R) = dest_eq eq 731 in block INCONSISTENT 2 ( 732 toML LEFT minprec L >> 733 add_break(1,0) >> 734 add_string "=" >> 735 add_break(1,0) >> 736 toML RIGHT i R 737 ) 738 end 739 fun pp_pattern i s (L,R) = 740 block INCONSISTENT 0 ( 741 add_string (fix_reserved s) >> 742 block INCONSISTENT 2 ( 743 block INCONSISTENT 0 ( 744 pr_list (toML LEFT minprec) (add_string "," >> add_break(0,0)) L 745 ) >> 746 add_string " ->" >> 747 add_break(1,0) >> 748 toML RIGHT i R 749 ) >> 750 add_newline 751 ) 752 fun caml_strip_comb t = let 753 val (t1, t2) = listSyntax.dest_mem t 754 in 755 (full_name openthys (false, "list", "MEM", bool), [t1, t2]) 756 end handle _ => apfst const_map (strip_comb t) 757 fun clauses_to_patterns els = map (((snd o caml_strip_comb)##I) o dest_eq) els 758 fun pp_clauses (s,els) = 759 block INCONSISTENT 2 ( 760 add_string (s^" ") >> 761 (if length els = 1 then 762 pp_clause minprec (hd els) >> add_newline 763 else 764 let 765 val (fname, args) = caml_strip_comb (lhs (hd els)) 766 val vs = vars_of_types (map type_of args) 767 val pats = clauses_to_patterns els 768 in 769 add_string fname >> add_break(1,0) >> 770 pr_list (toML LEFT minprec) (add_break(1,0)) vs >> 771 add_break(1,0) >> 772 add_string "=" >> 773 add_break(1,0) >> 774 add_string "match " >> 775 block INCONSISTENT 0 ( 776 pr_list (toML LEFT minprec) 777 (add_string "," >> add_break(0,0)) 778 vs 779 ) >> 780 add_string " with" >> 781 add_break(1,0) >> 782 block INCONSISTENT 0 ( 783 pp_pattern 100 " " (hd pats) >> 784 (case tl pats of 785 [] => nothing 786 | pats' => 787 pr_list (pp_pattern 100 "| ") nothing pats') 788 ) 789 end) 790 ) 791 fun contains_const c t = can (find_term (same_const c)) t; 792 fun contains_consts l t = 793 isSome (List.find (fn c => contains_const c t) l); 794 fun pp tm = 795 let val eqns = map (snd o strip_forall) 796 (strip_conj (snd (strip_forall tm))) 797 val clauses = partitions same_fn eqns (* term list list *) 798 val rhsides = map rhs eqns 799 val lhsides = eqns |> map lhs |> filter is_fn_app 800 |> map (fst o strip_comb) 801 |> filter (not o same_const IN_tm) 802 val possibly_recursive = 803 isSome (List.find (contains_consts lhsides) rhsides) 804 val s = if possibly_recursive then "let rec" else "let" 805 val clauses' = (s,hd clauses)::map (pair "and") (tl clauses) 806 in B 0 (pr_list pp_clauses add_newline clauses') 807 end 808 in 809 pp 810 end; 811 812(*---------------------------------------------------------------------------*) 813(* Now print datatype declarations in ML. First tweak the existing type *) 814(* prettyprinter so it generates syntactically correct ML types *) 815(*---------------------------------------------------------------------------*) 816 817fun adjust_tygram tygram = 818 let open type_grammar HOLgrammars 819 val g0 = List.foldl (fn (s,g) => remove_binary_tyop g s) 820 tygram 821 ["+", "#", "|->", "**"] 822 in 823 new_binary_tyop g0 {precedence = 70, infix_form = "*", 824 opname = "prod", associativity = NONASSOC} 825 end; 826 827fun prim_pp_type_as_ML tygram ppstrm = 828 trace ("Greek tyvars",0) 829 (type_pp.pp_type (adjust_tygram tygram) PPBackEnd.raw_terminal ppstrm) 830 831fun pp_type_as_ML ppstrm = prim_pp_type_as_ML (Parse.type_grammar()) ppstrm; 832 833(*---------------------------------------------------------------------------*) 834(* Elements of a theory presentation. *) 835(*---------------------------------------------------------------------------*) 836 837datatype elem 838 = DEFN of thm 839 | DEFN_NOSIG of thm 840 | DATATYPE of hol_type quotation 841 | EQDATATYPE of string list * hol_type quotation 842 | ABSDATATYPE of string list * hol_type quotation 843 | OPEN of string list 844 | MLSIG of string 845 | MLSTRUCT of string; 846 847(*---------------------------------------------------------------------------*) 848(* Internal version of elem (nearly identical, except that datatype *) 849(* declarations have been parsed) and some standard definitions from *) 850(* datatypes (e.g. size functions) and record types (accessor and field *) 851(* update functions) are automatically added. *) 852(*---------------------------------------------------------------------------*) 853 854datatype elem_internal 855 = iDEFN of thm 856 | iDEFN_NOSIG of thm 857 | iDATATYPE of ParseDatatype.AST list 858 | iEQDATATYPE of string list * ParseDatatype.AST list 859 | iABSDATATYPE of string list * ParseDatatype.AST list 860 | iOPEN of string list 861 | iMLSIG of string 862 | iMLSTRUCT of string; 863 864 865(* ---------------------------------------------------------------------- 866 A datatype declaration results in some extra HOL function 867 definitions being automatically made. These are, usually, 868 invisible to the user, but are important and usually need to have 869 ML generated for them. Currently, only the access and update 870 functions for records are generated. We used to also write out the 871 size functions for datatypes as well, but they were not used, so 872 they are going for the time being. In many cases suitable update 873 and access functions are defined by the datatype package and stuck 874 into the TypeBase. All record declarations are handled by the 875 following code, which generates "fake" theorems as definitions for 876 the various constants. 877 ---------------------------------------------------------------------- *) 878 879fun diag vlist flist = tl 880 (itlist2 (fn v => fn f => fn A => 881 case A of [] => [[v],[f v]] 882 | h::t => (v::h) :: (f v::h) :: map (cons v) t) 883 vlist flist []); 884 885fun gen_updates ty (fields : (string * TypeBase.rcd_fieldinfo) list) = 886 let open pairSyntax 887 val {Tyop,Thy,Args} = dest_thy_type ty 888 fun mk_upd_const (fname,{fupd,...}) = fupd 889 val upds = map mk_upd_const fields 890 val fns = map (fn upd_t => mk_var ("f", #1(dom_rng (type_of upd_t)))) upds 891 val fake_tyc = 892 mk_record_vconstr(Tyop,list_mk_fun(map (#ty o snd) fields, ty)) 893 val vars = itlist 894 (fn (n,(_,{ty,...})) => fn acc => 895 mk_var("v"^int_to_string n,ty) :: acc) 896 (enumerate 1 fields) [] 897 val pat = list_mk_comb(fake_tyc,vars) 898 val lefts = map2 (fn upd => fn f => list_mk_comb(upd,[f,pat])) upds fns 899 val diags = diag vars (map (curry mk_comb) fns) 900 fun mapthis (l, d) = let 901 val rtys = map type_of d 902 val rtyc = mk_record_vconstr(Tyop, list_mk_fun(rtys, type_of l)) 903 in 904 mk_eq(l, list_mk_comb(rtyc, d)) 905 end 906 val eqns = ListPair.map mapthis (lefts, diags) 907 val mk_thm = mk_oracle_thm "EmitML fake thm" 908 in 909 map (curry mk_thm []) eqns 910 end 911 handle e => raise wrap_exn "EmitML" "gen_updates" e; 912 913fun gen_accesses ty (fields : (string * TypeBase.rcd_fieldinfo) list) = 914 let open pairSyntax 915 val {Tyop,Thy,Args} = dest_thy_type ty 916 fun mk_proj_const (fname,{accessor,...}) = accessor 917 val projs = map mk_proj_const fields 918 val fake_tyc = 919 mk_record_vconstr(Tyop,list_mk_fun(map (#ty o snd) fields, ty)) 920 val vars = itlist 921 (fn (n,(_,{ty,...})) => fn acc => 922 mk_var("v"^int_to_string n,ty) :: acc) 923 (enumerate 1 fields) [] 924 val pat = list_mk_comb(fake_tyc,vars) 925 val lefts = map (fn proj => mk_comb(proj,pat)) projs 926 val eqns = rev(map2 (curry mk_eq) lefts vars) 927 val mk_thm = mk_oracle_thm "EmitML fake thm" 928 in 929 map (curry mk_thm []) eqns 930 end 931 handle e => raise wrap_exn "EmitML" "gen_accesses" e; 932 933fun datatype_silent_defs tyAST = 934 let val tyop = hd (map fst tyAST) 935 val tyrecd = hd (Type.decls tyop) 936 in 937 if tyop = "num" then [] else 938 case TypeBase.read tyrecd 939 of NONE => (WARN "datatype_silent_defs" 940 ("No info in the TypeBase for "^Lib.quote tyop); []) 941 | SOME tyinfo => 942 let open TypeBasePure 943 val size_def = [] (* [snd (valOf(size_of tyinfo))] handle _ => [] *) 944 val (updates_defs, access_defs) = 945 case fields_of tyinfo (* test for record type *) 946 of [] => ([],[]) 947 | fields => let val ty = ty_of tyinfo 948 in (gen_updates ty fields, gen_accesses ty fields) 949 end 950 in 951 map (iDEFN o !reshape_thm_hook) 952 (size_def @ updates_defs @ access_defs) 953 end 954 end; 955 956(*---------------------------------------------------------------------------*) 957(* Map from external presentation to internal *) 958(*---------------------------------------------------------------------------*) 959 960(* Ocaml won't accept capitalized types *) 961(* Adds abbreviations with lowercase first letters *) 962 963fun ocaml_type_abbrevs decls = 964let 965 val type_names = map fst decls 966 val candidate_tyis = 967 TypeBasePure.get (TypeBase.theTypeBase()) (hd type_names) 968 val newtypes = if null candidate_tyis then [] else 969 Prim_rec.doms_of_tyaxiom 970 (TypeBasePure.axiom_of (hd candidate_tyis)) 971 fun do_abbrev(name, typ) = 972 if Char.isUpper (String.sub(name,0)) then 973 Parse.temp_type_abbrev(lowerize name, typ) 974 else 975 () 976in 977 if length type_names = length newtypes then 978 app do_abbrev (zip type_names newtypes) 979 else 980 () 981end; 982 983local 984 open ParseDatatype 985 fun cmk s = {name = s, terms = Term.decls s} 986 fun rmk s = 987 {name = s, terms = Term.decls (RecordType.mk_recordtype_constructor s)} 988in 989fun constructors decls = 990 case decls of 991 [] => [] 992 | (s, Constructors clist) :: rst => map (cmk o #1) clist @ constructors rst 993 | (s,Record flds)::rst => rmk s :: constructors rst 994 995fun constrl [] = [] 996 | constrl ((s,Constructors clist)::rst) = (s,clist)::constrl rst 997 | constrl ((s,Record flds)::rst) = 998 (s, [(RecordType.mk_recordtype_constructor s,map snd flds)])::constrl rst 999end; 1000 1001 1002 1003 1004 1005fun elemi (DEFN th) (cs,il) = (cs,iDEFN (!reshape_thm_hook th) :: il) 1006 | elemi (DEFN_NOSIG th) (cs,il) = (cs,iDEFN_NOSIG (!reshape_thm_hook th)::il) 1007 | elemi (DATATYPE q) (cs,il) = 1008 let val tyAST = ParseDatatype.hparse (type_grammar()) q 1009 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1010 val defs = datatype_silent_defs tyAST 1011 in (cs, defs @ (iDATATYPE tyAST :: il)) 1012 end 1013 | elemi (EQDATATYPE(sl,q)) (cs,il) = 1014 let val tyAST = ParseDatatype.hparse (type_grammar()) q 1015 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1016 val defs = datatype_silent_defs tyAST 1017 in (cs,defs @ (iEQDATATYPE(sl,tyAST) :: il)) 1018 end 1019 | elemi (ABSDATATYPE(sl,q)) (cs,il) = (* build rewrites for pseudo constrs *) 1020 let open ParseDatatype 1021 val tyAST = hparse (type_grammar()) q 1022 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1023 val pconstrs = constrl tyAST 1024 val constr_names = flatten(map (map fst o snd) pconstrs) 1025 val constr_arities = flatten(map (map (length o snd) o snd) pconstrs) 1026 val constrs = map (hd o Term.decls) constr_names 1027 val constrs' = zip constrs constr_arities 1028 fun is_multi (_,n) = n >= 2 1029 val mconstrs = filter is_multi constrs' 1030 val _ = List.app new_pseudo_constr mconstrs 1031 (* val _ = schedule this call for exported theory *) 1032 in 1033 (mconstrs@cs, iABSDATATYPE(sl,tyAST) :: il) 1034 end 1035 | elemi (OPEN sl) (cs,il) = (cs,iOPEN sl :: il) 1036 | elemi (MLSIG s) (cs,il) = (cs,iMLSIG s :: il) 1037 | elemi (MLSTRUCT s) (cs,il) = (cs,iMLSTRUCT s :: il); 1038 1039fun internalize elems = 1040 let val (cs, ielems) = rev_itlist elemi elems ([],[]) 1041 in (rev cs, rev ielems) 1042 end; 1043 1044local open ParseDatatype 1045fun replace f (v as dVartype _) = v 1046 | replace f (aq as dAQ _) = aq 1047 | replace f (dTyop{Tyop,Thy,Args}) = 1048 f Tyop handle _ => dTyop{Tyop=Tyop,Thy=Thy,Args=map (replace f) Args} 1049in 1050fun replaceForm f (Constructors alist) = 1051 Constructors (map (I##map (replace f)) alist) 1052 | replaceForm f other = other 1053 1054fun pretype_of ty = 1055 dVartype(dest_vartype ty) 1056 handle _ => 1057 let val (s,args) = dest_type ty 1058 in dTyop{Tyop=s,Thy=NONE,Args=map pretype_of args} 1059 end 1060end; 1061 1062(*---------------------------------------------------------------------------*) 1063(* Initially, datatype descriptions do not have arguments to the type *) 1064(* operators being defined. This function finds out what they should be *) 1065(* and substitutes them through the rhs of the datatype declaration. *) 1066(* The DATATYPE description requires looking info up in the type base, in *) 1067(* order to see what order multiple type variables should be in. The *) 1068(* EQDATATYPE clause expects the type variables to be given in the correct *) 1069(* order in the first argument. *) 1070(*---------------------------------------------------------------------------*) 1071 1072fun repair_type_decls (iDATATYPE decls) = 1073 let val type_names = map fst decls 1074 val candidate_tyis = 1075 TypeBasePure.get (TypeBase.theTypeBase()) (hd type_names) 1076 val tyax = TypeBasePure.axiom_of (hd candidate_tyis) 1077 val newtypes = Prim_rec.doms_of_tyaxiom tyax 1078 val tyvars = map dest_vartype (snd (dest_type (hd newtypes))) 1079 val alist = map (fn x => (fst(dest_type x),pretype_of x)) newtypes 1080 fun alist_fn name = snd (valOf (assoc1 name alist)) 1081 in 1082 (tyvars, map (I##replaceForm alist_fn) decls) 1083 end 1084 | repair_type_decls (iEQDATATYPE (tyvars,decls)) = 1085 let open ParseDatatype 1086 val tyvarsl = map dVartype tyvars 1087 val tynames = map fst decls 1088 val newtypes = map (fn s => dTyop{Tyop=s,Thy=NONE,Args=tyvarsl}) tynames 1089 val alist = zip tynames newtypes 1090 fun alist_fn name = snd (valOf (assoc1 name alist)) 1091 in 1092 (tyvars, map (I##replaceForm alist_fn) decls) 1093 end 1094 | repair_type_decls (iABSDATATYPE stuff) = repair_type_decls (iEQDATATYPE stuff) 1095 | repair_type_decls arg = raise ERR "repair_type_decls" "unexpected input"; 1096 1097fun pp_datatype_as_ML (tyvars,decls) = 1098 let open Portable ParseDatatype PP smpp 1099 val fix_cons = fix_reserved o capitalize 1100 val fix_type = fix_reserved o lowerize 1101 val ppty = pp_type_as_ML 1102 fun pp_comp_ty ty = 1103 if Lib.can dom_rng ty orelse is_pair_type ty 1104 then (add_string "(" >> ppty ty >> add_string")") 1105 else ppty ty 1106 fun pp_tyl tyl = 1107 block INCONSISTENT 0 ( 1108 pr_list pp_comp_ty (add_string" *" >> add_break(1,0)) tyl 1109 ) 1110 fun pp_tyvars [] = nothing 1111 | pp_tyvars [v] = add_string v >> add_break(1,0) 1112 | pp_tyvars vlist = 1113 B 1 ( 1114 add_string"(" >> 1115 pr_list add_string (add_string",") vlist >> 1116 add_string")" 1117 ) 1118 fun pp_clause r clause = 1119 (if !r then (r := false; add_string "= ") else add_string "| ") >> 1120 (case clause of 1121 (con,[]) => add_string (fix_cons con) 1122 | (con,args) => 1123 block INCONSISTENT 0 ( 1124 B 0 (add_string (fix_cons con) >> add_string " of ") >> 1125 pp_tyl (map ParseDatatype.pretypeToType args) 1126 ) 1127 ) 1128 fun pp_decl (tyvars,r) (name,Constructors clauselist) = 1129 B 5 ( 1130 B 0 ( 1131 (if !r then 1132 (r := false; 1133 add_string (if !emitOcaml then "type" else "datatype")) 1134 else 1135 nothing) >> 1136 add_break(1,0) >> pp_tyvars tyvars >> add_string (fix_type name) 1137 ) >> add_break(1,0) >> 1138 B 0 ( 1139 pr_list (pp_clause (ref true)) (add_break(1,0)) clauselist 1140 ) 1141 ) 1142 | pp_decl (tyvars,_) (name,Record flist) = 1143 let open ParseDatatype 1144 val fields = map (I##pretypeToType) flist 1145 in 1146 B 0 ( 1147 add_string (if !emitOcaml then "type" else "datatype") >> 1148 add_break(1,0) >> 1149 pp_tyvars tyvars >> 1150 add_string(fix_type name^" = ") >> 1151 add_string(fix_cons name^" of ") >> 1152 pp_tyl (map snd fields) 1153 ) 1154 end 1155 in 1156 B 0 ( 1157 pr_list (pp_decl (tyvars,ref true)) 1158 (add_newline >> add_string "and" >> add_newline) 1159 decls 1160 ) 1161 end; 1162 1163(*---------------------------------------------------------------------------*) 1164(* Get the name of all constants introduced by the definition. Probably *) 1165(* won't work in general for constant specifications. *) 1166(*---------------------------------------------------------------------------*) 1167 1168fun consts_of_def thm = 1169 let val eqns = strip_conj (snd (strip_forall (concl thm))) 1170 val allCs = map (fst o strip_comb o lhs o snd o strip_forall) eqns 1171 in op_mk_set same_const allCs 1172 end; 1173 1174fun original_type name ty = 1175let val l = size name 1176 val s = if String.sub(name,0) = #" " andalso String.sub(name,l - 1) = #" " 1177 then String.substring(name,1,l - 2) 1178 else name 1179 val d = decls s 1180 handle Option => raise ERR "original_type" 1181 ("Cannot find " ^ quote name ^ Hol_pp.type_to_string ty) 1182 val tm = valOf (List.find (fn t => can (match_type ty) (type_of t)) d) 1183in 1184 type_of tm 1185end; 1186 1187fun pp_sig (s,elems) = 1188 let open Portable PP smpp 1189 val ppty = pp_type_as_ML 1190 val pp_datatype = pp_datatype_as_ML 1191 fun pp_eqdatatype b (tyvars,astl) = 1192 let val tynames = map fst astl 1193 val tys = map (fn s => (tyvars,s)) tynames 1194 fun pp_tydec (tyvars,s) = 1195 B 0 ( 1196 add_string (if b andalso not (!emitOcaml) 1197 then "eqtype " else "type ") >> 1198 (if null tyvars then add_string s 1199 else if List.length tyvars = 1 then 1200 add_string (hd tyvars) >> add_string(" "^s) 1201 else 1202 add_string "(" >> 1203 pr_list add_string (add_string",") tyvars >> 1204 add_string(") "^s)) 1205 ) 1206 in 1207 block CONSISTENT 0 ( 1208 pr_list pp_tydec add_newline (map (pair tyvars) tynames) 1209 ) 1210 end 1211 fun pp_valdec c = 1212 let val (is_type_cons,_,name,ty) = ConstMapML.apply c 1213 val ty = if !emitOcaml then original_type name ty else ty 1214 in 1215 B 3 ( 1216 add_string "val " >> 1217 add_string (fix_name ("",is_type_cons,name)) >> add_break(1,0) >> 1218 add_string ": " >> ppty ty 1219 ) 1220 end 1221 fun pp_el (iDATATYPE astl) = pp_datatype (repair_type_decls (iDATATYPE astl)) 1222 | pp_el (iEQDATATYPE (tyvarsl,astl)) = pp_eqdatatype true (tyvarsl,astl) 1223 | pp_el (iABSDATATYPE (tyvarsl,astl)) = pp_eqdatatype false (tyvarsl,astl) 1224 | pp_el (iDEFN thm) = 1225 pr_list pp_valdec add_newline (consts_of_def thm) 1226 | pp_el (iMLSIG s) = add_string s 1227 | pp_el (iDEFN_NOSIG thm) = nothing 1228 | pp_el (iMLSTRUCT s) = nothing 1229 | pp_el (iOPEN slist) = nothing 1230 in 1231 B 0 ( 1232 add_string ((if !emitOcaml then "module type " else "signature ") ^ 1233 ML s ^ " =") >> 1234 add_newline >> 1235 B 2 ( 1236 add_string "sig" >> add_newline >> 1237 B 0 ( 1238 pr_list pp_el add_newline 1239 (filter (fn (iDEFN_NOSIG _) => false 1240 | (iOPEN _) => false 1241 | (iMLSTRUCT _) => false 1242 | otherwise => true) elems) 1243 ) 1244 ) >> 1245 add_newline >> 1246 add_string "end" >> add_newline 1247 ) 1248 end 1249 handle e => raise wrap_exn "EmitML" "pp_sig" e; 1250 1251val MLinfixes = 1252 String.fields Char.isSpace "* / div mod + - ^ @ <> > < >= <= := o before"; 1253 1254fun pp_struct (s,elems,cnames) = 1255 let open Portable PP smpp 1256 val openthys = ref [] 1257 fun opens() = !openthys 1258 val pp_datatype = pp_datatype_as_ML 1259 fun pp_el (iDATATYPE astl) = pp_datatype (repair_type_decls (iDATATYPE astl)) 1260 | pp_el (iEQDATATYPE (tyvarsl,astl)) = 1261 pp_datatype (repair_type_decls (iEQDATATYPE(tyvarsl,astl))) 1262 | pp_el (iABSDATATYPE (tyvarsl,astl)) = 1263 pp_datatype (repair_type_decls (iABSDATATYPE(tyvarsl,astl))) 1264 | pp_el (iDEFN thm) = 1265 (if !emitOcaml then pp_defn_as_OCAML else pp_defn_as_ML) 1266 (s::opens()) 1267 (concl thm) 1268 | pp_el (iDEFN_NOSIG thm) = pp_el (iDEFN thm) 1269 | pp_el (iMLSIG s) = nothing 1270 | pp_el (iMLSTRUCT s) = add_string s >> add_newline 1271 | pp_el (iOPEN slist) = (openthys := union slist (!openthys); 1272 B 0 ( 1273 pr_list 1274 (add_string o curry String.^ "open " o ML) 1275 add_newline slist >> 1276 add_newline 1277 )) 1278 val (struct_mod, punct) = if !emitOcaml then 1279 ("module ", " : ") 1280 else 1281 ("structure ", " :> ") 1282 in 1283 block CONSISTENT 0 ( 1284 add_string (struct_mod ^ ML s ^ punct ^ ML s ^ " =") >> 1285 add_newline >> 1286 block CONSISTENT 2 ( 1287 add_string "struct" >> add_newline >> 1288 block CONSISTENT 0 ( 1289 (if !emitOcaml then nothing 1290 else 1291 block INCONSISTENT 7 ( 1292 add_string"nonfix " >> 1293 pr_list add_string (add_break(1,0)) (union cnames MLinfixes) >> 1294 add_string ";" 1295 ) >> add_newline) >> 1296 add_newline >> 1297 pr_list pp_el add_newline 1298 (filter (fn (iMLSIG _) => false | otherwise => true) elems) 1299 ) 1300 ) >> add_newline >> 1301 add_string"end" >> add_newline 1302 ) 1303 end 1304 handle e => raise wrap_exn "EmitML" "pp_struct" e; 1305 1306 1307(*---------------------------------------------------------------------------*) 1308(* Dealing with eqtypes. When a HOL function uses equality on the rhs, the *) 1309(* type of the function does not reflect this. However, in ML, eqtypes *) 1310(* are used to signal this. The compiler generates code for the equality *) 1311(* test in that case. So we need to take a HOL definition and compute an ML *) 1312(* type for it, which can include eqtypes. The strategy taken is to search *) 1313(* the rhs for any constants whose generic type has eqtype constraints on *) 1314(* some type variables. By matching the generic constant against the instance*) 1315(* we can find if any eqtype variables are bound to polymorphic types. If so,*) 1316(* the type variables in the polymorphic type get the eqtype attribute. *) 1317(*---------------------------------------------------------------------------*) 1318 1319fun is_eqtyvar ty = 1320 (case String.explode (dest_vartype ty) 1321 of #"'" :: #"'" ::rst => true 1322 | otherwise => false) 1323 handle HOL_ERR _ => raise ERR "is_eqtyvar" "not a type variable"; 1324 1325fun tyvar_to_eqtyvar ty = 1326 let val tyname = dest_vartype ty 1327 in 1328 case String.explode tyname 1329 of #"'" :: #"'" :: _ => raise ERR "tyvar_to_eqtyvar" "already an eqtyvar" 1330 | #"'" :: _ => with_flag (Feedback.emit_WARNING,false) 1331 mk_vartype ("'"^tyname) 1332 | otherwise => raise ERR "tyvar_to_eqtyvar" "unexpected syntax" 1333 end; 1334 1335fun const_eqtyvars genty c2 = 1336 let val bindings = match_type genty (type_of c2) 1337 val bindings' = Lib.filter (is_eqtyvar o #redex) bindings 1338 val bindings'' = Lib.filter (polymorphic o #residue) bindings' 1339 in 1340 Type.type_varsl (map #residue bindings'') 1341 end; 1342 1343fun generic_const thy name = Term.prim_mk_const{Thy=thy,Name=name}; 1344 1345(*---------------------------------------------------------------------------*) 1346(* Gets possibly eq-style type from const map. *) 1347(*---------------------------------------------------------------------------*) 1348 1349fun generic_type c = 1350 #4 (ConstMapML.apply c) handle HOL_ERR _ => type_of c; 1351 1352fun term_eqtyvars tm = 1353 case dest_term tm 1354 of CONST _ => const_eqtyvars (generic_type tm) tm 1355 | VAR _ => [] 1356 | COMB(t1,t2) => union (term_eqtyvars t1) (term_eqtyvars t2) 1357 | LAMB(_,tm) => term_eqtyvars tm; 1358 1359(*---------------------------------------------------------------------------*) 1360(* Translate the type of a defined constant to reflect any uses of equality *) 1361(* in the body of the definition. *) 1362(*---------------------------------------------------------------------------*) 1363 1364fun munge_def_type def = 1365 let val (L,R) = unzip (map (dest_eq o snd o strip_forall) 1366 (strip_conj (snd (strip_forall (concl def))))) 1367 val clist = op_mk_set same_const (map (fst o strip_comb) L) 1368 val tainted = U (map term_eqtyvars R) 1369 val theta = map (fn tyv => tyv |-> tyvar_to_eqtyvar tyv) tainted 1370 in 1371 map (inst theta) clist 1372 end 1373 handle e => raise wrap_exn "EmitML" "munge_def_type" e; 1374 1375(*---------------------------------------------------------------------------*) 1376(* Get the newly introduced constants out of a list of function definitions *) 1377(* and datatype definitions. We have to be aware that a constant may have *) 1378(* been defined in an ancestor theory. *) 1379(*---------------------------------------------------------------------------*) 1380 1381fun add (is_constr, s) {name, terms} = let 1382 fun perterm c = 1383 case ConstMapML.exact_peek c of 1384 NONE => ConstMapML.prim_insert(c, (is_constr, s, name, type_of c)) 1385 | SOME _ => () 1386in 1387 List.app perterm terms 1388end 1389 1390fun install_consts _ [] k = k ([], []) 1391 | install_consts s (iDEFN_NOSIG thm::rst) k = install_consts s (iDEFN thm::rst) k 1392 | install_consts s (iDEFN thm::rst) k = 1393 let val clist0 = munge_def_type thm 1394 val clist = 1395 (* IN is only allowed to be defined in the setML module/structure; 1396 due to the special-case of MEM, listML may appear to define it too 1397 *) 1398 if s <> "set" then filter (not o same_const IN_tm) clist0 1399 else clist0 1400 val _ = List.app 1401 (fn c => add (false, s) {name = nameOfC c, terms = [c]}) 1402 clist 1403 in 1404 install_consts s rst 1405 (fn (cs, nms) => k (clist @ cs, map nameOfC clist @ nms)) 1406 end 1407 | install_consts s (iDATATYPE ty::rst) k = 1408 let 1409 val constrs = constructors ty 1410 val allterms = op_U aconv (map #terms constrs) 1411 val _ = List.app (add (true, s)) constrs 1412 in 1413 install_consts s rst 1414 (fn (cs,nms) => k (allterms @ cs, map #name constrs @ nms)) 1415 end 1416 | install_consts s (iEQDATATYPE (tyvars,ty)::rst) k = 1417 let 1418 val constrs = constructors ty 1419 val allterms = op_U aconv (map #terms constrs) 1420 val _ = List.app (add (true, s)) constrs 1421 in 1422 install_consts s rst 1423 (fn (cs,nms) => k (allterms @ cs, map #name constrs @ nms)) 1424 end 1425 | install_consts s (iABSDATATYPE (tyvars,ty)::rst) k = 1426 install_consts s (iEQDATATYPE (tyvars,ty)::rst) k 1427 | install_consts s (other::rst) k = install_consts s rst k; 1428 1429 1430(*---------------------------------------------------------------------------*) 1431(* Append code to the theory file that will load the const map with the *) 1432(* definitions and datatype constructors exported as ML. *) 1433(*---------------------------------------------------------------------------*) 1434 1435fun emit_adjoin_call thy (consts,pcs) = let 1436 fun extern_pc (c,a) = 1437 let val {Thy=thy,Name=n,...} = dest_thy_const c 1438 val n' = mlquote n 1439 val thy' = mlquote thy 1440 in ("(prim_mk_const{Name="^n'^",Thy="^thy'^"},"^Int.toString a^")") 1441 end 1442 fun safetyprint ty = String.toString 1443 (trace ("Unicode",0) 1444 (HOLPP.pp_to_string 10000 1445 (Parse.mlower o 1446 type_pp.pp_type (fst Parse.min_grammars) 1447 PPBackEnd.raw_terminal)) 1448 ty) 1449 1450 fun pr3 ({Name,Thy,Ty}, (b,s2,ty)) = let 1451 open PP smpp 1452 val S = add_string 1453 val BB = block INCONSISTENT 0 1454 fun brk n = add_break (1,n) 1455 fun ppty ty = 1456 BB (S "typ" >> brk 0 >> S "\"" >> S (safetyprint Ty) >> S "\"") 1457 in 1458 S "(" >> BB ( 1459 S "{" >> BB ( 1460 BB (S "Name =" >> brk 0 >> S (mlquote Name ^ ",")) >> brk 0 >> 1461 BB (S "Thy =" >> brk 0 >> S (mlquote Thy ^",")) >> brk 0 >> 1462 BB (S "Ty =" >> brk 2 >> ppty Ty) 1463 ) >> S "}," >> brk 0 >> 1464 S "(" >> BB ( 1465 S (Bool.toString b ^ ",") >> brk 0 >> 1466 S (Lib.mlquote s2 ^ ",") >> brk 0 >> 1467 ppty ty 1468 ) >> S ")" 1469 ) >> S ")" 1470 end 1471 in 1472 Theory.adjoin_to_theory 1473 {sig_ps = NONE, 1474 struct_ps = SOME (fn _ => 1475 let open PP 1476 val S = add_string 1477 val BR = add_break 1478 val B = PP.block PP.CONSISTENT 0 1479 fun getdata c = let 1480 val (b,pfx,s,ty) = ConstMapML.apply c 1481 in 1482 (b,s,ty) 1483 end 1484 in 1485 B ( 1486 [ 1487 S "val _ = ", NL, 1488 S " let open Parse", NL, 1489 S " fun doit (r,(b,s,ty)) = ", NL, 1490 S " let val c = Term.mk_thy_const r", NL, 1491 S (" in ConstMapML.prim_insert(c,(b,"^Lib.quote thy^",s,ty))"), 1492 NL, 1493 S " end", NL, 1494 S " fun typ s = Feedback.trace(\"Vartype Format Complaint\", 0)\n\ 1495 \ (#1 (parse_from_grammars min_grammars))\n\ 1496 \ [QUOTE (\":\"^s)]", NL, 1497 S " in", NL, 1498 S " List.app doit [", NL, 1499 S " ", 1500 block INCONSISTENT 0 ( 1501 pr_list (Parse.mlower o pr3) [S",", BR(1,0)] 1502 (map (fn c => (dest_thy_const c, getdata c)) consts) 1503 ), NL, 1504 S " ]", NL, 1505 S " end", NL, NL] @ 1506 (if null pcs then [] 1507 else [ 1508 S "val _ = List.app EmitML.new_pseudo_constr", NL, 1509 S " [", 1510 block INCONSISTENT 0 ( 1511 pr_list S [S",", BR(1,0)] (map extern_pc pcs) 1512 ), 1513 S"]", NL, NL 1514 ]) 1515 ) 1516 end)} 1517 handle e => raise ERR "emit_adjoin_call" "" 1518 end; 1519 1520(*---------------------------------------------------------------------------*) 1521(* Write the ML out to a signature and structure file. We first run over the *) 1522(* definitions and lift out the newly defined constants. These get inserted *) 1523(* into the "const map", which is accessed when prettyprinting the *) 1524(* definitions. We also have to detect eqtypes and ensure that the const map *) 1525(* is properly updated when the theory is loaded. *) 1526(*---------------------------------------------------------------------------*) 1527 1528fun emit_xML (Ocaml,sigSuffix,structSuffix) p (s,elems_0) = 1529 let val _ = emitOcaml := Ocaml 1530 val (pcs,elems) = internalize elems_0 (* pcs = pseudo-constrs *) 1531 val path = if p="" then FileSys.getDir() else p 1532 val pathPrefix = Path.concat(path, capitalize s) 1533 val sigfile = pathPrefix^ sigSuffix 1534 val structfile = pathPrefix^ structSuffix 1535 fun trydelete s = OS.FileSys.remove s handle OS.SysErr _ => () 1536 fun cleanFiles() = (trydelete sigfile; trydelete structfile) 1537 in 1538 let val sigStrm = TextIO.openOut sigfile 1539 val structStrm = TextIO.openOut structfile 1540 val out = curry TextIO.output 1541 val (consts, usednames) = install_consts s elems (fn x => x) 1542 in 1543 (PP.prettyPrint(out sigStrm, 75) (Parse.mlower (pp_sig (s,elems))); 1544 PP.prettyPrint(out structStrm, 75) 1545 (Parse.mlower (pp_struct (s,elems,usednames))); 1546 TextIO.closeOut sigStrm; 1547 TextIO.closeOut structStrm; 1548 HOL_MESG ("emitML: " ^ s ^ "{" ^ sigSuffix ^ "," ^ structSuffix ^ "}\n\ 1549 \ written to directory "^path); 1550 emit_adjoin_call s (consts,pcs) 1551 ) 1552 handle e => (List.app TextIO.closeOut [sigStrm, structStrm]; 1553 cleanFiles(); 1554 raise wrap_exn "EmitML" "emitML" e) 1555 end handle Io _ => 1556 raise mk_HOL_ERR "EmitML" "emitML" 1557 ("I/O error prevented exporting files to "^Lib.quote path) 1558 end 1559 1560val emit_xML = 1561 (fn info => fn p => fn stuff => 1562 Feedback.trace ("Unicode", 0) 1563 (emit_xML info p) 1564 stuff) 1565 1566val emitML = emit_xML (false,!sigSuffix,!structSuffix); 1567 1568val emitCAML = emit_xML (true,!sigCamlSuffix,!structCamlSuffix); 1569 1570fun eSML d l = with_flag (type_pp.pp_array_types, false) 1571 (emitML (!Globals.emitMLDir)) (d, l); 1572fun eCAML d l = with_flag (type_pp.pp_array_types, false) 1573 (emitCAML (!Globals.emitCAMLDir)) (d, l); 1574 1575fun MLSIGSTRUCT ll = 1576 foldr (fn (x,l) => MLSIG x :: MLSTRUCT x :: l) [] (ll @ [""]); 1577 1578val pp_datatype_as_ML = fn dty => Parse.mlower (pp_datatype_as_ML dty) 1579val pp_defn_as_ML = fn sl => Parse.mlower o pp_defn_as_ML sl 1580val pp_term_as_ML = fn sl => fn sd => Parse.mlower o pp_term_as_ML sl sd 1581val pp_type_as_ML = Parse.mlower o pp_type_as_ML 1582 1583end (* struct *) 1584