+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
let get_parent id ids_to_terms ids_to_father_ids =
match Hashtbl.find ids_to_father_ids id with
None -> None
;;
let get_context ids_to_terms ids_to_father_ids =
- let module P = ProofEngine in
let module C = Cic in
let rec aux id =
match get_parent id ids_to_terms ids_to_father_ids with
| C.Sort _
| C.Implicit
| C.Cast _ -> []
- | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Prod _ -> []
- | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
+ | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Lambda _ -> []
- | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
+ | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def s)]
| C.LetIn _ -> []
| C.Appl _
| C.Const _ -> []
- | C.Abst _ -> assert false
| C.MutInd _
| C.MutConstruct _
| C.MutCase _ -> []
let counter = ref 0 in
List.rev_map
(function (name,_,ty,bo) ->
- let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
+ let res = Some (C.Name name, (C.Def (C.Fix (!counter,ifl)))) in
incr counter ;
res
) ifl
let counter = ref 0 in
List.rev_map
(function (name,ty,bo) ->
- let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
+ let res = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
incr counter ;
res
) ifl
exception NotImplemented;;
-(* It returns true iff the proof has been perforated, i.e. if a subterm *)
-(* has been changed into a meta. *)
+(* A subterm is changed into a fresh meta *)
let to_sequent id ids_to_terms ids_to_father_ids =
let module P = ProofEngine in
let term = Hashtbl.find ids_to_terms id in
let context = get_context ids_to_terms ids_to_father_ids id in
- let type_checker_env_of_context =
- List.map
- (function
- P.Declaration,_,t -> t
- | P.Definition,_,_ -> raise NotImplemented
- ) context
+ let metasenv =
+ match !P.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ let ty = CicTypeChecker.type_of_aux' metasenv context term in
+ P.perforate context term ty (* P.perforate also sets the goal *)
+;;
+
+exception FocusOnlyOnMeta;;
+
+(* If the current selection is a Meta, that Meta becomes the current goal *)
+let focus id ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+ let term = Hashtbl.find ids_to_terms id in
+ let context = get_context ids_to_terms ids_to_father_ids id in
+ let metasenv =
+ match !P.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
in
- let metasenv =
- match !P.proof with
- None -> assert false
- | Some (metasenv,_,_) -> metasenv
- in
- let ty =
- CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
- in
- let (meta,perforated) =
- (* If the selected term is already a meta, we return it. *)
- (* Otherwise, we are trying to refine a non-meta term... *)
- match term with
- Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
- | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
- in
- perforated
+ let ty = CicTypeChecker.type_of_aux' metasenv context term in
+ match term with
+ Cic.Meta (n,_) -> P.goal := Some n
+ | _ -> raise FocusOnlyOnMeta
;;