Many improvements in tactics (and tactical) representation:

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

diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml
index b52fb78826a53ff12a8ef333058ac1d32a2dcf67..75f421cede4ec24c666700a69a1316d56fbdd818 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.ml
+++ b/helm/gTopLevel/primitiveTactics.ml
@@ -195,22 +195,13 @@ let new_metasenv_for_apply proof context ty =
     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
      res,newmetasenv,arguments,newmeta,lastmeta
 
-let apply_tac ~status:(proof, goal) ~term =
+let apply_tac ~term ~status:(proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let metasenv =
-   match proof with
-      None -> assert false
-    | Some (_,metasenv,_,_) -> metasenv
-  in
-  let metano,context,ty =
-   match goal with
-      None -> assert false
-    | Some metano ->
-       List.find (function (m,_,_) -> m=metano) metasenv
-  in
+  let (_,metasenv,_,_) = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let termty = CicTypeChecker.type_of_aux' metasenv context term in
     (* newmeta is the lowest index of the new metas introduced *)
     let (consthead,newmetas,arguments,newmeta,_) =
@@ -240,53 +231,33 @@ let apply_tac ~status:(proof, goal) ~term =
             subst_meta_and_metasenv_in_proof
               proof metano subst_in newmetasenv''
           in
-           (newproof,
-            (match newmetasenv''' with
-            | [] -> None
-            | (i,_,_)::_ -> Some i))
+           (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
 
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
-let apply_tac ~status ~term =
+let apply_tac ~term ~status =
   try
-    apply_tac ~status ~term
+    apply_tac ~term ~status
       (* TODO cacciare anche altre eccezioni? *)
   with CicUnification.UnificationFailed as e ->
     raise (Fail (Printexc.to_string e))
 
-let intros_tac ~status:(proof, goal) ~name =
+let intros_tac ~name ~status:(proof, goal) =
  let module C = Cic in
  let module R = CicReduction in
-  let metasenv =
-   match proof with
-      None -> assert false
-    | Some (_,metasenv,_,_) -> metasenv
-  in
-  let metano,context,ty =
-   match goal with
-      None -> assert false
-    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
-  in
+  let (_,metasenv,_,_) = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta = new_meta ~proof in
     let (context',ty',bo') = lambda_abstract context newmeta ty name in
      let (newproof, _) =
        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
      in
-      let newgoal = Some newmeta in
-       (newproof, newgoal)
+      (newproof, [newmeta])
 
-let cut_tac ~status:(proof, goal) ~term =
+let cut_tac ~term ~status:(proof, goal) =
  let module C = Cic in
-  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
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let newmeta1 = new_meta ~proof in
    let newmeta2 = newmeta1 + 1 in
    let context_for_newmeta1 =
@@ -304,21 +275,12 @@ let cut_tac ~status:(proof, goal) ~term =
       subst_meta_in_proof proof metano bo'
        [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
      in
-      let newgoal = Some newmeta1 in
-       (newproof, newgoal)
+      (newproof, [newmeta1 ; newmeta2])
 
-let letin_tac ~status:(proof, goal) ~term =
+let letin_tac ~term ~status:(proof, goal) =
  let module C = Cic in
-  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
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let _ = CicTypeChecker.type_of_aux' metasenv context term in
     let newmeta = new_meta ~proof in
     let context_for_newmeta =
@@ -331,34 +293,20 @@ let letin_tac ~status:(proof, goal) ~term =
         subst_meta_in_proof
           proof metano bo'[newmeta,context_for_newmeta,newmetaty]
       in
-       let newgoal = Some newmeta in
-        (newproof, newgoal)
+       (newproof, [newmeta])
 
   (** functional part of the "exact" tactic *)
-let exact_tac ~status:(proof, goal) ~term =
+let exact_tac ~term ~status:(proof, goal) =
  (* Assumption: the term bo must be closed in the current context *)
- let metasenv =
-  match proof with
-     None -> assert false
-   | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
-  match goal with
-     None -> assert false
-   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  let module T = CicTypeChecker in
  let module R = CicReduction in
  if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
   begin
    let (newproof, metasenv') =
      subst_meta_in_proof proof metano term [] in
-   let newgoal =
-    (match metasenv' with
-       [] -> None
-     | (n,_,_)::_ -> Some n)
-   in
-   (newproof, newgoal)
+   (newproof, [])
   end
  else
   raise (Fail "The type of the provided term is not the one expected.")
@@ -366,22 +314,13 @@ let exact_tac ~status:(proof, goal) ~term =
 
 (* not really "primite" tactics .... *)
 
-let elim_intros_simpl_tac ~status:(proof, goal) ~term =
+let elim_intros_simpl_tac ~term ~status:(proof, goal) =
  let module T = CicTypeChecker in
  let module U = UriManager in
  let module R = CicReduction in
  let module C = Cic in
-  let curi,metasenv =
-   match proof with
-      None -> assert false
-    | Some (curi,metasenv,_,_) -> curi,metasenv
-  in
-  let metano,context,ty =
-   match goal with
-      None -> assert false
-    | Some metano ->
-       List.find (function (m,_,_) -> m=metano) metasenv
-  in
+  let (curi,metasenv,_,_) = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
    let termty = T.type_of_aux' metasenv context term in
    let uri,cookingno,typeno,args =
     match termty with
@@ -537,7 +476,4 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*)
                         proof metano apply_subst' newmetasenv'''
                     in
                      (newproof,
-                      (match newmetasenv'''' with
-                      | [] -> None
-                      | (i,_,_)::_ -> Some i))
-
+                      List.map (function (i,_,_) -> i) new_uninstantiatedmetas)