X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=9144f4740e1aa52e31b71c9c978e1ab0e269947c;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=277451bf42ed2774e99c46303822c03f47f1dec0;hpb=e627ae3edfbe950b87069b625ec9317acaf03ec5;p=helm.git diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 277451bf4..9144f4740 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -1,3 +1,28 @@ +(* 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 @@ -5,7 +30,6 @@ let get_parent id ids_to_terms ids_to_father_ids = ;; 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 @@ -20,15 +44,14 @@ let get_context ids_to_terms ids_to_father_ids = | 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 _ -> [] @@ -37,7 +60,7 @@ let get_context ids_to_terms ids_to_father_ids = 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 @@ -45,7 +68,7 @@ let get_context ids_to_terms ids_to_father_ids = 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 @@ -57,33 +80,34 @@ let get_context ids_to_terms ids_to_father_ids = 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 ;;