From 670911cb7c47a0deaf69b11bbaec4946b3f8e6c6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 3 Apr 2008 16:16:59 +0000 Subject: [PATCH] guarded_by_destructor ported, many auxiliary functions still to be done --- .../components/ng_kernel/nCicTypeChecker.ml | 1051 +++++++---------- 1 file changed, 447 insertions(+), 604 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index fd7e756ce..4679de20a 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -14,79 +14,13 @@ exception TypeCheckerFailure of string Lazy.t exception AssertFailure of string Lazy.t +let shift_k e (c,rf,x,safes) = + e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,List.map ((+)1) safes +;; + (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *) (* -let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = - let rec aux k t = - let module C = Cic in - let res = - match t with - C.Rel n as t when n <= k -> t - | C.Rel _ -> - raise (TypeCheckerFailure (lazy "unbound variable found in constructor type")) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i,l) -> - let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in - C.Meta (i,l') - | C.Sort _ - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) - | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) - | C.Appl l -> C.Appl (List.map (aux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> - if exp_named_subst != [] then - raise (TypeCheckerFailure - (lazy ("non-empty explicit named substitution is applied to "^ - "a mutual inductive type which is being defined"))) ; - C.Rel (k + number_of_types - tyno) ; - | C.MutInd (uri',tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.MutInd (uri',tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst - in - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, aux k outty, aux k t, - List.map (aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - cb t res; - res - in - aux 0 -;; - exception CicEnvironmentError;; (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) @@ -323,18 +257,18 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debrujinedte = debrujin_constructor uri len te in + let debruijnedte = debruijn_constructor uri len te in let augmented_term = List.fold_right (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl debrujinedte + itl debruijnedte in let _,ugraph' = type_of ~logger augmented_term ugraph in (* let's check also the positivity conditions *) if not (are_all_occurrences_positive tys uri indparamsno i 0 len - debrujinedte) + debruijnedte) then begin prerr_endline (UriManager.string_of_uri uri); @@ -361,490 +295,6 @@ and check_mutual_inductive_defs uri obj ugraph = lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) -and recursive_args context n nn te = - let module C = Cic in - match CicReduction.whd context te with - C.Rel _ -> [] - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ (*CSC ??? *) -> - raise (AssertFailure (lazy "3")) (* due to type-checking *) - | C.Prod (name,so,de) -> - (not (does_not_occur context n nn so)) :: - (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de) - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "4")) (* due to type-checking *) - | C.Appl _ -> [] - | C.Const _ -> raise (AssertFailure (lazy "5")) - | C.MutInd _ - | C.MutConstruct _ - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *) - -and get_new_safes ~subst context p c rl safes n nn x = - let module C = Cic in - let module U = UriManager in - let module R = CicReduction in - match (R.whd ~subst context c, R.whd ~subst context p, rl) with - (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) -> - (* we are sure that the two sources are convertible because we *) - (* have just checked this. So let's go along ... *) - let safes' = - List.map (fun x -> x + 1) safes - in - let safes'' = - if b then 1::safes' else safes' - in - get_new_safes ~subst ((Some (name,(C.Decl so)))::context) - ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) - | (C.Prod _, (C.MutConstruct _ as e), _) - | (C.Prod _, (C.Rel _ as e), _) - | (C.MutInd _, e, []) - | (C.Appl _, e, []) -> (e,safes,n,nn,x,context) - | (c,p,l) -> - (* CSC: If the next exception is raised, it just means that *) - (* CSC: the proof-assistant allows to use very strange things *) - (* CSC: as a branch of a case whose type is a Prod. In *) - (* CSC: particular, this means that a new (C.Prod, x,_) case *) - (* CSC: must be considered in this match. (e.g. x = MutCase) *) - raise - (AssertFailure (lazy - (Printf.sprintf "Get New Safes: c=%s ; p=%s" - (CicPp.ppterm c) (CicPp.ppterm p)))) - -and split_prods ~subst context n te = - let module C = Cic in - let module R = CicReduction in - match (n, R.whd ~subst context te) with - (0, _) -> context,te - | (n, C.Prod (name,so,ta)) when n > 0 -> - split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta - | (_, _) -> raise (AssertFailure (lazy "8")) - -and eat_lambdas ~subst context n te = - let module C = Cic in - let module R = CicReduction in - match (n, R.whd ~subst context te) with - (0, _) -> (te, 0, context) - | (n, C.Lambda (name,so,ta)) when n > 0 -> - let (te, k, context') = - eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta - in - (te, k + 1, context') - | (n, te) -> - raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))) - -(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) -and check_is_really_smaller_arg ~subst context n nn kl x safes te = - (*CSC: forse la whd si puo' fare solo quando serve veramente. *) - (*CSC: cfr guarded_by_destructors *) - let module C = Cic in - let module U = UriManager in - match CicReduction.whd ~subst context te with - C.Rel m when List.mem m safes -> true - | C.Rel _ -> false - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -(* | C.Cast (te,ty) -> - check_is_really_smaller_arg ~subst n nn kl x safes te && - check_is_really_smaller_arg ~subst n nn kl x safes ty*) -(* | C.Prod (_,so,ta) -> - check_is_really_smaller_arg ~subst n nn kl x safes so && - check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta*) - | C.Prod _ -> raise (AssertFailure (lazy "10")) - | C.Lambda (name,so,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ty,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst context n nn kl x safes ty && - check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.Appl (he::_) -> - (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) - (*CSC: solo perche' non abbiamo trovato controesempi *) - check_is_really_smaller_arg ~subst context n nn kl x safes he - | C.Appl [] -> raise (AssertFailure (lazy "11")) - | C.Const _ - | C.MutInd _ -> raise (AssertFailure (lazy "12")) - | C.MutConstruct _ -> false - | C.MutCase (uri,i,outtype,term,pl) -> - (match term with - C.Rel m when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let tys = - List.map - (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl - in - let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - List.fold_right - (fun p i -> - i && check_is_really_smaller_arg ~subst context n nn kl x safes p) - pl true - else - let pl_and_cl = - try - List.combine pl cl - with - 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' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map (fun (n,_,ty,_) -> - Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - List.fold_right - (fun p i -> - i && check_is_really_smaller_arg ~subst context n nn kl x safes p) - pl true - else - let pl_and_cl = - try - List.combine pl cl - with - 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' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | _ -> - List.fold_right - (fun p i -> - i && check_is_really_smaller_arg ~subst context n nn kl x safes p - ) pl true - ) - | C.Fix (_, fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,_,ty,bo) i -> - i && - check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true - | C.CoFix (_, fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,ty,bo) i -> - i && - check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true - -and guarded_by_destructors ~subst context n nn kl x safes = - let module C = Cic in - let module U = UriManager in - function - C.Rel m when m > n && m <= nn -> false - | C.Rel m -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> true - | Some (_,C.Def (bo,_)) -> - guarded_by_destructors ~subst context m nn kl x safes - (CicSubstitution.lift m bo) - | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) - ) - | C.Meta _ - | C.Sort _ - | C.Implicit _ -> true - | C.Cast (te,ty) -> - guarded_by_destructors ~subst context n nn kl x safes te && - guarded_by_destructors ~subst context n nn kl x safes ty - | C.Prod (name,so,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.Lambda (name,so,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ty,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst context n nn kl x safes ty && - guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - let k = List.nth kl (m - n - 1) in - if not (List.length tl > k) then false - else - List.fold_right - (fun param i -> - i && guarded_by_destructors ~subst context n nn kl x safes param - ) tl true && - check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) - | C.Appl tl -> - List.fold_right - (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - tl 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 (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - exp_named_subst true - | C.MutCase (uri,i,outtype,term,pl) -> - (match CicReduction.whd ~subst context term with - C.Rel m when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let len = List.length tl in - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map (fun (n,_,ty,_) -> - Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - let debrujinedty = debrujin_constructor uri len ty in - (id, snd (split_prods ~subst tys paramsno ty), - snd (split_prods ~subst tys paramsno debrujinedty) - )) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,len,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun p i -> - i && guarded_by_destructors ~subst context n nn kl x safes p) - pl true - else - let pl_and_cl = - try - List.combine pl cl - with - Invalid_argument _ -> - raise (TypeCheckerFailure (lazy "not enough patterns")) - in - guarded_by_destructors ~subst context n nn kl x safes outtype && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun (p,(_,c,brujinedc)) i -> - let rl' = recursive_args lefts_and_tys 0 len brujinedc in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - guarded_by_destructors ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map - (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun p i -> - i && guarded_by_destructors ~subst context n nn kl x safes p) - pl true - else - let pl_and_cl = - try - List.combine pl cl - with - Invalid_argument _ -> - raise (TypeCheckerFailure (lazy "not enough patterns")) - in - guarded_by_destructors ~subst context n nn kl x safes outtype && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun t i -> - i && guarded_by_destructors ~subst context n nn kl x safes t) - tl true && - List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e, safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - guarded_by_destructors ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | _ -> - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p) - pl true - ) - | C.Fix (_, fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,_,ty,bo) i -> - i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true - | C.CoFix (_, fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,ty,bo) i -> - i && - guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true - (* the boolean h means already protected *) (* args is the list of arguments the type of the constructor that may be *) (* found in head position must be applied to. *) @@ -1129,45 +579,117 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype = | _ -> None in - type_of_aux ~logger context t ugraph - -;; - -(** wrappers which instantiate fresh loggers *) - -(* check_allowed_sort_elimination uri i s1 s2 - This function is used outside the kernel to determine in advance whether - a MutCase will be allowed or not. - [uri,i] is the type of the term to match - [s1] is the sort of the term to eliminate (i.e. the head of the arity - of the inductive type [uri,i]) - [s2] is the sort of the goal (i.e. the head of the type of the outtype - of the MutCase) *) -let check_allowed_sort_elimination uri i s1 s2 = - fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[] - ~logger:(new CicLogger.logger) [] uri i true - (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) - CicUniv.empty_ugraph) + type_of_aux ~logger context t ugraph + +;; + +(** wrappers which instantiate fresh loggers *) + +(* check_allowed_sort_elimination uri i s1 s2 + This function is used outside the kernel to determine in advance whether + a MutCase will be allowed or not. + [uri,i] is the type of the term to match + [s1] is the sort of the term to eliminate (i.e. the head of the arity + of the inductive type [uri,i]) + [s2] is the sort of the goal (i.e. the head of the type of the outtype + of the MutCase) *) +let check_allowed_sort_elimination uri i s1 s2 = + fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[] + ~logger:(new CicLogger.logger) [] uri i true + (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) + CicUniv.empty_ugraph) +;; + +Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; + +*) + +module C = NCic +module R = NCicReduction +module Ref = NReference +module S = NCicSubstitution +module U = NCicUtils +module E = NCicEnvironment + +let rec split_prods ~subst context n te = + match (n, R.whd ~subst context te) with + | (0, _) -> context,te + | (n, C.Prod (name,so,ta)) when n > 0 -> + split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta + | (_, _) -> raise (AssertFailure (lazy "split_prods")) +;; + +let debruijn_constructor ?(cb=fun _ _ -> ()) uri number_of_types t = assert false +(* + let rec aux k t = + let module C = Cic in + let res = + match t with + C.Rel n as t when n <= k -> t + | C.Rel _ -> + raise (TypeCheckerFailure (lazy "unbound variable found in constructor type")) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i,l) -> + let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in + C.Meta (i,l') + | C.Sort _ + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) + | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) + | C.Appl l -> C.Appl (List.map (aux k) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> + if exp_named_subst != [] then + raise (TypeCheckerFailure + (lazy ("non-empty explicit named substitution is applied to "^ + "a mutual inductive type which is being defined"))) ; + C.Rel (k + number_of_types - tyno) ; + | C.MutInd (uri',tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutInd (uri',tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, aux k outty, aux k t, + List.map (aux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + cb t res; + res + in + aux 0*) ;; -Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);; - -*) - -module C = NCic -module R = NCicReduction -module Ref = NReference -module S = NCicSubstitution -module U = NCicUtils -module E = NCicEnvironment - -let rec split_prods ~subst context n te = - match (n, R.whd ~subst context te) with - | (0, _) -> context,te - | (n, C.Prod (name,so,ta)) when n > 0 -> - split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta - | (_, _) -> raise (AssertFailure (lazy "split_prods")) -;; let sort_of_prod ~subst context (name,s) (t1, t2) = let t1 = R.whd ~subst context t1 in @@ -1209,6 +731,22 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = aux ty_he args_with_ty ;; +let fix_lefts_in_constrs ~subst paramsno tyl i = + let len = List.length tyl in + let _,_,arity,cl = List.nth tyl i in + let tys = List.map (fun (_,n,ty,_) -> n,C.Decl ty) tyl in + let cl' = + List.map + (fun (_,id,ty) -> + let debruijnedty = debruijn_constructor ref len ty in + id, snd (split_prods ~subst tys paramsno ty), + snd (split_prods ~subst tys paramsno debruijnedty)) + cl + in + let lefts = fst (split_prods ~subst [] paramsno arity) in + tys@lefts, len, cl' +;; + exception DoesOccur;; let does_not_occur ~subst context n nn t = @@ -1233,6 +771,8 @@ let does_not_occur ~subst context n nn t = with DoesOccur -> false ;; +exception NotGuarded;; + let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = function | C.Rel n -> @@ -1506,9 +1046,312 @@ let rec typeof ~subst ~metasenv context term = typeof_aux context term and check_mutual_inductive_defs _ = assert false -and eat_lambdas ~subst _ _ _ = assert false + +and eat_lambdas ~subst context n te = + match (n, R.whd ~subst context te) with + | (0, _) -> (te, context) + | (n, C.Lambda (name,so,ta)) when n > 0 -> + eat_lambdas ~subst ((name,(C.Decl so))::context) (n - 1) ta + | (n, te) -> + raise (AssertFailure + (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te)))) + +and guarded_by_destructors ~subst context recfuns t = + let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in + let rec aux (context, recfuns, x, safes as k) = function + | C.Rel m when List.mem_assoc m recfuns -> raise NotGuarded + | C.Rel m -> + (match List.nth context (m-1) with + | _,C.Decl _ -> () + | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo)) + | C.Meta _ -> () + | C.Appl ((C.Rel m)::tl) when List.mem_assoc m recfuns -> + let rec_no = List.assoc m recfuns in + if not (List.length tl > rec_no) then raise NotGuarded + else + let rec_arg = List.nth tl rec_no in + aux k rec_arg; + List.iter (aux k) tl + | C.Match (ref,outtype,term,pl) as t -> + (match R.whd ~subst context term with + | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x -> + let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in + if not isinductive then recursor aux k t + else + let lefts_and_tys,len,cl = fix_lefts_in_constrs ~subst paramsno tl i in + let args = match t with C.Appl (_::tl) -> tl | _ -> [] in + aux k outtype; + List.iter (aux k) args; + List.iter2 + (fun p (_,c,bruijnedc) -> + let rl = recursive_args ~subst lefts_and_tys 0 len bruijnedc in + let p, k = get_new_safes ~subst k p rl in + aux k p) + pl cl + | _ -> recursor aux k t) + | t -> recursor aux k t + in + try aux (context, recfuns, 1, []) t;true + with NotGuarded -> false + +(* + | C.Fix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,_,ty,bo) i -> + i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo + ) fl true + | C.CoFix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,ty,bo) i -> + i && + guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && + guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo + ) fl true +*) + and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false -and guarded_by_destructors ~subst _ _ _ _ _ _ _ = assert false + +and recursive_args ~subst context n nn te = + match R.whd context te with + | C.Rel _ -> [] + | C.Prod (name,so,de) -> + (not (does_not_occur ~subst context n nn so)) :: + (recursive_args ~subst ((name,(C.Decl so))::context) (n+1) (nn + 1) de) + | _ -> raise (AssertFailure (lazy ("recursive_args"))) + +and get_new_safes ~subst (context, recfuns, x, safes as k) p rl = + match R.whd ~subst context p, rl with + | C.Lambda (name,so,ta), b::tl -> + let safes = (if b then [0] else []) @ safes in + get_new_safes ~subst + (shift_k (name,(C.Decl so)) (context, recfuns, x, safes)) ta tl + | C.Meta _ as e, _ | e, [] -> e, k + | _ -> raise (AssertFailure (lazy "Ill formed pattern")) + +and split_prods ~subst context n te = + match n, R.whd ~subst context te with + | 0, _ -> context,te + | n, C.Prod (name,so,ta) when n > 0 -> + split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta + | _ -> raise (AssertFailure (lazy "split_prods")) + +(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) +and check_is_really_smaller_arg ~subst context n nn kl x safes te = +assert false (* + (*CSC: forse la whd si puo' fare solo quando serve veramente. *) + (*CSC: cfr guarded_by_destructors *) + let module C = Cic in + let module U = UriManager in + match CicReduction.whd ~subst context te with + C.Rel m when List.mem m safes -> true + | C.Rel _ -> false + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit _ + | C.Cast _ +(* | C.Cast (te,ty) -> + check_is_really_smaller_arg ~subst n nn kl x safes te && + check_is_really_smaller_arg ~subst n nn kl x safes ty*) +(* | C.Prod (_,so,ta) -> + check_is_really_smaller_arg ~subst n nn kl x safes so && + check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) + (List.map (fun x -> x + 1) safes) ta*) + | C.Prod _ -> raise (AssertFailure (lazy "10")) + | C.Lambda (name,so,ta) -> + check_is_really_smaller_arg ~subst context n nn kl x safes so && + check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (name,so,ty,ta) -> + check_is_really_smaller_arg ~subst context n nn kl x safes so && + check_is_really_smaller_arg ~subst context n nn kl x safes ty && + check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.Appl (he::_) -> + (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) + (*CSC: solo perche' non abbiamo trovato controesempi *) + check_is_really_smaller_arg ~subst context n nn kl x safes he + | C.Appl [] -> raise (AssertFailure (lazy "11")) + | C.Const _ + | C.MutInd _ -> raise (AssertFailure (lazy "12")) + | C.MutConstruct _ -> false + | C.MutCase (uri,i,outtype,term,pl) -> + (match term with + C.Rel m when List.mem m safes || m = x -> + let (lefts_and_tys,len,isinductive,paramsno,cl) = + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.InductiveDefinition (tl,_,paramsno,_) -> + let tys = + List.map + (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl + in + let (_,isinductive,_,cl) = List.nth tl i in + let cl' = + List.map + (fun (id,ty) -> + (id, snd (split_prods ~subst tys paramsno ty))) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) + in + (tys@lefts,List.length tl,isinductive,paramsno,cl') + | _ -> + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) + in + if not isinductive then + List.fold_right + (fun p i -> + i && check_is_really_smaller_arg ~subst context n nn kl x safes p) + pl true + else + let pl_and_cl = + try + List.combine pl cl + with + 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' = + let debruijnedte = debruijn_constructor uri len c in + recursive_args lefts_and_tys 0 len debruijnedte + in + let (e,safes',n',nn',x',context') = + get_new_safes ~subst context p c rl' safes n nn x + in + i && + check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e + ) pl_and_cl true + | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> + let (lefts_and_tys,len,isinductive,paramsno,cl) = + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.InductiveDefinition (tl,_,paramsno,_) -> + let (_,isinductive,_,cl) = List.nth tl i in + let tys = + List.map (fun (n,_,ty,_) -> + Some(Cic.Name n,(Cic.Decl ty))) tl + in + let cl' = + List.map + (fun (id,ty) -> + (id, snd (split_prods ~subst tys paramsno ty))) cl in + let lefts = + match tl with + [] -> assert false + | (_,_,ty,_)::_ -> + fst (split_prods ~subst [] paramsno ty) + in + (tys@lefts,List.length tl,isinductive,paramsno,cl') + | _ -> + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) + in + if not isinductive then + List.fold_right + (fun p i -> + i && check_is_really_smaller_arg ~subst context n nn kl x safes p) + pl true + else + let pl_and_cl = + try + List.combine pl cl + with + 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' = + let debruijnedte = debruijn_constructor uri len c in + recursive_args lefts_and_tys 0 len debruijnedte + in + let (e,safes',n',nn',x',context') = + get_new_safes ~subst context p c rl' safes n nn x + in + i && + check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e + ) pl_and_cl true + | _ -> + List.fold_right + (fun p i -> + i && check_is_really_smaller_arg ~subst context n nn kl x safes p + ) pl true + ) + | C.Fix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,_,ty,bo) i -> + i && + check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo + ) fl true + | C.CoFix (_, fl) -> + let len = List.length fl in + let n_plus_len = n + len + and nn_plus_len = nn + len + and x_plus_len = x + len + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + and safes' = List.map (fun x -> x + len) safes in + List.fold_right + (fun (_,ty,bo) i -> + i && + check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl + x_plus_len safes' bo + ) fl true + *) + and returns_a_coinductive ~subst _ _ = assert false and type_of_constant ref = assert false (* USARE typecheck_obj0 *) @@ -1576,9 +1419,9 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = | C.Fixpoint (inductive,fl,_) -> let types,kl,len = List.fold_left - (fun (types,kl,len) (_,n,k,ty,_) -> + (fun (types,kl,len) (_,name,k,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in - ((n,(C.Decl (S.lift len ty)))::types, k::kl,len+1) + ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1) ) ([],[],0) fl in List.iter (fun (_,name,x,ty,bo) -> @@ -1587,13 +1430,13 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = 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 + let m, context = eat_lambdas ~subst types (x + 1) bo in + (* guarded by destructors conditions D{f,k,x,M} *) + let rec enum_from k = + function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl in - (* guarded by destructors conditions D{f,k,x,M} *) - if not (guarded_by_destructors ~subst context eaten - (len + eaten) kl 1 [] m) - then + if not (guarded_by_destructors + ~subst context (enum_from (x+1) kl) m) then raise(TypeCheckerFailure(lazy("Fix: not guarded by destructors"))) end else match returns_a_coinductive ~subst [] ty with -- 2.39.2