From fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 12 Jul 2005 14:54:18 +0000 Subject: [PATCH] Added a function equations_for_goal similar to signature_of_goal. --- helm/ocaml/tactics/metadataQuery.ml | 44 ++++++++++++++++++++++++++++ helm/ocaml/tactics/metadataQuery.mli | 3 ++ 2 files changed, 47 insertions(+) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index a01044e8c..160e2ff08 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -28,6 +28,8 @@ open Printf 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 @@ -195,6 +197,28 @@ let close_with_types s metasenv context = 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 @@ -225,6 +249,26 @@ let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as 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 diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index c4b844537..08ac016bf 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -31,6 +31,9 @@ val signature_of_goal: dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list +val equations_for_goal: + dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list + val locate: dbd:Mysql.dbd -> ?vars:bool -> string -> UriManager.uri list -- 2.39.2