863 only returns a single matching -- since terms are linear, and variable arguments are Vars, order shouldn't matter, so we can ignore permutations. |
863 only returns a single matching -- since terms are linear, and variable arguments are Vars, order shouldn't matter, so we can ignore permutations. |
864 doesn't work with polymorphism (for which we'd need to use type unification) -- this is OK since no terms should be polymorphic, since Leo2 proofs aren't. |
864 doesn't work with polymorphism (for which we'd need to use type unification) -- this is OK since no terms should be polymorphic, since Leo2 proofs aren't. |
865 *) |
865 *) |
866 fun use_candidate target_ty params acc cur_ty = |
866 fun use_candidate target_ty params acc cur_ty = |
867 if null params then |
867 if null params then |
868 if Type.eq_type Vartab.empty (cur_ty, target_ty) then |
868 if cur_ty = target_ty then |
869 SOME (rev acc) |
869 SOME (rev acc) |
870 else NONE |
870 else NONE |
871 else |
871 else |
872 let |
872 let |
873 val (arg_ty, val_ty) = Term.dest_funT cur_ty |
873 val (arg_ty, val_ty) = Term.dest_funT cur_ty |
874 (*now find a param of type arg_ty*) |
874 (*now find a param of type arg_ty*) |
875 val (candidate_param, params') = |
875 val (candidate_param, params') = |
876 find_and_remove |
876 find_and_remove (snd #> pair arg_ty #> op =) params |
877 (snd #> pair arg_ty #> Type.eq_type Vartab.empty) |
|
878 params |
|
879 in |
877 in |
880 use_candidate target_ty params' (candidate_param :: acc) val_ty |
878 use_candidate target_ty params' (candidate_param :: acc) val_ty |
881 end |
879 end |
882 handle TYPE ("dest_funT", _, _) => NONE |
880 handle TYPE ("dest_funT", _, _) => NONE |
883 | DEST_LIST => NONE |
881 | DEST_LIST => NONE |