X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=74542a22696ce39cac7d3d9e81f63acf67a6817c;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;hp=4035b32172a67f288a18db73b3b55e4a85a9d29a;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 4035b3217..74542a226 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -36,13 +36,13 @@ 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) "")) ;; -let debug_print = prerr_endline ;; +let debug_print = fun _ -> () ;; let rec split l n = match (l,n) with @@ -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,16 +180,16 @@ 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 -> - (*prerr_endline s;*) + (*debug_print s;*) 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,13 +219,13 @@ 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 with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) ty,ugraph2) | _ -> raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) @@ -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,17 +568,17 @@ 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 ) with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) 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,18 +601,19 @@ 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 -> - (*prerr_endline s;*) + (*debug_print s;*) 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 @@ -1394,12 +1395,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context function [] -> [] | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1481,15 +1482,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst metasenv context canonical_context l ugraph in (* assuming subst is well typed !!!!! *) - ((CicSubstitution.lift_meta l ty), ugraph1) - (* type_of_aux context (CicSubstitution.lift_meta l term) *) + ((CicSubstitution.subst_meta l ty), ugraph1) + (* type_of_aux context (CicSubstitution.subst_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let ugraph1 = check_metasenv_consistency ~logger ~subst metasenv context canonical_context l ugraph in - ((CicSubstitution.lift_meta l ty),ugraph1)) + ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in @@ -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,17 +2035,17 @@ 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);*) + (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; - (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *) + (* debug_print ("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 @@ -2110,7 +2111,7 @@ let typecheck uri ugraph = object. *) Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print s;*) uobj,ugraph1 ;;