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 definitions *) 867(* being automatically made. These are, usually, invisible to the user, but *) 868(* are important and usually need to have ML generated for them. Currently, *) 869(* only the access and update functions for records are generated. We used *) 870(* to also write out the size functions for datatypes as well, but they were *) 871(* not used, so they are going for the time being. *) 872(* *) 873(* In many cases suitable update and access functions are defined by the *) 874(* datatype package and stuck into the TypeBase. However, large records are *) 875(* modelled differently, for efficiency. The threshold number of fields is *) 876(* controlled by Datatype.big_record_size. A big record has a different *) 877(* shape, i.e., recursion theorem. To handle such records, we generate *) 878(* fake "theorems" of the right form. This should be OK, as they are only *) 879(* created for exporting the ML functions, and they are tagged. In fact, all *) 880(* record declarations are handled by the following code. *) 881(*---------------------------------------------------------------------------*) 882 883fun diag vlist flist = tl 884 (itlist2 (fn v => fn f => fn A => 885 case A of [] => [[v],[f v]] 886 | h::t => (v::h) :: (f v::h) :: map (cons v) t) 887 vlist flist []); 888 889fun gen_updates ty fields = 890 let open pairSyntax 891 val {Tyop,Thy,Args} = dest_thy_type ty 892 fun mk_upd_const (fname,_) = 893 let 894 val rpty = Pretype.fromType ty 895 val op -=> = Pretype.mk_fun_ty infix -=> 896 open errormonad 897 val upd_ptyM = lift2 (fn ty1 => fn ty2 => ty1 -=> (rpty -=> ty2)) 898 Pretype.new_uvar Pretype.new_uvar 899 val ln = locn.Loc_None 900 val qid = Absyn.QIDENT(ln, Thy, Tyop^"_"^fname^"_fupd") 901 val ptm0_M = Parse.absyn_to_preterm qid 902 val ptm_M = 903 lift2 (fn ptm0 => fn upd_pty => 904 Preterm.Constrained{Locn = ln, Ptm = ptm0, Ty = upd_pty}) 905 ptm0_M upd_ptyM 906 val toTerm = ptm_M >- (fn pt => 907 Preterm.typecheck_phase1 NONE pt >> Preterm.to_term pt) 908 in 909 with_flag (Globals.guessing_tyvars, true) 910 (Preterm.smash toTerm) 911 Pretype.Env.empty 912 end 913 val upds = map mk_upd_const fields 914 val fns = map (fn upd_t => mk_var ("f", #1(dom_rng (type_of upd_t)))) upds 915 val fake_tyc = mk_record_vconstr(Tyop,list_mk_fun(map snd fields, ty)) 916 val vars = itlist 917 (fn (n,(_,ty)) => fn acc => 918 mk_var("v"^int_to_string n,ty) :: acc) 919 (enumerate 1 fields) [] 920 val pat = list_mk_comb(fake_tyc,vars) 921 val lefts = map2 (fn upd => fn f => list_mk_comb(upd,[f,pat])) upds fns 922 val diags = diag vars (map (curry mk_comb) fns) 923 fun mapthis (l, d) = let 924 val rtys = map type_of d 925 val rtyc = mk_record_vconstr(Tyop, list_mk_fun(rtys, type_of l)) 926 in 927 mk_eq(l, list_mk_comb(rtyc, d)) 928 end 929 val eqns = ListPair.map mapthis (lefts, diags) 930 val mk_thm = mk_oracle_thm "EmitML fake thm" 931 in 932 map (curry mk_thm []) eqns 933 end 934 handle e => raise wrap_exn "EmitML" "gen_updates" e; 935 936fun gen_accesses ty fields = 937 let open pairSyntax 938 val {Tyop,Thy,Args} = dest_thy_type ty 939 fun mk_proj_const (fname,fty) = 940 mk_thy_const{Name=Tyop^"_"^fname,Thy=Thy, Ty = ty --> fty} 941 val projs = map mk_proj_const fields 942 val fake_tyc = mk_record_vconstr(Tyop,list_mk_fun(map snd fields, ty)) 943 val vars = itlist 944 (fn (n,(_,ty)) => fn acc => 945 mk_var("v"^int_to_string n,ty) :: acc) 946 (enumerate 1 fields) [] 947 val pat = list_mk_comb(fake_tyc,vars) 948 val lefts = map (fn proj => mk_comb(proj,pat)) projs 949 val eqns = rev(map2 (curry mk_eq) lefts vars) 950 val mk_thm = mk_oracle_thm "EmitML fake thm" 951 in 952 map (curry mk_thm []) eqns 953 end 954 handle e => raise wrap_exn "EmitML" "gen_accesses" e; 955 956fun datatype_silent_defs tyAST = 957 let val tyop = hd (map fst tyAST) 958 val tyrecd = hd (Type.decls tyop) 959 in 960 if tyop = "num" then [] else 961 case TypeBase.read tyrecd 962 of NONE => (WARN "datatype_silent_defs" 963 ("No info in the TypeBase for "^Lib.quote tyop); []) 964 | SOME tyinfo => 965 let open TypeBasePure 966 val size_def = [] (* [snd (valOf(size_of tyinfo))] handle _ => [] *) 967 val (updates_defs, access_defs) = 968 case fields_of tyinfo (* test for record type *) 969 of [] => ([],[]) 970 | fields => let val ty = ty_of tyinfo 971 in (gen_updates ty fields, gen_accesses ty fields) 972 end 973 in 974 map (iDEFN o !reshape_thm_hook) 975 (size_def @ updates_defs @ access_defs) 976 end 977 end; 978 979(*---------------------------------------------------------------------------*) 980(* Map from external presentation to internal *) 981(*---------------------------------------------------------------------------*) 982 983(* Ocaml won't accept capitalized types *) 984(* Adds abbreviations with lowercase first letters *) 985 986fun ocaml_type_abbrevs decls = 987let 988 val type_names = map fst decls 989 val candidate_tyis = 990 TypeBasePure.get (TypeBase.theTypeBase()) (hd type_names) 991 val newtypes = if null candidate_tyis then [] else 992 Prim_rec.doms_of_tyaxiom 993 (TypeBasePure.axiom_of (hd candidate_tyis)) 994 fun do_abbrev(name, typ) = 995 if Char.isUpper (String.sub(name,0)) then 996 Parse.temp_type_abbrev(lowerize name, typ) 997 else 998 () 999in 1000 if length type_names = length newtypes then 1001 app do_abbrev (zip type_names newtypes) 1002 else 1003 () 1004end; 1005 1006local 1007 open ParseDatatype 1008 fun cmk s = {name = s, terms = Term.decls s} 1009 fun rmk s = 1010 {name = s, terms = Term.decls (RecordType.mk_recordtype_constructor s)} 1011in 1012fun constructors decls = 1013 case decls of 1014 [] => [] 1015 | (s, Constructors clist) :: rst => map (cmk o #1) clist @ constructors rst 1016 | (s,Record flds)::rst => rmk s :: constructors rst 1017 1018fun constrl [] = [] 1019 | constrl ((s,Constructors clist)::rst) = (s,clist)::constrl rst 1020 | constrl ((s,Record flds)::rst) = 1021 (s, [(RecordType.mk_recordtype_constructor s,map snd flds)])::constrl rst 1022end; 1023 1024 1025 1026 1027 1028fun elemi (DEFN th) (cs,il) = (cs,iDEFN (!reshape_thm_hook th) :: il) 1029 | elemi (DEFN_NOSIG th) (cs,il) = (cs,iDEFN_NOSIG (!reshape_thm_hook th)::il) 1030 | elemi (DATATYPE q) (cs,il) = 1031 let val tyAST = ParseDatatype.hparse (type_grammar()) q 1032 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1033 val defs = datatype_silent_defs tyAST 1034 in (cs, defs @ (iDATATYPE tyAST :: il)) 1035 end 1036 | elemi (EQDATATYPE(sl,q)) (cs,il) = 1037 let val tyAST = ParseDatatype.hparse (type_grammar()) q 1038 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1039 val defs = datatype_silent_defs tyAST 1040 in (cs,defs @ (iEQDATATYPE(sl,tyAST) :: il)) 1041 end 1042 | elemi (ABSDATATYPE(sl,q)) (cs,il) = (* build rewrites for pseudo constrs *) 1043 let open ParseDatatype 1044 val tyAST = hparse (type_grammar()) q 1045 val _ = if !emitOcaml then ocaml_type_abbrevs tyAST else () 1046 val pconstrs = constrl tyAST 1047 val constr_names = flatten(map (map fst o snd) pconstrs) 1048 val constr_arities = flatten(map (map (length o snd) o snd) pconstrs) 1049 val constrs = map (hd o Term.decls) constr_names 1050 val constrs' = zip constrs constr_arities 1051 fun is_multi (_,n) = n >= 2 1052 val mconstrs = filter is_multi constrs' 1053 val _ = List.app new_pseudo_constr mconstrs 1054 (* val _ = schedule this call for exported theory *) 1055 in 1056 (mconstrs@cs, iABSDATATYPE(sl,tyAST) :: il) 1057 end 1058 | elemi (OPEN sl) (cs,il) = (cs,iOPEN sl :: il) 1059 | elemi (MLSIG s) (cs,il) = (cs,iMLSIG s :: il) 1060 | elemi (MLSTRUCT s) (cs,il) = (cs,iMLSTRUCT s :: il); 1061 1062fun internalize elems = 1063 let val (cs, ielems) = rev_itlist elemi elems ([],[]) 1064 in (rev cs, rev ielems) 1065 end; 1066 1067local open ParseDatatype 1068fun replace f (v as dVartype _) = v 1069 | replace f (aq as dAQ _) = aq 1070 | replace f (dTyop{Tyop,Thy,Args}) = 1071 f Tyop handle _ => dTyop{Tyop=Tyop,Thy=Thy,Args=map (replace f) Args} 1072in 1073fun replaceForm f (Constructors alist) = 1074 Constructors (map (I##map (replace f)) alist) 1075 | replaceForm f other = other 1076 1077fun pretype_of ty = 1078 dVartype(dest_vartype ty) 1079 handle _ => 1080 let val (s,args) = dest_type ty 1081 in dTyop{Tyop=s,Thy=NONE,Args=map pretype_of args} 1082 end 1083end; 1084 1085(*---------------------------------------------------------------------------*) 1086(* Initially, datatype descriptions do not have arguments to the type *) 1087(* operators being defined. This function finds out what they should be *) 1088(* and substitutes them through the rhs of the datatype declaration. *) 1089(* The DATATYPE description requires looking info up in the type base, in *) 1090(* order to see what order multiple type variables should be in. The *) 1091(* EQDATATYPE clause expects the type variables to be given in the correct *) 1092(* order in the first argument. *) 1093(*---------------------------------------------------------------------------*) 1094 1095fun repair_type_decls (iDATATYPE decls) = 1096 let val type_names = map fst decls 1097 val candidate_tyis = 1098 TypeBasePure.get (TypeBase.theTypeBase()) (hd type_names) 1099 val tyax = TypeBasePure.axiom_of (hd candidate_tyis) 1100 val newtypes = Prim_rec.doms_of_tyaxiom tyax 1101 val tyvars = map dest_vartype (snd (dest_type (hd newtypes))) 1102 val alist = map (fn x => (fst(dest_type x),pretype_of x)) newtypes 1103 fun alist_fn name = snd (valOf (assoc1 name alist)) 1104 in 1105 (tyvars, map (I##replaceForm alist_fn) decls) 1106 end 1107 | repair_type_decls (iEQDATATYPE (tyvars,decls)) = 1108 let open ParseDatatype 1109 val tyvarsl = map dVartype tyvars 1110 val tynames = map fst decls 1111 val newtypes = map (fn s => dTyop{Tyop=s,Thy=NONE,Args=tyvarsl}) tynames 1112 val alist = zip tynames newtypes 1113 fun alist_fn name = snd (valOf (assoc1 name alist)) 1114 in 1115 (tyvars, map (I##replaceForm alist_fn) decls) 1116 end 1117 | repair_type_decls (iABSDATATYPE stuff) = repair_type_decls (iEQDATATYPE stuff) 1118 | repair_type_decls arg = raise ERR "repair_type_decls" "unexpected input"; 1119 1120fun pp_datatype_as_ML (tyvars,decls) = 1121 let open Portable ParseDatatype PP smpp 1122 val fix_cons = fix_reserved o capitalize 1123 val fix_type = fix_reserved o lowerize 1124 val ppty = pp_type_as_ML 1125 fun pp_comp_ty ty = 1126 if Lib.can dom_rng ty orelse is_pair_type ty 1127 then (add_string "(" >> ppty ty >> add_string")") 1128 else ppty ty 1129 fun pp_tyl tyl = 1130 block INCONSISTENT 0 ( 1131 pr_list pp_comp_ty (add_string" *" >> add_break(1,0)) tyl 1132 ) 1133 fun pp_tyvars [] = nothing 1134 | pp_tyvars [v] = add_string v >> add_break(1,0) 1135 | pp_tyvars vlist = 1136 B 1 ( 1137 add_string"(" >> 1138 pr_list add_string (add_string",") vlist >> 1139 add_string")" 1140 ) 1141 fun pp_clause r clause = 1142 (if !r then (r := false; add_string "= ") else add_string "| ") >> 1143 (case clause of 1144 (con,[]) => add_string (fix_cons con) 1145 | (con,args) => 1146 block INCONSISTENT 0 ( 1147 B 0 (add_string (fix_cons con) >> add_string " of ") >> 1148 pp_tyl (map ParseDatatype.pretypeToType args) 1149 ) 1150 ) 1151 fun pp_decl (tyvars,r) (name,Constructors clauselist) = 1152 B 5 ( 1153 B 0 ( 1154 (if !r then 1155 (r := false; 1156 add_string (if !emitOcaml then "type" else "datatype")) 1157 else 1158 nothing) >> 1159 add_break(1,0) >> pp_tyvars tyvars >> add_string (fix_type name) 1160 ) >> add_break(1,0) >> 1161 B 0 ( 1162 pr_list (pp_clause (ref true)) (add_break(1,0)) clauselist 1163 ) 1164 ) 1165 | pp_decl (tyvars,_) (name,Record flist) = 1166 let open ParseDatatype 1167 val fields = map (I##pretypeToType) flist 1168 in 1169 B 0 ( 1170 add_string (if !emitOcaml then "type" else "datatype") >> 1171 add_break(1,0) >> 1172 pp_tyvars tyvars >> 1173 add_string(fix_type name^" = ") >> 1174 add_string(fix_cons name^" of ") >> 1175 pp_tyl (map snd fields) 1176 ) 1177 end 1178 in 1179 B 0 ( 1180 pr_list (pp_decl (tyvars,ref true)) 1181 (add_newline >> add_string "and" >> add_newline) 1182 decls 1183 ) 1184 end; 1185 1186(*---------------------------------------------------------------------------*) 1187(* Get the name of all constants introduced by the definition. Probably *) 1188(* won't work in general for constant specifications. *) 1189(*---------------------------------------------------------------------------*) 1190 1191fun consts_of_def thm = 1192 let val eqns = strip_conj (snd (strip_forall (concl thm))) 1193 val allCs = map (fst o strip_comb o lhs o snd o strip_forall) eqns 1194 in op_mk_set same_const allCs 1195 end; 1196 1197fun original_type name ty = 1198let val l = size name 1199 val s = if String.sub(name,0) = #" " andalso String.sub(name,l - 1) = #" " 1200 then String.substring(name,1,l - 2) 1201 else name 1202 val d = decls s 1203 handle Option => raise ERR "original_type" 1204 ("Cannot find " ^ quote name ^ Hol_pp.type_to_string ty) 1205 val tm = valOf (List.find (fn t => can (match_type ty) (type_of t)) d) 1206in 1207 type_of tm 1208end; 1209 1210fun pp_sig (s,elems) = 1211 let open Portable PP smpp 1212 val ppty = pp_type_as_ML 1213 val pp_datatype = pp_datatype_as_ML 1214 fun pp_eqdatatype b (tyvars,astl) = 1215 let val tynames = map fst astl 1216 val tys = map (fn s => (tyvars,s)) tynames 1217 fun pp_tydec (tyvars,s) = 1218 B 0 ( 1219 add_string (if b andalso not (!emitOcaml) 1220 then "eqtype " else "type ") >> 1221 (if null tyvars then add_string s 1222 else if List.length tyvars = 1 then 1223 add_string (hd tyvars) >> add_string(" "^s) 1224 else 1225 add_string "(" >> 1226 pr_list add_string (add_string",") tyvars >> 1227 add_string(") "^s)) 1228 ) 1229 in 1230 block CONSISTENT 0 ( 1231 pr_list pp_tydec add_newline (map (pair tyvars) tynames) 1232 ) 1233 end 1234 fun pp_valdec c = 1235 let val (is_type_cons,_,name,ty) = ConstMapML.apply c 1236 val ty = if !emitOcaml then original_type name ty else ty 1237 in 1238 B 3 ( 1239 add_string "val " >> 1240 add_string (fix_name ("",is_type_cons,name)) >> add_break(1,0) >> 1241 add_string ": " >> ppty ty 1242 ) 1243 end 1244 fun pp_el (iDATATYPE astl) = pp_datatype (repair_type_decls (iDATATYPE astl)) 1245 | pp_el (iEQDATATYPE (tyvarsl,astl)) = pp_eqdatatype true (tyvarsl,astl) 1246 | pp_el (iABSDATATYPE (tyvarsl,astl)) = pp_eqdatatype false (tyvarsl,astl) 1247 | pp_el (iDEFN thm) = 1248 pr_list pp_valdec add_newline (consts_of_def thm) 1249 | pp_el (iMLSIG s) = add_string s 1250 | pp_el (iDEFN_NOSIG thm) = nothing 1251 | pp_el (iMLSTRUCT s) = nothing 1252 | pp_el (iOPEN slist) = nothing 1253 in 1254 B 0 ( 1255 add_string ((if !emitOcaml then "module type " else "signature ") ^ 1256 ML s ^ " =") >> 1257 add_newline >> 1258 B 2 ( 1259 add_string "sig" >> add_newline >> 1260 B 0 ( 1261 pr_list pp_el add_newline 1262 (filter (fn (iDEFN_NOSIG _) => false 1263 | (iOPEN _) => false 1264 | (iMLSTRUCT _) => false 1265 | otherwise => true) elems) 1266 ) 1267 ) >> 1268 add_newline >> 1269 add_string "end" >> add_newline 1270 ) 1271 end 1272 handle e => raise wrap_exn "EmitML" "pp_sig" e; 1273 1274val MLinfixes = 1275 String.fields Char.isSpace "* / div mod + - ^ @ <> > < >= <= := o before"; 1276 1277fun pp_struct (s,elems,cnames) = 1278 let open Portable PP smpp 1279 val openthys = ref [] 1280 fun opens() = !openthys 1281 val pp_datatype = pp_datatype_as_ML 1282 fun pp_el (iDATATYPE astl) = pp_datatype (repair_type_decls (iDATATYPE astl)) 1283 | pp_el (iEQDATATYPE (tyvarsl,astl)) = 1284 pp_datatype (repair_type_decls (iEQDATATYPE(tyvarsl,astl))) 1285 | pp_el (iABSDATATYPE (tyvarsl,astl)) = 1286 pp_datatype (repair_type_decls (iABSDATATYPE(tyvarsl,astl))) 1287 | pp_el (iDEFN thm) = 1288 (if !emitOcaml then pp_defn_as_OCAML else pp_defn_as_ML) 1289 (s::opens()) 1290 (concl thm) 1291 | pp_el (iDEFN_NOSIG thm) = pp_el (iDEFN thm) 1292 | pp_el (iMLSIG s) = nothing 1293 | pp_el (iMLSTRUCT s) = add_string s >> add_newline 1294 | pp_el (iOPEN slist) = (openthys := union slist (!openthys); 1295 B 0 ( 1296 pr_list 1297 (add_string o curry String.^ "open " o ML) 1298 add_newline slist >> 1299 add_newline 1300 )) 1301 val (struct_mod, punct) = if !emitOcaml then 1302 ("module ", " : ") 1303 else 1304 ("structure ", " :> ") 1305 in 1306 block CONSISTENT 0 ( 1307 add_string (struct_mod ^ ML s ^ punct ^ ML s ^ " =") >> 1308 add_newline >> 1309 block CONSISTENT 2 ( 1310 add_string "struct" >> add_newline >> 1311 block CONSISTENT 0 ( 1312 (if !emitOcaml then nothing 1313 else 1314 block INCONSISTENT 7 ( 1315 add_string"nonfix " >> 1316 pr_list add_string (add_break(1,0)) (union cnames MLinfixes) >> 1317 add_string ";" 1318 ) >> add_newline) >> 1319 add_newline >> 1320 pr_list pp_el add_newline 1321 (filter (fn (iMLSIG _) => false | otherwise => true) elems) 1322 ) 1323 ) >> add_newline >> 1324 add_string"end" >> add_newline 1325 ) 1326 end 1327 handle e => raise wrap_exn "EmitML" "pp_struct" e; 1328 1329 1330(*---------------------------------------------------------------------------*) 1331(* Dealing with eqtypes. When a HOL function uses equality on the rhs, the *) 1332(* type of the function does not reflect this. However, in ML, eqtypes *) 1333(* are used to signal this. The compiler generates code for the equality *) 1334(* test in that case. So we need to take a HOL definition and compute an ML *) 1335(* type for it, which can include eqtypes. The strategy taken is to search *) 1336(* the rhs for any constants whose generic type has eqtype constraints on *) 1337(* some type variables. By matching the generic constant against the instance*) 1338(* we can find if any eqtype variables are bound to polymorphic types. If so,*) 1339(* the type variables in the polymorphic type get the eqtype attribute. *) 1340(*---------------------------------------------------------------------------*) 1341 1342fun is_eqtyvar ty = 1343 (case String.explode (dest_vartype ty) 1344 of #"'" :: #"'" ::rst => true 1345 | otherwise => false) 1346 handle HOL_ERR _ => raise ERR "is_eqtyvar" "not a type variable"; 1347 1348fun tyvar_to_eqtyvar ty = 1349 let val tyname = dest_vartype ty 1350 in 1351 case String.explode tyname 1352 of #"'" :: #"'" :: _ => raise ERR "tyvar_to_eqtyvar" "already an eqtyvar" 1353 | #"'" :: _ => with_flag (Feedback.emit_WARNING,false) 1354 mk_vartype ("'"^tyname) 1355 | otherwise => raise ERR "tyvar_to_eqtyvar" "unexpected syntax" 1356 end; 1357 1358fun const_eqtyvars genty c2 = 1359 let val bindings = match_type genty (type_of c2) 1360 val bindings' = Lib.filter (is_eqtyvar o #redex) bindings 1361 val bindings'' = Lib.filter (polymorphic o #residue) bindings' 1362 in 1363 Type.type_varsl (map #residue bindings'') 1364 end; 1365 1366fun generic_const thy name = Term.prim_mk_const{Thy=thy,Name=name}; 1367 1368(*---------------------------------------------------------------------------*) 1369(* Gets possibly eq-style type from const map. *) 1370(*---------------------------------------------------------------------------*) 1371 1372fun generic_type c = 1373 #4 (ConstMapML.apply c) handle HOL_ERR _ => type_of c; 1374 1375fun term_eqtyvars tm = 1376 case dest_term tm 1377 of CONST _ => const_eqtyvars (generic_type tm) tm 1378 | VAR _ => [] 1379 | COMB(t1,t2) => union (term_eqtyvars t1) (term_eqtyvars t2) 1380 | LAMB(_,tm) => term_eqtyvars tm; 1381 1382(*---------------------------------------------------------------------------*) 1383(* Translate the type of a defined constant to reflect any uses of equality *) 1384(* in the body of the definition. *) 1385(*---------------------------------------------------------------------------*) 1386 1387fun munge_def_type def = 1388 let val (L,R) = unzip (map (dest_eq o snd o strip_forall) 1389 (strip_conj (snd (strip_forall (concl def))))) 1390 val clist = op_mk_set same_const (map (fst o strip_comb) L) 1391 val tainted = U (map term_eqtyvars R) 1392 val theta = map (fn tyv => tyv |-> tyvar_to_eqtyvar tyv) tainted 1393 in 1394 map (inst theta) clist 1395 end 1396 handle e => raise wrap_exn "EmitML" "munge_def_type" e; 1397 1398(*---------------------------------------------------------------------------*) 1399(* Get the newly introduced constants out of a list of function definitions *) 1400(* and datatype definitions. We have to be aware that a constant may have *) 1401(* been defined in an ancestor theory. *) 1402(*---------------------------------------------------------------------------*) 1403 1404fun add (is_constr, s) {name, terms} = let 1405 fun perterm c = 1406 case ConstMapML.exact_peek c of 1407 NONE => ConstMapML.prim_insert(c, (is_constr, s, name, type_of c)) 1408 | SOME _ => () 1409in 1410 List.app perterm terms 1411end 1412 1413fun install_consts _ [] k = k ([], []) 1414 | install_consts s (iDEFN_NOSIG thm::rst) k = install_consts s (iDEFN thm::rst) k 1415 | install_consts s (iDEFN thm::rst) k = 1416 let val clist0 = munge_def_type thm 1417 val clist = 1418 (* IN is only allowed to be defined in the setML module/structure; 1419 due to the special-case of MEM, listML may appear to define it too 1420 *) 1421 if s <> "set" then filter (not o same_const IN_tm) clist0 1422 else clist0 1423 val _ = List.app 1424 (fn c => add (false, s) {name = nameOfC c, terms = [c]}) 1425 clist 1426 in 1427 install_consts s rst 1428 (fn (cs, nms) => k (clist @ cs, map nameOfC clist @ nms)) 1429 end 1430 | install_consts s (iDATATYPE ty::rst) k = 1431 let 1432 val constrs = constructors ty 1433 val allterms = U (map #terms constrs) 1434 val _ = List.app (add (true, s)) constrs 1435 in 1436 install_consts s rst 1437 (fn (cs,nms) => k (allterms @ cs, map #name constrs @ nms)) 1438 end 1439 | install_consts s (iEQDATATYPE (tyvars,ty)::rst) k = 1440 let 1441 val constrs = constructors ty 1442 val allterms = U (map #terms constrs) 1443 val _ = List.app (add (true, s)) constrs 1444 in 1445 install_consts s rst 1446 (fn (cs,nms) => k (allterms @ cs, map #name constrs @ nms)) 1447 end 1448 | install_consts s (iABSDATATYPE (tyvars,ty)::rst) k = 1449 install_consts s (iEQDATATYPE (tyvars,ty)::rst) k 1450 | install_consts s (other::rst) k = install_consts s rst k; 1451 1452 1453(*---------------------------------------------------------------------------*) 1454(* Append code to the theory file that will load the const map with the *) 1455(* definitions and datatype constructors exported as ML. *) 1456(*---------------------------------------------------------------------------*) 1457 1458fun emit_adjoin_call thy (consts,pcs) = let 1459 fun extern_pc (c,a) = 1460 let val {Thy=thy,Name=n,...} = dest_thy_const c 1461 val n' = mlquote n 1462 val thy' = mlquote thy 1463 in ("(prim_mk_const{Name="^n'^",Thy="^thy'^"},"^Int.toString a^")") 1464 end 1465 fun safetyprint ty = String.toString 1466 (trace ("Unicode",0) 1467 (HOLPP.pp_to_string 10000 1468 (Parse.mlower o 1469 type_pp.pp_type (fst Parse.min_grammars) 1470 PPBackEnd.raw_terminal)) 1471 ty) 1472 1473 fun pr3 ({Name,Thy,Ty}, (b,s2,ty)) = let 1474 open PP smpp 1475 val S = add_string 1476 val BB = block INCONSISTENT 0 1477 fun brk n = add_break (1,n) 1478 fun ppty ty = 1479 BB (S "typ" >> brk 0 >> S "\"" >> S (safetyprint Ty) >> S "\"") 1480 in 1481 S "(" >> BB ( 1482 S "{" >> BB ( 1483 BB (S "Name =" >> brk 0 >> S (mlquote Name ^ ",")) >> brk 0 >> 1484 BB (S "Thy =" >> brk 0 >> S (mlquote Thy ^",")) >> brk 0 >> 1485 BB (S "Ty =" >> brk 2 >> ppty Ty) 1486 ) >> S "}," >> brk 0 >> 1487 S "(" >> BB ( 1488 S (Bool.toString b ^ ",") >> brk 0 >> 1489 S (Lib.mlquote s2 ^ ",") >> brk 0 >> 1490 ppty ty 1491 ) >> S ")" 1492 ) >> S ")" 1493 end 1494 in 1495 Theory.adjoin_to_theory 1496 {sig_ps = NONE, 1497 struct_ps = SOME (fn _ => 1498 let open PP 1499 val S = add_string 1500 val BR = add_break 1501 val B = PP.block PP.CONSISTENT 0 1502 fun getdata c = let 1503 val (b,pfx,s,ty) = ConstMapML.apply c 1504 in 1505 (b,s,ty) 1506 end 1507 in 1508 B ( 1509 [ 1510 S "val _ = ", NL, 1511 S " let open Parse", NL, 1512 S " fun doit (r,(b,s,ty)) = ", NL, 1513 S " let val c = Term.mk_thy_const r", NL, 1514 S (" in ConstMapML.prim_insert(c,(b,"^Lib.quote thy^",s,ty))"), 1515 NL, 1516 S " end", NL, 1517 S " fun typ s = Feedback.trace(\"Vartype Format Complaint\", 0)\n\ 1518 \ (#1 (parse_from_grammars min_grammars))\n\ 1519 \ [QUOTE (\":\"^s)]", NL, 1520 S " in", NL, 1521 S " List.app doit [", NL, 1522 S " ", 1523 block INCONSISTENT 0 ( 1524 pr_list (Parse.mlower o pr3) [S",", BR(1,0)] 1525 (map (fn c => (dest_thy_const c, getdata c)) consts) 1526 ), NL, 1527 S " ]", NL, 1528 S " end", NL, NL] @ 1529 (if null pcs then [] 1530 else [ 1531 S "val _ = List.app EmitML.new_pseudo_constr", NL, 1532 S " [", 1533 block INCONSISTENT 0 ( 1534 pr_list S [S",", BR(1,0)] (map extern_pc pcs) 1535 ), 1536 S"]", NL, NL 1537 ]) 1538 ) 1539 end)} 1540 handle e => raise ERR "emit_adjoin_call" "" 1541 end; 1542 1543(*---------------------------------------------------------------------------*) 1544(* Write the ML out to a signature and structure file. We first run over the *) 1545(* definitions and lift out the newly defined constants. These get inserted *) 1546(* into the "const map", which is accessed when prettyprinting the *) 1547(* definitions. We also have to detect eqtypes and ensure that the const map *) 1548(* is properly updated when the theory is loaded. *) 1549(*---------------------------------------------------------------------------*) 1550 1551fun emit_xML (Ocaml,sigSuffix,structSuffix) p (s,elems_0) = 1552 let val _ = emitOcaml := Ocaml 1553 val (pcs,elems) = internalize elems_0 (* pcs = pseudo-constrs *) 1554 val path = if p="" then FileSys.getDir() else p 1555 val pathPrefix = Path.concat(path, capitalize s) 1556 val sigfile = pathPrefix^ sigSuffix 1557 val structfile = pathPrefix^ structSuffix 1558 fun trydelete s = OS.FileSys.remove s handle OS.SysErr _ => () 1559 fun cleanFiles() = (trydelete sigfile; trydelete structfile) 1560 in 1561 let val sigStrm = TextIO.openOut sigfile 1562 val structStrm = TextIO.openOut structfile 1563 val out = curry TextIO.output 1564 val (consts, usednames) = install_consts s elems (fn x => x) 1565 in 1566 (PP.prettyPrint(out sigStrm, 75) (Parse.mlower (pp_sig (s,elems))); 1567 PP.prettyPrint(out structStrm, 75) 1568 (Parse.mlower (pp_struct (s,elems,usednames))); 1569 TextIO.closeOut sigStrm; 1570 TextIO.closeOut structStrm; 1571 HOL_MESG ("emitML: " ^ s ^ "{" ^ sigSuffix ^ "," ^ structSuffix ^ "}\n\ 1572 \ written to directory "^path); 1573 emit_adjoin_call s (consts,pcs) 1574 ) 1575 handle e => (List.app TextIO.closeOut [sigStrm, structStrm]; 1576 cleanFiles(); 1577 raise wrap_exn "EmitML" "emitML" e) 1578 end handle Io _ => 1579 raise mk_HOL_ERR "EmitML" "emitML" 1580 ("I/O error prevented exporting files to "^Lib.quote path) 1581 end 1582 1583val emit_xML = 1584 (fn info => fn p => fn stuff => 1585 Feedback.trace ("Unicode", 0) 1586 (emit_xML info p) 1587 stuff) 1588 1589val emitML = emit_xML (false,!sigSuffix,!structSuffix); 1590 1591val emitCAML = emit_xML (true,!sigCamlSuffix,!structCamlSuffix); 1592 1593fun eSML d l = with_flag (type_pp.pp_array_types, false) 1594 (emitML (!Globals.emitMLDir)) (d, l); 1595fun eCAML d l = with_flag (type_pp.pp_array_types, false) 1596 (emitCAML (!Globals.emitCAMLDir)) (d, l); 1597 1598fun MLSIGSTRUCT ll = 1599 foldr (fn (x,l) => MLSIG x :: MLSTRUCT x :: l) [] (ll @ [""]); 1600 1601val pp_datatype_as_ML = fn dty => Parse.mlower (pp_datatype_as_ML dty) 1602val pp_defn_as_ML = fn sl => Parse.mlower o pp_defn_as_ML sl 1603val pp_term_as_ML = fn sl => fn sd => Parse.mlower o pp_term_as_ML sl sd 1604val pp_type_as_ML = Parse.mlower o pp_type_as_ML 1605 1606end (* struct *) 1607