From b20889b47bf949b17a6297ac39a5c0df0301de9e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 12 Nov 2006 18:58:56 +0000 Subject: [PATCH] The pretty printers in CicPp now have an optional ~metasenv argument to show the globally restricted arguments of a metavariable local context as locally restricted. The pretty printers in CicMetaSubst have the same argument, but the argument is mandatory. --- components/cic_proof_checking/cicPp.ml | 57 ++++++--- components/cic_proof_checking/cicPp.mli | 6 +- components/cic_unification/cicMetaSubst.ml | 49 ++++---- components/cic_unification/cicMetaSubst.mli | 15 ++- components/cic_unification/cicRefine.ml | 122 +++++++++---------- components/cic_unification/cicUnification.ml | 78 ++++++------ components/library/cicCoercion.ml | 2 +- components/library/refinementTool.ml | 2 +- components/tactics/inversion.ml | 4 +- 9 files changed, 185 insertions(+), 150 deletions(-) diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml index f3560cc3a..55d94899b 100644 --- a/components/cic_proof_checking/cicPp.ml +++ b/components/cic_proof_checking/cicPp.ml @@ -62,6 +62,7 @@ let rec get_nth l n = (* pretty-prints a term t of cic in an environment l where l is a list of *) (* identifier names used to resolve DeBrujin indexes. The head of l is the *) (* name associated to the greatest DeBrujin index in t *) +let pp ?metasenv = let rec pp t l = let module C = Cic in match t with @@ -79,10 +80,33 @@ let rec pp t l = | C.Var (uri,exp_named_subst) -> UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l | C.Meta (n,l1) -> - "?" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ - "]" + (match metasenv with + None -> + "?" ^ (string_of_int n) ^ "[" ^ + String.concat " ; " + (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ + "]" + | Some metasenv -> + try + let _,context,_ = CicUtil.lookup_meta n metasenv in + "?" ^ (string_of_int n) ^ "[" ^ + String.concat " ; " + (List.rev + (List.map2 + (fun x y -> + match x,y with + _, None + | None, _ -> "_" + | Some _, Some t -> pp t l + ) context l1)) ^ + "]" + with + CicUtil.Meta_not_found _ -> + "???" ^ (string_of_int n) ^ "[" ^ + String.concat " ; " + (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ + "]" + ) | C.Sort s -> (match s with C.Prop -> "Prop" @@ -223,10 +247,12 @@ and pp_exp_named_subst exp_named_subst l = (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l) exp_named_subst ) ^ "]" +in + pp ;; -let ppterm t = - pp t [] +let ppterm ?metasenv t = + pp ?metasenv t [] ;; (* ppinductiveType (typename, inductive, arity, cons) *) @@ -241,20 +267,20 @@ let ppinductiveType (typename, inductive, arity, cons) = cons "" ;; -let ppcontext ?(sep = "\n") context = +let ppcontext ?metasenv ?(sep = "\n") context = let separate s = if s = "" then "" else s ^ sep in fst (List.fold_right (fun context_entry (i,name_context) -> match context_entry with Some (n,Cic.Decl t) -> Printf.sprintf "%s%s : %s" (separate i) (ppname n) - (pp t name_context), (Some n)::name_context + (pp ?metasenv t name_context), (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n) (match ty with None -> "_" - | Some ty -> pp ty name_context) - (pp bo name_context), (Some n)::name_context + | Some ty -> pp ?metasenv ty name_context) + (pp ?metasenv bo name_context), (Some n)::name_context | None -> Printf.sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[])) @@ -292,11 +318,13 @@ let ppobj obj = (match context_entry with Some (n,C.Decl at) -> (separate i) ^ - ppname n ^ ":" ^ pp at name_context ^ " ", + ppname n ^ ":" ^ + pp ~metasenv:conjectures at name_context ^ " ", (Some n)::name_context | Some (n,C.Def (at,None)) -> (separate i) ^ - ppname n ^ ":= " ^ pp at name_context ^ " ", + ppname n ^ ":= " ^ pp ~metasenv:conjectures + at name_context ^ " ", (Some n)::name_context | None -> (separate i) ^ "_ :? _ ", None::name_context @@ -304,9 +332,10 @@ let ppobj obj = ) context ("",[]) in conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ - pp t name_context ^ "\n" ^ i + pp ~metasenv:conjectures t name_context ^ "\n" ^ i ) conjectures "" ^ - "\n" ^ pp value [] ^ " : " ^ pp ty [] + "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^ + pp ~metasenv:conjectures ty [] | C.InductiveDefinition (l, params, nparams, _) -> "Parameters = " ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^ diff --git a/components/cic_proof_checking/cicPp.mli b/components/cic_proof_checking/cicPp.mli index e84ae4fed..e898c352d 100644 --- a/components/cic_proof_checking/cicPp.mli +++ b/components/cic_proof_checking/cicPp.mli @@ -40,13 +40,13 @@ (* similar to the one used by Coq *) val ppobj : Cic.obj -> string -val ppterm : Cic.term -> string +val ppterm : ?metasenv:Cic.metasenv -> Cic.term -> string -val ppcontext : ?sep:string -> Cic.context -> string +val ppcontext : ?metasenv:Cic.metasenv -> ?sep:string -> Cic.context -> string (* Required only by the topLevel. It is the generalization of ppterm to *) (* work with environments. *) -val pp : Cic.term -> (Cic.name option) list -> string +val pp : ?metasenv:Cic.metasenv -> Cic.term -> (Cic.name option) list -> string val ppname : Cic.name -> string diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 8d53495bf..c097eacf2 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -293,67 +293,70 @@ let apply_subst_metasenv subst metasenv = (***** Pretty printing functions ******) -let ppterm subst term = CicPp.ppterm (apply_subst subst term) +let ppterm ~metasenv subst term = + CicPp.ppterm ~metasenv (apply_subst subst term) -let ppterm_in_name_context subst term name_context = - CicPp.pp (apply_subst subst term) name_context +let ppterm_in_name_context ~metasenv subst term name_context = + CicPp.pp ~metasenv (apply_subst subst term) name_context -let ppterm_in_context subst term context = +let ppterm_in_context ~metasenv subst term context = let name_context = List.map (function None -> None | Some (n,_) -> Some n) context in - ppterm_in_name_context subst term name_context + ppterm_in_name_context ~metasenv subst term name_context -let ppcontext' ?(sep = "\n") subst context = +let ppcontext' ~metasenv ?(sep = "\n") subst context = let separate s = if s = "" then "" else s ^ sep in List.fold_right (fun context_entry (i,name_context) -> match context_entry with Some (n,Cic.Decl t) -> sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_name_context subst t name_context), (Some n)::name_context + (ppterm_in_name_context ~metasenv subst t name_context), + (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) (match ty with None -> "_" - | Some ty -> ppterm_in_name_context subst ty name_context) - (ppterm_in_name_context subst bo name_context), (Some n)::name_context + | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context) + (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context | None -> sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) -let ppsubst_unfolded subst = +let ppsubst_unfolded ~metasenv subst = String.concat "\n" (List.map (fun (idx, (c, t,_)) -> - let context,name_context = ppcontext' ~sep:"; " subst c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context subst t name_context)) + (ppterm_in_name_context ~metasenv subst t name_context)) subst) (* Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) subst) *) ;; -let ppsubst subst = +let ppsubst ~metasenv subst = String.concat "\n" (List.map (fun (idx, (c, t, _)) -> - let context,name_context = ppcontext' ~sep:"; " [] c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context [] t name_context)) + (ppterm_in_name_context ~metasenv [] t name_context)) subst) ;; -let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) +let ppcontext ~metasenv ?sep subst context = + fst (ppcontext' ~metasenv ?sep subst context) let ppmetasenv ?(sep = "\n") subst metasenv = String.concat sep (List.map (fun (i, c, t) -> - let context,name_context = ppcontext' ~sep:"; " subst c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in sprintf "%s |- ?%d: %s" context i - (ppterm_in_name_context subst t name_context)) + (ppterm_in_name_context ~metasenv subst t name_context)) (List.filter (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv)) @@ -583,7 +586,7 @@ let rec restrict subst to_be_restricted metasenv = let error_msg = lazy (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" n (names_of_context_indexes context to_be_restricted) n - (ppterm subst term)) + (ppterm ~metasenv subst term)) in (* DEBUG debug_print (lazy error_msg); @@ -657,7 +660,7 @@ let delift n subst context metasenv l t = if (i = n) then raise (MetaSubstFailure (lazy (sprintf "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm subst t)))) + i (ppterm ~metasenv subst t)))) else begin (* I do not consider the term associated to ?i in subst since *) @@ -741,10 +744,10 @@ debug_print(lazy (sprintf )))); *) let msg = (lazy (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) + (ppterm ~metasenv subst t) (String.concat "; " (List.map - (function Some t -> ppterm subst t | None -> "_") + (function Some t -> ppterm ~metasenv subst t | None -> "_") l)))) in if @@ -909,6 +912,6 @@ let fpp_gen ppf s = Format.pp_print_newline ppf (); Format.pp_print_flush ppf () -let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) +let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) diff --git a/components/cic_unification/cicMetaSubst.mli b/components/cic_unification/cicMetaSubst.mli index 96f87205f..2b60b04e0 100644 --- a/components/cic_unification/cicMetaSubst.mli +++ b/components/cic_unification/cicMetaSubst.mli @@ -61,14 +61,17 @@ val delift_rels : (** {2 Pretty printers} *) -val ppsubst_unfolded: Cic.substitution -> string -val ppsubst: Cic.substitution -> string -val ppterm: Cic.substitution -> Cic.term -> string -val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string +val ppsubst_unfolded: metasenv:Cic.metasenv -> Cic.substitution -> string +val ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string +val ppterm: metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> string +val ppcontext: + metasenv:Cic.metasenv -> ?sep: string -> Cic.substitution -> Cic.context -> + string val ppterm_in_name_context: - Cic.substitution -> Cic.term -> (Cic.name option) list -> string + metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> + (Cic.name option) list -> string val ppterm_in_context: - Cic.substitution -> Cic.term -> Cic.context -> string + metasenv:Cic.metasenv -> Cic.substitution -> Cic.term -> Cic.context -> string val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string (** {2 Format-like pretty printers} diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index e1253f8e8..36347ccd1 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -146,12 +146,12 @@ let is_a_double_coercion t = | _ -> dummyres let more_args_than_expected - localization_tbl subst he context hetype' tlbody_and_type exn + localization_tbl metasenv subst he context hetype' tlbody_and_type exn = let msg = lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he context ^ - " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ + " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ " arguments that are more than expected") in @@ -427,11 +427,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl te' ~f:(fun _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst'' te' + CicMetaSubst.ppterm_in_context metasenv'' subst'' te' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst'' inferredty + CicMetaSubst.ppterm_in_context metasenv'' subst'' inferredty context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst'' ty' context)) exn + CicMetaSubst.ppterm_in_context metasenv'' subst'' ty' context)) exn ) | C.Prod (name,s,t) -> let carr t subst context = CicMetaSubst.apply_subst subst t in @@ -460,17 +460,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl t (Uncertain (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst t context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -485,10 +485,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl t (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort")))) in @@ -534,17 +534,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl s' (Uncertain (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -559,9 +559,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst s' context ^ + CicMetaSubst.ppterm_in_context ~metasenv subst s' context ^ " is not a type since it has type " ^ - CicMetaSubst.ppterm_in_context + CicMetaSubst.ppterm_in_context ~metasenv subst coercion_src context ^ " that is not a sort"))) in @@ -691,11 +691,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl term' exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst term' + CicMetaSubst.ppterm_in_context ~metasenv subst term' context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst actual_type + CicMetaSubst.ppterm_in_context ~metasenv subst actual_type context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_type' context)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) in let rec instantiate_prod t = function @@ -911,11 +911,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl p exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst p + CicMetaSubst.ppterm_in_context ~metasenv subst p context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst instance' + CicMetaSubst.ppterm_in_context ~metasenv subst instance' context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst instance + CicMetaSubst.ppterm_in_context ~metasenv subst instance context))) (subst,metasenv,ugraph5) pl' outtypeinstances in @@ -952,11 +952,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'] , subst',metasenv',ugraph' @@ -1005,11 +1005,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t enrich localization_tbl bo exn ~f:(function _ -> lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst bo + CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst ty_of_bo + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo context' ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst expected_ty + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty context)) in fl @ [bo'],subst',metasenv',ugraph' @@ -1070,7 +1070,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (try prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel."); fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -1081,19 +1081,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context with Invalid_argument _ -> raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" - (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) - (CicMetaSubst.ppcontext subst canonical_context)))) + (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext ~metasenv subst canonical_context)))) and check_exp_named_subst metasubst metasenv context tl ugraph = let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = @@ -1126,9 +1126,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il with _ -> raise (RefineFailure (lazy ("Wrong Explicit Named Substitution: " ^ - CicMetaSubst.ppterm metasubst' typeoft ^ + CicMetaSubst.ppterm metasenv' metasubst' typeoft ^ " not unifiable with " ^ - CicMetaSubst.ppterm metasubst' typeofvar))) + CicMetaSubst.ppterm metasenv' metasubst' typeofvar))) in (* FIXME: no mere tail recursive! *) let exp_name_subst, metasubst''', metasenv''', ugraph4 = @@ -1185,16 +1185,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (lazy (sprintf "%s is supposed to be a type, but its type is %s" - (CicMetaSubst.ppterm_in_context subst t context) - (CicMetaSubst.ppterm_in_context subst t2 context)))) + (CicMetaSubst.ppterm_in_context ~metasenv subst t context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)))) | _,_ -> enrich localization_tbl t (RefineFailure (lazy (sprintf "%s is supposed to be a type, but its type is %s" - (CicMetaSubst.ppterm_in_context subst s context) - (CicMetaSubst.ppterm_in_context subst t1 context)))) + (CicMetaSubst.ppterm_in_context ~metasenv subst s context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)))) and avoid_double_coercion context subst metasenv ugraph t ty = if not !pack_coercions then @@ -1317,8 +1317,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ we search a coercion of the head (saturated) to funclass *) let metasenv = pristinemenv in debug_print (lazy - ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ - " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' + ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^ + " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' (* ^ " cause: " ^ Lazy.force s *))); let how_many_args_are_needed = let rec aux n = function @@ -1355,7 +1355,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il HExtlib.list_findopt (fun coerc -> let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) @@ -1367,8 +1367,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il mk_prod_of_metas metasenv context subst remainder in debug_print (lazy - (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ - CicMetaSubst.ppterm subst hetype')); + (" unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ + CicMetaSubst.ppterm ~metasenv subst hetype')); let subst,metasenv,ugraph = fo_unif_subst_eat_prods subst context metasenv tty hetype' ugraph @@ -1392,7 +1392,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> subst,metasenv,ugraph,hetype',he,args_bo_and_ty | None -> - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} end coercion to funclass stuff *) (* }}} end fix_arity *) @@ -1432,21 +1432,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl hete exn ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.NotMetaClosed -> enrich localization_tbl hete exn ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion candidates -> let selected = @@ -1476,21 +1476,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Lazy.force e*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst hete + CicMetaSubst.ppterm_in_context ~metasenv subst hete context ^ " has type " ^ - CicMetaSubst.ppterm_in_context subst hety + CicMetaSubst.ppterm_in_context ~metasenv subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context + CicMetaSubst.ppterm_in_context ~metasenv subst s context (* "\nReason: " ^ Printexc.to_string exn*)))) exn (* }}} end coercion stuff *) in @@ -1508,7 +1508,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn (* }}} *) in @@ -1523,7 +1523,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il fix_arity metasenv context subst he hetype args_bo_and_ty ugraph with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - more_args_than_expected localization_tbl + more_args_than_expected localization_tbl metasenv subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph = diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index c9981bb11..86f280842 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -53,22 +53,22 @@ let foo () = (sprintf "Kernel Type checking error: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppterm [] term) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in raise (AssertFailure msg) | CicTypeChecker.AssertFailure msg -> let msg = lazy (sprintf "Kernel Type checking assertion failure: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppterm [] term) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppterm ~metasenv subst term) + (CicMetaSubst.ppterm ~metasenv [] term) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in raise (AssertFailure msg) in profiler_toa.HExtlib.profile foo () ;; @@ -367,16 +367,16 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (* (sprintf "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2))) *) | Invalid_argument _ -> raise (UnificationFailure (lazy "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) in subst,metasenv,ugraph1 | (C.Meta (n,_), C.Meta (m,_)) when n>m -> fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph @@ -464,8 +464,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then fo_unif_subst_exp_named_subst @@ -476,8 +476,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then @@ -489,8 +489,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only subst context metasenv te t2 ugraph @@ -665,7 +665,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv t1 t2' ugraph | _ -> raise (UnificationFailure - (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 )))) + (lazy ("not a mutind :"^CicMetaSubst.ppterm ~metasenv subst t2 )))) | _ -> raise exn))) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = @@ -685,8 +685,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy "6.1"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) *) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) *) | (C.Rel _, _) | (_, C.Rel _) -> if t1 = t2 then subst, metasenv,ugraph @@ -694,8 +694,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many @@ -739,8 +739,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ raise (UnificationFailure (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2))))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2))))) *) | (_,_) -> (* delta-beta reduction should almost never be a problem for @@ -759,8 +759,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) else try fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph @@ -771,8 +771,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (lazy (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) - (CicMetaSubst.ppterm subst t2)))) + (CicMetaSubst.ppterm ~metasenv subst t1) + (CicMetaSubst.ppterm ~metasenv subst t2)))) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph @@ -789,7 +789,7 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv String.concat " ; " (List.map (fun (uri,t) -> - UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t) + UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t) ) ens) in raise (UnificationFailure (lazy (sprintf @@ -809,7 +809,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = lazy ( if verbose then sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" - (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm ~metasenv subst t1) (try let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in CicPp.ppterm ty_t1 @@ -817,7 +817,7 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm subst t2) + (CicMetaSubst.ppterm ~metasenv subst t2) (try let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in CicPp.ppterm ty_t2 @@ -825,28 +825,28 @@ let enrich_msg msg subst context metasenv t1 t2 ugraph = | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) (Lazy.force msg) + (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg) else sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicMetaSubst.ppterm_in_context subst t1 context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context) (try let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicMetaSubst.ppterm_in_context subst ty_t1 context + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context with | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm_in_context subst t2 context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context) (try let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicMetaSubst.ppterm_in_context subst ty_t2 context + CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context with | UnificationFailure s | Uncertain s | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppcontext ~metasenv subst context) (CicMetaSubst.ppmetasenv subst metasenv) (Lazy.force msg) ) diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 33309f109..f06035604 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -216,7 +216,7 @@ let generate_composite_closure rt c1 c2 univ arity = let body_metasenv = order_body_menv term body_metasenv in debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); let subst = create_subst_from_metas_to_rels spline_len body_metasenv in - debug_print (lazy("SUBST: "^rt.RT.ppsubst subst)); + debug_print (lazy("SUBST: "^rt.RT.ppsubst body_metasenv subst)); let term = rt.RT.apply_subst subst term in debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term)); (match rt.RT.type_of_aux' metasenv [] term ugraph with diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml index 70af8740b..e9dae40d9 100644 --- a/components/library/refinementTool.ml +++ b/components/library/refinementTool.ml @@ -35,7 +35,7 @@ type kit = { type_of_rc; pack_coercion_obj: Cic.obj -> Cic.obj; apply_subst: Cic.substitution -> Cic.term -> Cic.term ; - ppsubst: Cic.substitution -> string; + ppsubst: metasenv:Cic.metasenv -> Cic.substitution -> string; ppmetasenv: Cic.substitution -> Cic.metasenv -> string; } diff --git a/components/tactics/inversion.ml b/components/tactics/inversion.ml index e381b3003..e7adcb7a8 100644 --- a/components/tactics/inversion.ml +++ b/components/tactics/inversion.ml @@ -224,7 +224,7 @@ let private_inversion_tac ~term = parameters_tys goalty uri_of_eq in (*DEBUG*) debug_print (lazy ("cut term " ^ CicPp.ppterm cut_term)); debug_print (lazy ("CONTEXT before apply HCUT: " ^ - (CicMetaSubst.ppcontext [] context ))); + (CicMetaSubst.ppcontext ~metasenv [] context ))); debug_print (lazy ("termty " ^ CicPp.ppterm termty)); (* cut DXn=DXn \to GOAL *) let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in @@ -255,7 +255,7 @@ let private_inversion_tac ~term = debug_print (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl rightparameters)))); debug_print (lazy ("CONTEXT before refinement: " ^ - (CicMetaSubst.ppcontext [] context ))); + (CicMetaSubst.ppcontext ~metasenv [] context ))); (*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^ CicPp.ppterm t)); let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t -- 2.39.2