X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=25042b4cdf8b1d6aee7f82145cee50ac4d29a9ca;hb=9ae6d985833cf9e6855f41c942dc3c3d24af10e0;hp=9b0de30f2e37de7f2d922d440de63030763d3400;hpb=63bf7f1e50ca65c2a224e34aa7d232bff10ea934;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 9b0de30f2..25042b4cd 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -11,13 +11,13 @@ (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *) -(* web interface stuff *) - -let logger = - ref (function (`Start_type_checking _|`Type_checking_completed _) -> ()) -;; - -let set_logger f = logger := f;; +module C = NCic +module R = NCicReduction +module Ref = NReference +module S = NCicSubstitution +module U = NCicUtils +module E = NCicEnvironment +module PP = NCicPp exception TypeCheckerFailure of string Lazy.t exception AssertFailure of string Lazy.t @@ -53,35 +53,35 @@ let get_fixed_args i l = let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;; let string_of_recfuns ~subst ~metasenv ~context l = - let pp = NCicPp.ppterm ~subst ~metasenv ~context in + let pp = PP.ppterm ~subst ~metasenv ~context in let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in - let dang, unf = List.partition (function (_,UnfFix _) -> false | _->true)rest in - "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (NCic.Rel i)) safe) ^ + let dang,unf = List.partition (function (_,UnfFix _)-> false | _->true)rest in + "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (C.Rel i)) safe) ^ "\n\tfix : "^String.concat "," (List.map - (function (i,UnfFix l)-> pp(NCic.Rel i)^"/"^String.concat "," (List.map + (function (i,UnfFix l)-> pp(C.Rel i)^"/"^String.concat "," (List.map string_of_bool l) | _ ->assert false) unf) ^ "\n\trec : "^String.concat "," (List.map - (function (i,Evil rno)->pp(NCic.Rel i)^"/"^string_of_int rno + (function (i,Evil rno)->pp(C.Rel i)^"/"^string_of_int rno | _ -> assert false) dang) ;; let fixed_args bos j n nn = let rec aux k acc = function - | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn -> + | C.Appl (C.Rel i::args) when i-k > n && i-k <= nn -> let rec combine l1 l2 = match l1,l2 with [],[] -> [] | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2 - | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *) + | he::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *) | [],_::_ -> assert false in let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in - List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) + List.map (fun ((b,x),i) -> b && x = C.Rel (k-i)) (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts)) - | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t + | t -> U.fold (fun _ k -> k+1) k aux acc t in List.fold_left (aux 0) (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos @@ -94,263 +94,6 @@ let rec list_iter_default2 f l1 def l2 = | a::ta, [] -> f a def; list_iter_default2 f ta def [] ;; - -(* -(* 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. *) -and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = - let module C = Cic in - (*CSC: There is a lot of code replication between the cases X and *) - (*CSC: (C.Appl X tl). Maybe it will be better to define a function *) - (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) - match CicReduction.whd ~subst context te with - C.Rel m when m > n && m <= nn -> h - | C.Rel _ -> true - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ - | C.Prod _ - | C.LetIn _ -> - (* the term has just been type-checked *) - raise (AssertFailure (lazy "17")) - | C.Lambda (name,so,de) -> - does_not_occur ~subst context n nn so && - guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context) - (n + 1) (nn + 1) h de args coInductiveTypeURI - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - h && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true - | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> - let consty = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - C.InductiveDefinition (itl,_,_,_) -> - let (_,_,_,cl) = List.nth itl i in - let (_,cons) = List.nth cl (j - 1) in - CicSubstitution.subst_vars exp_named_subst cons - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) - in - let rec analyse_branch context ty te = - match CicReduction.whd ~subst context ty with - C.Meta _ -> raise (AssertFailure (lazy "34")) - | C.Rel _ - | C.Var _ - | C.Sort _ -> - does_not_occur ~subst context n nn te - | C.Implicit _ - | C.Cast _ -> - raise (AssertFailure (lazy "24"))(* due to type-checking *) - | C.Prod (name,so,de) -> - analyse_branch ((Some (name,(C.Decl so)))::context) de te - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "25"))(* due to type-checking *) - | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.Appl ((C.MutInd (uri,_,_))::_) -> - guarded_by_constructors ~subst context n nn true te tl - coInductiveTypeURI - | C.Appl _ -> - does_not_occur ~subst context n nn te - | C.Const _ -> raise (AssertFailure (lazy "26")) - | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.MutInd _ -> - does_not_occur ~subst context n nn te - | C.MutConstruct _ -> raise (AssertFailure (lazy "27")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "28"))(* due to type-checking *) - in - let rec analyse_instantiated_type context ty l = - match CicReduction.whd ~subst context ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *) - | C.Prod (name,so,de) -> - begin - match l with - [] -> true - | he::tl -> - analyse_branch context so he && - analyse_instantiated_type - ((Some (name,(C.Decl so)))::context) de tl - end - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "30"))(* due to type-checking *) - | C.Appl _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.Const _ -> raise (AssertFailure (lazy "31")) - | C.MutInd _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.MutConstruct _ -> raise (AssertFailure (lazy "32")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "33"))(* due to type-checking *) - in - let rec instantiate_type args consty = - function - [] -> true - | tlhe::tltl as l -> - let consty' = CicReduction.whd ~subst context consty in - match args with - he::tl -> - begin - match consty' with - C.Prod (_,_,de) -> - let instantiated_de = CicSubstitution.subst he de in - (*CSC: siamo sicuri che non sia troppo forte? *) - does_not_occur ~subst context n nn tlhe & - instantiate_type tl instantiated_de tltl - | _ -> - (*CSC:We do not consider backbones with a MutCase, a *) - (*CSC:FixPoint, a CoFixPoint and so on in head position.*) - raise (AssertFailure (lazy "23")) - end - | [] -> analyse_instantiated_type context consty' l - (* These are all the other cases *) - in - instantiate_type args consty tl - | C.Appl ((C.CoFix (_,fl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - 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 - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo args coInductiveTypeURI - ) fl true - | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | 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) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutInd _ -> assert false - | 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 && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - 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 - 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 - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - 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 - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo - args coInductiveTypeURI - ) fl true - - 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) -;; - -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 @@ -364,13 +107,13 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context = let res = match t with | C.Meta (i,(s,C.Ctx l)) -> - let l1 = NCicUtils.sharing_map (aux (k-s)) l in + let l1 = U.sharing_map (aux (k-s)) l in if l1 == l then t else C.Meta (i,(s,C.Ctx l1)) | C.Meta _ -> t | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 -> C.Rel (k + number_of_types - no) - | t -> NCicUtils.map (fun _ k -> k+1) k aux t + | t -> U.map (fun _ k -> k+1) k aux t in cb t res; res in @@ -392,8 +135,8 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) = | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: expected two sorts, found = %s, %s" - (NCicPp.ppterm ~subst ~metasenv ~context t1) - (NCicPp.ppterm ~subst ~metasenv ~context t2)))) + (PP.ppterm ~subst ~metasenv ~context t1) + (PP.ppterm ~subst ~metasenv ~context t2)))) ;; let eat_prods ~subst ~metasenv context he ty_he args_with_ty = @@ -403,10 +146,10 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = match R.whd ~subst context ty_he with | C.Prod (n,s,t) -> (* - prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - " - ^ NCicPp.ppterm ~subst ~metasenv - ~context ty_arg); - prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context (S.subst ~avoid_beta_redexes:true arg t)); + prerr_endline (PP.ppterm ~subst ~metasenv ~context s ^ " - Vs - " + ^ PP.ppterm ~subst ~metasenv ~context ty_arg); + prerr_endline (PP.ppterm ~subst ~metasenv ~context + (S.subst ~avoid_beta_redexes:true arg t)); *) if R.are_convertible ~subst ~metasenv context ty_arg s then aux (S.subst ~avoid_beta_redexes:true arg t) tl @@ -416,20 +159,20 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty = (lazy (Printf.sprintf ("Appl: wrong application of %s: the parameter %s has type"^^ "\n%s\nbut it should have type \n%s\nContext:\n%s\n") - (NCicPp.ppterm ~subst ~metasenv ~context he) - (NCicPp.ppterm ~subst ~metasenv ~context arg) - (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) - (NCicPp.ppterm ~subst ~metasenv ~context s) - (NCicPp.ppcontext ~subst ~metasenv context)))) + (PP.ppterm ~subst ~metasenv ~context he) + (PP.ppterm ~subst ~metasenv ~context arg) + (PP.ppterm ~subst ~metasenv ~context ty_arg) + (PP.ppterm ~subst ~metasenv ~context s) + (PP.ppcontext ~subst ~metasenv context)))) | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Appl: %s is not a function, it cannot be applied" - (NCicPp.ppterm ~subst ~metasenv ~context + (PP.ppterm ~subst ~metasenv ~context (let res = List.length tl in let eaten = List.length args_with_ty - res in - (NCic.Appl + (C.Appl (he::List.map fst (fst (HExtlib.split_nth eaten args_with_ty))))))))) in @@ -445,35 +188,31 @@ let rec instantiate_parameters params c = | t,l -> raise (AssertFailure (lazy "1")) ;; -let specialize_inductive_type ~subst context ty_term = +let specialize_inductive_type_constrs ~subst context ty_term = match R.whd ~subst context ty_term with | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty -> let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in let left_args,_ = HExtlib.split_nth leftno args in - let itl = - List.map (fun (rel, name, arity, cl) -> - let arity = instantiate_parameters left_args arity in - let cl = - List.map (fun (rel, name, ty) -> - rel, name, instantiate_parameters left_args ty) - cl - in - rel, name, arity, cl) - itl - in - is_ind, leftno, itl, attrs, i + let _,_,_,cl = List.nth itl i in + List.map + (fun (rel,name,ty) -> rel, name, instantiate_parameters left_args ty) cl | _ -> assert false ;; -let fix_lefts_in_constrs ~subst r_uri r_len context ty_term = - let _,_,itl,_,i = specialize_inductive_type ~subst context ty_term in - let _,_,_,cl = List.nth itl i in - let cl = - List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl +let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term = + let cl = specialize_inductive_type_constrs ~subst context ty_term in + let len = List.length context in + let context_dcl = + match E.get_checked_obj r_uri with + | _,_,_,_, NCic.Inductive (_,_,tys,_) -> + context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys + | _ -> assert false in - List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl + context_dcl, + List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl, + len, len + r_len ;; exception DoesOccur;; @@ -555,7 +294,7 @@ 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) cl | _ -> false (* the inductive type indexes are s.t. n < x <= nn *) @@ -572,7 +311,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = | y -> raise (TypeCheckerFailure (lazy ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ string_of_int indparamsno ^ " fixed) is not homogeneous in "^ - "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct)))) + "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct)))) indparamsno tl in if last = 0 then @@ -597,7 +336,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = | C.Prod (name,source,dest) -> if not (does_not_occur ~subst context n nn source) then raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^ - NCicPp.ppterm ~context ~metasenv:[] ~subst te))); + PP.ppterm ~context ~metasenv:[] ~subst te))); are_all_occurrences_positive ~subst ((name,C.Decl source)::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> @@ -610,7 +349,7 @@ exception NotGuarded of string Lazy.t;; let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = - fun t -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*) + fun t -> (*prerr_endline (PP.ppterm ~metasenv ~subst ~context t);*) match t with | C.Rel n -> (try @@ -629,7 +368,7 @@ let rec typeof ~subst ~metasenv context term = 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 ~subst ~metasenv ~context t)))) + "%s not found" (PP.ppterm ~subst ~metasenv ~context t)))) in check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l; S.subst_meta l ty @@ -647,8 +386,8 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf ("Not well-typed lambda-abstraction: " ^^ "the source %s should be a type; instead it is a term " ^^ - "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s) - (NCicPp.ppterm ~subst ~metasenv ~context sort))))); + "of type %s") (PP.ppterm ~subst ~metasenv ~context s) + (PP.ppterm ~subst ~metasenv ~context sort))))); let ty = typeof_aux ((n,(C.Decl s))::context) t in C.Prod (n,s,ty) | C.LetIn (n,ty,t,bo) -> @@ -659,9 +398,9 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf "The type of %s is %s but it is expected to be %s" - (NCicPp.ppterm ~subst ~metasenv ~context t) - (NCicPp.ppterm ~subst ~metasenv ~context ty_t) - (NCicPp.ppterm ~subst ~metasenv ~context ty)))) + (PP.ppterm ~subst ~metasenv ~context t) + (PP.ppterm ~subst ~metasenv ~context ty_t) + (PP.ppterm ~subst ~metasenv ~context ty)))) else let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in S.subst ~avoid_beta_redexes:true t ty_bo @@ -669,10 +408,10 @@ let rec typeof ~subst ~metasenv context term = let ty_he = typeof_aux context he in let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in (* - prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he); - prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + prerr_endline ("HEAD: " ^ PP.ppterm ~subst ~metasenv ~context ty_he); + prerr_endline ("TARGS: " ^ String.concat " | " (List.map (PP.ppterm ~subst ~metasenv ~context) (List.map snd args_with_ty))); - prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + prerr_endline ("ARGS: " ^ String.concat " | " (List.map (PP.ppterm ~subst ~metasenv ~context) (List.map fst args_with_ty))); *) eat_prods ~subst ~metasenv context he ty_he args_with_ty @@ -693,21 +432,21 @@ let rec typeof ~subst ~metasenv context term = raise (TypeCheckerFailure (lazy (Printf.sprintf "Case analysis: analysed term %s is not an inductive one" - (NCicPp.ppterm ~subst ~metasenv ~context term)))) in + (PP.ppterm ~subst ~metasenv ~context term)))) in if not (Ref.eq r r') then raise (TypeCheckerFailure (lazy (Printf.sprintf ("Case analysys: analysed term type is %s, but is expected " ^^ "to be (an application of) %s") - (NCicPp.ppterm ~subst ~metasenv ~context ty) - (NCicPp.ppterm ~subst ~metasenv ~context (C.Const r'))))) + (PP.ppterm ~subst ~metasenv ~context ty) + (PP.ppterm ~subst ~metasenv ~context (C.Const r'))))) else try HExtlib.split_nth leftno tl with Failure _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "%s is partially applied" - (NCicPp.ppterm ~subst ~metasenv ~context ty)))) in + (PP.ppterm ~subst ~metasenv ~context ty)))) in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let sort_of_ind_type = if parameters = [] then C.Const r @@ -743,11 +482,11 @@ let rec typeof ~subst ~metasenv context term = (TypeCheckerFailure (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ "has type %s\nnot convertible with %s") - (NCicPp.ppterm ~subst ~metasenv ~context + (PP.ppterm ~subst ~metasenv ~context (C.Const (Ref.mk_constructor (j-1) r))) - (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2))) - (NCicPp.ppterm ~metasenv ~subst ~context p_ty) - (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); + (PP.ppterm ~metasenv ~subst ~context (List.nth pl (j-2))) + (PP.ppterm ~metasenv ~subst ~context p_ty) + (PP.ppterm ~metasenv ~subst ~context exp_p_ty)))); let res = outtype::arguments@[term] in R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false @@ -776,7 +515,7 @@ let rec typeof ~subst ~metasenv context term = ~subst ~metasenv term context canonical_context l = match l with - | shift, NCic.Irl n -> + | shift, C.Irl n -> let context = snd (HExtlib.split_nth shift context) in let rec compare = function | 0,_,[] -> () @@ -784,11 +523,11 @@ let rec typeof ~subst ~metasenv context term = | _,_,[] -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm ~subst ~context ~metasenv term)))) + (PP.ppterm ~subst ~context ~metasenv term)))) | m,[],_::_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Unbound variable -%d in %s" m - (NCicPp.ppterm ~subst ~metasenv ~context term)))) + (PP.ppterm ~subst ~metasenv ~context term)))) | m,t::tl,ct::ctl -> (match t,ct with (_,C.Decl t1), (_,C.Decl t2) @@ -800,15 +539,15 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "%s expected, which is not convertible with %s") - (NCicPp.ppterm ~subst ~metasenv ~context term) - (NCicPp.ppterm ~subst ~metasenv ~context t2) - (NCicPp.ppterm ~subst ~metasenv ~context t1)))) + (PP.ppterm ~subst ~metasenv ~context term) + (PP.ppterm ~subst ~metasenv ~context t2) + (PP.ppterm ~subst ~metasenv ~context t1)))) | _,_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "a definition expected, but a declaration found") - (NCicPp.ppterm ~subst ~metasenv ~context term))))); + (PP.ppterm ~subst ~metasenv ~context term))))); compare (m - 1,tl,ctl) in compare (n,context,canonical_context) @@ -852,8 +591,8 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context: " ^^ "expected a term convertible with %s, found %s") - (NCicPp.ppterm ~subst ~metasenv ~context ct) - (NCicPp.ppterm ~subst ~metasenv ~context t)))) + (PP.ppterm ~subst ~metasenv ~context ct) + (PP.ppterm ~subst ~metasenv ~context t)))) | t, (_,C.Decl ct) -> let type_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context type_t ct) then @@ -861,15 +600,15 @@ let rec typeof ~subst ~metasenv context term = (lazy (Printf.sprintf ("Not well typed metavariable local context: "^^ "expected a term of type %s, found %s of type %s") - (NCicPp.ppterm ~subst ~metasenv ~context ct) - (NCicPp.ppterm ~subst ~metasenv ~context t) - (NCicPp.ppterm ~subst ~metasenv ~context type_t)))) + (PP.ppterm ~subst ~metasenv ~context ct) + (PP.ppterm ~subst ~metasenv ~context t) + (PP.ppterm ~subst ~metasenv ~context type_t)))) ) l lifted_canonical_context with Invalid_argument _ -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm ~subst ~metasenv ~context term)))) + (PP.ppterm ~subst ~metasenv ~context term)))) and is_non_informative context paramsno c = let rec aux context c = @@ -894,8 +633,8 @@ let rec typeof ~subst ~metasenv context term = if not (R.are_convertible ~subst ~metasenv context so1 so2) then raise (TypeCheckerFailure (lazy (Printf.sprintf "In outtype: expected %s, found %s" - (NCicPp.ppterm ~subst ~metasenv ~context so1) - (NCicPp.ppterm ~subst ~metasenv ~context so2) + (PP.ppterm ~subst ~metasenv ~context so1) + (PP.ppterm ~subst ~metasenv ~context so2) ))); aux ((name, C.Decl so1)::context) (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 @@ -903,8 +642,8 @@ let rec typeof ~subst ~metasenv context term = if not (R.are_convertible ~subst ~metasenv context so ind) then raise (TypeCheckerFailure (lazy (Printf.sprintf "In outtype: expected %s, found %s" - (NCicPp.ppterm ~subst ~metasenv ~context ind) - (NCicPp.ppterm ~subst ~metasenv ~context so) + (PP.ppterm ~subst ~metasenv ~context ind) + (PP.ppterm ~subst ~metasenv ~context so) ))); (match arity1,ta with | (C.Sort (C.CProp | C.Type _), C.Sort _) @@ -967,53 +706,48 @@ and eat_lambdas ~subst ~metasenv context n te = eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta | (n, te) -> raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n - (NCicPp.ppterm ~subst ~metasenv ~context te)))) + (PP.ppterm ~subst ~metasenv ~context te)))) -and eat_or_subst_lambdas - ~subst ~metasenv app_all_args n te to_be_subst args (context, recfuns, x as k) +and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args + (context, recfuns, x as k) = match n, R.whd ~subst context te, to_be_subst, args with - | (0, _,_,_) when args = [] || not app_all_args -> te, k - | (0, _,_,_::_) -> C.Appl (te::args), k | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 -> - eat_or_subst_lambdas ~subst ~metasenv app_all_args - (n - 1) (S.subst arg ta) to_be_subst args k + eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta) + to_be_subst args k | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 -> - eat_or_subst_lambdas ~subst ~metasenv app_all_args - (n - 1) ta to_be_subst args (shift_k (name,(C.Decl so)) k) - | (n, te, _, _) when args = [] || not app_all_args -> te, k - | (n, te, _, _::_) -> C.Appl (te::args), k - | (_,_,_,[]) -> assert false (* caml thinks is missing *) + eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args + (shift_k (name,(C.Decl so)) k) + | (_, te, _, _) -> te, k and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = - let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in + let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in let rec aux (context, recfuns, x as k) t = - let t = R.whd ~delta:max_int ~subst context t in (* prerr_endline ("GB:\n" ^ - NCicPp.ppcontext ~subst ~metasenv context^ - NCicPp.ppterm ~metasenv ~subst ~context t^ + PP.ppcontext ~subst ~metasenv context^ + PP.ppterm ~metasenv ~subst ~context t^ string_of_recfuns ~subst ~metasenv ~context recfuns); *) try match t with | C.Rel m as t when is_dangerous m recfuns -> raise (NotGuarded (lazy - (NCicPp.ppterm ~subst ~metasenv ~context t ^ + (PP.ppterm ~subst ~metasenv ~context t ^ " is a partial application of a fix"))) | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns -> let rec_no = get_recno m recfuns in if not (List.length tl > rec_no) then raise (NotGuarded (lazy - (NCicPp.ppterm ~context ~subst ~metasenv t ^ + (PP.ppterm ~context ~subst ~metasenv t ^ " is a partial application of a fix"))) else let rec_arg = List.nth tl rec_no in if not (is_really_smaller r_uri r_len ~subst ~metasenv k rec_arg) then raise (NotGuarded (lazy (Printf.sprintf ("Recursive call %s, %s is not" - ^^ " smaller.\ncontext:\n%s") (NCicPp.ppterm ~context ~subst ~metasenv - t) (NCicPp.ppterm ~context ~subst ~metasenv rec_arg) - (NCicPp.ppcontext ~subst ~metasenv context)))); + ^^ " smaller.\ncontext:\n%s") (PP.ppterm ~context ~subst ~metasenv + t) (PP.ppterm ~context ~subst ~metasenv rec_arg) + (PP.ppcontext ~subst ~metasenv context)))); List.iter (aux k) tl | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns -> let fixed_args = get_fixed_args m recfuns in @@ -1023,10 +757,10 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = | _,C.Decl _ -> () | _,C.Def (bo,_) -> aux k (S.lift m bo)) | C.Meta _ -> () - | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,_))) as r)::args) -> + | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) -> if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args then - let fl,_,_ = E.get_checked_fixes r in + let fl,_,_ = E.get_checked_fixes_or_cofixes r in let ctx_tys, bos = List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl) in @@ -1042,11 +776,33 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = let extra_recfuns = HExtlib.list_mapi (fun _ i -> ctx_len - i, UnfFix fa) ctx_tys in - let k = context, extra_recfuns@recfuns, x in + let new_k = context, extra_recfuns@recfuns, x in let bos_and_ks = - HExtlib.list_mapi (fun bo fno -> - (* potrebbe anche aggiungere un arg di cui fa push alle safe *) - eat_or_subst_lambdas ~subst ~metasenv (fno=i) j bo fa args k) bos + HExtlib.list_mapi + (fun bo fno -> + let bo_and_k = + eat_or_subst_lambdas ~subst ~metasenv j bo fa args new_k + in + if + fno = i && + List.length args > recno && + (*case where the recursive argument is already really_smaller *) + is_really_smaller r_uri r_len ~subst ~metasenv k + (List.nth args recno) + then + let bo,(context, _, _ as new_k) = bo_and_k in + let bo, context' = + eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in + let new_context_part,_ = + HExtlib.split_nth (List.length context' - List.length context) + context' in + let k = List.fold_right shift_k new_context_part new_k in + let context, recfuns, x = k in + let k = context, (1,Safe)::recfuns, x in + bo,k + else + bo_and_k + ) bos in List.iter (fun (bo,k) -> aux k bo) bos_and_ks | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> @@ -1057,10 +813,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = if not isinductive then recursor aux k t else let ty = typeof ~subst ~metasenv context term in - let itl_ctx,dcl = fix_lefts_in_constrs ~subst r_uri r_len context ty in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst r_uri r_len context ty in let args = match t with C.Appl (_::tl) -> tl | _ -> [] in - let dc_ctx = context @ itl_ctx in - let start, stop = List.length context, List.length context + r_len in aux k outtype; List.iter (aux k) args; List.iter2 @@ -1080,48 +835,68 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = try aux (context, recfuns, 1) t with NotGuarded s -> raise (TypeCheckerFailure s) +and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn = + let rec aux context n nn h te = + match R.whd ~subst context te with + | C.Rel m when m > n && m <= nn -> h + | C.Rel _ | C.Meta _ -> true + | C.Sort _ + | C.Implicit _ + | C.Prod _ + | C.Const (Ref.Ref (_,_,Ref.Ind _)) + | C.LetIn _ -> raise (AssertFailure (lazy "17")) + | C.Lambda (name,so,de) -> + does_not_occur ~subst context n nn so && + aux ((name,C.Decl so)::context) (n + 1) (nn + 1) h de + | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + h && List.for_all (does_not_occur ~subst context n nn) tl + | C.Const (Ref.Ref (_,_,Ref.Con _)) -> true + | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (_,j)) as ref) :: tl) as t -> + let _, paramsno, _, _, _ = E.get_checked_indtys ref in + let ty_t = typeof ~subst ~metasenv context t in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst indURI indlen context ty_t in + let _, dc = List.nth dcl (j-1) in (* - | 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 ~metasenv _ _ _ _ _ _ _ = true - + prerr_endline (PP.ppterm ~subst ~metasenv ~context:dc_ctx dc); + prerr_endline (PP.ppcontext ~subst ~metasenv dc_ctx); + *) + let rec_params = recursive_args ~subst ~metasenv dc_ctx start stop dc in + let rec analyse_instantiated_type rec_spec args = + match rec_spec, args with + | h::rec_spec, he::args -> + aux context n nn h he && analyse_instantiated_type rec_spec args + | _,[] -> true + | _ -> raise (AssertFailure (lazy + ("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 && + analyse_instantiated_type rec_params args + | C.Appl ((C.Match (_,out,te,pl))::_) + | C.Match (_,out,te,pl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + List.for_all (does_not_occur ~subst context n nn) tl && + 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 + | 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 + let fl,_,_ = E.get_checked_fixes_or_cofixes ref in + let len = List.length fl in + let tys = List.map (fun (_,n,_,ty,_) -> n, C.Decl ty) fl in + List.for_all (does_not_occur ~subst context n nn) tl && + List.for_all + (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 + aux context 0 nn false t + and recursive_args ~subst ~metasenv context n nn te = match R.whd context te with | C.Rel _ | C.Appl _ | C.Const _ -> [] @@ -1130,7 +905,7 @@ and recursive_args ~subst ~metasenv context n nn te = (recursive_args ~subst ~metasenv ((name,(C.Decl so))::context) (n+1) (nn + 1) de) | t -> - raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst + raise (AssertFailure (lazy ("recursive_args:" ^ PP.ppterm ~subst ~metasenv ~context:[] t))) and get_new_safes ~subst (context, recfuns, x as k) p rl = @@ -1142,13 +917,6 @@ and get_new_safes ~subst (context, recfuns, x as k) p rl = | 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")) - and is_really_smaller r_uri r_len ~subst ~metasenv (context, recfuns, x as k) te = @@ -1158,28 +926,10 @@ and is_really_smaller is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t | C.Appl (he::_) -> is_really_smaller r_uri r_len ~subst ~metasenv k he - | C.Appl _ | C.Rel _ | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false + | C.Appl [] | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert 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 && - is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true*) | C.Meta _ -> true | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> (match term with @@ -1190,9 +940,8 @@ and is_really_smaller List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl else let ty = typeof ~subst ~metasenv context term in - let itl_ctx,dcl= fix_lefts_in_constrs ~subst r_uri r_len context ty in - let start, stop = List.length context, List.length context + r_len in - let dc_ctx = context @ itl_ctx in + let dc_ctx, dcl, start, stop = + specialize_and_abstract_constrs ~subst r_uri r_len context ty in List.for_all2 (fun p (_,dc) -> let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in @@ -1206,24 +955,14 @@ and returns_a_coinductive ~subst context ty = match R.whd ~subst context ty with | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) -> - let isinductive, _, _, _, _ = E.get_checked_indtys ref in - if isinductive then None else (Some uri) + let isinductive, _, itl, _, _ = E.get_checked_indtys ref in + if isinductive then None else (Some (uri,List.length itl)) | C.Prod (n,so,de) -> returns_a_coinductive ~subst ((n,C.Decl so)::context) de | _ -> None and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = - let cobj = - match E.get_obj uri with - | true, cobj -> cobj - | false, uobj -> - !logger (`Start_type_checking uri); - check_obj_well_typed uobj; - E.add_obj uobj; - !logger (`Type_checking_completed uri); - uobj - in - match cobj, ref with + match E.get_checked_obj uri, ref with | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i) -> let _,_,arity,_ = List.nth tl i in arity | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j)) -> @@ -1235,8 +974,9 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = arity | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) +;; -and check_obj_well_typed (uri,height,metasenv,subst,kind) = +let typecheck_obj (uri,height,metasenv,subst,kind) = (* CSC: here we should typecheck the metasenv and the subst *) assert (metasenv = [] && subst = []); match kind with @@ -1247,19 +987,20 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = raise (TypeCheckerFailure (lazy (Printf.sprintf ( "the type of the body is not convertible with the declared one.\n"^^ "inferred type:\n%s\nexpected type:\n%s") - (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) - (NCicPp.ppterm ~subst ~metasenv ~context:[] ty)))) + (PP.ppterm ~subst ~metasenv ~context:[] ty_te) + (PP.ppterm ~subst ~metasenv ~context:[] ty)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) | C.Inductive (is_ind, leftno, tyl, _) -> check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl | C.Fixpoint (inductive,fl,_) -> - let types, kl, len = + let types, kl = List.fold_left - (fun (types,kl,len) (_,name,k,ty,_) -> + (fun (types,kl) (_,name,k,ty,_) -> let _ = typeof ~subst ~metasenv [] ty in - ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1) - ) ([],[],0) fl + ((name,C.Decl ty)::types, k::kl) + ) ([],[]) fl in + let len = List.length types in let dfl, kl = List.split (List.map2 (fun (_,_,_,_,bo) rno -> @@ -1269,7 +1010,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = in List.iter2 (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)) + if not (R.are_convertible ~subst ~metasenv types ty_bo ty) then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) else if inductive then begin @@ -1294,17 +1035,55 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = 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 ~metasenv - types 0 len false bo [] uri) - then - raise (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) + raise (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some (r_uri, r_len) -> + (* guarded by constructors conditions C{f,M} *) + if not + (guarded_by_constructors ~subst ~metasenv types bo r_uri r_len len) + then + raise (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) ) fl dfl +;; + +(* trust *) + +let trust = ref (fun _ -> false);; +let set_trust f = trust := f +let trust_obj obj = !trust obj -let typecheck_obj = check_obj_well_typed;; + +(* web interface stuff *) + +let logger = + ref (function (`Start_type_checking _|`Type_checking_completed _|`Type_checking_interrupted _|`Type_checking_failed _|`Trust_obj _) -> ()) +;; + +let set_logger f = logger := f;; + +let typecheck_obj obj = + let u,_,_,_,_ = obj in + try + !logger (`Start_type_checking u); + typecheck_obj obj; + !logger (`Type_checking_completed u) + with + Sys.Break as e -> + !logger (`Type_checking_interrupted u); + raise e + | e -> + !logger (`Type_checking_failed u); + raise e +;; + +E.set_typecheck_obj + (fun obj -> + if trust_obj obj then + let u,_,_,_,_ = obj in + !logger (`Trust_obj u) + else + typecheck_obj obj) +;; (* EOF *)