version 0.7.1

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 9e5aa04ff6c71142660110f2e1513c532d45f54f..8a6ef81a277658d5e7cda8055768a925b7b3e574 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -142,7 +142,7 @@ let replace ~equality ~what ~with_what ~where =
         C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst)
      | C.Meta _ -> t
      | C.Sort _ -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
@@ -216,7 +216,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
     | C.Prod (n,s,t) ->
        C.Prod
@@ -315,7 +315,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
         in
          C.Meta(i,l')
      | C.Sort _ as t -> t
-     | C.Implicit as t -> t
+     | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
      | C.Prod (n,s,t) ->
         C.Prod (n, substaux k s, substaux (k + 1) t)
@@ -389,20 +389,21 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-       (match CicEnvironment.get_obj uri with
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        match o with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_) ->
+         | C.Variable (_,None,_,_,_) ->
             let t' = C.Var (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
-         | C.Variable (_,Some body,_,_) ->
+         | C.Variable (_,Some body,_,_,_) ->
             (reduceaux context l
               (CicSubstitution.subst_vars exp_named_subst' body))
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) ->
        C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
@@ -429,15 +430,16 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
-            C.Constant (_,Some body,_,_) ->
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+         match o with
+            C.Constant (_,Some body,_,_,_) ->
              (reduceaux context l
                (CicSubstitution.subst_vars exp_named_subst' body))
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = C.Const (uri,exp_named_subst') in
               if l = [] then t' else C.Appl (t'::l)
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              (reduceaux context l
                (CicSubstitution.subst_vars exp_named_subst' body))
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -490,11 +492,12 @@ let reduce context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,_,r) ->
-                   let (_,_,arity,_) = List.nth tl i in
-                    (arity,r)
-               | _ -> raise WrongUriToInductiveDefinition
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+                match o with
+                     C.InductiveDefinition (tl,_,r,_) ->
+                       let (_,_,arity,_) = List.nth tl i in
+                        (arity,r)
+                  | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
                let rec eat_first =
@@ -506,7 +509,7 @@ let reduce context =
                 eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit _ ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in
@@ -581,7 +584,7 @@ exception AlreadySimplified;;
 (* Takes a well-typed term and                                               *)
 (*  1) Performs beta-iota-zeta reduction until delta reduction is needed     *)
 (*  2) Attempts delta-reduction. If the residual is a Fix lambda-abstracted  *)
-(*     w.r.t. zero or more variables and if the Fix can be reduced, than it  *)
+(*     w.r.t. zero or more variables and if the Fix can be reductaed, than it  *)
 (*     is reduced, the delta-reduction is succesfull and the whole algorithm *)
 (*     is applied again to the new redex; Step 3) is applied to the result   *)
 (*     of the recursive simplification. Otherwise, if the Fix can not be     *)
@@ -593,6 +596,7 @@ exception AlreadySimplified;;
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
 (*CSC: It does not perform simplification in a Case *)
+
 let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
@@ -602,30 +606,33 @@ let simpl context =
   let module S = CicSubstitution in
    function
       C.Rel n as t ->
-       (match List.nth context (n-1) with
-           Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def (bo,_)) ->
-            try_delta_expansion l t (S.lift n bo)
-        | None -> raise RelToHiddenHypothesis
-       )
+       (try
+         match List.nth context (n-1) with
+            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
+          | Some (_,C.Def (bo,_)) ->
+             try_delta_expansion context l t (S.lift n bo)
+         | None -> raise RelToHiddenHypothesis
+        with
+         Failure _ -> assert false)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+         match o with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-          | C.Variable (_,None,_,_) ->
+          | C.Variable (_,None,_,_,_) ->
             let t' = C.Var (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
-          | C.Variable (_,Some body,_,_) ->
+          | C.Variable (_,Some body,_,_,_) ->
              reduceaux context l
               (CicSubstitution.subst_vars exp_named_subst' body)
         )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) ->
        C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
@@ -652,16 +659,17 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
-           C.Constant (_,Some body,_,_) ->
-            try_delta_expansion l
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+         match o with
+           C.Constant (_,Some body,_,_,_) ->
+            try_delta_expansion context l
              (C.Const (uri,exp_named_subst'))
              (CicSubstitution.subst_vars exp_named_subst' body)
-         | C.Constant (_,None,_,_) ->
+         | C.Constant (_,None,_,_,_) ->
             let t' = C.Const (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
+         | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
     | C.MutInd (uri,i,exp_named_subst) ->
@@ -710,11 +718,12 @@ let simpl context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,ingredients,r) ->
-                   let (_,_,arity,_) = List.nth tl i in
-                    (arity,r)
-               | _ -> raise WrongUriToInductiveDefinition
+              let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+                match o with
+                     C.InductiveDefinition (tl,ingredients,r,_) ->
+                       let (_,_,arity,_) = List.nth tl i in
+                        (arity,r)
+                  | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
                let rec eat_first =
@@ -726,7 +735,7 @@ let simpl context =
                 eat_first (r,tl)
               in
                reduceaux context (ts@l) (List.nth pl (j-1))
-         | C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit _ ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
            let outtype' = reduceaux context [] outtype in
@@ -792,7 +801,7 @@ let simpl context =
  and reduceaux_exp_named_subst context l =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
- and try_delta_expansion l term body =
+ and try_delta_expansion context l term body =
   let module C = Cic in
   let module S = CicSubstitution in
    try