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