From 6b1cb7a439b2e72ec3d6bbb9803e880c82d85020 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Jul 2008 11:07:16 +0000 Subject: [PATCH] tab -> ' ' --- .../cic_proof_checking/cicTypeChecker.ml | 672 +++++++++--------- 1 file changed, 336 insertions(+), 336 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 1756497c0..e3d9add62 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -173,8 +173,8 @@ let rec type_of_constant ~logger uri orig_ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> let _,ugraph = - type_of_aux' ~logger metasenv context ty ugraph - in + type_of_aux' ~logger metasenv context ty ugraph + in (metasenv @ [conj],ugraph) ) ([],CicUniv.empty_ugraph) conjs in @@ -222,13 +222,13 @@ and type_of_variable ~logger uri orig_ugraph = match bo with None -> ugraph | Some bo -> - let ty_bo,ugraph = type_of ~logger bo ugraph in + let ty_bo,ugraph = type_of ~logger bo ugraph in let b,ugraph = R.are_convertible [] ty_bo ty ugraph in if not b then raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) - else - ugraph + else + ugraph in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj @@ -240,7 +240,7 @@ and type_of_variable ~logger uri orig_ugraph = | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError) | _ -> - raise (TypeCheckerFailure (lazy + raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) and does_not_occur ?(subst=[]) context n nn te = @@ -305,7 +305,7 @@ and does_not_occur ?(subst=[]) context n nn te = (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -321,7 +321,7 @@ and does_not_occur ?(subst=[]) context n nn te = (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -418,8 +418,8 @@ and weakly_positive context n nn uri te = (n + 1) (nn + 1) uri dest | C.Prod (name,source,dest) -> does_not_occur context n nn - (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((Some (name,(C.Decl source)))::context) + (subst_inductive_type_with_dummy_mutind source)&& + weakly_positive ((Some (name,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest | _ -> raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) @@ -454,16 +454,16 @@ and strictly_positive context n nn te = | (C.MutInd (uri,i,exp_named_subst)) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let (ok,paramsno,ity,cl,name) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.InductiveDefinition (tl,_,paramsno,_) -> - let (name,_,ity,cl) = List.nth tl i in + let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) (* (true, paramsno, ity, cl, name) *) | _ -> - raise - (TypeCheckerFailure - (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) + raise + (TypeCheckerFailure + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -562,7 +562,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = List.fold_right (fun (_,_,ty,cl) (i,ugraph) -> let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in - let ugraph'' = + let ugraph'' = List.fold_left (fun ugraph (name,te) -> let te = debrujin_constructor uri len [] te in @@ -589,20 +589,20 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in (* let's check also the positivity conditions *) if - not - (are_all_occurrences_positive context uri indparamsno + not + (are_all_occurrences_positive context uri indparamsno (i+indparamsno) indparamsno (len+indparamsno) te) then begin prerr_endline (UriManager.string_of_uri uri); prerr_endline (string_of_int (List.length tys)); - raise - (TypeCheckerFailure + raise + (TypeCheckerFailure (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else - ugraph + ugraph ) ugraph cl in - (i + 1),ugraph'' + (i + 1),ugraph'' ) itl (1,ugrap1) in ugraph2 @@ -612,11 +612,11 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = and check_mutual_inductive_defs uri obj ugraph = match obj with Cic.InductiveDefinition (itl, params, indparamsno, _) -> - typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph + typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> - raise (TypeCheckerFailure ( - lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + raise (TypeCheckerFailure ( + lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = let module C = Cic in @@ -626,17 +626,17 @@ and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> - logger#log (`Start_type_checking uri) ; - let inferred_ugraph = + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in - CicEnvironment.set_type_checking_info uri (obj,ugraph,ul); - logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') - | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError - ) + CicEnvironment.set_type_checking_info uri (obj,ugraph,ul); + logger#log (`Type_checking_completed uri) ; + (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError + ) in match cobj with | C.InductiveDefinition (dl,_,_,_) -> @@ -645,36 +645,36 @@ and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) - + and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> - logger#log (`Start_type_checking uri) ; - let inferred_ugraph = - check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph - in + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph + in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in - CicEnvironment.set_type_checking_info uri (obj, ugraph, ul); - logger#log (`Type_checking_completed uri) ; - (match + CicEnvironment.set_type_checking_info uri (obj, ugraph, ul); + logger#log (`Type_checking_completed uri) ; + (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj _ -> - raise CicEnvironmentError) + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> + raise CicEnvironmentError) in match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,ugraph1 | _ -> - raise (TypeCheckerFailure + raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) and recursive_args context n nn te = @@ -838,7 +838,7 @@ and check_is_really_smaller_arg (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.for_all (fun (_,_,_,bo) -> @@ -962,7 +962,7 @@ and guarded_by_destructors (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl in + ) ([],0) fl in let safes' = List.map (fun x -> x + len) safes in List.for_all (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l && @@ -1001,7 +1001,7 @@ and guarded_by_destructors (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1144,17 +1144,17 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger + check_allowed_sort_elimination ~subst ~metasenv ~logger ((Some (name,C.Decl so1))::context) uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 else - false,ugraph1 + false,ugraph1 | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in if not b then - false,ugraph1 + false,ugraph1 else check_allowed_sort_elimination_aux ugraph1 ((Some (name,C.Decl so))::context) ta true @@ -1163,7 +1163,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i | (C.Sort C.Prop, C.Sort (C.CProp _)) | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let itl_len = List.length itl in let (name,_,ty,cl) = List.nth itl i in @@ -1182,8 +1182,8 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i false,ugraph | _ -> raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph @@ -1191,7 +1191,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i | (C.Sort C.Set, C.Sort (C.CProp _)) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl @@ -1199,11 +1199,11 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let (_,_,_,cl) = List.nth itl i in (List.fold_right (fun (_,x) (i,ugraph) -> - if i then - is_small ~logger tys paramsno x ugraph - else - false,ugraph - ) cl (true,ugraph)) + if i then + is_small ~logger tys paramsno x ugraph + else + false,ugraph + ) cl (true,ugraph)) | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ @@ -1214,7 +1214,7 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i | (_,_) -> false,ugraph in check_allowed_sort_elimination_aux ugraph context arity2 need_dummy - + and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in @@ -1287,33 +1287,33 @@ and check_metasenv_consistency ~logger ~subst metasenv context in (*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!" else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*) - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context optimized_t ct ugraph - in - if not b then - raise - (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) - else - ugraph1 + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) + else + ugraph1 | Some t,Some (_,C.Decl ct) -> let type_t,ugraph1 = - type_of_aux' ~logger ~subst metasenv context t ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv context type_t ct ugraph1 - in + type_of_aux' ~logger ~subst metasenv context t ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv context type_t ct ugraph1 + in if not b then raise (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" - (CicPp.ppterm ct) (CicPp.ppterm t) - (CicPp.ppterm type_t)))) - else - ugraph2 + (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" + (CicPp.ppterm ct) (CicPp.ppterm t) + (CicPp.ppterm type_t)))) + else + ugraph2 | None, _ -> raise (TypeCheckerFailure - (lazy ("Not well typed metavariable local context: "^ - "an hypothesis, that is not hidden, is not instantiated"))) + (lazy ("Not well typed metavariable local context: "^ + "an hypothesis, that is not hidden, is not instantiated"))) ) ugraph l lifted_canonical_context @@ -1335,36 +1335,36 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Some (_,C.Decl t) -> S.lift n t,ugraph | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph | None -> raise - (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) + (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> incr fdebug ; - let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph - in - let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in - let ty1 = CicSubstitution.subst_vars exp_named_subst ty in - decr fdebug ; - ty1,ugraph2 + let ugraph1 = + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + in + let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in + let ty1 = CicSubstitution.subst_vars exp_named_subst ty in + decr fdebug ; + ty1,ugraph2 | C.Meta (n,l) -> (try let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in (* assuming subst is well typed !!!!! *) ((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 + 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 + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> @@ -1380,17 +1380,17 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in let b,ugraph3 = - R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 + R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 in - if b then + if b then ty,ugraph3 - else + else raise (TypeCheckerFailure - (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) + (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) | C.Prod (name,s,t) -> let sort1,ugraph1 = type_of_aux ~logger context s ugraph in let sort2,ugraph2 = - type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 in sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2 | C.Lambda (n,s,t) -> @@ -1405,9 +1405,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (CicPp.ppterm sort1)))) ) ; let type2,ugraph2 = - type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 in - (C.Prod (n,s,type2)),ugraph2 + (C.Prod (n,s,type2)),ugraph2 | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) let ty',ugraph1 = type_of_aux ~logger context s ugraph in @@ -1435,57 +1435,57 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) let ty1,ugraph2 = - type_of_aux ~logger - ((Some (n,(C.Def (s,ty))))::context) t ugraph1 + type_of_aux ~logger + ((Some (n,(C.Def (s,ty))))::context) t ugraph1 in (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype,ugraph1 = type_of_aux ~logger context he ugraph in let tlbody_and_type,ugraph2 = - List.fold_right ( - fun x (l,ugraph) -> - let ty,ugraph1 = type_of_aux ~logger context x ugraph in - (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) - ((x,ty)::l,ugraph1)) - tl ([],ugraph1) + List.fold_right ( + fun x (l,ugraph) -> + let ty,ugraph1 = type_of_aux ~logger context x ugraph in + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) + ((x,ty)::l,ugraph1)) + tl ([],ugraph1) in - (* TASSI: questa c'era nel mio... ma non nel CVS... *) - (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) - eat_prods ~subst context hetype tlbody_and_type ugraph2 + (* TASSI: questa c'era nel mio... ma non nel CVS... *) + (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) + eat_prods ~subst context hetype tlbody_and_type ugraph2 | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in let cty1 = - CicSubstitution.subst_vars exp_named_subst cty + CicSubstitution.subst_vars exp_named_subst cty in - decr fdebug ; - cty1,ugraph2 + decr fdebug ; + cty1,ugraph2 | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - decr fdebug ; - cty,ugraph2 + decr fdebug ; + cty,ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let mty,ugraph2 = - type_of_mutual_inductive_constr ~logger uri i j ugraph1 + type_of_mutual_inductive_constr ~logger uri i j ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - cty,ugraph2 + cty,ugraph2 | C.MutCase (uri,i,outtype,term,pl) -> let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in let (need_dummy, k) = @@ -1494,100 +1494,100 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = match outtype with C.Sort _ -> (true, 0) | C.Prod (name, s, t) -> - let (b, n) = - guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd ~subst context s with + let (b, n) = + guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd ~subst context s with (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) + | C.Appl ((C.MutInd (uri',i',_)) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - "Malformed case analasys' output type %s" - (CicPp.ppterm outtype)))) + raise + (TypeCheckerFailure + (lazy (sprintf + "Malformed case analasys' output type %s" + (CicPp.ppterm outtype)))) in (* let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux context term ugraph1 in + let ty,ugraph2 = type_of_aux context term ugraph1 in match R.whd ~subst context ty with (*CSC manca il caso dei CAST *) (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) (*CSC: Hint: nella DTD servono per gli stylesheet. *) C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i))) + if U.eq uri uri' && i = i' then + ([],[],exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri) i))) | C.Appl - ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, "^ - "but is expected to be (an application of) "^ - "%s#1/%d{_}") - (CicPp.ppterm typ') (U.string_of_uri uri) i))) + ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> + if U.eq uri uri' && i = i' then + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s, "^ + "but is expected to be (an application of) "^ + "%s#1/%d{_}") + (CicPp.ppterm typ') (U.string_of_uri uri) i))) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysis: "^ - "analysed term %s is not an inductive one") - (CicPp.ppterm term)))) + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysis: "^ + "analysed term %s is not an inductive one") + (CicPp.ppterm term)))) *) let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) in + if not b then (b, k - 1) else (b, k) in let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in + let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in match R.whd ~subst context ty with C.MutInd (uri',i',exp_named_subst) as typ -> if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 + ([],[],exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) -> if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | _ -> raise - (TypeCheckerFailure - (lazy (sprintf - "Case analysis: analysed term %s is not an inductive one" + (TypeCheckerFailure + (lazy (sprintf + "Case analysis: analysed term %s is not an inductive one" (CicPp.ppterm term)))) in - (* - let's control if the sort elimination is allowed: - [(I q1 ... qr)|B] - *) + (* + let's control if the sort elimination is allowed: + [(I q1 ... qr)|B] + *) let sort_of_ind_type = if parameters = [] then C.MutInd (uri,i,exp_named_subst) @@ -1595,12 +1595,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in let type_of_sort_of_ind_ty,ugraph3 = - type_of_aux ~logger context sort_of_ind_type ugraph2 in + type_of_aux ~logger context sort_of_ind_type ugraph2 in let b,ugraph4 = - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 in - if not b then + if not b then raise (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); (* let's check if the type of branches are right *) @@ -1627,24 +1627,24 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let (_,branches_ok,ugraph5) = List.fold_left (fun (j,b,ugraph) p -> - if b then + if b then let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl - (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) + if parameters = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl + (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in - let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in - let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in - (* 2 is skipped *) - let ty_branch = - type_of_branch ~subst context parsno need_dummy outtype cons - ty_cons in - let b1,ugraph4 = - R.are_convertible - ~subst ~metasenv context ty_p ty_branch ugraph3 - in + let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in + let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in + (* 2 is skipped *) + let ty_branch = + type_of_branch ~subst context parsno need_dummy outtype cons + ty_cons in + let b1,ugraph4 = + R.are_convertible + ~subst ~metasenv context ty_p ty_branch ugraph3 + in (* Debugging code if not b1 then begin @@ -1654,13 +1654,13 @@ prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons); prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch); end; *) - if not b1 then - debug_print (lazy - ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch)); - (j + 1,b1,ugraph4) - else - (j,false,ugraph) + if not b1 then + debug_print (lazy + ("#### " ^ CicPp.ppterm ty_p ^ + " <==> " ^ CicPp.ppterm ty_branch)); + (j + 1,b1,ugraph4) + else + (j,false,ugraph) ) (1,true,ugraph4) pl in if not branches_ok then @@ -1681,22 +1681,22 @@ end; let _,ugraph1 = type_of_aux ~logger context ty ugraph in (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, k::kl,ugraph1,len+1) - ) ([],[],ugraph,0) fl + ) ([],[],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (name,x,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types@context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types@context) - ty_bo (CicSubstitution.lift len ty) ugraph1 in - if b then - begin - let (m, eaten, context') = - eat_lambdas ~subst (types @ context) (x + 1) bo - in + let ty_bo,ugraph1 = + type_of_aux ~logger (types@context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types@context) + ty_bo (CicSubstitution.lift len ty) ugraph1 in + if b then + begin + let (m, eaten, context') = + eat_lambdas ~subst (types @ context) (x + 1) bo + in let rec_uri, rec_uri_len = let he = match List.hd context' with @@ -1716,74 +1716,74 @@ end; | _ -> assert false) | _ -> assert false in - (* - let's control the guarded by - destructors conditions D{f,k,x,M} - *) - if not (guarded_by_destructors ~logger ~metasenv ~subst + (* + let's control the guarded by + destructors conditions D{f,k,x,M} + *) + if not (guarded_by_destructors ~logger ~metasenv ~subst rec_uri rec_uri_len context' eaten (len + eaten) kl 1 [] m) then - raise - (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) - else - ugraph2 - end + raise + (TypeCheckerFailure + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) + else + ugraph2 + end else - raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) + raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) ) ugraph1 fl in - (*CSC: controlli mancanti solo su D{f,k,x,M} *) + (*CSC: controlli mancanti solo su D{f,k,x,M} *) let (_,_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 | C.CoFix (i,fl) -> let types,ugraph1,len = - List.fold_left - (fun (l,ugraph,len) (n,ty,_) -> + List.fold_left + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = - type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + type_of_aux ~logger context ty ugraph in + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, ugraph1,len+1) - ) ([],ugraph,0) fl + ) ([],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (_,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types @ context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types @ context) ty_bo - (CicSubstitution.lift len ty) ugraph1 - in - if b then - begin - (* let's control that the returned type is coinductive *) - match returns_a_coinductive ~subst context ty with - None -> - raise - (TypeCheckerFailure - (lazy "CoFix: does not return a coinductive type")) - | Some uri -> - (* - let's control the guarded by constructors - conditions C{f,M} - *) - if not (guarded_by_constructors ~logger ~subst ~metasenv uri + let ty_bo,ugraph1 = + type_of_aux ~logger (types @ context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types @ context) ty_bo + (CicSubstitution.lift len ty) ugraph1 + in + if b then + begin + (* let's control that the returned type is coinductive *) + match returns_a_coinductive ~subst context ty with + None -> + raise + (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some uri -> + (* + let's control the guarded by constructors + conditions C{f,M} + *) + if not (guarded_by_constructors ~logger ~subst ~metasenv uri (types @ context) 0 len false bo) then - raise - (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) - else - ugraph2 - end - else - raise - (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) + raise + (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) + else + ugraph2 + end + else + raise + (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) ) ugraph1 fl in let (_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 and check_exp_named_subst uri ~logger ~subst context ens ugraph = let params = @@ -1805,27 +1805,27 @@ end; in let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with - [] -> ugraph + [] -> ugraph | ((uri,t) as item)::tl -> - let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in - let typeofvar = + let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in + let typeofvar = CicSubstitution.subst_vars esubsts ty_uri in - let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in - let b,ugraph3 = + let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in + let b,ugraph3 = CicReduction.are_convertible ~subst ~metasenv - context typeoft typeofvar ugraph2 - in - if b then + context typeoft typeofvar ugraph2 + in + if b then check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3 else begin - CicReduction.fdebug := 0 ; - ignore - (CicReduction.are_convertible - ~subst ~metasenv context typeoft typeofvar ugraph2) ; - fdebug := 0 ; - debug typeoft [typeofvar] ; - raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) + CicReduction.fdebug := 0 ; + ignore + (CicReduction.are_convertible + ~subst ~metasenv context typeoft typeofvar ugraph2) ; + fdebug := 0 ; + debug typeoft [typeofvar] ; + raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in check_same_order params ens ; @@ -1887,39 +1887,39 @@ end; match l with [] -> hetype,ugraph | (hete, hety)::tl -> - (match (CicReduction.whd ~subst context hetype) with + (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> - let b,ugraph1 = + let b,ugraph1 = (*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then( prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*) - CicReduction.are_convertible - ~subst ~metasenv context hety s ugraph - in - if b then - begin - CicReduction.fdebug := -1 ; - eat_prods ~subst context - (CicSubstitution.subst ~avoid_beta_redexes:true hete t) + CicReduction.are_convertible + ~subst ~metasenv context hety s ugraph + in + if b then + begin + CicReduction.fdebug := -1 ; + eat_prods ~subst context + (CicSubstitution.subst ~avoid_beta_redexes:true hete t) tl ugraph1 - (*TASSI: not sure *) - end - else - begin - CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible - ~subst ~metasenv context s hety ugraph) ; - fdebug := 0 ; - debug s [hety] ; - raise - (TypeCheckerFailure - (lazy (sprintf - ("Appl: wrong parameter-type, expected %s, found %s") - (CicPp.ppterm hetype) (CicPp.ppterm s)))) - end - | _ -> - raise (TypeCheckerFailure - (lazy "Appl: this is not a function, it cannot be applied")) - ) + (*TASSI: not sure *) + end + else + begin + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible + ~subst ~metasenv context s hety ugraph) ; + fdebug := 0 ; + debug s [hety] ; + raise + (TypeCheckerFailure + (lazy (sprintf + ("Appl: wrong parameter-type, expected %s, found %s") + (CicPp.ppterm hetype) (CicPp.ppterm s)))) + end + | _ -> + raise (TypeCheckerFailure + (lazy "Appl: this is not a function, it cannot be applied")) + ) and returns_a_coinductive ~subst context ty = let module C = Cic in @@ -1942,7 +1942,7 @@ prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) @@ -1978,7 +1978,7 @@ and is_small_or_non_informative ~condition ~logger context paramsno c ugraph = is_small_or_non_informative_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 else - false,ugraph1 + false,ugraph1 | _ -> true,ugraph (*CSC: we trust the type-checker *) in let (context',dx) = split_prods ~subst:[] context paramsno c in @@ -2057,7 +2057,7 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) = None -> ugraph | Some bo -> let ty_bo,ugraph = type_of ~logger bo ugraph in - let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in + let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in if not b then raise (TypeCheckerFailure (lazy "the body is not the one expected")) -- 2.39.2