From: Enrico Tassi Date: Mon, 7 Apr 2008 10:22:52 +0000 (+0000) Subject: context, metasenv and subst made mandatory in CicPp X-Git-Tag: make_still_working~5439 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c8abd24ff28dfd95f1428dae80c5807a328e9ae;p=helm.git context, metasenv and subst made mandatory in CicPp --- diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index b21274fea..94acaf3f4 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -4,7 +4,7 @@ let ppterm = let set_ppterm f = ppterm := f;; -let ppterm ?(context=[]) ?(subst=[]) ?(metasenv=[]) t = +let ppterm ~context ~subst ~metasenv t = !ppterm ~context ~subst ~metasenv t ;; @@ -36,12 +36,13 @@ let trivial_pp_term ~context ~subst ~metasenv = ;; let ppobj = function - | (u,_,_,_,NCic.Fixpoint (b, fl, _)) -> + | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) -> "let rec "^NUri.string_of_uri u^"\n"^ String.concat "\nand " (List.map (fun (_,name,n,ty,bo) -> - name ^ " on " ^ string_of_int n ^ " : " ^ ppterm ty ^ " :=\n"^ - ppterm bo) fl) + name ^ " on " ^ string_of_int n ^ " : " ^ + ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^ + ppterm ~metasenv ~subst ~context:[] bo) fl) | (u,_,_,_,NCic.Inductive (b, _,tl, _)) -> "inductive" | (u,_,_,_,NCic.Constant (_,_,_, _, _)) -> "constant" ;; diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index 19b754eea..96a141ff7 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -5,9 +5,9 @@ val set_ppterm: NCic.term -> string) -> unit val ppterm: - ?context:NCic.context -> - ?subst:NCic.substitution -> - ?metasenv:NCic.metasenv -> + context:NCic.context -> + subst:NCic.substitution -> + metasenv:NCic.metasenv -> NCic.term -> string val trivial_pp_term: diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 7e9cd70b2..f96a6f317 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -584,7 +584,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types = aux 0 ;; -let sort_of_prod ~subst context (name,s) (t1, t2) = +let sort_of_prod ~metasenv ~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 match t1, t2 with @@ -599,7 +599,8 @@ let sort_of_prod ~subst context (name,s) (t1, t2) = | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: expected two sorts, found = %s, %s" - (NCicPp.ppterm t1) (NCicPp.ppterm t2)))) + (NCicPp.ppterm ~subst ~metasenv ~context t1) + (NCicPp.ppterm ~subst ~metasenv ~context t2)))) ;; let eat_prods ~subst ~metasenv context ty_he args_with_ty = @@ -620,7 +621,8 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = (TypeCheckerFailure (lazy (Printf.sprintf ("Appl: wrong parameter-type, expected %s, found %s") - (NCicPp.ppterm ty_arg) (NCicPp.ppterm s)))) + (NCicPp.ppterm ~subst ~metasenv ~context ty_arg) + (NCicPp.ppterm ~subst ~metasenv ~context s)))) | _ -> raise (TypeCheckerFailure @@ -685,22 +687,22 @@ let rec typeof ~subst ~metasenv context term = | C.Sort s -> C.Sort (C.Type 0) | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Meta (n,l) as t -> - let canonical_context,ty = + let canonical_ctx,ty = try let _,c,_,ty = U.lookup_subst n subst in c,ty with U.Subst_not_found _ -> try 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 t)))) + "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t)))) in - check_metasenv_consistency t context canonical_context l; + check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l; S.subst_meta l ty | C.Const ref -> type_of_constant ref | C.Prod (name,s,t) -> let sort1 = typeof_aux context s in let sort2 = typeof_aux ((name,(C.Decl s))::context) t in - sort_of_prod ~subst context (name,s) (sort1,sort2) + sort_of_prod ~metasenv ~subst context (name,s) (sort1,sort2) | C.Lambda (n,s,t) -> let sort = typeof_aux context s in (match R.whd ~subst context sort with @@ -710,7 +712,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 s) (NCicPp.ppterm sort))))); + "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s) + (NCicPp.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) -> @@ -720,7 +723,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 t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty)))) + (NCicPp.ppterm ~subst ~metasenv ~context t) + (NCicPp.ppterm ~subst ~metasenv ~context ty_t) + (NCicPp.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 @@ -749,19 +754,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 term)))) in + (NCicPp.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 ty) (NCicPp.ppterm (C.Const r'))))) + (NCicPp.ppterm ~subst ~metasenv ~context ty) + (NCicPp.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 ty)))) in + raise (TypeCheckerFailure (lazy (Printf.sprintf + "%s is partially applied" + (NCicPp.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 @@ -803,10 +810,12 @@ let rec typeof ~subst ~metasenv context term = raise (TypeCheckerFailure (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ - "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const - (Ref.mk_constructor j r))) - (NCicPp.ppterm ~context (List.nth pl (j-1))) - (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); + "has type %s\nnot convertible with %s") + (NCicPp.ppterm ~subst ~metasenv ~context + (C.Const (Ref.mk_constructor j r))) + (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-1))) + (NCicPp.ppterm ~metasenv ~subst ~context p_ty) + (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty)))); let res = outtype::arguments@[term] in R.head_beta_reduce (C.Appl res) | C.Match _ -> assert false @@ -831,7 +840,9 @@ let rec typeof ~subst ~metasenv context term = (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - with the actual context *) - and check_metasenv_consistency term context canonical_context l = + and check_metasenv_consistency + ~subst ~metasenv term context canonical_context l + = match l with | shift, NCic.Irl n -> let context = snd (HExtlib.split_nth shift context) in @@ -841,10 +852,11 @@ let rec typeof ~subst ~metasenv context term = | _,_,[] -> raise (AssertFailure (lazy (Printf.sprintf "Local and canonical context %s have different lengths" - (NCicPp.ppterm term)))) + (NCicPp.ppterm ~subst ~context ~metasenv term)))) | m,[],_::_ -> raise (TypeCheckerFailure (lazy (Printf.sprintf - "Unbound variable -%d in %s" m (NCicPp.ppterm term)))) + "Unbound variable -%d in %s" m + (NCicPp.ppterm ~subst ~metasenv ~context term)))) | m,t::tl,ct::ctl -> (match t,ct with (_,C.Decl t1), (_,C.Decl t2) @@ -856,15 +868,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 term) (NCicPp.ppterm t2) (NCicPp.ppterm t1) - ))) + (NCicPp.ppterm ~subst ~metasenv ~context term) + (NCicPp.ppterm ~subst ~metasenv ~context t2) + (NCicPp.ppterm ~subst ~metasenv ~context t1)))) | _,_ -> raise - (TypeCheckerFailure - (lazy (Printf.sprintf + (TypeCheckerFailure (lazy (Printf.sprintf ("Not well typed metavariable local context for %s: " ^^ "a definition expected, but a declaration found") - (NCicPp.ppterm term))))); + (NCicPp.ppterm ~subst ~metasenv ~context term))))); compare (m - 1,tl,ctl) in compare (n,context,canonical_context) @@ -908,7 +920,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 ct) (NCicPp.ppterm t)))) + (NCicPp.ppterm ~subst ~metasenv ~context ct) + (NCicPp.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 @@ -916,13 +929,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 ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t)))) + (NCicPp.ppterm ~subst ~metasenv ~context ct) + (NCicPp.ppterm ~subst ~metasenv ~context t) + (NCicPp.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 term)))) + (NCicPp.ppterm ~subst ~metasenv ~context term)))) and is_non_informative context paramsno c = let rec aux context c = @@ -973,20 +988,21 @@ let rec typeof ~subst ~metasenv context term = and check_mutual_inductive_defs _ = () -and eat_lambdas ~subst context n te = +and eat_lambdas ~subst ~metasenv 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 + eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta | (n, te) -> - raise (AssertFailure - (lazy (Printf.sprintf "9 (%d, %s)" n (NCicPp.ppterm te)))) + raise (AssertFailure (lazy (Printf.sprintf "9 (%d, %s)" n + (NCicPp.ppterm ~subst ~metasenv ~context te)))) -and guarded_by_destructors ~subst context recfuns t = +and guarded_by_destructors ~subst ~metasenv 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 as t when List.mem_assoc m recfuns -> - raise (NotGuarded (lazy (NCicPp.ppterm ~context t ^ " passed around"))) + raise (NotGuarded (lazy + (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around"))) | C.Rel m -> (match List.nth context (m-1) with | _,C.Decl _ -> () @@ -996,13 +1012,13 @@ and guarded_by_destructors ~subst context recfuns t = let rec_no = List.assoc m recfuns in if not (List.length tl > rec_no) then raise (NotGuarded (lazy - (NCicPp.ppterm ~context ~subst t ^ + (NCicPp.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 ~subst k rec_arg) then raise (NotGuarded (lazy - (NCicPp.ppterm ~context ~subst rec_arg ^ " not smaller"))); + (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller"))); List.iter (aux k) tl | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t -> (match R.whd ~subst context term with @@ -1186,15 +1202,16 @@ 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); + prerr_endline ("TY: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] ty); + prerr_endline ("BO: " ^ NCicPp.ppterm ~subst ~metasenv ~context:[] 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" - (NCicPp.ppterm ty_te) (NCicPp.ppterm ty)))) + (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te) + (NCicPp.ppterm ~subst ~metasenv ~context:[] ty)))) | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty) | C.Inductive _ as obj -> check_mutual_inductive_defs obj | C.Fixpoint (inductive,fl,_) -> @@ -1212,12 +1229,13 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) else if inductive then begin - let m, context = eat_lambdas ~subst types (x + 1) bo in + let m, context = eat_lambdas ~subst ~metasenv 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 ~subst context (enum_from (x+1) kl) m; + guarded_by_destructors + ~subst ~metasenv context (enum_from (x+1) kl) m end else match returns_a_coinductive ~subst [] ty with | None -> @@ -1225,7 +1243,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = (lazy "CoFix: does not return a coinductive type")) | Some uri -> (* guarded by constructors conditions C{f,M} *) - if not (guarded_by_constructors ~subst + if not (guarded_by_constructors ~subst ~metasenv types 0 len false bo [] uri) then raise (TypeCheckerFailure