1027 *}

  1028 

  1029 (*

  1030 ML {*

  1031   fun patunif_in_emptyenv (t, u) =

  1032     let

  1033       val init = Envir.empty 0;

  1034       val env = Pattern.unify @{theory} (t, u) init;

  1035     in

  1036       (env |> Envir.term_env |> Vartab.dest,

  1037        env |> Envir.type_env |> Vartab.dest)

  1038     end

  1039 *}

  1040 

  1041 text {*

  1042 @{ML_response [display, gray]

  1043  "val t1 = @{term_pat \"(% x y. ?f y x)\"};

  1044  val u1 = @{term_pat \"z::bool\"};

  1045    (* type conflict isnt noticed *)

  1046  patunif_in_emptyenv (t1, u1);"

  1047  "check missing"

  1048 *}

  1049 @{ML_response [display, gray] 

  1050  "val t2 = @{term_pat \"(% y. ?f y)\"} |> Term.strip_abs_body;

  1051  val u2 = @{term_pat \"z::bool\"};

  1052    (* fails because of loose bounds *)

  1053  (* patunif_in_emptyenv (t2, u2) *)"

  1054  "check missing"

  1055 *}

  1056 @{ML_response [display, gray]

  1057  "val t3 = @{term_pat \"(% y. plu (?f y) (% x. g x))\"};

  1058  val u3 = @{term_pat \"(% y. plu y (% x. g x))\"};

  1059    (* eta redexe im term egal, hidden polym wird inst *)

  1060  patunif_in_emptyenv (t3, u3)"

  1061  "check missing"

  1062 *}

  1063 @{ML_response [display, gray] 

  1064  "val t4 = @{term_pat \"(% y. plu (?f y) ((% x. g x) k))\"};

  1065  val u4 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};

  1066    (* beta redexe are largely ignored, hidden polymorphism is instantiated *)

  1067  patunif_in_emptyenv (t4, u4)"

  1068  "check missing"

  1069 *}

  1070 @{ML_response [display, gray]

  1071  "val t5 = @{term_pat \"(% y. plu ((% x. ?f) y) ((% x. g x) k))\"};

  1072  val u5 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};

  1073    (* fails: can't have beta redexes which seperate a var from its arguments *)

  1074  (* patunif_in_emptyenv (t5, u5) *)"

  1075 *}

  1076 

  1077 @{ML_response [display, gray] 

  1078  "val t6 = @{term_pat \"(% x y. ?f x y) a b\"};

  1079  val u6 = @{term_pat \"c\"};

  1080  (* Pattern.pattern assumes argument is beta-normal *)

  1081  Pattern.pattern t6; 

  1082    (* fails: can't have beta redexes which seperate a var from its arguments,

  1083        otherwise this would be general unification for general a,b,c *)

  1084  (* patunif_in_emptyenv (t6, u6) *)"

  1085 *}

  1086 @{ML_response [display, gray]

  1087  "val t7 = @{term_pat \"(% y. plu ((% x. ?f x) y) ((% x. g x) k))\"};

  1088  val u7 = @{term_pat \"(% y. plu y ((% x. g x) k))\"};

  1089    (* eta redexe die Pattern trennen brauchen nicht normalisiert sein *)

  1090  patunif_in_emptyenv (t7, u7)"

  1091 *}

  1092 @{ML_response [display, gray] 

  1093  "val t8 = @{term_pat \"(% y. ?f y)\"};

  1094  val u8 = @{term_pat \"(% y. y ?f)\"};

  1095    (* variables of the same name are identified *)

  1096  (* patunif_in_emptyenv (t8, u8) *)"

  1097 *}

  1098 

  1099 @{ML_response [display, gray]

  1100  "val t9 = @{term_pat \"(% y. ?f y)\"};

  1101  val u9 = @{term_pat \"(% y. ?f y)\"};

  1102    (* trivial solutions are empty and don't contain ?f = ?f etc *)

  1103  patunif_in_emptyenv (t9, u9)"

  1104 *}

  1105 @{ML_response [display, gray] 

  1106  "val t10 = @{term_pat \"(% y. (% x. ?f x) y)\"};

  1107  val u10 = @{term_pat \"(% y. ?f y)\"};

  1108    (* trivial solutions are empty and don't contain ?f = ?f etc *)

  1109  patunif_in_emptyenv (t10, u10)"

  1110 *}

  1111 @{ML_response [display, gray]

  1112  "val t11 = @{term_pat \"(% z. ?f z)\"};

  1113  val u11 = @{term_pat \"(% z. k (?f z))\"};

  1114    (* fails: occurs check *)

  1115  (* patunif_in_emptyenv (t11, u11) *)"

  1116 *}

  1117 @{ML_response [display, gray]

  1118  "val t12 = @{term_pat \"(% z. ?f z)\"};

  1119  val u12 = @{term_pat \"?g a\"};

  1120    (* fails: *both* terme have to be higher-order patterns *)

  1121  (* patunif_in_emptyenv (t12, u12) *)"

  1122 *}

  1123 *}

  1124 *)

  1125 

  1126 text {*