To protect your data, the CISO officer has suggested users to enable GitLab 2FA as soon as possible.

Commit 2d935438 authored by Alexander Soen's avatar Alexander Soen
Browse files

Change list translation method

Translation method now uses an intermediary type datastructure.
It is similar to the previous method which was done in two stages.

To do:
  - Clean up code base
  - Add abstractions
  - Fix the testing script
parent 99edb424
CLINE_OPTIONS = --qof
INCLUDES = $(CMLDIR) $(CMLDIR)/translator/ $(CMLDIR)/candle/standard/ml_kernel/ $(CMLDIR)/explorer/pp/astPP $(HOLDIR)/examples/formal-languages/context-free/ $(CMLDIR)/compiler/parsing ../
This diff is collapsed.
......@@ -7,6 +7,11 @@ val _ = new_theory "datatypeTranslateTestsTheory"
val dict = ref (Binarymap.mkDict KernelSig.name_compare :
(KernelSig.kernelname, (hol_type * term)) Binarymap.dict)
fun insert_dict dict (kernelname, info_tuple) =
let
val tmp = Binarymap.insert (!dict, kernelname, info_tuple)
in dict := tmp end;
val _ = insert_dict dict ((mk_kn "pred_set" "INSERT"),
(``:α -> (α -> bool) -> (α -> bool)``,
``CONS : α -> α list -> α list``))
......@@ -22,12 +27,23 @@ fun assert_translate_interm dict init_tm assert_tm =
prove (mk_eq (fin_tm, assert_tm), simp[])
end
val _ = assert_translate dict ``{}:'a -> bool`` ``[]:'a list``
val _ = assert_translate dict ``{x:num}`` ``[x:num]``
val _ = assert_translate dict ``{ODD}`` ``[ODD]:(num -> bool) list``
val _ = assert_translate dict ``{{}:'a -> bool}`` ``[[]:'a list]``
val _ = assert_translate dict ``{{}; x:num}`` ``[[]; x:num]``
val _ = assert_translate dict ``{}:'a -> bool=y`` ``[]:'a list=y``
val _ = assert_translate dict ``[{3}]`` ``[[3]]``
val _ = assert_translate_interm dict
``{}:'a -> bool`` ``[]:'a list``
val _ = assert_translate_interm dict
``{x:num}`` ``[x:num]``
val _ = assert_translate_interm dict
``{ODD}`` ``[ODD]:(num -> bool) list``
val _ = assert_translate_interm dict
``{{}:'a -> bool}`` ``[[]:'a list]``
val _ = assert_translate_interm dict
``{{}; x:num -> bool}`` ``[[]; x:num list]``
val _ = assert_translate_interm dict
``{}:'a -> bool=y`` ``[]:'a list=y``
val _ = assert_translate_interm dict
``[{3}]`` ``[[3]]``
val _ = assert_translate_interm dict
``(x = y) x {3}`` ``(x = y) x [3]``
val _ = assert_translate_interm dict
``x={2}`` ``x=[2]``
val _ = export_theory ()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment