X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=c68982ff7dddea804aba27eeb53b8f478d62cfdf;hb=341a777b344e7adb1e989dda3fdd643a3d9fb5f5;hp=464186f2e0d1cdf91798761326cc524637733bdb;hpb=1df8405217896500edba22b61653e03b5289747c;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 464186f2e..c68982ff7 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -138,8 +138,6 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = (PP.ppterm ~subst ~metasenv ~context t2)))) ;; -(* REMINDER: eat_prods was here *) - (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) let rec instantiate_parameters params c = @@ -226,50 +224,73 @@ let rec eat_or_subst_lambdas | (_, te, _, _) -> te, k ;; +let check_homogeneous_call ~subst context indparamsno n uri reduct tl = + let last = + List.fold_left + (fun k x -> + if k = 0 then 0 + else + match R.whd context x with + | C.Rel m when m = n - (indparamsno - k) -> k - 1 + | _ -> raise (TypeCheckerFailure (lazy + ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ + string_of_int indparamsno ^ " fixed) is not homogeneous in "^ + "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct)))) + indparamsno tl + in + if last <> 0 then + raise (TypeCheckerFailure + (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ + NUri.string_of_uri uri))) +;; -(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) -(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *) -(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *) -(*CSC strictly_positive *) -(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) -let rec weakly_positive ~subst context n nn uri te = -(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) +(* Inductive types being checked for positivity have *) +(* indexes x s.t. n < x <= nn. *) +let rec weakly_positive ~subst context n nn uri indparamsno posuri te = + (*CSC: Not very nice. *) let dummy = C.Sort C.Prop in - (*CSC: mettere in cicSubstitution *) + (*CSC: to be moved in cicSubstitution? *) let rec subst_inductive_type_with_dummy _ = function | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy - | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::_) - when NUri.eq uri' uri -> dummy + | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) + when NUri.eq uri' uri -> + let _, rargs = HExtlib.split_nth lno tl in + if rargs = [] then dummy else C.Appl (dummy :: rargs) | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t in - match R.whd context te with - | C.Const (Ref.Ref (uri',Ref.Ind _)) - | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind _)))::_) - when NUri.eq uri' uri -> true - | C.Prod (name,source,dest) when - does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> - (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive ~subst context n nn - (subst_inductive_type_with_dummy () source) && - weakly_positive ~subst ((name,C.Decl source)::context) - (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) -> - does_not_occur ~subst context n nn - (subst_inductive_type_with_dummy () source)&& - weakly_positive ~subst ((name,C.Decl source)::context) - (n + 1) (nn + 1) uri dest - | _ -> - raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + (* this function has the same semantics of are_all_occurrences_positive + but the i-th context entry role is played by dummy and some checks + are skipped because we already know that are_all_occurrences_positive + of uri in te. *) + let rec aux context n nn te = + match R.whd context te with + | t when t = dummy -> true + | C.Appl (te::rargs) when te = dummy -> + List.for_all (does_not_occur ~subst context n nn) rargs + | C.Prod (name,source,dest) when + does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive ~subst context n nn indparamsno posuri source && + aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) -> + does_not_occur ~subst context n nn source && + aux ((name,C.Decl source)::context) (n + 1) (nn + 1) dest + | _ -> + raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + in + aux context n nn (subst_inductive_type_with_dummy () te) -and strictly_positive ~subst context n nn te = +and strictly_positive ~subst context n nn indparamsno posuri te = match R.whd context te with | t when does_not_occur ~subst context n nn t -> true - | C.Rel _ -> true + | C.Rel _ when indparamsno = 0 -> true + | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn -> + check_homogeneous_call ~subst context indparamsno n posuri reduct tl; + List.for_all (does_not_occur ~subst context n nn) tl | C.Prod (name,so,ta) -> does_not_occur ~subst context n nn so && - strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - List.for_all (does_not_occur ~subst context n nn) tl + strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) + indparamsno posuri ta | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as r)::tl) -> let _,paramsno,tyl,_,i = E.get_checked_indtys r in let _,name,ity,cl = List.nth tyl i in @@ -282,32 +303,16 @@ and strictly_positive ~subst context n nn te = ok && List.for_all (does_not_occur ~subst context n nn) arguments && List.for_all - (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl + (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) + uri indparamsno posuri) cl | _ -> false (* the inductive type indexes are s.t. n < x <= nn *) and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = match R.whd context te with | C.Appl ((C.Rel m)::tl) as reduct when m = i -> - let last = - List.fold_left - (fun k x -> - if k = 0 then 0 - else - match R.whd context x with - | C.Rel m when m = n - (indparamsno - k) -> k - 1 - | _ -> raise (TypeCheckerFailure (lazy - ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ - string_of_int indparamsno ^ " fixed) is not homogeneous in "^ - "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct)))) - indparamsno tl - in - if last = 0 then - List.for_all (does_not_occur ~subst context n nn) tl - else - raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ - NUri.string_of_uri uri))) + check_homogeneous_call ~subst context indparamsno n uri reduct tl; + List.for_all (does_not_occur ~subst context n nn) tl | C.Rel m when m = i -> if indparamsno = 0 then true @@ -315,9 +320,9 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = raise (TypeCheckerFailure (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ NUri.string_of_uri uri))) - | C.Prod (name,source,dest) when + | C.Prod (name,source,dest) when does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest -> - strictly_positive ~subst context n nn source && + strictly_positive ~subst context n nn indparamsno uri source && are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest @@ -328,7 +333,6 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> -prerr_endline ("MM: " ^ NCicPp.ppterm ~subst ~metasenv:[] ~context te); raise (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^ (NUri.string_of_uri uri)))) @@ -628,15 +632,16 @@ let rec typeof ~subst ~metasenv context term = * have them already *) let _,leftno,itl,_,i = E.get_checked_indtys r in let itl_len = List.length itl in - let _,_,_,cl = List.nth itl i in + let _,itname,ittype,cl = List.nth itl i in let cl_len = List.length cl in - (* is it a singleton or empty non recursive and non informative - definition? *) + (* is it a singleton, non recursive and non informative + definition or an empty one? *) if not (cl_len = 0 || (itl_len = 1 && cl_len = 1 && - is_non_informative leftno - (let _,_,x = List.hd cl in x))) + let _,_,constrty = List.hd cl in + is_non_recursive_singleton r itname ittype constrty && + is_non_informative leftno constrty)) then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed"))); @@ -681,6 +686,11 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty = in aux ty_he args_with_ty +and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty = + let ctx = [iname, C.Decl ity] in + let cty = debruijn uri 1 [] cty in + does_not_occur ~subst:[] ctx 0 1 cty + and is_non_informative paramsno c = let rec aux context c = match R.whd context c with @@ -939,8 +949,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = ("Too many args for constructor: " ^ String.concat " " (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args)))) in - let left, args = HExtlib.split_nth paramsno tl in - List.for_all (does_not_occur ~subst context n nn) left && + let _, args = HExtlib.split_nth paramsno tl in analyse_instantiated_type rec_params args | C.Appl ((C.Match (_,out,te,pl))::_) | C.Match (_,out,te,pl) as t -> @@ -949,6 +958,9 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && List.for_all (aux context n nn h) pl +(* IMPOSSIBLE unsless we allow to pass cofix to other fix/cofix as we do for + higher order fix in g_b_destructors. + | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref) | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in @@ -960,6 +972,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = (fun (_,_,_,_,bo) -> aux (context@tys) n nn h (debruijn u len context bo)) fl +*) | C.Const _ | C.Appl _ as t -> does_not_occur ~subst context n nn t in @@ -1058,7 +1071,7 @@ and get_relevance ~subst context t args = let rec aux context ty = function | [] -> [] | arg::tl -> match R.whd ~subst context ty with - | C.Prod (name,so,de) -> + | C.Prod (_,so,de) -> let sort = typeof ~subst ~metasenv:[] context so in let new_ty = S.subst ~avoid_beta_redexes:true arg de in (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[] @@ -1148,35 +1161,6 @@ let typecheck_subst ~metasenv subst = ) [] subst) ;; -let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();; -(* let shift e (k, context) = k+1,e::context in - let rec aux (evil, context as k) () t = - match R.whd ~subst context t with - | C.Rel i when i = evil -> (* - raise (TypeCheckerFailure (lazy (Printf.sprintf - "Argument %s declared as irrelevante is used in a relevant position" - (PP.ppterm ~subst ~metasenv ~context (C.Rel i))))) *) () - | C.Meta _ -> () - | C.Lambda (name,so,tgt) -> - (* checking so is not needed since the implicit version of CC - * has untyped lambdas (curry style), see Barras and Bernardo *) - aux (shift (name,C.Decl so) k) () tgt - | C.Appl (C.Const ref::args) -> - let relevance = NCicEnvironment.get_relevance ref in - HExtlib.list_iter_default2 - (fun t -> function false -> () | _ -> aux k () t) - args true relevance - | C.Match (_, _, _, []) -> () - | C.Match (ref, _, t, [p]) -> - aux k () p; - let _,lno,itl,_,_ = E.get_checked_indtys ref in - let _,_,_,cl = List.hd itl in - let _,_,c = List.hd cl in - if not (is_non_informative lno c) then aux k () t - | C.Match (_, _, t, pl) -> List.iter (aux k ()) (t::pl) - | t -> U.fold shift k aux () t - in - aux (1, context) () *) let typecheck_obj (uri,_height,metasenv,subst,kind) = (* height is not checked since it is only used to implement an optimization *)