parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / proofEngineStructuralRules.ml

diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml
index acc4bb1640ac112819ff403e2728d34f3ffe864f..47921953742be893160a5c5751570af6923b1d87 100644 (file)
--- a/helm/software/components/tactics/proofEngineStructuralRules.ml
+++ b/helm/software/components/tactics/proofEngineStructuralRules.ml
@@ -30,7 +30,7 @@ module C = Cic
 
 let clearbody ~hyp = 
  let clearbody (proof, goal) =
-   let curi,metasenv,pbo,pty = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,_,_ = CicUtil.lookup_meta goal metasenv in
      let string_of_name =
       function
@@ -46,25 +46,14 @@ let clearbody ~hyp =
                (fun entry context ->
                  match entry with
                     Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' ->
-                     let cleared_entry =
-                      let ty =
-                       match ty with
-                          Some ty -> ty
-                        | None ->
-                           fst
-                            (CicTypeChecker.type_of_aux' metasenv context term
-                              CicUniv.empty_ugraph) (* TASSI: FIXME *)
-                      in
-                       Some (C.Name hyp, Cic.Decl ty)
-                     in
+                     let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in
                       cleared_entry::context
                   | None -> None::context
-                  | Some (n,C.Decl t)
-                  | Some (n,C.Def (t,None)) ->
+                  | Some (n,C.Decl t) ->
                      let _,_ =
                       try
                        CicTypeChecker.type_of_aux' metasenv context t
-                        CicUniv.empty_ugraph (* TASSI: FIXME *)
+                        CicUniv.oblivion_ugraph (* TASSI: FIXME *)
                       with
                        _ ->
                          raise
@@ -75,13 +64,29 @@ let clearbody ~hyp =
                           ))
                      in
                       entry::context
-                  | Some (_,Cic.Def (_,Some _)) -> assert false
+                  | Some (n,Cic.Def (te,ty)) ->
+                     (try
+                       ignore
+                        (CicTypeChecker.type_of_aux' metasenv context te
+                          CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+                       ignore
+                        (CicTypeChecker.type_of_aux' metasenv context ty
+                          CicUniv.oblivion_ugraph (* TASSI: FIXME *));
+                      with
+                       _ ->
+                         raise
+                          (PET.Fail
+                            (lazy ("The correctness of hypothesis " ^
+                             string_of_name n ^
+                             " relies on the body of " ^ hyp)
+                          )));
+                     entry::context
                ) canonical_context []
              in
               let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                 CicUniv.empty_ugraph (* TASSI: FIXME *)
+                 CicUniv.oblivion_ugraph (* TASSI: FIXME *)
                with
                 _ ->
                  raise
@@ -93,13 +98,13 @@ let clearbody ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clearbody
 
 let clear_one ~hyp =
  let clear_one (proof, goal) =
-   let curi,metasenv,pbo,pty = proof in
+   let curi,metasenv,_subst,pbo,pty, attrs = proof in
     let metano,context,ty =
      CicUtil.lookup_meta goal metasenv
     in
@@ -120,13 +125,12 @@ let clear_one ~hyp =
                       (true, None::context)
                   | None -> (b, None::context)
                   | Some (n,C.Decl t)
-                  | Some (n,Cic.Def (t,Some _))
-                  | Some (n,C.Def (t,None)) ->
+                  | Some (n,Cic.Def (t,_)) ->
                       if b then
                          let _,_ =
                           try
                            CicTypeChecker.type_of_aux' metasenv context t
-                            CicUniv.empty_ugraph
+                            CicUniv.oblivion_ugraph
                           with _ ->
                            raise
                             (PET.Fail
@@ -143,7 +147,7 @@ let clear_one ~hyp =
              let _,_ =
                try
                 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
-                 CicUniv.empty_ugraph 
+                 CicUniv.oblivion_ugraph 
                with _ ->
                 raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
               in
@@ -151,7 +155,7 @@ let clear_one ~hyp =
          | t -> t
        ) metasenv
      in
-      (curi,metasenv',pbo,pty), [goal]
+      (curi,metasenv',_subst,pbo,pty, attrs), [goal]
  in
   PET.mk_tactic clear_one
 
@@ -176,7 +180,7 @@ let rename ~froms ~tos =
          try List.combine froms tos
         with Invalid_argument _ -> raise (PET.Fail (lazy error))
       in
-      let curi, metasenv, pbo, pty = proof in
+      let curi, metasenv, _subst, pbo, pty, attrs = proof in
       let metano, _, _ = CicUtil.lookup_meta goal metasenv in      
       let rename_map = function
          | Some (Cic.Name hyp, decl_or_def) as entry ->
@@ -191,15 +195,6 @@ let rename ~froms ~tos =
          | conjecture -> conjecture
       in
       let metasenv = List.map map metasenv in
-      (curi, metasenv, pbo, pty), [goal]
+      (curi, metasenv, _subst, pbo, pty, attrs), [goal]
    in
    PET.mk_tactic rename
-
-let set_goal n =
-  PET.mk_tactic
-    (fun (proof, goal) ->
-       let (_, metasenv, _, _) = proof in
-       if CicUtil.exists_meta n metasenv then
-         (proof, [n])
-       else
-         raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))