module Constr = MetadataConstraints
module PET = ProofEngineTypes
+exception Goal_is_not_an_equation
+
let debug_print = fun _ -> ()
(** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
+let close_with_constructors s metasenv context =
+ Constr.UriManagerSet.fold
+ (fun e bag ->
+ let t = CicUtil.term_of_uri e in
+ match t with
+ Cic.MutInd (uri,_,_)
+ | Cic.MutConstruct (uri,_,_,_) ->
+ (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ Cic.InductiveDefinition(tl,_,_,_) ->
+ snd
+ (List.fold_left
+ (fun (i,s) (_,_,_,cl) ->
+ let _,s =
+ List.fold_left
+ (fun (j,s) _ ->
+ let curi = UriManager.uri_of_uriref uri i (Some j) in
+ j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
+ (i+1,s)) (0,bag) tl)
+ | _ -> assert false)
+ | _ -> bag)
+ s s
+
let apply_tac_verbose =
let profiler = CicUtil.profile "apply_tac_verbose" in
fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
uris
+let equations_for_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+ let (_, metasenv, _, _) = proof in
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let main, sig_constants = Constr.signature_of ty in
+ match main with
+ None -> raise Goal_is_not_an_equation
+ | Some (m,l) ->
+ if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then
+ let set = signature_of_hypothesis context in
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let set = close_with_types set metasenv context in
+ let set = close_with_constructors set metasenv context in
+ let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+ else raise Goal_is_not_an_equation
+
let experimental_hint
~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
let debug_metadata = function
| None -> ()
| Some (outer, inners) ->
- let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n uri in
- Printf.eprintf "\n%s: %s\n" "fwd" outer;
+ let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in
+ Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer);
List.iter f inners; prerr_newline ()
let fwd_simpl ~dbd t =
let compare (_, x) (_, y) = compare x y in
let filter n (uri, rank) =
if rank > 0 then Some (UriManager.uri_of_string uri) else None
- in
- match get_metadata t with
+ in
+ let metadata = get_metadata t in debug_metadata metadata;
+ match metadata with
| None -> []
| Some (outer, inners) ->
let select = "source, h_inner, h_index" in
(Mysql.escape (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
let result = Mysql.exec dbd query in
- let lemmas = Mysql.map result ~f:(map inners) in
+ let lemmas = Mysql.map ~f:(map inners) result in
let ranked = List.fold_left rank [] lemmas in
let ordered = List.rev (List.fast_sort compare ranked) in
- map_filter filter 0 ordered
+ map_filter filter 0 ordered
+
+(* get_decomposables ********************************************************)
+
+let decomposables ~dbd =
+ let map row = match row.(0) with
+ | None -> None
+ | Some str ->
+ match CicUtil.term_of_uri (UriManager.uri_of_string str) with
+ | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno)
+ | _ ->
+ raise (UriManager.IllFormedUri str)
+ in
+ let select, from = "source", "decomposables" in
+ let query = Printf.sprintf "SELECT %s FROM %s" select from in
+ let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in
+ map_filter (fun _ x -> x) 0 decomposables