From 08e9d02504942642a917c0d3e4b4795e65172d89 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 17:43:20 +0000 Subject: [PATCH] some debug printings --- helm/software/components/ng_kernel/nCicPp.ml | 3 ++- .../components/ng_kernel/nCicTypeChecker.ml | 19 ++++++++++++++++++- 2 files changed, 20 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 7af5d17a6..b21274fea 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -42,7 +42,8 @@ let ppobj = function (List.map (fun (_,name,n,ty,bo) -> name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ty ^ " :=\n"^ ppterm bo) fl) - | _ -> "todo" + | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive" + | (u,_,_,_,NCic.Constant (_,_,_, _, _)) -> "constant" ;; diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 81f633bb6..ceb14d17c 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -608,6 +608,11 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = | (arg, ty_arg)::tl -> (match R.whd ~subst context ty_he with | C.Prod (n,s,t) -> +(* + prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm + ~context ty_arg); + prerr_endline (NCicPp.ppterm ~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 else @@ -667,7 +672,9 @@ let does_not_occur ~subst context n nn t = exception NotGuarded;; let rec typeof ~subst ~metasenv context term = - let rec typeof_aux context = function + let rec typeof_aux context = + fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *) + match t with | C.Rel n -> (try match List.nth context (n - 1) with @@ -720,6 +727,13 @@ let rec typeof ~subst ~metasenv context term = | C.Appl (he::(_::_ as args)) -> 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 ~context ty_he); + prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~context) (List.map snd args_with_ty))); + prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm + ~context) (List.map fst args_with_ty))); +*) eat_prods ~subst ~metasenv context ty_he args_with_ty | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) -> @@ -1167,8 +1181,11 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = assert (metasenv = [] && subst = []); match kind with | C.Constant (_,_,Some te,ty,_) -> + prerr_endline ("TY: " ^ NCicPp.ppterm ty); + prerr_endline ("BO: " ^ NCicPp.ppterm te); let _ = typeof ~subst ~metasenv [] ty in let ty_te = typeof ~subst ~metasenv [] te in + prerr_endline "XXXX"; if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then raise (TypeCheckerFailure (lazy (Printf.sprintf "the type of the body is not the one expected:\n%s\nvs\n%s" -- 2.39.2