1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 let get_parent id ids_to_terms ids_to_father_ids =
27 match Hashtbl.find ids_to_father_ids id with
29 | Some id -> Some (id, Hashtbl.find ids_to_terms id)
32 let get_context ids_to_terms ids_to_father_ids =
35 match get_parent id ids_to_terms ids_to_father_ids with
37 | Some (parentid,parent) ->
38 let term = Hashtbl.find ids_to_terms id in
47 | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
49 | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
51 | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
58 (*CSC: sbagliato: manca il when *)
60 let counter = ref 0 in
62 (function (name,_,ty,bo) ->
63 let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
68 let counter = ref 0 in
70 (function (name,ty,bo) ->
71 let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
76 binding@(aux parentid)
81 exception NotImplemented;;
83 (* A subterm is changed into a fresh meta *)
84 let to_sequent id ids_to_terms ids_to_father_ids =
85 let module P = ProofEngine in
86 let term = Hashtbl.find ids_to_terms id in
87 let context = get_context ids_to_terms ids_to_father_ids id in
91 | Some (_,metasenv,_,_) -> metasenv
93 let ty = CicTypeChecker.type_of_aux' metasenv context term in
94 P.perforate context term ty (* P.perforate also sets the goal *)
97 exception FocusOnlyOnMeta;;
99 (* If the current selection is a Meta, that Meta becomes the current goal *)
100 let focus id ids_to_terms ids_to_father_ids =
101 let module P = ProofEngine in
102 let term = Hashtbl.find ids_to_terms id in
103 let context = get_context ids_to_terms ids_to_father_ids id in
107 | Some (_,metasenv,_,_) -> metasenv
109 let ty = CicTypeChecker.type_of_aux' metasenv context term in
111 Cic.Meta (n,_) -> P.goal := Some n
112 | _ -> raise FocusOnlyOnMeta