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