From 7db7305941a97d43480cf58c08a154ed79f300cb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Apr 2002 16:53:48 +0000 Subject: [PATCH] * 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. --- helm/ocaml/cic/cic.ml | 8 ++ .../cic_proof_checking/cicTypeChecker.ml | 74 ++++++++++++------- .../cic_proof_checking/cicTypeChecker.mli | 3 +- 3 files changed, 56 insertions(+), 29 deletions(-) diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 64b7f857c..0a43c4c57 100644 --- 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 ba72a37a2..4ff7d9392 100644 --- 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 8c0354398..93f956143 100644 --- 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 -- 2.39.2