support for terms with metas in check

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionMachine.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e0fd252a6b6b8a254c25b60bd9a82f76eed7fd8a..0610504c4faeaa389c8c65e6ea804acb1542d6fe 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -38,7 +38,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -354,11 +354,11 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
          else
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -386,12 +386,12 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.Const (uri,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
-               C.Constant (_,_,_,params) -> params
+               C.Constant (_,_,_,params,_) -> params
              | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> params
+             | C.CurrentProof (_,_,_,_,params,_) -> params
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
           in
@@ -402,13 +402,13 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.MutInd (uri,i,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -418,13 +418,13 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
        | C.MutConstruct (uri,i,j,exp_named_subst) ->
           let params =
            let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -543,17 +543,17 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           reduce (0, [], [], RS.from_ens (List.assq uri ens), s)
          else
           ( let o,_ = 
-             CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph
+             CicEnvironment.get_cooked_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' = unwind k e ens t in
                 if s = [] then t' else
                  C.Appl (t'::(RS.from_stack_list ~unwind s))
-            | C.Variable (_,Some body,_,_) ->
+            | C.Variable (_,Some body,_,_,_) ->
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
@@ -601,18 +601,18 @@ if List.mem uri params then prerr_endline "---- OK2" ;
   *)
      | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) ->
         (let o,_ = 
-          CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph 
+          CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
         in
          match o with
-            C.Constant (_,Some body,_,_) ->
+            C.Constant (_,Some body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = unwind k e ens t in
               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s)
@@ -659,10 +659,10 @@ if List.mem uri params then prerr_endline "---- OK2" ;
            | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
               let (arity, r) =
                let o,_ = 
-                 CicEnvironment.get_cooked_obj mutind CicUniv.empty_ugraph
+                 CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                in
                  match o with
-                      C.InductiveDefinition (tl,ingredients,r) ->
+                      C.InductiveDefinition (tl,ingredients,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
                          (arity,r)
                     | _ -> raise WrongUriToInductiveDefinition