From 3bb77a573204ea2266a7befd6360521f94c61f9b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 1 Apr 2008 17:51:14 +0000 Subject: [PATCH] typeof_obj0 implemented --- .../components/ng_kernel/nCicTypeChecker.ml | 190 ++++++------------ 1 file changed, 58 insertions(+), 132 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 0299df7a7..ecc63445c 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -602,6 +602,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 +663,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 && @@ -1563,6 +1565,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 +1616,59 @@ 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 -- 2.39.2