* env renamed to context everywhere in cicTypeChecker.ml

* Definitions should be allowed in the contexts as well as Declarations.
  This is the very first step: the notion of context is introduced in cic.ml
  and the interface of cicTypeChecker.mli reflects that. (Of course, also the
  interface of cicReduction should do the same!)
  The new implementation just raises an exception when a definition is found
  in the context.

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 64b7f857cce087cc7f5925654939c2a613768434..0a43c4c571e80021fb625906c3d72a590442ddb6 100644 (file)
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -144,3 +144,11 @@ and 'a exactness =
    Possible of 'a                            (* an approximation to something *)
  | Actual of 'a                              (* something *)
 ;;
+
+(* Contexts are lists of context_entry *)
+type context_entry =
+   Decl of term
+ | Def of term
+;;
+
+type context = context_entry list;;

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index ba72a37a2a6edbfe8300007f140358765a46e7cc..4ff7d93921f8ed2b284a02961adac4d589f4c741 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -34,15 +34,15 @@ exception NotWellFormedTypeOfInductiveConstructor of string;;
 exception WrongRequiredArgument of string;;
 
 let fdebug = ref 0;;
-let debug t env =
+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
  in
   if !fdebug = 0 then
-   raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) ""))
-   (*print_endline ("\n" ^ List.fold_right debug_aux (t::env) "") ; flush stdout*)
+   raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))
+   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
 ;;
 
 let rec split l n =
@@ -1023,8 +1023,8 @@ 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 *)
-and type_of_aux' metasenv env t =
- let rec type_of_aux env =
+and type_of_aux' metasenv context t =
+ let rec type_of_aux context =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
@@ -1033,7 +1033,7 @@ and type_of_aux' metasenv env t =
       C.Rel n ->
        let t =
         try
-         List.nth env (n - 1)
+         List.nth context (n - 1)
         with
          _ -> raise (NotWellTyped "Not a close term")
        in
@@ -1048,25 +1048,25 @@ and type_of_aux' metasenv env t =
     | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
        let _ = type_of ty in
-        if R.are_convertible (type_of_aux env te) ty then ty
+        if R.are_convertible (type_of_aux context te) ty then ty
         else raise (NotWellTyped "Cast")
     | C.Prod (_,s,t) ->
-       let sort1 = type_of_aux env s
-       and sort2 = type_of_aux (s::env) t in
+       let sort1 = type_of_aux context s
+       and sort2 = type_of_aux (s::context) t in
         sort_of_prod (sort1,sort2)
    | C.Lambda (n,s,t) ->
-       let sort1 = type_of_aux env s
-       and type2 = type_of_aux (s::env) t in
-        let sort2 = type_of_aux (s::env) type2 in
+       let sort1 = type_of_aux context s
+       and type2 = type_of_aux (s::context) t in
+        let sort2 = type_of_aux (s::context) type2 in
          (* only to check if the product is well-typed *)
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
        let t' = CicSubstitution.subst s t in
-        type_of_aux env t'
+        type_of_aux context t'
    | C.Appl (he::tl) when List.length tl > 0 ->
-      let hetype = type_of_aux env he
-      and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
+      let hetype = type_of_aux context he
+      and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
        eat_prods hetype tlbody_and_type
    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
    | C.Const (uri,cookingsno) ->
@@ -1085,7 +1085,7 @@ and type_of_aux' metasenv env t =
       in
        cty
    | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
-      let outsort = type_of_aux env outtype in
+      let outsort = type_of_aux context outtype in
       let (need_dummy, k) =
        let rec guess_args t =
         match CicReduction.whd t with
@@ -1109,7 +1109,7 @@ and type_of_aux' metasenv env t =
          if not b then (b, k - 1) else (b, k)
       in
       let (parameters, arguments) =
-        match R.whd (type_of_aux env term) with
+        match R.whd (type_of_aux context term) with
            (*CSC manca il caso dei CAST *)
            C.MutInd (uri',_,i') ->
             (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
@@ -1134,7 +1134,7 @@ and type_of_aux' metasenv env t =
          C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
        in
         if not (check_allowed_sort_elimination uri i need_dummy
-         sort_of_ind_type (type_of_aux env sort_of_ind_type) outsort)
+         sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
         then
          raise (NotWellTyped "MutCase: not allowed sort elimination") ;
 
@@ -1156,9 +1156,9 @@ and type_of_aux' metasenv env t =
                (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
              in
               (j + 1, b &&
-               R.are_convertible (type_of_aux env p)
+               R.are_convertible (type_of_aux context p)
                 (type_of_branch parsno need_dummy outtype cons
-                  (type_of_aux env cons))
+                  (type_of_aux context cons))
               )
            ) (1,true) (List.combine pl cl)
          in
@@ -1174,13 +1174,14 @@ and type_of_aux' metasenv env t =
    | C.Fix (i,fl) ->
       let types_times_kl =
        List.rev
-        (List.map (fun (_,k,ty,_) -> let _ = type_of_aux env ty in (ty,k)) fl)
+        (List.map
+          (fun (_,k,ty,_) -> let _ = type_of_aux context ty in (ty,k)) fl)
       in
       let (types,kl) = List.split types_times_kl in
        let len = List.length types in
         List.iter
          (fun (name,x,ty,bo) ->
-           if (R.are_convertible (type_of_aux (types @ env) bo)
+           if (R.are_convertible (type_of_aux (types @ context) bo)
             (CicSubstitution.lift len ty))
            then
             begin
@@ -1198,12 +1199,13 @@ and type_of_aux' metasenv env t =
         ty
    | C.CoFix (i,fl) ->
       let types =
-       List.rev (List.map (fun (_,ty,_) -> let _ = type_of_aux env ty in ty) fl)
+       List.rev
+        (List.map (fun (_,ty,_) -> let _ = type_of_aux context ty in ty) fl)
       in
        let len = List.length types in
         List.iter
          (fun (_,ty,bo) ->
-           if (R.are_convertible (type_of_aux (types @ env) bo)
+           if (R.are_convertible (type_of_aux (types @ context) bo)
             (CicSubstitution.lift len ty))
            then
             begin
@@ -1286,19 +1288,19 @@ and type_of_aux' metasenv env t =
     | _ -> None
 
  in
-  type_of_aux env t
+  type_of_aux context t
 
 (* is a small constructor? *)
 (*CSC: ottimizzare calcolando staticamente *)
 and is_small paramsno c =
- let rec is_small_aux env c =
+ let rec is_small_aux context c =
   let module C = Cic in
    match CicReduction.whd c with
       C.Prod (_,so,de) ->
        (*CSC: [] is an empty metasenv. Is it correct? *)
-       let s = type_of_aux' [] env so in
+       let s = type_of_aux' [] context so in
         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-        is_small_aux (so::env) de
+        is_small_aux (so::context) de
     | _ -> true (*CSC: we trust the type-checker *)
  in
   let (sx,dx) = split_prods paramsno c in
@@ -1347,3 +1349,19 @@ let typecheck uri =
       Logger.log (`Type_checking_completed uri)
 ;;
 
+(*******************************************************)
+(*CSC: Da qua in avanti deve sparire tutto *)
+exception NotImplemented
+let wrong_context_of_context context =
+ let module C = Cic in
+  List.map
+   (function
+       C.Decl bt -> bt
+     | C.Def bt -> raise NotImplemented
+   ) context
+;;
+
+let type_of_aux' metasenv context t =
+ let context' = wrong_context_of_context context in
+  type_of_aux' metasenv context' t
+;;

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 8c0354398e4d375d21eacdf59d9e1940c3818aef..93f956143bcfdbc8042e7e444e149b199e03c63b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -35,4 +35,5 @@ val typecheck : UriManager.uri -> unit
 
 (* used only in the toplevel *)
 (* type_of_aux' metasenv context term *)
-val type_of_aux': (int * Cic.term) list -> Cic.term list -> Cic.term -> Cic.term
+val type_of_aux':
+ (int * Cic.term) list -> Cic.context -> Cic.term -> Cic.term