1structure lisp_synthesisLib :> lisp_synthesisLib = 2struct 3 4open HolKernel boolLib bossLib; 5open lisp_extractTheory lisp_extractLib; 6open lisp_compilerTheory; 7 8open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 9open optionTheory arithmeticTheory relationTheory; 10open stringLib pairSyntax; 11 12 13(* we define lisp_Define and lisp_tDefine which record definitions 14 that are to be exported to verified deep embeddings *) 15 16local 17 val defs_inds = ref (tl [("",TRUTH,TRUTH)]) 18in 19 fun add_def def = let 20 val name = def |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator 21 |> dest_const |> fst 22 val ind_name = name ^ "_ind" 23 val ind = fetch "-" ind_name handle HOL_ERR _ => TRUTH 24 val xs = filter (fn (n,def,ind) => not (n = name)) (!defs_inds) 25 val _ = defs_inds := xs @ [(name,SPEC_ALL def,ind)] 26 in def end 27 fun get_defs_inds () = !defs_inds 28end 29 30fun lisp_Define t = add_def (Define t); 31fun lisp_tDefine name t tac = add_def (tDefine name t tac); 32 33 34(* the main synthesis function: shallow -> deep *) 35 36fun synthesise_deep_embeddings () = let 37 val defs_inds = map (fn (name,def,ind) => (def,ind)) (get_defs_inds()) 38 val base_name = "deep_embedding" 39 val (deep,certs) = deep_embeddings base_name defs_inds 40 val deep_simp = SIMP_RULE std_ss [GSYM CONJ_ASSOC,fns_assum_def,EVERY_DEF] deep 41 (* printing in Lisp syntax *) 42 val xs = deep |> SPEC_ALL |> concl |> rand |> rand 43 val tm = EVAL ``verified_string ^xs`` |> concl |> rand 44 val _ = if can (match_term ``NONE:'a option``) tm then () else let 45 val str = stringSyntax.fromHOLstring (rand tm) 46 in print ("\n\nDeep embedding in Lisp syntax:\n\n" ^ str ^ "\n\n") end 47 in LIST_CONJ (deep_simp::certs) end 48 49 50end 51