ocaml/andrea5.ml

   1 (* percorsi di differenza etc. *)\r
   2 \r
   3 open Lambda3;;\r
   4 \r
   5 type formula =\r
   6   | Var of int\r
   7   | And of formula * formula\r
   8   | Or of formula * formula\r
   9 ;;\r
  10 \r
  11 let rec mk_k_vars k =\r
  12   if k = 0 then []\r
  13   else `Var (k-1) :: (mk_k_vars (k-1))\r
  14 ;;\r
  15 \r
  16 let is_lambda = function\r
  17   | `Lam _ -> true\r
  18   | _ -> false\r
  19 ;;\r
  20 \r
  21 let rec diff k level t1 t2 =\r
  22   if is_lambda t1 || is_lambda t2\r
  23   then let vars = mk_k_vars k in\r
  24        let level = level + k in\r
  25        diff k level (mk_appl (lift k t1) vars) (mk_appl (lift k t2) vars)\r
  26   else assert false\r
  27 ;;\r