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

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

Translation of sets of sets now possible

Currently the expected translation function works for constants. This
needs to be extended for other term types.

The robustness of the type inference can also be improved on.
Currently the new type is generated by appending new elements to a list
which has an implicit ordering.
parent 44af04aa
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 ();
......@@ -13,6 +13,14 @@ open HolKernel Parse boolLib bossLib;
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";
......@@ -31,6 +39,62 @@ fun mk_kn (thy_str : string) (nam_str : string) : KernelSig.kernelname =
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
......@@ -48,9 +112,161 @@ fun translate dict tm =
end
end
else if is_comb tm then
failwith "unimplemented"
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 tm
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)
end
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)
| [] => tlist
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, SOME (match_type ety new_cty))
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 := unique_append relation (! type_map)
in
na :: update_types xs
end
end
val update_args = update_types args
val new_type = type_subst (! type_map) func_gentype
val new_argtype = take (strip_type_n (new_type) (length arg), (length arg))
in
list_mk_comb (type_cast funct new_type, map (uncurry type_cast) (zip update_args new_argtype))
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";
......
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