From cb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Jul 2005 10:26:24 +0000 Subject: [PATCH] the decompose tactic is now working --- helm/matita/matita.ma.templ | 2 +- helm/matita/matitaEngine.ml | 25 ++- helm/matita/tests/fguidi.ma | 8 +- helm/ocaml/cic_notation/grafiteAst.ml | 6 +- helm/ocaml/cic_notation/grafiteAstPp.ml | 11 +- helm/ocaml/cic_notation/grafiteParser.ml | 9 +- helm/ocaml/cic_transformations/tacticAst.ml | 6 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 11 +- helm/ocaml/tactics/eliminationTactics.ml | 192 ++++++++++-------- helm/ocaml/tactics/eliminationTactics.mli | 9 +- helm/ocaml/tactics/fwdSimplTactic.ml | 26 +-- helm/ocaml/tactics/metadataQuery.ml | 18 +- helm/ocaml/tactics/metadataQuery.mli | 1 + helm/ocaml/tactics/proofEngineHelpers.ml | 10 + helm/ocaml/tactics/proofEngineHelpers.mli | 4 + helm/ocaml/tactics/tactics.mli | 10 +- 16 files changed, 214 insertions(+), 134 deletions(-) diff --git a/helm/matita/matita.ma.templ b/helm/matita/matita.ma.templ index 4fa107ce0..6852ad0c9 100644 --- a/helm/matita/matita.ma.templ +++ b/helm/matita/matita.ma.templ @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index aff9144cc..9fc24acf1 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -68,7 +68,15 @@ let tactic_of_ast = function let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | GrafiteAst.DecideEquality _ -> Tactics.decide_equality - | GrafiteAst.Decompose (_,term) -> Tactics.decompose term + | GrafiteAst.Decompose (_, types, what, names) -> + let to_type = function + | GrafiteAst.Type (uri, typeno) -> uri, typeno + | GrafiteAst.Ident _ -> assert false + in + let user_types = List.rev_map to_type types in + let dbd = MatitaDb.instance () in + let mk_fresh_name_callback = namer_of names in + Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term | GrafiteAst.Elim (_, what, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what @@ -185,9 +193,18 @@ let disambiguate_tactic status = function status, GrafiteAst.Cut (loc, ident, cic) | GrafiteAst.DecideEquality loc -> status, GrafiteAst.DecideEquality loc - | GrafiteAst.Decompose (loc,term) -> - let status,term = disambiguate_term status term in - status, GrafiteAst.Decompose(loc,term) + | GrafiteAst.Decompose (loc, types, what, names) -> + let disambiguate (status, types) = function + | GrafiteAst.Type _ -> assert false + | GrafiteAst.Ident id -> + match disambiguate_term status (CicNotationPt.Ident (id, None)) with + | status, Cic.MutInd (uri, tyno, _) -> + status, (GrafiteAst.Type (uri, tyno) :: types) + | _ -> + raise Disambiguate.NoWellTypedInterpretation + in + let status, types = List.fold_left disambiguate (status, []) types in + status, GrafiteAst.Decompose(loc, types, what, names) | GrafiteAst.Discriminate (loc,term) -> let status,term = disambiguate_term status term in status, GrafiteAst.Discriminate(loc,term) diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index 8958b250d..77d3b44bf 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -90,10 +90,10 @@ qed. theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)). intros. auto. qed. + (* theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). -intros 1. elim x. -clear x. auto. -clear H. fwd H1 [H]. decompose H. +intros 1. elim x; clear H. (* clear x *) +auto. +fwd H1 [H]. decompose H. *) - diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index a5c4db085..f15417fc8 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -30,6 +30,10 @@ type loc = CicNotationPt.location type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term +type ('term, 'ident) type_spec = + | Ident of 'ident + | Type of UriManager.uri * int + type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term @@ -43,7 +47,7 @@ type ('term, 'ident) tactic = | Contradiction of loc | Cut of loc * 'ident option * 'term | DecideEquality of loc - | Decompose of loc * 'term + | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list | Discriminate of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list | ElimType of loc * 'term * 'term option * int option * 'ident list diff --git a/helm/ocaml/cic_notation/grafiteAstPp.ml b/helm/ocaml/cic_notation/grafiteAstPp.ml index 029152e36..6af1efd71 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.ml +++ b/helm/ocaml/cic_notation/grafiteAstPp.ml @@ -78,8 +78,15 @@ let rec pp_tactic = function "cut " ^ pp_term_ast term ^ (match ident with None -> "" | Some id -> " as " ^ id) | DecideEquality _ -> "decide equality" - | Decompose (_, term) -> - sprintf "decompose %s" (pp_term_ast term) + | Decompose (_, [], what, names) -> + sprintf "decompose %s%s" what (pp_intros_specs (None, names)) + | Decompose (_, types, what, names) -> + let to_ident = function + | Ident id -> id + | Type _ -> assert false + in + let types = List.rev_map to_ident types in + sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ pp_term_ast term ^ diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 908ad007f..cceeaf10d 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -125,8 +125,13 @@ EXTEND GrafiteAst.Cut (loc, ident, t) | IDENT "decide"; IDENT "equality" -> GrafiteAst.DecideEquality loc - | IDENT "decompose"; where = tactic_term -> - GrafiteAst.Decompose (loc, where) + | IDENT "decompose"; types = OPT ident_list0; what = IDENT; + OPT "names"; num = OPT [num = int -> num]; + idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + let types = match types with None -> [] | Some types -> types in + let to_spec id = GrafiteAst.Ident id in + GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) | IDENT "discriminate"; t = tactic_term -> GrafiteAst.Discriminate (loc, t) | IDENT "elim"; what = tactic_term; diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index e4f454ed6..48fbc4aa2 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -30,6 +30,10 @@ type loc = CicAst.location type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term +type ('term, 'ident) type_spec = + | Ident of 'ident + | Type of UriManager.uri * int + type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term @@ -43,7 +47,7 @@ type ('term, 'ident) tactic = | Contradiction of loc | Cut of loc * 'ident option * 'term | DecideEquality of loc - | Decompose of loc * 'term + | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list | Discriminate of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list | ElimType of loc * 'term * 'term option * int option * 'ident list diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 794e09e70..d8f54a49f 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -78,8 +78,15 @@ let rec pp_tactic = function "cut " ^ pp_term_ast term ^ (match ident with None -> "" | Some id -> " as " ^ id) | DecideEquality _ -> "decide equality" - | Decompose (_, term) -> - sprintf "decompose %s" (pp_term_ast term) + | Decompose (_, [], what, names) -> + sprintf "decompose %s%s" what (pp_intros_specs (None, names)) + | Decompose (_, types, what, names) -> + let to_ident = function + | Ident id -> id + | Type _ -> assert false + in + let types = List.rev_map to_ident types in + sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names)) | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ pp_term_ast term ^ diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index e52fff6e4..96dc5d15a 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -23,18 +23,14 @@ * http://cs.unibo.it/helm/. *) -(** DEBUGGING *) - - (** perform debugging output? *) -let debug = false -let debug_print = fun _ -> () - - (** debugging print *) -let warn s = - if debug then - debug_print ("DECOMPOSE: " ^ s) - - +module C = Cic +module P = PrimitiveTactics +module T = Tacticals +module S = ProofEngineStructuralRules +module F = FreshNamesGenerator +module E = ProofEngineTypes +module H = ProofEngineHelpers +module Q = MetadataQuery (* let induction_tac ~term status = @@ -57,81 +53,113 @@ let induction_tac ~term status = ;; *) -let elim_type_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) +(* unexported tactics *******************************************************) + +let get_name context index = + try match List.nth context (pred index) with + | Some (Cic.Name name, _) -> Some name + | _ -> None + with Invalid_argument "List.nth" -> None + +let rec scan_tac ~old_context_length ~index ~tactic = + let scan_tac status = + let (proof, goal) = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let context_length = List.length context in + let rec aux index = + match get_name context index with + | _ when index <= 0 -> (proof, [goal]) + | None -> aux (pred index) + | Some what -> + let tac = T.then_ ~start:(tactic ~what) + ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic) + in + try E.apply_tactic tac status + with E.Fail _ -> aux (pred index) + in aux (index + context_length - old_context_length - 1) + in + E.mk_tactic scan_tac + +let rec check_inductive_types types = function + | C.MutInd (uri, typeno, _) -> List.mem (uri, typeno) types + | C.Appl (hd :: tl) -> check_inductive_types types hd + | _ -> false + +let elim_clear_tac ~mk_fresh_name_callback ~types ~what = + let elim_clear_tac status = + let (proof, goal) = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let index, ty = H.lookup_type metasenv context what in + if check_inductive_types types ty then + let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) + ~continuation:(S.clear what) + in + E.apply_tactic tac status + else raise (E.Fail "unexported elim_clear: not an eliminable type") + in + E.mk_tactic elim_clear_tac + +(* elim type ****************************************************************) + +let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth ?using what = - let elim_type_tac status = - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - ProofEngineTypes.apply_tactic - (T.thens - ~start: (P.cut_tac what) - ~continuations:[ P.elim_intros_simpl_tac ?depth ?using ~mk_fresh_name_callback (C.Rel 1) ; T.id_tac ]) - status - in - ProofEngineTypes.mk_tactic elim_type_tac -;; + let elim what = P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what in + let elim_type_tac status = + let tac = T.thens ~start: (P.cut_tac what) + ~continuations:[elim (C.Rel 1); T.id_tac] + in + E.apply_tactic tac status + in + E.mk_tactic elim_type_tac +(* decompose ****************************************************************) -(* Decompose related stuff *) +(* robaglia --------------------------------------------------------------- *) -exception InteractiveUserUriChoiceNotRegistered + (** perform debugging output? *) +let debug = false +let debug_print = fun _ -> () -let interactive_user_uri_choice = - (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) : - (selection_mode:[`SINGLE | `EXTENDED] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - title:string -> msg:string -> string list -> string list) ref) -;; + (** debugging print *) +let warn s = + if debug then + debug_print ("DECOMPOSE: " ^ s) -let decompose_tac ?(uris_choice_callback=(function l -> l)) term = - let decompose_tac uris_choice_callback term status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let old_context_len = List.length context in - let termty,_ = - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let rec make_list termty = - (* N.B.: altamente inefficente? *) - let rec search_inductive_types urilist termty = - (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) - match termty with - (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> - (uri,typeno,exp_named_subst)::urilist - | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> - (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) - | _ -> urilist - (* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) - in - let rec purge_duplicates urilist = - let rec aux triple urilist = - match urilist with - [] -> [] - | hd::tl -> - if (hd = triple) - then aux triple tl - else hd::(aux triple tl) - in - match urilist with - [] -> [] - | hd::tl -> hd::(purge_duplicates (aux hd tl)) - in - purge_duplicates (search_inductive_types [] termty) +(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) +let search_inductive_types ty = + let rec aux types = function + | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> + (uri, typeno) :: types + | C.Appl applist -> List.fold_left aux types applist + | _ -> types + in + aux [] ty +(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) + +(* roba seria ------------------------------------------------------------- *) + +let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) + ?(user_types=[]) ~dbd what = + let decompose_tac status = + let (proof, goal) = status in + let _, metasenv,_,_ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let types = List.rev_append user_types (Q.decomposables dbd) in + let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in + let old_context_length = List.length context in + let tac = T.then_ ~start:(tactic ~what) + ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic) in + E.apply_tactic tac status + in + E.mk_tactic decompose_tac + +(* +module R = CicReduction - let urilist = - (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *) - (* N.B.: due to a bug in uris_choice_callback exp_named_subst are not significant (they all are []) *) - uris_choice_callback (make_list termty) in - - let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status = + let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status = let (proof, goal) = status in warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); if nr_of_hyp_still_to_elim <> 0 then @@ -184,8 +212,4 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = in elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status - in - ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term) -;; - - +*) diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli index 111bc5747..5074f8134 100644 --- a/helm/ocaml/tactics/eliminationTactics.mli +++ b/helm/ocaml/tactics/eliminationTactics.mli @@ -27,10 +27,7 @@ val elim_type_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic -(* The default callback always decomposes the term as much as possible *) val decompose_tac: - ?uris_choice_callback: - ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list -> - (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) -> - Cic.term -> - ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?user_types:((UriManager.uri * int) list) -> + dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 57c980513..bd2ac9fde 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -23,9 +23,8 @@ * http://cs.unibo.it/helm/. *) -(* + module PEH = ProofEngineHelpers -*) module U = CicUniv module TC = CicTypeChecker module PET = ProofEngineTypes @@ -37,7 +36,6 @@ module MI = CicMkImplicit module PESR = ProofEngineStructuralRules let fail_msg0 = "unexported clearbody: invalid argument" -let fail_msg1 = "fwd: argument is not premise in the current goal" let fail_msg2 = "fwd: no applicable simplification" let error msg = raise (PET.Fail msg) @@ -106,7 +104,9 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in let lemma = FNG.clean_dummy_dependent_types lemma in let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in - let conclusion = Cic.Appl (what :: List.rev metas) in + let conclusion = + match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas) + in let tac = T.thens ~start:(letin_tac conclusion) ~continuations:[clearbody ~index:1] in @@ -122,20 +122,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub (* fwd **********************************************************************) let fwd_simpl_tac - ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - ~dbd hyp - = - let find_type metasenv context = - let rec aux p = function - | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t - | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> - p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph) - | _ :: tail -> aux (succ p) tail - | [] -> error fail_msg1 - in - aux 1 context - in + ?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[]) + ~dbd hyp = let lapply_tac to_what lemma = lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma in @@ -143,7 +131,7 @@ let fwd_simpl_tac let (proof, goal) = status in let _, metasenv, _, _ = proof in let _, context, ty = CicUtil.lookup_meta goal metasenv in - let index, major = find_type metasenv context in + let index, major = PEH.lookup_type metasenv context hyp in match MetadataQuery.fwd_simpl ~dbd major with | [] -> error fail_msg2 | uri :: _ -> diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 160e2ff08..9355dfc10 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -581,7 +581,23 @@ let fwd_simpl ~dbd t = (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 + +(* 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 diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 08ac016bf..b2bd57bf3 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -66,3 +66,4 @@ val instance: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list +val decomposables: dbd:Mysql.dbd -> (UriManager.uri * int) list diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 712d8ba58..ae6c7ef50 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -607,3 +607,13 @@ let saturate_term newmeta metasenv context ty = let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in res,metasenv @ newmetasenv,arguments,lastmeta +let lookup_type metasenv context hyp = + let rec aux p = function + | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t + | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t + | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> + p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph) + | _ :: tail -> aux (succ p) tail + | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal") + in + aux 1 context diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index b77fd88ac..013d6292a 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -88,3 +88,7 @@ val select: val saturate_term: int -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term * Cic.metasenv * Cic.term list * int + +(* returns the index and the type of a premise in a context *) +val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term + diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index ff888d78b..5baeeb33c 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -17,13 +17,9 @@ val cut : Cic.term -> ProofEngineTypes.tactic val decide_equality : ProofEngineTypes.tactic val decompose : - ?uris_choice_callback:((UriManager.uri * int * - (UriManager.uri * Cic.term) list) - list -> - (UriManager.uri * int * - (UriManager.uri * Cic.term) list) - list) -> - Cic.term -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + ?user_types:(UriManager.uri * int) list -> + dbd:Mysql.dbd -> string -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> -- 2.39.2