From 3eca59409abc3dc4a3c4b07752282fb47e2a5c30 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 10:24:50 +0000 Subject: [PATCH] - bugfix: print metas local context in the rigth order - renamed string_of_name to ppname and exported it --- helm/ocaml/cic_proof_checking/cicPp.ml | 12 ++++++------ helm/ocaml/cic_proof_checking/cicPp.mli | 3 +++ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index a8d9eaa0b..5c5bd71ff 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -41,7 +41,7 @@ exception NotEnoughElements;; (* Utility functions *) -let string_of_name = +let ppname = function Cic.Name s -> s | Cic.Anonymous -> "_" @@ -79,7 +79,7 @@ let rec pp t l = | C.Meta (n,l1) -> "?" ^ (string_of_int n) ^ "[" ^ String.concat " ; " - (List.map (function None -> "_" | Some t -> pp t l) l1) ^ + (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ "]" | C.Sort s -> (match s with @@ -96,9 +96,9 @@ let rec pp t l = ) | C.Cast (v,t) -> pp v l | C.Lambda (b,s,t) -> - "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.LetIn (b,s,t) -> - "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) + "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.Appl li -> "(" ^ (List.fold_right @@ -226,11 +226,11 @@ let ppobj obj = (match context_entry with Some (n,C.Decl at) -> (separate i) ^ - string_of_name n ^ ":" ^ pp at name_context ^ " ", + ppname n ^ ":" ^ pp at name_context ^ " ", (Some n)::name_context | Some (n,C.Def (at,None)) -> (separate i) ^ - string_of_name n ^ ":= " ^ pp at name_context ^ " ", + ppname n ^ ":= " ^ pp at name_context ^ " ", (Some n)::name_context | None -> (separate i) ^ "_ :? _ ", None::name_context diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli index 9f68d0525..371b75e29 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.mli +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -45,3 +45,6 @@ val ppterm : Cic.term -> 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 ppname : Cic.name -> string + -- 2.39.2