debian version 0.0.5-6

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

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 4035b32172a67f288a18db73b3b55e4a85a9d29a..2a7f8c4ae16ed82a9c7800df1345577cae5756fb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -36,7 +36,7 @@ let debug t context =
  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
    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
@@ -123,7 +123,7 @@ let rec type_of_constant ~logger uri ugraph =
  let module R = CicReduction in
  let module U = UriManager in
  let cobj,ugraph =
-   match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
     | CicEnvironment.UncheckedObj uobj ->
        logger#log (`Start_type_checking uri) ;
@@ -136,7 +136,7 @@ let rec type_of_constant ~logger uri ugraph =
 
        let ugraph_dust = 
          (match uobj with
-           C.Constant (_,Some te,ty,_) ->
+           C.Constant (_,Some te,ty,_,_) ->
            let _,ugraph = type_of ~logger ty ugraph in
            let type_of_te,ugraph' = type_of ~logger te ugraph in
               let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
@@ -147,11 +147,11 @@ let rec type_of_constant ~logger uri ugraph =
                 (CicPp.ppterm ty)))
               else
                 ugraph'
-         | C.Constant (_,None,ty,_) ->
+         | C.Constant (_,None,ty,_,_) ->
            (* only to check that ty is well-typed *)
            let _,ugraph' = type_of ~logger ty ugraph in 
            ugraph'
-         | C.CurrentProof (_,conjs,te,ty,_) ->
+         | C.CurrentProof (_,conjs,te,ty,_,_) ->
              let _,ugraph1 =
               List.fold_left
                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -180,7 +180,7 @@ let rec type_of_constant ~logger uri ugraph =
         try
           CicEnvironment.set_type_checking_info uri;
           logger#log (`Type_checking_completed uri) ;
-          match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+          match CicEnvironment.is_type_checked ~trust:false ugraph uri with
                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
         with Invalid_argument s ->
@@ -188,8 +188,8 @@ let rec type_of_constant ~logger uri ugraph =
           uobj,ugraph_dust       
   in
    match cobj,ugraph with
-      (C.Constant (_,_,ty,_)),g -> ty,g
-    | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g
+      (C.Constant (_,_,ty,_,_)),g -> ty,g
+    | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
     | _ ->
         raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
 
@@ -198,9 +198,9 @@ and type_of_variable ~logger uri ugraph =
  let module R = CicReduction in
  let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
-  match CicEnvironment.is_type_checked ~trust:true uri ugraph with
-     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph'
-   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
+  match CicEnvironment.is_type_checked ~trust:true ugraph uri with
+     CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+   | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
       logger#log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _,ugraph1 = type_of ~logger ty ugraph in
@@ -219,8 +219,8 @@ and type_of_variable ~logger uri ugraph =
        (try
           CicEnvironment.set_type_checking_info uri ;
           logger#log (`Type_checking_completed uri) ;
-          match CicEnvironment.is_type_checked ~trust:false uri ugraph with
-               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> 
+          match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+               CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> 
                 ty,ugraph'
             | CicEnvironment.CheckedObj _ 
              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -404,9 +404,9 @@ and strictly_positive context n nn te =
       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
       let (ok,paramsno,ity,cl,name) =
-       let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
        match o with
-           C.InductiveDefinition (tl,_,paramsno) ->
+           C.InductiveDefinition (tl,_,paramsno,_) ->
             let (name,_,ity,cl) = List.nth tl i in
              (List.length tl = 1, paramsno, ity, cl, name)
          | _ ->
@@ -545,7 +545,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 (* inductive block definition.                         *)
 and check_mutual_inductive_defs uri obj ugraph =
   match obj with
-      Cic.InductiveDefinition (itl, params, indparamsno) ->
+      Cic.InductiveDefinition (itl, params, indparamsno, _) ->
        typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
     | _ ->
        raise (TypeCheckerFailure (
@@ -557,7 +557,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-   match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
      | CicEnvironment.UncheckedObj uobj ->
         logger#log (`Start_type_checking uri) ;
@@ -568,7 +568,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
           try 
             CicEnvironment.set_type_checking_info uri ;
             logger#log (`Type_checking_completed uri) ;
-            (match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+            (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
                  CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
                | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
             )
@@ -578,7 +578,7 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
                 uobj,ugraph1_dust
   in
     match cobj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,arity,_) = List.nth dl i in
            arity,ugraph1
       | _ ->
@@ -590,7 +590,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj,ugraph1 =
-    match CicEnvironment.is_type_checked ~trust:true uri ugraph with
+    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
       | CicEnvironment.UncheckedObj uobj ->
          logger#log (`Start_type_checking uri) ;
@@ -601,10 +601,11 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
            try
              CicEnvironment.set_type_checking_info uri ;
              logger#log (`Type_checking_completed uri) ;
-             (match CicEnvironment.is_type_checked 
-                ~trust:false uri ugraph with
-                    CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' 
-                  | CicEnvironment.UncheckedObj _ -> 
+             (match 
+                 CicEnvironment.is_type_checked ~trust:false ugraph uri 
+               with
+                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' 
+              | CicEnvironment.UncheckedObj _ -> 
                       raise CicEnvironmentError)
            with
                Invalid_argument s ->
@@ -612,7 +613,7 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
                  uobj,ugraph1_dust
   in
     match cobj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,ugraph1
@@ -739,9 +740,9 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
       (match term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
-           let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let tys =
                  List.map
                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
@@ -778,9 +779,9 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                ) (List.combine pl cl) true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
-            let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
                   List.map (fun (n,_,ty,_) ->
@@ -905,9 +906,9 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
       (match term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
-           let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let len = List.length tl in
                  let (_,isinductive,_,cl) = List.nth tl i in
                   let tys =
@@ -950,9 +951,9 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                ) (List.combine pl cl) true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
-           let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+           let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-               C.InductiveDefinition (tl,_,paramsno) ->
+               C.InductiveDefinition (tl,_,paramsno,_) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
                   List.map
@@ -1063,11 +1064,11 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
       let consty =
        let obj,_ = 
          try 
-           CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+           CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
          with Not_found -> assert false
        in
        match obj with
-          C.InductiveDefinition (itl,_,_) ->
+          C.InductiveDefinition (itl,_,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
             let (_,cons) = List.nth cl (j - 1) in
              CicSubstitution.subst_vars exp_named_subst cons
@@ -1250,9 +1251,9 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
    (* TASSI: da verificare *)
 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
-       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-         C.InductiveDefinition (itl,_,_) ->
+         C.InductiveDefinition (itl,_,_,_) ->
            let (_,_,_,cl) = List.nth itl i in
            (* is a singleton definition or the empty proposition? *)
            (List.length cl = 1 || List.length cl = 0) , ugraph
@@ -1270,9 +1271,9 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
       (* TASSI: da verificare *)
       when need_dummy ->
-       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-           C.InductiveDefinition (itl,_,paramsno) ->
+           C.InductiveDefinition (itl,_,paramsno,_) ->
             let tys =
              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
             in
@@ -1298,9 +1299,9 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
            C.Sort C.Prop -> true,ugraph1
          | (C.Sort C.Set | C.Sort C.CProp) ->
-             (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-               C.InductiveDefinition (itl,_,_) ->
+               C.InductiveDefinition (itl,_,_,_) ->
                    let (_,_,_,cl) = List.nth itl i in
                    (* is a singleton definition? *)
                    List.length cl = 1,ugraph1
@@ -1324,9 +1325,9 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
          | C.Sort C.CProp -> true,ugraph1
          | C.Sort (C.Type _) ->
              (* TASSI: da verificare *)
-             (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
               match o with
-               C.InductiveDefinition (itl,_,paramsno) ->
+               C.InductiveDefinition (itl,_,paramsno,_) ->
                  let (_,_,_,cl) = List.nth itl i in
                  let tys =
                    List.map
@@ -1722,11 +1723,11 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       let parsno =
         let obj,_ =
           try
-            CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+            CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
           with Not_found -> assert false
         in
         match obj with
-            C.InductiveDefinition (_,_,parsno) -> parsno
+            C.InductiveDefinition (_,_,parsno,_) -> parsno
           | _ ->
               raise (TypeCheckerFailure
                 ("Unknown mutual inductive definition:" ^
@@ -1961,11 +1962,11 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
        (*CSC: definire una funzioncina per questo codice sempre replicato *)
         let obj,_ =
           try
-            CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
+            CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
           with Not_found -> assert false
         in
         (match obj with
-           C.InductiveDefinition (itl,_,_) ->
+           C.InductiveDefinition (itl,_,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
          | _ ->
@@ -1974,9 +1975,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               UriManager.string_of_uri uri))
         )
     | C.Appl ((C.MutInd (uri,i,_))::_) ->
-       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
-           C.InductiveDefinition (itl,_,_) ->
+           C.InductiveDefinition (itl,_,_,_) ->
             let (_,is_inductive,_,_) = List.nth itl i in
              if is_inductive then None else (Some uri)
          | _ ->
@@ -2034,7 +2035,7 @@ let typecheck uri ugraph =
  let module U = UriManager in
  let logger = new CicLogger.logger in
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
-   match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+   match CicEnvironment.is_type_checked ~trust:false ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
        (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
        cobj,ugraph'
@@ -2044,7 +2045,7 @@ let typecheck uri ugraph =
       (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
       let ugraph1 = 
        (match uobj with
-         C.Constant (_,Some te,ty,_) ->
+         C.Constant (_,Some te,ty,_,_) ->
            let _,ugraph1 = type_of ~logger ty ugraph in
           let ty_te,ugraph2 = type_of ~logger te ugraph1 in
            let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
@@ -2053,11 +2054,11 @@ let typecheck uri ugraph =
                 ("Unknown constant:" ^ U.string_of_uri uri))
            else
              ugraph3
-        | C.Constant (_,None,ty,_) ->
+        | C.Constant (_,None,ty,_,_) ->
           (* only to check that ty is well-typed *)
           let _,ugraph1 = type_of ~logger ty ugraph in
          ugraph1
-        | C.CurrentProof (_,conjs,te,ty,_) ->
+        | C.CurrentProof (_,conjs,te,ty,_,_) ->
            let _,ugraph1 =
             List.fold_left
              (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -2079,7 +2080,7 @@ let typecheck uri ugraph =
                 (CicPp.ppterm ty)))
            else
              ugraph4
-        | C.Variable (_,bo,ty,_) ->
+        | C.Variable (_,bo,ty,_,_) ->
            (* only to check that ty is well-typed *)
            let _,ugraph1 = type_of ~logger ty ugraph in
             (match bo with
@@ -2099,7 +2100,7 @@ let typecheck uri ugraph =
        try
          CicEnvironment.set_type_checking_info uri;
          logger#log (`Type_checking_completed uri);
-         match CicEnvironment.is_type_checked ~trust:false uri ugraph with
+         match CicEnvironment.is_type_checked ~trust:false ugraph uri with
              CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
            | _ -> raise CicEnvironmentError
        with