;;
+let rec saturate_equations env goal accept_fun passive active =
+ elapsed_time := Unix.gettimeofday () -. !start_time;
+ if !elapsed_time > !time_limit then
+ (active, passive)
+ else
+ let (sign, current), passive = select env [1, [goal]] passive active in
+ let res = forward_simplify env (sign, current) ~passive active in
+ match res with
+ | None ->
+ saturate_equations env goal accept_fun passive active
+ | Some (sign, current) ->
+ assert (sign = Positive);
+ debug_print
+ (lazy "\n================================================");
+ debug_print (lazy (Printf.sprintf "selected: %s %s"
+ (string_of_sign sign)
+ (string_of_equality ~env current)));
+ let new' = infer env sign current active in
+ let active =
+ if is_identity env current then active
+ else
+ let al, tbl = active in
+ al @ [(sign, current)], Indexing.index tbl current
+ in
+ let rec simplify new' active passive =
+ let new' = forward_simplify_new env new' ~passive active in
+ let active, passive, newa, retained =
+ backward_simplify env new' ~passive active in
+ match newa, retained with
+ | None, None -> active, passive, new'
+ | Some (n, p), None
+ | None, Some (n, p) ->
+ let nn, np = new' in
+ simplify (nn @ n, np @ p) active passive
+ | Some (n, p), Some (rn, rp) ->
+ let nn, np = new' in
+ simplify (nn @ n @ rn, np @ p @ rp) active passive
+ in
+ let active, passive, new' = simplify new' active passive in
+ let _ =
+ debug_print
+ (lazy
+ (Printf.sprintf "active:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active))))))
+ in
+ let _ =
+ match new' with
+ | neg, pos ->
+ debug_print
+ (lazy
+ (Printf.sprintf "new':\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
+ let new' = match new' with _, pos -> [], List.filter accept_fun pos in
+ let passive = add_to_passive passive new' in
+ saturate_equations env goal accept_fun passive active
+;;
+
+
+
let main dbd full term metasenv ugraph =
let module C = Cic in
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
;;
+
+
+let main_demod_equalities dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 in
+ let _, metasenv, meta_proof, _ = proof in
+ let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ let eq_indexes, equalities, maxm = find_equalities context proof in
+ let lib_eq_uris, library_equalities, maxm =
+ find_library_equalities dbd context (proof, goal') (maxm+2)
+ in
+ let library_equalities = List.map snd library_equalities in
+ maxmeta := maxm+2; (* TODO ugly!! *)
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let new_meta_goal, metasenv, type_of_goal =
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ debug_print
+ (lazy
+ (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+ (CicPp.ppterm ty)));
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let env = (metasenv, context, ugraph) in
+ let t1 = Unix.gettimeofday () in
+ try
+ let goal = Inference.BasicProof new_meta_goal, [], goal in
+ let equalities =
+ let equalities = equalities @ library_equalities in
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let active = others @ others_simpl in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ (Indexing.empty_table ()) active
+ in
+ let res = forward_simplify env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl (e::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+ in
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = List.map (fun e -> (Positive, e)) tl in
+ let res =
+ List.rev (List.map snd (simpl (Positive, hd) others []))
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res))));
+ res
+ in
+ let active = make_active () in
+ let passive = make_passive [] equalities in
+ Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
+ Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+ Printf.printf "\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env) equalities));
+ print_endline "--------------------------------------------------";
+ let start = Unix.gettimeofday () in
+ print_endline "GO!";
+ start_time := Unix.gettimeofday ();
+ if !time_limit < 1. then time_limit := 60.;
+ let ra, rp =
+ saturate_equations env goal (fun e -> true) passive active
+ in
+ let finish = Unix.gettimeofday () in
+ Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+ (String.concat "\n"
+ (List.map (fun (s, e) -> (string_of_equality ~env e)) (fst ra)))
+ (String.concat "\n"
+ (List.map (string_of_equality ~env)
+ (match rp with (n, _), (p, _), _ -> p)));
+ print_newline ();
+ with e ->
+ debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+;;
projects / helm.git / commitdiff