From c7619e91ca47d2551e08d0dbfc6aaa66de7eca63 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:21:16 +0000 Subject: [PATCH] - added string_of_sort - attributes support --- helm/ocaml/cic_proof_checking/cicPp.ml | 23 +++++++++++++++-------- helm/ocaml/cic_proof_checking/cicPp.mli | 2 ++ 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index d2cf1a623..abb1b86f3 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -110,7 +110,7 @@ let rec pp t l = | C.MutInd (uri,n,exp_named_subst) -> (try match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (name,_,_,_) = get_nth dl (n+1) in name ^ pp_exp_named_subst exp_named_subst l | _ -> raise CicPpInternalError @@ -120,7 +120,7 @@ let rec pp t l = | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in let (id,_) = get_nth cons n2 in id ^ pp_exp_named_subst exp_named_subst l @@ -133,7 +133,7 @@ let rec pp t l = | C.MutCase (uri,n1,ty,te,patterns) -> let connames = (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in List.map (fun (id,_) -> id) cons | _ -> raise CicPpInternalError @@ -217,21 +217,21 @@ let ppobj obj = let module C = Cic in let module U = UriManager in match obj with - C.Constant (name, Some t1, t2, params) -> + C.Constant (name, Some t1, t2, params, _) -> "Definition of " ^ name ^ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 [] - | C.Constant (name, None, ty, params) -> + | C.Constant (name, None, ty, params, _) -> "Axiom " ^ name ^ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ "):\n" ^ pp ty [] - | C.Variable (name, bo, ty, params) -> + | C.Variable (name, bo, ty, params, _) -> "Variable " ^ name ^ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ ")" ^ ":\n" ^ pp ty [] ^ "\n" ^ (match bo with None -> "" | Some bo -> ":= " ^ pp bo []) - | C.CurrentProof (name, conjectures, value, ty, params) -> + | C.CurrentProof (name, conjectures, value, ty, params, _) -> "Current Proof of " ^ name ^ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ ")" ^ ":\n" ^ @@ -259,9 +259,16 @@ let ppobj obj = pp t name_context ^ "\n" ^ i ) conjectures "" ^ "\n" ^ pp value [] ^ " : " ^ pp ty [] - | C.InductiveDefinition (l, params, nparams) -> + | C.InductiveDefinition (l, params, nparams, _) -> "Parameters = " ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^ "NParams = " ^ string_of_int nparams ^ "\n" ^ List.fold_right (fun x i -> ppinductiveType x ^ i) l "" ;; + +let ppsort = function + | Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type _ -> "Type" + | Cic.CProp -> "CProp" + diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli index 417378d29..22c414031 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.mli +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -50,3 +50,5 @@ val pp : Cic.term -> (Cic.name option) list -> string val ppname : Cic.name -> string +val ppsort: Cic.sort -> string + -- 2.39.2