X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=81f633bb6c850362623c0b617ff3ccc41e86b52f;hb=dff76b5e1557ff32872f4e48854daaa6c42e5ad2;hp=80d4dea0ec3bae7c8648a6d5043a4a6f39faa6a8;hpb=a287d1b295b81866d6aba85955cc835a57e9ae9e;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 80d4dea0e..81f633bb6 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -11,6 +11,14 @@ (* $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;; + exception TypeCheckerFailure of string Lazy.t exception AssertFailure of string Lazy.t @@ -257,7 +265,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debruijnedte = debruijn_constructor uri len te in + let debruijnedte = debruijn uri len te in let augmented_term = List.fold_right (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) @@ -517,67 +525,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = args coInductiveTypeURI ) fl true -and type_of_branch ~subst context argsno need_dummy outtype term constype = - let module C = Cic in - let module R = CicReduction in - match R.whd ~subst context constype with - C.MutInd (_,_,_) -> - if need_dummy then - outtype - else - C.Appl [outtype ; term] - | C.Appl (C.MutInd (_,_,_)::tl) -> - let (_,arguments) = split tl argsno - in - if need_dummy && arguments = [] then - outtype - else - C.Appl (outtype::arguments@(if need_dummy then [] else [term])) - | C.Prod (name,so,de) -> - let term' = - match CicSubstitution.lift 1 term with - C.Appl l -> C.Appl (l@[C.Rel 1]) - | t -> C.Appl [t ; C.Rel 1] - in - C.Prod (name,so,type_of_branch ~subst - ((Some (name,(C.Decl so)))::context) argsno need_dummy - (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (AssertFailure (lazy "20")) - - and returns_a_coinductive ~subst context ty = - let module C = Cic in - match CicReduction.whd ~subst context ty with - C.MutInd (uri,i,_) -> - (*CSC: definire una funzioncina per questo codice sempre replicato *) - 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 (_,is_inductive,_,_) = List.nth itl i in - if is_inductive then None else (Some uri) - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - ) - | C.Appl ((C.MutInd (uri,i,_))::_) -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,_,_) -> - let (_,is_inductive,_,_) = List.nth itl i in - if is_inductive then None else (Some uri) - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - ) - | C.Prod (n,so,de) -> - returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de - | _ -> None - in type_of_aux ~logger context t ugraph @@ -619,78 +566,24 @@ let rec split_prods ~subst context n te = | (_, _) -> raise (AssertFailure (lazy "split_prods")) ;; -let debruijn_constructor ?(cb=fun _ _ -> ()) uri number_of_types t = assert false -(* +let debruijn ?(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) + | C.Meta (i,(s,C.Ctx l)) -> + let l1 = NCicUtils.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 in - cb t res; - res + cb t res; res in - aux 0*) + aux 0 ;; - let sort_of_prod ~subst context (name,s) (t1, t2) = let t1 = R.whd ~subst context t1 in let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in @@ -731,14 +624,14 @@ 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 fix_lefts_in_constrs ~subst uri 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 + let debruijnedty = debruijn uri len ty in id, snd (split_prods ~subst tys paramsno ty), snd (split_prods ~subst tys paramsno debruijnedty)) cl @@ -872,9 +765,9 @@ let rec typeof ~subst ~metasenv context term = in if List.length pl <> constructorsno then raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match"))); - let j,branches_ok = + let j,branches_ok,p_ty, exp_p_ty = List.fold_left - (fun (j,b) p -> + (fun (j,b,old_p_ty,old_exp_p_ty) p -> if b then let cons = let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in @@ -884,23 +777,42 @@ let rec typeof ~subst ~metasenv context term = let ty_p = typeof_aux context p in let ty_cons = typeof_aux context cons in let ty_branch = - type_of_branch ~subst context leftno outtype cons ty_cons in - j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch + type_of_branch ~subst context leftno outtype cons ty_cons 0 + in + j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch, + ty_p, ty_branch else - j,false - ) (1,true) pl - in - if not branches_ok then - raise - (TypeCheckerFailure - (lazy (Printf.sprintf "Branch for constructor %s has wrong type" - (NCicPp.ppterm (C.Const - (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))))); - let res = outtype::arguments@[term] in - R.head_beta_reduce (C.Appl res) + j,false,old_p_ty,old_exp_p_ty + ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl + in + if not branches_ok then + raise + (TypeCheckerFailure + (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ + "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const + (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j))))) + (NCicPp.ppterm ~context (List.nth pl (j-1))) + (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); + let res = outtype::arguments@[term] in + R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false - and type_of_branch ~subst context leftno outty cons tycons = assert false + and type_of_branch ~subst context leftno outty cons tycons liftno = + match R.whd ~subst context tycons with + | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons] + | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) -> + let _,arguments = HExtlib.split_nth leftno tl in + C.Appl (S.lift liftno outty::arguments@[cons]) + | C.Prod (name,so,de) -> + let cons = + match S.lift 1 cons with + | C.Appl l -> C.Appl (l@[C.Rel 1]) + | t -> C.Appl [t ; C.Rel 1] + in + C.Prod (name,so, + type_of_branch ~subst ((name,(C.Decl so))::context) + leftno outty cons de (liftno+1)) + | _ -> raise (AssertFailure (lazy "type_of_branch")) (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -987,10 +899,10 @@ let rec typeof ~subst ~metasenv context term = let type_t = typeof_aux context t in if not (R.are_convertible ~subst ~metasenv context type_t ct) then raise (TypeCheckerFailure - (lazy (Printf.sprintf - ("Not well typed metavariable local context: "^^ - "expected a term of type %s, found %s of type %s") - (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) + (lazy (Printf.sprintf + ("Not well typed metavariable local context: "^^ + "expected a term of type %s, found %s of type %s") + (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) ) l lifted_canonical_context with Invalid_argument _ -> @@ -1045,7 +957,7 @@ let rec typeof ~subst ~metasenv context term = in typeof_aux context term -and check_mutual_inductive_defs _ = assert false +and check_mutual_inductive_defs _ = () and eat_lambdas ~subst context n te = match (n, R.whd ~subst context te) with @@ -1070,21 +982,22 @@ and guarded_by_destructors ~subst context recfuns t = if not (List.length tl > rec_no) then raise NotGuarded else let rec_arg = List.nth tl rec_no in - aux k rec_arg; + if not (is_really_smaller ~subst k rec_arg) then raise + NotGuarded; List.iter (aux k) tl - | C.Match (ref,outtype,term,pl) as t -> + | C.Match (Ref.Ref (_,uri,_) as 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 c_ctx,len,cl = fix_lefts_in_constrs ~subst uri 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 (_,_,bruijnedc) -> - let rl = recursive_args ~subst lefts_and_tys 0 len bruijnedc in + let rl = recursive_args ~subst c_ctx 0 len bruijnedc in let p, k = get_new_safes ~subst k p rl in aux k p) pl cl @@ -1160,161 +1073,23 @@ and split_prods ~subst context n te = 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) -> +and is_really_smaller ~subst (context, recfuns, x, safes as k) te = + match R.whd ~subst context te with + | C.Rel m when List.mem m safes -> true + | C.Rel _ -> false + | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd")) + | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _ + | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) -> + raise (AssertFailure (lazy "not a constructor")) + | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl")) + | C.Appl (he::_) -> + (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) + (*CSC: solo perche' non abbiamo trovato controesempi *) + (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*) + is_really_smaller ~subst k he + | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false + | 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 @@ -1329,81 +1104,65 @@ assert false (* List.fold_right (fun (_,_,ty,bo) i -> i && - check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl + is_really_smaller ~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 - *) + ) fl true*) + | C.Meta _ -> + true (* XXX if this check is repeated when the user completes the + definition *) + | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) -> + (match term with + | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x -> + let isinductive, paramsno, tl, _, i = E.get_checked_indtys ref in + if not isinductive then + List.for_all (is_really_smaller ~subst k) pl + else + let c_ctx,len,cl = fix_lefts_in_constrs ~subst uri paramsno tl i in + List.for_all2 + (fun p (_,_,debruijnedte) -> + let rl' = recursive_args ~subst c_ctx 0 len debruijnedte in + let e, k = get_new_safes ~subst k p rl' in + is_really_smaller ~subst k e) + pl cl + | _ -> List.for_all (is_really_smaller ~subst k) pl) -and returns_a_coinductive ~subst _ _ = assert false +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) + | C.Prod (n,so,de) -> + returns_a_coinductive ~subst ((n,C.Decl so)::context) de + | _ -> None -and type_of_constant ref = assert false (* USARE typecheck_obj0 *) -(* ALIAS typecheck *) -(* - let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj uobj -> - logger#log (`Start_type_checking uri) ; - let ugraph1_dust = - typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in - try - CicEnvironment.set_type_checking_info uri ; - logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') - | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError - ) - with - (* - this is raised if set_type_checking_info is called on an object - that has no associated universe file. If we are in univ_maker - phase this is OK since univ_maker will properly commit the - object. - *) - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph1_dust +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); + if not (fst (E.get_obj uri)) then + raise (AssertFailure (lazy "environment error")); + uobj in -CASO COSTRUTTORE - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) -CASO TIPO INDUTTIVO - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) -CASO COSTANTE -CASO FIX/COFIX -*) + match cobj, 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)) -> + let _,_,_,cl = List.nth tl i in + let _,_,arity = List.nth cl (j-1) in + arity + | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) -> + let _,_,_,arity,_ = List.nth fl i in + arity + | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty + | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) -and typecheck_obj0 (uri,height,metasenv,subst,kind) = +and check_obj_well_typed (uri,height,metasenv,subst,kind) = (* CSC: here we should typecheck the metasenv and the subst *) assert (metasenv = [] && subst = []); match kind with @@ -1415,7 +1174,7 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = "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.Inductive _ as obj -> check_mutual_inductive_defs obj | C.Fixpoint (inductive,fl,_) -> let types,kl,len = List.fold_left @@ -1425,6 +1184,7 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = ) ([],[],0) fl in List.iter (fun (_,name,x,ty,bo) -> + let bo = debruijn uri len bo in 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"))) @@ -1452,9 +1212,6 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = (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 - let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist) -*) -;; +let typecheck_obj = check_obj_well_typed;; + +(* EOF *)