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

Commit 8a091fe1 authored by Alexander Soen's avatar Alexander Soen
Browse files

Fix bug for vars in comb arguments

parent 52d6d61b
......@@ -293,8 +293,12 @@ fun match_comp inst1 inst2 =
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)
if can (match_type a_res) res 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)
(append (match_type res a_res) acc2)
else
match_comp_one_acc a_inst rest (r :: acc1) acc2
end
......@@ -306,7 +310,7 @@ fun match_comp inst1 inst2 =
end
in
foldl (uncurry match_comp_one) inst2 inst1
end
end;
(*
......@@ -435,22 +439,24 @@ fun translate_e dict tm expty =
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 =
fun do_args inst' acc type_ref args =
case args of
[] => (acc1, acc2)
[] => (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 new_inst = match_comp a_inst inst'
(*
val tm' = Term.inst a_inst tm
val type_ref' = type_subst new_inst drest
val inst' = new_inst
val acc = a1' :: acc
val type_ref = drest
val (a1::rest) = rest
*)
in
do_args (tm,new_inst) (a1'::acc2) drest rest
do_args new_inst (a1'::acc) drest rest
end
val ((_, inst) , args') = do_args (hdtm, inst0) [] (type_of hdtm) args
val (inst, args') = do_args inst0 [] (type_of hdtm) args
in
(list_mk_comb (Term.inst inst hdtm, map (Term.inst inst) (rev args')), inst)
end
......
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