X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=5f0ba8aaa97ee00f7c085f70386e17b5244e3484;hb=d2c60bae1c4badba0a0f29e3fd2faed6d3a1869e;hp=ca8c0b54dc52cb0d35a8ab528859f67fbfc33451;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index ca8c0b54d..5f0ba8aaa 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -28,13 +28,24 @@ open ProofEngineTypes
 
   (* proof assistant status *)
 
-let proof = ref (None : proof)
-let goal = ref (None : goal)
+let proof = ref (None : proof option)
+let goal = ref (None : goal option)
 
 let apply_tactic ~tactic:tactic =
-  let (newproof, newgoal) = tactic ~status:(!proof, !goal) in
-  proof := newproof;
-  goal := newgoal
+ match !proof,!goal with
+    None,_
+  | _,None -> assert false
+  | Some proof', Some goal' ->
+     let (newproof, newgoals) = tactic ~status:(proof', goal') in
+     proof := Some newproof;
+     goal :=
+      (match newgoals, newproof with
+          goal::_, _ -> Some goal
+        | [], (_,(goal,_,_)::_,_,_) ->
+           (* the tactic left no open goal ; let's choose the first open goal *)
+(*CSC: here we could implement and use a proof-tree like notion... *)
+           Some goal
+        | _, _ -> None)
 
 (* metas_in_term term                                                *)
 (* Returns the ordered list of the metas that occur in [term].       *)
@@ -80,10 +91,10 @@ let metas_in_term term =
 (* are efficiency reasons.                                                   *)
 let perforate context term ty =
  let module C = Cic in
-  let newmeta = new_meta !proof in
-   match !proof with
-      None -> assert false
-    | Some (uri,metasenv,bo,gty) ->
+  match !proof with
+     None -> assert false
+   | Some (uri,metasenv,bo,gty as proof') ->
+      let newmeta = new_meta proof' in
        (* We push the new meta at the end of the list for pretty-printing *)
        (* purposes: in this way metas are ordered.                        *)
        let metasenv' = metasenv@[newmeta,context,ty] in
@@ -213,7 +224,8 @@ let fold term =
    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
    let replace =
     ProofEngineReduction.replace
-     ~equality:(ProofEngineReduction.syntactic_equality)
+     ~equality:
+      (ProofEngineReduction.syntactic_equality ~alpha_equivalence:false)
      ~what:term' ~with_what:term
    in
     let ty' = replace ty in
@@ -235,53 +247,6 @@ let fold term =
       proof := Some (curi,metasenv',pbo,pty) ;
       goal := Some metano
 
-exception NotConvertible
-
-(*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
-(*CSC: while [goal_input] can have a richer context (because of binders) *)
-(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
-(*CSC: Is that evident? Is that right? Or should it be changed?          *)
-let change ~goal_input ~input =
- let curi,metasenv,pbo,pty =
-  match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
-  match !goal with
-     None -> assert false
-   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
-  (* are_convertible works only on well-typed terms *)
-  ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
-  if CicReduction.are_convertible context goal_input input then
-   begin
-    let replace =
-     ProofEngineReduction.replace
-      ~equality:(==) ~what:goal_input ~with_what:input
-    in
-    let ty' = replace ty in
-    let context' =
-     List.map
-      (function
-          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
-        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
-        | None -> None
-      ) context
-    in
-     let metasenv' = 
-      List.map
-       (function
-           (n,_,_) when n = metano -> (metano,context',ty')
-         | _ as t -> t
-       ) metasenv
-     in
-      proof := Some (curi,metasenv',pbo,pty) ;
-      goal := Some metano
-   end
-  else
-   raise NotConvertible
-
 (************************************************************)
 (*              Tactics defined elsewhere                   *)
 (************************************************************)
@@ -296,6 +261,8 @@ let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
 let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
 let elim_intros_simpl term =
   apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
+let change ~goal_input:what ~input:with_what =
+  apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)
 
   (* structural tactics *)
 
@@ -306,4 +273,5 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
 
 let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
 let ring () = apply_tactic Ring.ring_tac
-
+let fourier () = apply_tactic FourierR.fourier_tac
+let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term)