397 |
397 |
398 local |
398 local |
399 |
399 |
400 structure Code_Antiq_Data = Proof_Data |
400 structure Code_Antiq_Data = Proof_Data |
401 ( |
401 ( |
402 type T = (string list * string list) * (bool |
402 type T = string list * (bool |
403 * (string * (string * string) list) lazy); |
403 * (string * (string * string) list) lazy); |
404 val empty: T = (([], []), (true, (Lazy.value ("", [])))); |
404 val empty: T = ([], (true, (Lazy.value ("", [])))); |
405 fun init _ = empty; |
405 fun init _ = empty; |
406 ); |
406 ); |
407 |
407 |
408 val is_first_occ = fst o snd o Code_Antiq_Data.get; |
408 val is_first_occ = fst o snd o Code_Antiq_Data.get; |
409 |
409 |
410 fun register_code new_tycos new_consts ctxt = |
410 fun register_code new_consts ctxt = |
411 let |
411 let |
412 val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; |
412 val (consts, _) = Code_Antiq_Data.get ctxt; |
413 val tycos' = fold (insert (op =)) new_tycos tycos; |
|
414 val consts' = fold (insert (op =)) new_consts consts; |
413 val consts' = fold (insert (op =)) new_consts consts; |
415 val program = Code_Thingol.consts_program ctxt consts'; |
414 val program = Code_Thingol.consts_program ctxt consts'; |
416 val acc_code = Lazy.lazy (fn () => |
415 val acc_code = Lazy.lazy (fn () => |
417 evaluation_code ctxt Code_Target.generatedN program tycos' consts' |
416 evaluation_code ctxt Code_Target.generatedN program [] consts' |
418 |> apsnd snd); |
417 |> apsnd snd); |
419 in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; |
418 in Code_Antiq_Data.put (consts', (false, acc_code)) ctxt end; |
420 |
419 |
421 fun register_const const = register_code [] [const]; |
420 fun register_const const = register_code [const]; |
422 |
421 |
423 fun print_code is_first const ctxt = |
422 fun print_code is_first const ctxt = |
424 let |
423 let |
425 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
424 val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; |
426 val (ml_code, consts_map) = Lazy.force acc_code; |
425 val (ml_code, consts_map) = Lazy.force acc_code; |