Meta implemented.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 63366b4b9997f5897027117458c17a98a7627f05..c818431376ca9d4972972bbf1740ffd4a8b32986 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -97,9 +97,9 @@ let rec cooked_type_of_constant uri cookingsno =
          | C.Axiom (_,ty,_) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()
          | C.Axiom (_,ty,_) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()

-         | C.CurrentProof (_,_,te,ty) ->
-             let _ = type_of ty in
-              if not (R.are_convertible (type_of te) ty) then
+         | C.CurrentProof (_,conjs,te,ty) ->
+             let _ = type_of_aux' conjs [] ty in
+              if not (R.are_convertible (type_of_aux' conjs [] te) ty) then

                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;
                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;


@@ -1048,7 +1048,7 @@ and type_of_branch argsno need_dummy outtype term constype =
        
  
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
        
  
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)

-and type_of_aux' env t =
+and type_of_aux' metasenv env t =

  let rec type_of_aux env =
   let module C = Cic in
   let module R = CicReduction in
  let rec type_of_aux env =
   let module C = Cic in
   let module R = CicReduction in


@@ -1068,7 +1068,7 @@ and type_of_aux' env t =
       let ty = type_of_variable uri in
        decr fdebug ;
        ty
       let ty = type_of_variable uri in
        decr fdebug ;
        ty

-    | C.Meta n -> raise NotImplemented
+    | C.Meta n -> List.assoc n metasenv

     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->


@@ -1320,7 +1320,8 @@ and is_small paramsno c =
   let module C = Cic in
    match CicReduction.whd c with
       C.Prod (_,so,de) ->
   let module C = Cic in
    match CicReduction.whd c with
       C.Prod (_,so,de) ->

-       let s = type_of_aux' env so in
+       (*CSC: [] is an empty metasenv. Is it correct? *)
+       let s = type_of_aux' [] env so in

         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
         is_small_aux (so::env) de
     | _ -> true (*CSC: we trust the type-checker *)
         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
         is_small_aux (so::env) de
     | _ -> true (*CSC: we trust the type-checker *)


@@ -1329,7 +1330,7 @@ and is_small paramsno c =
    is_small_aux (List.rev sx) dx
 
 and type_of t =
    is_small_aux (List.rev sx) dx
 
 and type_of t =

- type_of_aux' [] t
+ type_of_aux' [] [] t

 ;;
 
 let typecheck uri =
 ;;
 
 let typecheck uri =


@@ -1349,12 +1350,12 @@ let typecheck uri =
         | C.Axiom (_,ty,_) ->
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
         | C.Axiom (_,ty,_) ->
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()

-        | C.CurrentProof (_,_,te,ty) ->
-           (*CSC [] wrong *)
-           let _ = type_of ty in
-            debug (type_of te) [] ;
-            if not (R.are_convertible (type_of te) ty) then
-             raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+        | C.CurrentProof (_,conjs,te,ty) ->
+           (*CSC [] wrong *)
+            let _ = type_of_aux' conjs [] ty in
+             debug (type_of_aux' conjs [] te) [] ;
+             if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+              raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))

         | C.Variable (_,bo,ty) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in
         | C.Variable (_,bo,ty) ->
            (* only to check that ty is well-typed *)
            let _ = type_of ty in


@@ -1370,3 +1371,4 @@ let typecheck uri =
       CicEnvironment.set_type_checking_info uri ;
       log (`Type_checking_completed uri)
 ;;
       CicEnvironment.set_type_checking_info uri ;
       log (`Type_checking_completed uri)
 ;;

+