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

Commit 52d6d61b authored by Alexander Soen's avatar Alexander Soen
Browse files

Add basic set translation for const, vars & combs

The datatype translation seems to be working now for standard sets.
Currently abstractions need to be implementation and also a mechanism to
generally translate theorems and other objects in hol.
parent 0142a14c
......@@ -39,8 +39,6 @@ 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
......@@ -77,6 +75,7 @@ fun nonred_insert elm alist =
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
......@@ -130,6 +129,7 @@ fun translate dict tm =
else if is_abs tm then
failwith "unimplemented"
else failwith "invalid input";
*)
fun inst_type_var ty =
let
......@@ -149,6 +149,7 @@ 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
......@@ -210,7 +211,6 @@ fun exp_translate dict tm expect_ty =
else
failwith "not implemented";
fun translate dict tm =
if is_const tm then
let
......@@ -271,4 +271,200 @@ fun translate dict tm =
failwith "unimplemented"
else failwith "invalid input";
*)
fun lookup_const dict tm =
let
val {Name, Thy, Ty} = dest_thy_const tm
in
Binarymap.peek (dict, mk_kn Thy Name)
end;
fun match_comp inst1 inst2 =
let
fun match_comp_one a_inst inst =
let
fun match_comp_one_acc (a_inst as ({redex=a_red, residue=a_res}))
inst acc1 acc2 =
case inst of
[] => (acc1, acc2)
| ({redex=red, residue=res}) :: rest =>
let
val r = ({redex=red, residue=type_subst [a_inst] res})
in
if a_red = red then
match_comp_one_acc a_inst rest (r :: acc1)
(append (match_type a_res res) acc2)
else
match_comp_one_acc a_inst rest (r :: acc1) acc2
end
val (inst', to_comp) = match_comp_one_acc a_inst inst [] [];
in
case to_comp of
[] => a_inst :: inst'
| _ => foldl (uncurry match_comp_one) inst' to_comp
end
in
foldl (uncurry match_comp_one) inst2 inst1
end
(*
fun translate dict tm =
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 => tm
| SOME (key_type, tm') =>
let
val inst = match_type key_type Ty
val {Name=name', Thy=thy', Ty=ty'} = dest_thy_const tm'
in
mk_thy_const {Name=name', Thy=thy', Ty=(type_subst inst ty')}
end
end
else if is_comb tm then
let
val (head, args) = strip_comb tm
val (hdtm, _) = translate_e dict head
(* need different translation? *)
val tys = strip_type_n (type_of hdtm) (length args)
val hd_inst = match_type (last tys) expty'
val hdtm' = Term.inst hd_inst hdtm
val exptyl = take (strip_type_n (type_of hdtm') (length args), (length args))
val args' = map (#1 o (uncurry (translate_e dict))) (zip args (map SOME exptyl))
(* Need to generalize the args type and also updating the inst? *)
in
end;
fun translate_e dict tm expty =
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 => (
case expty of
NONE =>
let
val tm0 = prim_mk_const {Thy = Thy, Name = Name}
val ty0 = inst_type_var (type_of tm0)
val poly_inst = match_type (type_of tm) ty0
in
(Term.inst poly_inst tm, [])
end
| SOME expty' =>
let
val tm0 = prim_mk_const {Thy = Thy, Name = Name}
val ty0 = inst_type_var (type_of tm0)
val poly_inst = match_type (type_of tm) ty0
val inst = match_type ty0 expty'
in
(Term.inst poly_inst tm, inst)
end)
| SOME (key_type, tm') => (
case expty of
NONE =>
let
val ty0 = inst_type_var (type_of tm')
val poly_inst = match_type (type_of tm') ty0
in
(Term.inst poly_inst tm', [])
end
| SOME expty' =>
let
val ty0 = inst_type_var (type_of tm')
val poly_inst = match_type (type_of tm') ty0
val inst = match_type ty0 expty'
in
(Term.inst poly_inst tm', inst)
end)
end
else if is_comb tm then
case expty of
NONE => failwith "Unimplemented"
| SOME expty' =>
let
val (head, args) = strip_comb tm
val (hdtm, _) = translate_e dict head NONE
(* need different translation? *)
val tys = strip_type_n (type_of hdtm) (length args)
val hd_inst = match_type (last tys) expty'
val hdtm' = Term.inst hd_inst hdtm
val exptyl = take (strip_type_n (type_of hdtm') (length args), (length args))
val args' = map (#1 o (uncurry (translate_e dict))) (zip args (map SOME exptyl))
(* Need to generalize the args type and also updating the inst? *)
in
(list_mk_comb (hdtm, args'), hd_inst)
end
else
failwith "Unimplemented";
*)
fun translate_e dict tm expty =
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 =>
let
val tm0 = prim_mk_const {Thy = Thy, Name = Name}
val ty0 = inst_type_var (type_of tm0)
val poly_inst = match_type (type_of tm) ty0
val inst = match_type expty ty0
in
(Term.inst poly_inst 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
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
fun do_args (acc1 as (tm, inst)) acc2 type_ref args =
case args of
[] => (acc1, acc2)
| 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 tm' = Term.inst a_inst tm
val type_ref' = type_subst new_inst drest
*)
in
do_args (tm,new_inst) (a1'::acc2) drest rest
end
val ((_, inst) , args') = do_args (hdtm, inst0) [] (type_of hdtm) 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 int_translate dict tm = #1 (translate_e dict tm (gen_tyvar ()));
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