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

Commit ed21b02d authored by Alexander Soen's avatar Alexander Soen
Browse files

Change translation method

The translation method has been changed into two phases. The first is to
determine the final type of what the translated term would be. The
second, is with this type information, to create the final translated
term.

To do:
  -- Implement abstractions for translation
parent c7b78051
open HolKernel Parse boolLib bossLib;
(*
Translates from sets to lists and fmaps to a tree structure
This translation is done because the translator is unable to translate the
previous type; it is also benificial to be able to have efficient datatypes
in the translation (ie set implementation vs lists).
Plan: Make it such that there exists a recursive type checker to see if a
function/constant/variable/abstraction needs to be translated.
A translator to actually translate these objects
Hopefully something able to prove some properties which will ensure
that the translation is correct
-- Translate the head and determine the expected type of it
-- Split this up to match the args
-- If types match don't do anything
-- Else translate the arg
-- If types now match make a rel and translate (can match)
-- Else fail
--
*)
val _ = new_theory "datatypeTranslate";
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;
fun mk_kn (thy_str : string) (nam_str : string) : KernelSig.kernelname =
{Thy=thy_str, Name=nam_str};
val _ = insert_dict dict ((mk_kn "pred_set" "EMPTY"), (``:α -> bool``, ``[] : α list``));
val _ = insert_dict dict ((mk_kn "pred_set" "INSERT"), (``:α -> (α -> bool) -> (α -> bool)``, ``CONS : α -> α list -> α list``));
C>
fun strip_type_n ty n =
if (n > 0) then
case dest_type ty of
("fun", [x, xs]) => x :: strip_type_n xs (n-1)
| _ => [ty]
else [ty];
fun strip_type ty =
case dest_type ty of
("fun", [x, xs]) => x :: strip_type xs
| _ => [ty];
fun list_mk_type tyl =
case tyl of
[x] => x
| x :: xs => mk_type ("fun", [x, list_mk_type xs])
| _ => failwith "cannot make type"
fun strip_type_meta ty =
case dest_type ty of
(meta, [x, xs]) => (meta, x) :: strip_type_meta xs
| (meta, [x]) => [(meta, x)];
fun list_mk_type tyl =
case tyl of
[x] => x
| x :: xs => mk_type ("fun", [x, list_mk_type xs])
| _ => failwith "cannot make type"
fun nonred_insert elm alist =
let
val (key, v) = elm
in
if (key = v) then alist else elm :: alist
end;
fun ualist_insert (elm : hol_type * hol_type) (alist : (hol_type * hol_type) list) =
let
val (key, v) = elm
fun new_el l =
case l of
((x,y) :: xs) =>
if (key = x) then
(if (v = y) then false else failwith "type miss-match")
else (new_el xs)
| [] => true
in
if new_el alist then nonred_insert elm alist else alist
end;
fun gen_type_dif tylist pty nty narg =
foldl (uncurry ualist_insert) tylist
(zip (strip_type_n pty narg) (strip_type_n nty narg));
fun translate dict tm =
if is_const tm then
let
val {Name=name, Thy=thy, Ty=ty} = dest_thy_const tm
in
case Binarymap.peek (!dict, mk_kn thy name) of
NONE => tm
| SOME (store_type, conv_val) =>
let
val type_matcher = match_type store_type ty
val {Name=cname, Thy=cthy, Ty=cty} = dest_thy_const conv_val
val new_cty = type_subst type_matcher cty
in
mk_thy_const {Name=cname, Thy=cthy, Ty=new_cty}
end
end
else if is_comb tm then
let
val (func, arg) = strip_comb tm
val funct = translate dict func
val argt = map (translate dict) arg
val typeshift = (type_of func, type_of funct) ::
(zip (map type_of arg) (map type_of argt))
in
list_mk_comb (funct, argt)
end
else if is_var tm then
let
val (var_str, var_ty) = dest_var tm
in
tm
end
else if is_abs tm then
failwith "unimplemented"
else failwith "invalid input";
fun inst_type_var ty =
let
val subst_map = ref ([] : (hol_type, hol_type) Lib.subst)
fun inst_type_var_aux ty' =
if is_vartype ty' then
if ty' = type_subst (! subst_map) ty' then
let
val n_ty_var = gen_tyvar ()
val _ = subst_map := append (! subst_map) (match_type ty' n_ty_var)
in n_ty_var end
else
type_subst (! subst_map) ty'
else
case dest_type ty' of
(str, []) => ty'
| (str, tlist) => mk_type (str, map inst_type_var_aux tlist)
in inst_type_var_aux ty end;
fun type_cast tm new_type =
if is_const tm then
let
val {Name=name, Thy=thy, Ty=ty} = dest_thy_const tm
in
mk_thy_const {Name=name, Thy=thy, Ty=new_type}
end
else if is_var tm then
let
val (name, _) = dest_var
in
mk_var (name, new_type)
end
else if is_comb tm then
let
val (func, arg) = strip_comb tm
val arg_types = take (strip_type_n new_type (length arg), (length arg))
val arg_pairs = zip arg arg_types
in
list_mk_comb (type_cast func new_type, map (uncurry type_cast) arg_pairs
fun exp_translate dict tm expect_ty =
if is_const tm then
let
val {Name=name, Thy=thy, Ty=ty} = dest_thy_const tm
in
case Binarymap.peek (!dict, mk_kn thy name) of
NONE => (tm, NONE, NONE)
| SOME (store_type, conv_val) =>
let
val type_matcher = match_type store_type ty
val {Name=cname, Thy=cthy, Ty=cty} = dest_thy_const conv_val
val new_cty = type_subst type_matcher cty
in
case expect_ty of
NONE =>
(mk_thy_const {Name=cname, Thy=cthy, Ty=new_cty}, SOME cty, NONE)
| SOME ety =>
if is_vartype ety then
(if can (match_type ety) new_cty then
(mk_thy_const {Name=cname, Thy=cthy, Ty=new_cty}, SOME cty, SOME (match_type ety new_cty))
else
failwith "Cannot match type")
else
(if type_subst (match_type ety new_cty) ety = new_cty then
(mk_thy_const {Name=cname, Thy=cthy, Ty=new_cty}, SOME cty, NONE)
else
failwith "Type miss-match in expected type and created")
end
end
else
failwith "not implemented";
fun translate dict tm =
if is_const tm then
let
val {Name=name, Thy=thy, Ty=ty} = dest_thy_const tm
in
case Binarymap.peek (!dict, mk_kn thy name) of
NONE => tm
| SOME (store_type, conv_val) =>
let
val type_matcher = match_type store_type ty
val {Name=cname, Thy=cthy, Ty=cty} = dest_thy_const conv_val
val new_cty = type_subst type_matcher cty
in
mk_thy_const {Name=cname, Thy=cthy, Ty=new_cty}
end
end
else if is_comb tm then
let
val (func, arg) = strip_comb tm
val (funct, SOME expty, _) = exp_translate dict func NONE
val func_gentype = inst_type_var (expty)
val type_map = ref (match_type func_gentype (type_of funct))
val expect_argtype = take (strip_type_n (func_gentype) (length arg), (length arg))
val args = zip arg expect_argtype
fun update_types arguments =
case arguments of
[] => []
| (a, ety) :: xs =>
let
val (na, _, rel) = exp_translate dict a (SOME ety)
in
case rel of
NONE =>
(* Missing case, need to change exp_translate *)
na :: update_types xs
| SOME relation =>
let
val _ = type_map := append relation (! type_map)
in
na :: update_types xs
end
end;
val update_args = update_types args
val new_types = type_subst (! type_map) func_gentype
in
list_mk_comb (funct, argt)
end
else if is_var tm then
let
val (var_str, var_ty) = dest_var tm
in
tm
end
else if is_abs tm then
failwith "unimplemented"
else failwith "invalid input";
val _ = export_theory ();
......@@ -36,8 +36,9 @@ fun mk_kn (thy_str : string) (nam_str : string) : KernelSig.kernelname =
{Thy=thy_str, Name=nam_str};
val _ = insert_dict dict ((mk_kn "pred_set" "EMPTY"), (``:α -> bool``, ``[] : α list``));
val _ = insert_dict dict ((mk_kn "min" "="), (``:α -> α -> bool``, ``$=``));
val _ = insert_dict dict ((mk_kn "pred_set" "INSERT"), (``:α -> (α -> bool) -> (α -> bool)``, ``CONS : α -> α list -> α list``));
val _ = insert_dict dict ((mk_kn "pred_set" "EMPTY"), (``:α -> bool``, ``[] : α list``));
fun strip_type_n ty n =
if (n > 0) then
......@@ -149,7 +150,6 @@ fun inst_type_var ty =
| (str, tlist) => mk_type (str, map inst_type_var_aux tlist)
in inst_type_var_aux ty end;
(*
fun type_cast tm new_type =
if is_const tm then
let
......@@ -166,7 +166,7 @@ fun type_cast tm new_type =
else if is_comb tm then
let
val (func, arg) = strip_comb tm
val arg_types = take (strip_type_n new_type (length arg), (length arg))
val arg_types = List.take (strip_type_n new_type (length arg), (length arg))
val arg_pairs = zip arg arg_types
in
list_mk_comb (type_cast func new_type, map (uncurry type_cast) arg_pairs)
......@@ -174,6 +174,7 @@ fun type_cast tm new_type =
else
failwith "unimplemented";
(*
fun unique_append flist tlist =
case flist of
x :: xs => if mem x tlist then unique_append xs tlist else unique_append xs (x :: tlist)
......@@ -312,6 +313,15 @@ fun match_comp inst1 inst2 =
foldl (uncurry match_comp_one) inst2 inst1
end;
fun strip_type_narg ty n =
if (n > 0) then
case dest_type ty of
("fun", [x, xs]) => x :: strip_type_narg xs (n-1)
| _ => [ty]
else [];
else failwith "";
(*
fun translate dict tm =
......@@ -434,50 +444,248 @@ fun translate_e dict tm expty =
(Term.inst poly_inst tm', inst)
end
end
else if is_comb tm then
let
val (head, args) = strip_comb tm
val hd_expty = List.foldr (fn (_, ty) => gen_tyvar() --> ty) expty args
val (hdtm, inst0) = translate_e dict head hd_expty
(*
val inst' = inst0
val acc = []
val type_ref = type_of hdtm
val (a1::rest) = args
*)
fun do_args inst' acc type_ref args =
case args of
[] => (inst', acc)
| a1::rest =>
let
val (d,drest) = dom_rng (type_ref)
val (a1',a_inst) = translate_e dict a1 d
val new_inst = match_comp a_inst inst'
(*
val inst' = new_inst
val acc = a1' :: acc
val type_ref = drest
val (a1::rest) = rest
*)
else if is_comb tm then
let
val (head, args) = strip_comb tm
val hd_expty = List.foldr (fn (_, ty) => gen_tyvar() --> ty) expty args
val (hdtm, inst0) = translate_e dict head hd_expty
(*
val inst' = inst0
val acc = []
val type_ref = type_of hdtm
val (a1::rest) = args
*)
fun do_args inst' acc type_ref args =
case args of
[] => (inst', acc)
| a1::rest =>
let
val (d,drest) = dom_rng (type_ref)
val (a1',a_inst) = translate_e dict a1 d
val new_inst = match_comp a_inst inst'
(*
val inst' = new_inst
val acc = a1' :: acc
val type_ref = drest
val (a1::rest) = rest
*)
in
do_args new_inst (a1'::acc) drest rest
end
val (inst, args') = do_args inst0 [] hd_expty args
in
(list_mk_comb (Term.inst inst hdtm, map (Term.inst inst) (rev args')), inst)
end
else if is_var tm then
let
val (name, _) = dest_var tm
val ty0 = gen_tyvar ()
val inst = match_type expty ty0
in
(mk_var (name, ty0), inst)
end
else
failwith "Unimplemented";
fun inter_translate dict tm = #1 (translate_e dict tm (gen_tyvar ()));
fun head_translate dict tm expty args =
let
val CONST {Name, Thy, Ty} = dest_term tm
in
case Binarymap.peek(dict, mk_kn Thy Name) of
NONE =>
let
val ty0 = List.foldr (fn (_, ty) => gen_tyvar() --> ty) expty args
val tm' = mk_const (strcat Name "'", ty0) (* Need some method of changing the type of f ???? *)
val inst = match_type expty ty0
in
(tm', inst)
end
| SOME (key_type, tm') =>
let
val ty0 = inst_type_var (type_of tm')
val poly_inst = match_type (type_of tm') ty0
val inst = match_type expty ty0
in
(Term.inst poly_inst tm', inst)
end
end
(* Test cases *)
(*
Current Issues:
translating:
f x = {x}, typing of argument of $=
abstractions
*)
fun gen ty =
if is_vartype ty then [ty]
else
let val {Args,Thy,Tyop} = dest_thy_type ty
fun normal_op ty =
let
in
if Tyop = "fun" andalso Thy = "min" then
let val arg2 = hd (tl Args)
in
do_args new_inst (a1'::acc) drest rest
if Type.compare(arg2,bool) = EQUAL then
let
val arg1's = gen (hd Args)
in
map (fn arg1' => arg1' --> bool) arg1's @
map listSyntax.mk_list_type arg1's
end
else
normal_op ty
end
val (inst, args') = do_args inst0 [] hd_expty args
in
(list_mk_comb (Term.inst inst hdtm, map (Term.inst inst) (rev args')), inst)
end
else if is_var tm then
let
val (name, _) = dest_var tm
val ty0 = gen_tyvar ()
val inst = match_type expty ty0
in
(mk_var (name, ty0), inst)
end
else
failwith "Unimplemented";
else normal_op ty
end
fun int_translate dict tm = #1 (translate_e dict tm (gen_tyvar ()));
fun find_type dict tm ty =
if is_const tm then
let
val CONST {Name, Thy, Ty} = dest_term tm
in
case Binarymap.peek (dict, mk_kn Thy Name) of
NONE => (type_of tm, type_of tm)
| SOME (keyty, tm') =>
let
val keyty0 = inst_type_var keyty
val inst0 = match_type keyty keyty0
val ty0 = type_subst inst0 (type_of tm')
in
(keyty0, ty0)
end
end
else if is_var tm then
(ty, ty)
else if is_comb tm then
let
val (head0, args0) = strip_comb tm
val (pred_hdty, post_hdty) = find_type dict head0 ty
val pred_argsty = strip_type_narg pred_hdty (length args0)
val post_argsty = strip_type_narg post_hdty (length args0)
(*
val args = args0
val pred_argsty' = pred_argsty
val post_argsty' = post_argsty
val pred_hdty' = pred_hdty
val post_hdty' = post_hdty
val (x::xs) = args
val (y::ys) = pred_argsty'
val (z::zs) = post_argsty'
*)
fun do_args args pred_argsty' post_argsty' pred_hdty' post_hdty' =
case (args, pred_argsty', post_argsty') of
([], [], []) => (pred_hdty', post_hdty')
| (x::xs, y::ys, z::zs) =>
let
val (pred_arg, post_arg) = find_type dict x y
(*
val (pred_arg, post_arg) = (get_ty pred, get_ty post)
*)
in
if Type.compare (pred_arg, post_arg) = EQUAL then
(*
val args = xs
val pred_argsty' = ys
val post_argsty' = zs
val pred_hdty' = pred_hdty'
val post_hdty' = post_hdty'
val (x::xs) = args
val (y::ys) = pred_argsty'
val (z::zs) = post_argsty'
*)
do_args xs ys zs pred_hdty' post_hdty'
else
let
val pred_inst = if can (match_type y) pred_arg then
match_type y pred_arg
else []
val post_inst = if can (match_type z) post_arg then
match_type z post_arg
else []
val ys' = map (type_subst pred_inst) ys
val zs' = map (type_subst post_inst) zs
val pred_hdty'' = type_subst pred_inst pred_hdty'
val post_hdty'' = type_subst post_inst post_hdty'
(*
val args = xs
val pred_argsty' = ys'
val post_argsty' = zs'
val pred_hdty' = pred_hdty''
val post_hdty' = post_hdty''
val (x::xs) = args
val (y::ys) = pred_argsty'
val (z::zs) = post_argsty'
*)
in
do_args xs ys' zs' pred_hdty'' post_hdty''
end
end
val (pred_hdty', post_hdty') =
do_args args0 pred_argsty post_argsty pred_hdty post_hdty
fun get_fin_ty ty = last (strip_type_n ty (length args0))
in
(get_fin_ty pred_hdty', get_fin_ty post_hdty')
end
else failwith "";
fun translate_conc dict tm ty =
if is_const tm then
let
val CONST {Name=name, Thy=thy, Ty=_} = dest_term tm
in
case Binarymap.peek (dict, mk_kn thy name) of
NONE => mk_thy_const {Name=name, Thy=thy, Ty=ty}
| SOME (_, tm') =>
let
val CONST {Name=name', Thy=thy', Ty=_} = dest_term tm'
in
mk_thy_const {Name=name', Thy=thy', Ty=ty}
end
end
else if is_var tm then
let
val (name, _) = dest_var tm
in
mk_var (name, ty)
end
else if is_comb tm then
let
val (head, args) = strip_comb tm
val (pred_hdty, post_hdty) = find_type dict head (gen_tyvar ())
val inst = match_type (last (strip_type_n post_hdty (length args))) ty
val hdty = type_subst inst post_hdty
val head' = translate_conc dict head hdty
val argsty = strip_type_narg post_hdty (length args)
val argsty' = map (type_subst inst) argsty
val args' = map2 (translate_conc dict) args argsty'
in
list_mk_comb (head', args')
end
else if is_abs tm then
failwith "Unimplmented"
else failwith "Term type cannot be identified";
fun translate_interm dict tm =
let
val ty = type_of tm
val (key_ty, fin_ty0) = find_type dict tm (gen_tyvar ())
val fin_inst = match_type key_ty ty
val fin_ty = type_subst fin_inst fin_ty0
in
translate_conc dict tm fin_ty
end;
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