;;
+let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker in
+ let candidates =
+ List.map
+ (fun uri ->
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ t, ty)
+ (MetadataQuery.equations_for_goal ~dbd status)
+ in
+ let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
+ and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
+ let iseq uri =
+ uri == eq_uri1 || uri == eq_uri2
+ in
+ let rec aux newmeta = function
+ | [] -> [], newmeta
+ | (term, termty)::tl ->
+ let res, newmeta =
+ match termty with
+ | C.Prod (name, s, t) ->
+ let head, newmetas, args, newmeta =
+ ProofEngineHelpers.saturate_term newmeta [] [] termty
+ in
+ let p =
+ if List.length args = 0 then
+ term
+ else
+ C.Appl (term::args)
+ in (
+ match head with
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ Printf.printf "OK: %s\n" (CicPp.ppterm term);
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ )
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+ let o = !Utils.compare_terms t1 t2 in
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+ Some e, (newmeta+1)
+ | _ -> None, newmeta
+ in
+ match res with
+ | Some e ->
+ let tl, newmeta' = aux newmeta tl in
+ e::tl, max newmeta newmeta'
+ | None ->
+ aux newmeta tl
+ in
+ aux maxmeta candidates
+;;
+
+
let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
let table = Hashtbl.create (List.length args) in
| hd::[] -> Some hd
| _ -> None
;;
+
+
;;
-let get_from_user () =
- let dbd = Mysql.quick_connect
- ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+let get_from_user ~(dbd:Mysql.dbd) =
let rec get () =
match read_line () with
| "" -> []
let module T = CicTypeChecker in
let module PET = ProofEngineTypes in
let module PP = CicPp in
- let term, metasenv, ugraph = get_from_user () in
+ let dbd = Mysql.quick_connect
+ ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+ let term, metasenv, ugraph = get_from_user ~dbd 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 _, metasenv, meta_proof, _ = proof in
let _, context, goal = CicUtil.lookup_meta goal' metasenv in
let equalities, maxm = find_equalities context proof in
+ let library_equalities, maxm =
+ find_library_equalities ~dbd (proof, goal') (maxm+1) 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 saturation_tactic status =
+ let module C = Cic in
+ let saturation_tac (proof, goal) =
+ maxmeta := 0;
+(* if List.length goals <> 1 then *)
+(* raise (ProofEngineTypes.Fail "There should be only one open goal"); *)
+
+(* let goal' = List.hd goals in *)
+ let goal' = goal in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ let equalities, maxm = find_equalities context proof in
+ maxmeta := maxm+2;
+ let new_meta_goal, metasenv, type_of_goal =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+ print_newline ();
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let ugraph = CicUniv.empty_ugraph in
+ let env = (metasenv, context, ugraph) in
+ try
+ let term_equality = equality_of_term new_meta_goal goal in
+(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
+ let active = make_active () in
+ let passive = make_passive [term_equality] equalities in
+ let res = given_clause_fullred env passive active in
+ match res with
+ | Success (Some goal, env) ->
+ Printf.printf "OK, found a proof!\n";
+ let proof = Inference.build_proof_term goal in
+ let names = names_of_context context in
+ print_endline (CicPp.pp proof names);
+ let newmetasenv =
+ let i1 =
+ match new_meta_goal with
+ | C.Meta (i, _) -> i | _ -> assert false
+ in
+ let i2 =
+ match meta_proof with
+ | C.Meta (i, _) -> i | _ -> assert false
+ in
+ List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv
+ in
+ let newstatus =
+ try
+ let ty, ug =
+ CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+ in
+ Printf.printf
+ "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+ (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+ (string_of_bool
+ (fst (CicReduction.are_convertible
+ context type_of_goal ty ug)));
+ ((uri, newmetasenv, proof, term_to_prove), [])
+ with e ->
+ raise (ProofEngineTypes.Fail
+ "Found a proof, but it doesn't typecheck")
+ in
+ newstatus
+ | _ ->
+ raise (ProofEngineTypes.Fail "NO proof found")
+ with e ->
+ raise (ProofEngineTypes.Fail "saturation failed")
+ in
+ ProofEngineTypes.mk_tactic saturation_tac
+;;
+
+
+
let configuration_file = ref "../../matita/matita.conf.xml";;
let _ =
]
] in
let ens = [
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
C.Rel 4);
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
C.Rel 3);
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
C.Rel 2);
] in
let term2 = C.Appl [
Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty);
;;
+
+let test_lib () =
+ let uri = Sys.argv.(1) in
+ let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
+ Printf.printf "type: %s\n" (CicPp.ppterm ty);
+;;
+
+
(* differing ();; *)
(* next_after ();; *)
(* discrimination_tree_test ();; *)
(* path_indexing_test ();; *)
(* test_subst ();; *)
Helm_registry.load_from "../../matita/matita.conf.xml";
-test_refl ();;
+(* test_refl ();; *)
+test_lib ();;
projects / helm.git / commitdiff