Email Gateway (Aug 19 2022 at 16:23): Email Gateway (Aug 19 2022 at 16:23):From: M A <tesleft@hotmail.com>
Hi,
how to export hashtable code to haskell code?
after following codegen.pdf, there is no outputthe export-code reserved word do not have color, where is missing?
http://brynosaurus.com/isabelle/dict/
module exportexample(ht_lookup, ht_remove, ht_insert) where {theory exportexampleimports Datatypebegindatatype ('a,'b) dict = "'a => 'b option"datatype 'a hashfunc = "'a => nat"datatype ('a,'b) hashtab = "('a,'b) dict list"
primrec dict_cons :: "('a,'b) dict""dict_cons == (%n. None)"
primrec dict_insert :: "['a, 'b, ('a,'b) dict] => ('a,'b) dict""dict_insert n v D == (%n'. if n' = n then Some v else D n')"
primrec dict_remove :: "['a, ('a,'b) dict] => ('a,'b) dict""dict_remove n D == (%n'. if n' = n then None else D n')"
primrec dict_lookup :: "['a, ('a,'b) dict] => 'b option""dict_lookup n D == D n"
primrec dict_scan :: "('a,'b) dict => ('a * 'b) set""dict_scan D == {(n,v). D n = Some v}"
primrec ht_remove :: "['a, ('a,'b) hashtab, 'a hashfunc] => ('a,'b) hashtab""ht_remove n H F == list_update H (F n) (dict_remove n (H!(F n)))"
primrec ht_insert :: "['a, 'b, ('a,'b) hashtab, 'a hashfunc] => ('a,'b) hashtab""ht_insert n v H F == list_update H (F n) (dict_insert n v (H!(F n)))"
primrec ht_lookup :: "['a, ('a,'b) hashtab, 'a hashfunc] => 'b option""ht_lookup n H F == dict_lookup n (H!(F n))"
export-code ht_lookup ht_remove ht_insert in Haskellmodule-name exportexample file c:/end}
Regards,
Martin
Last updated: Nov 21 2024 at 12:39 UTC