helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4 type result =
   5   | Failure
   6   | Success of Cic.term option * environment
   7 ;;
   8
   9
  10 type equality_sign = Negative | Positive;;
  11
  12 let string_of_sign = function
  13   | Negative -> "Negative"
  14   | Positive -> "Positive"
  15 ;;
  16
  17
  18 module OrderedEquality =
  19 struct
  20   type t = Inference.equality
  21
  22   let compare eq1 eq2 =
  23     match meta_convertibility_eq eq1 eq2 with
  24     | true -> 0
  25     | false -> Pervasives.compare eq1 eq2
  26 end
  27
  28 module EqualitySet = Set.Make(OrderedEquality);;
  29
  30
  31
  32 let select env passive =
  33   match passive with
  34   | hd::tl, pos -> (Negative, hd), (tl, pos)
  35   | [], hd::tl -> (Positive, hd), ([], tl)
  36   | _, _ -> assert false
  37 ;;
  38
  39
  40 (*
  41 let select env passive =
  42   match passive with
  43   | neg, pos when EqualitySet.is_empty neg ->
  44       let elem = EqualitySet.min_elt pos in
  45       (Positive, elem), (neg, EqualitySet.remove elem pos)
  46   | neg, pos ->
  47       let elem = EqualitySet.min_elt neg in
  48       (Negative, elem), (EqualitySet.remove elem neg, pos)
  49 ;;
  50 *)
  51
  52
  53 (* TODO: find a better way! *)
  54 let maxmeta = ref 0;;
  55
  56 let infer env sign current active =
  57   let rec infer_negative current = function
  58     | [] -> [], []
  59     | (Negative, _)::tl -> infer_negative current tl
  60     | (Positive, equality)::tl ->
  61         let res = superposition_left env current equality in
  62         let neg, pos = infer_negative current tl in
  63         res @ neg, pos
  64
  65   and infer_positive current = function
  66     | [] -> [], []
  67     | (Negative, equality)::tl ->
  68         let res = superposition_left env equality current in
  69         let neg, pos = infer_positive current tl in
  70         res @ neg, pos
  71     | (Positive, equality)::tl ->
  72         let maxm, res = superposition_right !maxmeta env current equality in
  73         let maxm, res' = superposition_right maxm env equality current in
  74         maxmeta := maxm;
  75         let neg, pos = infer_positive current tl in
  76
  77 (*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
  78 (*           (string_of_equality ~env current) (string_of_equality ~env equality) *)
  79 (*           (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
  80 (*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
  81 (*           (string_of_equality ~env equality) (string_of_equality ~env current) *)
  82 (*           (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
  83
  84         neg, res @ res' @ pos
  85   in
  86   match sign with
  87   | Negative -> infer_negative current active
  88   | Positive -> infer_positive current active
  89 ;;
  90
  91
  92 let contains_empty env (negative, positive) =
  93   let metasenv, context, ugraph = env in
  94   try
  95     let (proof, _, _, _) =
  96       List.find
  97         (fun (proof, (ty, left, right), m, a) ->
  98            fst (CicReduction.are_convertible context left right ugraph))
  99         negative
 100     in
 101     true, Some proof
 102   with Not_found ->
 103     false, None
 104 ;;
 105
 106
 107 let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
 108   let find sign eq1 eq2 =
 109     if meta_convertibility_eq eq1 eq2 then (
 110 (*       Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *)
 111 (*         (string_of_sign sign) (string_of_equality eq1); *)
 112       true
 113     ) else
 114       false
 115   in
 116   let ok sign equalities equality =
 117     not (List.exists (find sign equality) equalities)
 118   in
 119   let neg = List.filter (ok Negative passive_neg) new_neg in
 120   let pos = List.filter (ok Positive passive_pos) new_pos in
 121 (*   let neg, pos = new_neg, new_pos in *)
 122   (neg @ passive_neg, passive_pos @ pos)
 123 ;;
 124
 125
 126 let is_identity ((_, context, ugraph) as env) = function
 127   | ((_, (ty, left, right), _, _) as equality) ->
 128       let res =
 129         (left = right ||
 130             (fst (CicReduction.are_convertible context left right ugraph)))
 131       in
 132 (*       if res then ( *)
 133 (*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
 134 (*         print_newline (); *)
 135 (*       ); *)
 136       res
 137 ;;
 138
 139
 140 let forward_simplify env (sign, current) active =
 141 (*   if sign = Negative then *)
 142 (*     Some (sign, current) *)
 143 (*   else *)
 144     let rec aux env (sign, current) =
 145       function
 146         | [] -> Some (sign, current)
 147         | (Negative, _)::tl -> aux env (sign, current) tl
 148         | (Positive, equality)::tl ->
 149             let newmeta, current = demodulation !maxmeta env current equality in
 150             maxmeta := newmeta;
 151             if is_identity env current then
 152               None
 153             else
 154               aux env (sign, current) tl
 155     in
 156     aux env (sign, current) active
 157 ;;
 158
 159
 160 let forward_simplify_new env (new_neg, new_pos) active =
 161   let remove_identities equalities =
 162     let ok eq = not (is_identity env eq) in
 163     List.filter ok equalities
 164   in
 165   let rec simpl active target =
 166     match active with
 167     | [] -> target
 168     | (Negative, _)::tl -> simpl tl target
 169     | (Positive, source)::tl ->
 170         let newmeta, target = demodulation !maxmeta env target source in
 171         maxmeta := newmeta;
 172         if is_identity env target then target
 173         else simpl tl target
 174   in
 175   let new_neg = List.map (simpl active) new_neg
 176   and new_pos = List.map (simpl active) new_pos in
 177   new_neg, remove_identities new_pos
 178 ;;
 179
 180
 181 let backward_simplify env (sign, current) active =
 182   match sign with
 183   | Negative -> active
 184   | Positive ->
 185       let active =
 186         List.map
 187           (fun (s, equality) ->
 188              (*            match s with *)
 189              (*            | Negative -> s, equality *)
 190              (*            | Positive -> *)
 191              let newmeta, equality =
 192                demodulation !maxmeta env equality current in
 193              maxmeta := newmeta;
 194              s, equality)
 195           active
 196       in
 197       let active =
 198         List.filter (fun (s, eq) -> not (is_identity env eq)) active
 199       in
 200       let find eq1 where =
 201         List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 202       in
 203       List.fold_right
 204         (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
 205         active []
 206 ;;
 207
 208
 209 (*
 210 let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) =
 211   let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in
 212   add_all passive_neg new_neg, add_all passive_pos new_pos
 213 ;;
 214 *)
 215
 216
 217 let rec given_clause env passive active =
 218   match passive with
 219 (*   | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *)
 220 (*       Failure *)
 221   | [], [] -> Failure
 222   | passive ->
 223 (*       Printf.printf "before select\n"; *)
 224       let (sign, current), passive = select env passive in
 225 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 226 (*         (string_of_sign sign) (string_of_equality ~env current); *)
 227       match forward_simplify env (sign, current) active with
 228       | None when sign = Negative ->
 229           Printf.printf "OK!!! %s %s" (string_of_sign sign)
 230             (string_of_equality ~env current);
 231           print_newline ();
 232           let proof, _, _, _ = current in
 233           Success (Some proof, env)
 234       | None ->
 235           Printf.printf "avanti... %s %s" (string_of_sign sign)
 236             (string_of_equality ~env current);
 237           print_newline ();
 238           given_clause env passive active
 239       | Some (sign, current) ->
 240 (*           Printf.printf "sign: %s\ncurrent: %s\n" *)
 241 (*             (string_of_sign sign) (string_of_equality ~env current); *)
 242 (*           print_newline (); *)
 243
 244           let new' = infer env sign current active in
 245
 246           let active =
 247             backward_simplify env (sign, current) active
 248 (*             match new' with *)
 249 (*             | [], [] -> backward_simplify env (sign, current) active *)
 250 (*             | _ -> active *)
 251           in
 252
 253           let new' = forward_simplify_new env new' active in
 254
 255           print_endline "\n================================================";
 256           let _ =
 257             Printf.printf "active:\n%s\n"
 258               (String.concat "\n"
 259                  ((List.map
 260                      (fun (s, e) -> (string_of_sign s) ^ " " ^
 261                         (string_of_equality ~env e)) active)));
 262             print_newline ();
 263           in
 264 (*           let _ = *)
 265 (*             match new' with *)
 266 (*             | neg, pos -> *)
 267 (*                 Printf.printf "new':\n%s\n" *)
 268 (*                   (String.concat "\n" *)
 269 (*                      ((List.map *)
 270 (*                          (fun e -> "Negative " ^ *)
 271 (*                             (string_of_equality ~env e)) neg) @ *)
 272 (*                         (List.map *)
 273 (*                            (fun e -> "Positive " ^ *)
 274 (*                               (string_of_equality ~env e)) pos))); *)
 275 (*                 print_newline (); *)
 276 (*           in                 *)
 277           match contains_empty env new' with
 278           | false, _ ->
 279               let active =
 280                 match sign with
 281                 | Negative -> (sign, current)::active
 282                 | Positive -> active @ [(sign, current)]
 283               in
 284               let passive = add_to_passive passive new' in
 285               given_clause env passive active
 286           | true, proof ->
 287               Success (proof, env)
 288 ;;
 289
 290
 291 let get_from_user () =
 292   let dbd = Mysql.quick_connect
 293     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 294   let rec get () =
 295     match read_line () with
 296     | "" -> []
 297     | t -> t::(get ())
 298   in
 299   let term_string = String.concat "\n" (get ()) in
 300   let env, metasenv, term, ugraph =
 301     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 302   in
 303   term, metasenv, ugraph
 304 ;;
 305
 306
 307 let main () =
 308   let module C = Cic in
 309   let module T = CicTypeChecker in
 310   let module PET = ProofEngineTypes in
 311   let module PP = CicPp in
 312   let term, metasenv, ugraph = get_from_user () in
 313   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 314   let proof, goals =
 315     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 316   let goal = List.nth goals 0 in
 317   let _, metasenv, meta_proof, _ = proof in
 318   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 319   let equalities, maxm = find_equalities context proof in
 320   maxmeta := maxm; (* TODO ugly!! *)
 321   let env = (metasenv, context, ugraph) in
 322   try
 323     let term_equality = equality_of_term meta_proof goal in
 324     let meta_proof, (eq_ty, left, right), _, _ = term_equality in
 325     let active = [] in
 326 (*     let passive = *)
 327 (*       (EqualitySet.singleton term_equality, *)
 328 (*        List.fold_left *)
 329 (*          (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *)
 330 (*     in *)
 331     let passive = [term_equality], equalities in
 332     Printf.printf "\ncurrent goal: %s ={%s} %s\n"
 333       (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
 334     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 335     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 336     Printf.printf "\nequalities:\n";
 337     List.iter
 338       (function (_, (ty, t1, t2), _, _) ->
 339          let w1 = weight_of_term t1 in
 340          let w2 = weight_of_term t2 in
 341          let res = nonrec_kbo t1 t2 in
 342          Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
 343            (PP.ppterm t1) (string_of_weight w1)
 344            (string_of_comparison res)
 345            (PP.ppterm t2) (string_of_weight w2))
 346       equalities;
 347     print_endline "--------------------------------------------------";
 348     let start = Sys.time () in
 349     print_endline "GO!";
 350     let res = given_clause env passive active in
 351     let finish = Sys.time () in
 352     match res with
 353     | Failure ->
 354         Printf.printf "NO proof found! :-(\n\n"
 355     | Success (Some proof, env) ->
 356         Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
 357           (finish -. start);
 358     | Success (None, env) ->
 359         Printf.printf "Success, but no proof?!?\n\n"
 360   with exc ->
 361     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 362 ;;
 363
 364
 365 let _ =
 366   let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in
 367   Helm_registry.load_from configuration_file
 368 in
 369 main ()