Many many improvements:

[helm.git] / helm / gTopLevel / logicalOperations.ml

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 80f7d04cbfde32f72f49ef650d6ad412c93087b6..a9274fba6cb0a4035719dfb9d18033a3ded93af9 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -5,7 +5,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,11 +19,11 @@ 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 _ -> []
@@ -37,7 +36,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 +44,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,8 +56,7 @@ 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
@@ -68,16 +66,24 @@ let to_sequent id ids_to_terms ids_to_father_ids =
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in
-    let ty =
-     CicTypeChecker.type_of_aux' metasenv
-      (P.cic_context_of_named_context 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
+     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 ty = CicTypeChecker.type_of_aux' metasenv context term in
+     match term with
+        Cic.Meta (n,_) -> P.goal := Some n
+      | _ -> raise FocusOnlyOnMeta
 ;;