X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=fd7e756ce9a0552f6ce0ccaa8b85aecc8f970ffc;hb=507636cbb473500f40d0969a30e7afc7ddd88f2d;hp=0299df7a76edd12ff5bfda7ba9ab1aff28207e2e;hpb=7bf119d0c9d56ca0cb75c448beebf57bba7c8c6e;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 0299df7a7..fd7e756ce 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -89,90 +89,6 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = exception CicEnvironmentError;; -and does_not_occur ?(subst=[]) context n nn te = - let module C = Cic in - match te with - C.Rel m when m > n && m <= nn -> false - | C.Rel m -> - (try - (match List.nth context (m-1) with - Some (_,C.Def (bo,_)) -> - does_not_occur ~subst context n nn (CicSubstitution.lift m bo) - | _ -> true) - with - Failure _ -> assert false) - | C.Sort _ - | C.Implicit _ -> true - | C.Meta (_,l) -> - List.fold_right - (fun x i -> - match x with - None -> i - | Some x -> i && does_not_occur ~subst context n nn x) l true && - (try - let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in - does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term) - with - CicUtil.Subst_not_found _ -> true) - | C.Cast (te,ty) -> - does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty - | C.Prod (name,so,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) - (nn + 1) dest - | C.Lambda (name,so,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) - dest - | C.LetIn (name,so,ty,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst context n nn ty && - does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) - (n + 1) (nn + 1) dest - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) - | C.MutInd (_,_,exp_named_subst) - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x) - exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> - does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let nn_plus_len = nn + len in - let tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let nn_plus_len = nn + len in - let tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo - ) fl true - (*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 *) @@ -602,6 +518,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = Invalid_argument _ -> raise (TypeCheckerFailure (lazy "not enough patterns")) in + (*CSC: supponiamo come prima che nessun controllo sia necessario*) + (*CSC: sugli argomenti di una applicazione *) List.fold_right (fun (p,(_,c)) i -> let rl' = @@ -661,7 +579,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = let debrujinedte = debrujin_constructor uri len c in recursive_args lefts_and_tys 0 len debrujinedte in - let (e, safes',n',nn',x',context') = + let (e,safes',n',nn',x',context') = get_new_safes ~subst context p c rl' safes n nn x in i && @@ -1291,6 +1209,30 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = aux ty_he args_with_ty ;; +exception DoesOccur;; + +let does_not_occur ~subst context n nn t = + let rec aux (context,n,nn as k) _ = function + | C.Rel m when m > n && m <= nn -> raise DoesOccur + | C.Rel m -> + (try (match List.nth context (m-1) with + | _,C.Def (bo,_) -> aux k () (S.lift m bo) + | _ -> ()) + with Failure _ -> assert false) + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () + | C.Meta (mno,(s,l)) -> + (try + let _,_,term,_ = U.lookup_subst mno subst in + aux (context,n+s,nn+s) () (S.subst_meta (0,l) term) + with CicUtil.Subst_not_found _ -> match l with + | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur + | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc) + | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t + in + try aux (context,n,nn) () t; true + with DoesOccur -> false +;; + let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = function | C.Rel n -> @@ -1305,10 +1247,10 @@ let rec typeof ~subst ~metasenv context term = | C.Meta (n,l) as t -> let canonical_context,ty = try - let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty - with NCicUtils.Subst_not_found _ -> try - let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty - with NCicUtils.Meta_not_found _ -> + let _,c,_,ty = U.lookup_subst n subst in c,ty + with U.Subst_not_found _ -> try + let _,_,c,ty = U.lookup_meta n metasenv in c,ty + with U.Meta_not_found _ -> raise (AssertFailure (lazy (Printf.sprintf "%s not found" (NCicPp.ppterm t)))) in @@ -1473,7 +1415,7 @@ let rec typeof ~subst ~metasenv context term = S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl) in lift_metas 1 canonical_context in - let l = NCicUtils.expand_local_context lc_kind in + let l = U.expand_local_context lc_kind in try List.iter2 (fun t ct -> @@ -1563,6 +1505,12 @@ let rec typeof ~subst ~metasenv context term = in typeof_aux context term +and check_mutual_inductive_defs _ = assert false +and eat_lambdas ~subst _ _ _ = assert false +and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false +and guarded_by_destructors ~subst _ _ _ _ _ _ _ = assert false +and returns_a_coinductive ~subst _ _ = assert false + and type_of_constant ref = assert false (* USARE typecheck_obj0 *) (* ALIAS typecheck *) (* @@ -1608,141 +1556,58 @@ CASO TIPO INDUTTIVO | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) +CASO COSTANTE +CASO FIX/COFIX *) -and typecheck_obj0 = function - obj -> assert false -(* - | C.Constant (_,Some te,ty,_,_) -> - let _,ugraph = type_of ~logger ty ugraph in - let ty_te,ugraph = type_of ~logger te ugraph in - let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in - if not b then - raise (TypeCheckerFailure - (lazy - ("the type of the body is not the one expected:\n" ^ - CicPp.ppterm ty_te ^ "\nvs\n" ^ - CicPp.ppterm ty))) - else - ugraph - | 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,_,_) -> - let _,ugraph = - List.fold_left - (fun (metasenv,ugraph) ((_,context,ty) as conj) -> - let _,ugraph = - type_of_aux' ~logger metasenv context ty ugraph - in - metasenv @ [conj],ugraph - ) ([],ugraph) conjs - in - let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in - let type_of_te,ugraph = - type_of_aux' ~logger conjs [] te ugraph - in - let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in - if not b then - raise (TypeCheckerFailure (lazy (sprintf - "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s" - (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))) - else - ugraph - | (C.InductiveDefinition _ as obj) -> - check_mutual_inductive_defs ~logger uri obj ugraph - | C.Fix (i,fl) -> - let types,kl,ugraph1,len = +and typecheck_obj0 (uri,height,metasenv,subst,kind) = + (* CSC: here we should typecheck the metasenv and the subst *) + assert (metasenv = [] && subst = []); + match kind with + | C.Constant (_,_,Some te,ty,_) -> + let _ = typeof ~subst ~metasenv [] ty in + let ty_te = typeof ~subst ~metasenv [] te in + if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then + raise (TypeCheckerFailure (lazy (Printf.sprintf + "the type of the body is not the one expected:\n%s\nvs\n%s" + (NCicPp.ppterm ty_te) (NCicPp.ppterm ty)))) + | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) + | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj + | C.Fixpoint (inductive,fl,_) -> + let types,kl,len = List.fold_left - (fun (types,kl,ugraph,len) (n,k,ty,_) -> - 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 + (fun (types,kl,len) (_,n,k,ty,_) -> + let _ = typeof ~subst ~metasenv [] ty in + ((n,(C.Decl (S.lift len ty)))::types, k::kl,len+1) + ) ([],[],0) fl in - let ugraph2 = - 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's control the guarded by - destructors conditions D{f,k,x,M} - *) - if not (guarded_by_destructors ~subst context' eaten - (len + eaten) kl 1 [] m) then - raise - (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors"))) - else - ugraph2 - end - else - raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) - ) ugraph1 fl in - (*CSC: controlli mancanti solo su D{f,k,x,M} *) - let (_,_,ty,_) = List.nth fl i in - ty,ugraph2 - | C.CoFix (i,fl) -> - let types,ugraph1,len = - 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, - ugraph1,len+1) - ) ([],ugraph,0) fl - in - let ugraph2 = - 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 ~subst - (types @ context) 0 len false bo [] uri) then - 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 - -*) + List.iter (fun (_,name,x,ty,bo) -> + let ty_bo = typeof ~subst ~metasenv types bo in + if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) + then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) + else + if inductive then begin + let m, eaten, context = + eat_lambdas ~subst types (x + 1) bo + in + (* guarded by destructors conditions D{f,k,x,M} *) + if not (guarded_by_destructors ~subst context eaten + (len + eaten) kl 1 [] m) + then + raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors"))) + end else + match returns_a_coinductive ~subst [] ty with + | None -> + raise (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some uri -> + (* guarded by constructors conditions C{f,M} *) + if not (guarded_by_constructors ~subst + types 0 len false bo [] uri) + then + raise (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) + ) fl let typecheck_obj (*uri*) obj = assert false (* let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in