X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicPp.ml;fp=components%2Fcic_proof_checking%2FcicPp.ml;h=1686cd3572ab57d09a255d9a47f5c6409db367bb;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml new file mode 100644 index 000000000..1686cd357 --- /dev/null +++ b/components/cic_proof_checking/cicPp.ml @@ -0,0 +1,534 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* This module implements a very simple Coq-like pretty printer that, given *) +(* an object of cic (internal representation) returns a string describing *) +(* the object in a syntax similar to that of coq *) +(* *) +(* It also contains the utility functions to check a name w.r.t the Matita *) +(* naming policy *) +(* *) +(*****************************************************************************) + +(* $Id$ *) + +exception CicPpInternalError;; +exception NotEnoughElements;; + +(* Utility functions *) + +let ppname = + function + Cic.Name s -> s + | Cic.Anonymous -> "_" +;; + +(* get_nth l n returns the nth element of the list l if it exists or *) +(* raises NotEnoughElements if l has less than n elements *) +let rec get_nth l n = + match (n,l) with + (1, he::_) -> he + | (n, he::tail) when n > 1 -> get_nth tail (n-1) + | (_,_) -> raise NotEnoughElements +;; + +(* pp t l *) +(* 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 + C.Rel n -> + begin + try + (match get_nth l n with + Some (C.Name s) -> s + | Some C.Anonymous -> "__" ^ string_of_int n + | None -> "_hidden_" ^ string_of_int n + ) + with + NotEnoughElements -> string_of_int (List.length l - n) + end + | 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) -> + (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 _ + | Invalid_argument _ -> + "???" ^ (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" + | C.Set -> "Set" + | C.Type _ -> "Type" + (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) + | C.CProp -> "CProp" + ) + | C.Implicit (Some `Hole) -> "%" + | C.Implicit _ -> "?" + | C.Prod (b,s,t) -> + (match b with + C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")" + | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")" + ) + | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")" + | C.Lambda (b,s,t) -> + "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")" + | C.LetIn (b,s,ty,t) -> + " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l) + | C.Appl li -> + "(" ^ + (List.fold_right + (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i) + li "" + ) ^ ")" + | C.Const (uri,exp_named_subst) -> + UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l + | C.MutInd (uri,n,exp_named_subst) -> + (try + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (dl,_,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + name ^ pp_exp_named_subst exp_named_subst l + | _ -> raise CicPpInternalError + with + Sys.Break as exn -> raise exn + | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1) + ) + | C.MutConstruct (uri,n1,n2,exp_named_subst) -> + (try + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + 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 + | _ -> raise CicPpInternalError + with + Sys.Break as exn -> raise exn + | _ -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^ + string_of_int n2 + ) + | C.MutCase (uri,n1,ty,te,patterns) -> + let connames_and_argsno = + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (dl,_,paramsno,_) -> + let (_,_,_,cons) = get_nth dl (n1+1) in + List.map + (fun (id,ty) -> + (* this is just an approximation since we do not have + reduction yet! *) + let rec count_prods toskip = + function + C.Prod (_,_,bo) when toskip > 0 -> + count_prods (toskip - 1) bo + | C.Prod (_,_,bo) -> 1 + count_prods 0 bo + | _ -> 0 + in + id, count_prods paramsno ty + ) cons + | _ -> raise CicPpInternalError + ) + in + let connames_and_argsno_and_patterns = + let rec combine = + function + [],[] -> [] + | [],l -> List.map (fun x -> "???",0,Some x) l + | l,[] -> List.map (fun (x,no) -> x,no,None) l + | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly)) + in + combine (connames_and_argsno,patterns) + in + "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^ + (String.concat "\n | " + (List.map + (fun (x,argsno,y) -> + let rec aux argsno l = + function + Cic.Lambda (name,ty,bo) when argsno > 0 -> + let args,res = aux (argsno - 1) (Some name::l) bo in + ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^ + ":" ^ pp ty l ^ ")")::args, res + | t when argsno = 0 -> [],pp t l + | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l + in + let pattern,body = + match y with + None -> x,"" + | Some y when argsno = 0 -> x,pp y l + | Some y -> + let args,body = aux argsno l y in + "(" ^ x ^ " " ^ String.concat " " args ^ ")",body + in + pattern ^ " => " ^ body + ) connames_and_argsno_and_patterns)) ^ + "\n]" + | C.Fix (no, funs) -> + let snames = List.map (fun (name,_,_,_) -> name) funs in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in + "\nFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" + | C.CoFix (no,funs) -> + let snames = List.map (fun (name,_,_) -> name) funs in + let names = + List.rev (List.map (function name -> Some (C.Name name)) snames) + in + "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^ + List.fold_right + (fun (name,ty,bo) i -> "\n" ^ name ^ + " : " ^ pp ty l ^ " := \n" ^ + pp bo (names@l) ^ i) + funs "" ^ + "}\n" +and pp_exp_named_subst exp_named_subst l = + if exp_named_subst = [] then "" else + "\\subst[" ^ + String.concat " ; " ( + List.map + (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l) + exp_named_subst + ) ^ "]" +in + pp +;; + +let ppterm ?metasenv t = + pp ?metasenv t [] +;; + +(* ppinductiveType (typename, inductive, arity, cons) *) +(* pretty-prints a single inductive definition *) +(* (typename, inductive, arity, cons) *) +let ppinductiveType (typename, inductive, arity, cons) = + (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^ + pp arity [] ^ " =\n " ^ + List.fold_right + (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ + (if i = "" then "\n" else "\n | ") ^ i) + cons "" +;; + +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 ?metasenv t name_context), (Some n)::name_context + | Some (n,Cic.Def (bo,ty)) -> + Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n) + (pp ?metasenv ty name_context) + (pp ?metasenv bo name_context), (Some n)::name_context + | None -> + Printf.sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[])) + +(* ppobj obj returns a string with describing the cic object obj in a syntax *) +(* similar to the one used by Coq *) +let ppobj obj = + let module C = Cic in + let module U = UriManager in + match obj with + 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, _) -> + "Axiom " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + "):\n" ^ pp ty [] + | 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, _) -> + "Current Proof of " ^ name ^ + "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ + ")" ^ ":\n" ^ + let separate s = if s = "" then "" else s ^ " ; " in + List.fold_right + (fun (n, context, t) i -> + let conjectures',name_context = + List.fold_right + (fun context_entry (i,name_context) -> + (match context_entry with + Some (n,C.Decl at) -> + (separate i) ^ + ppname n ^ ":" ^ + pp ~metasenv:conjectures at name_context ^ " ", + (Some n)::name_context + | Some (n,C.Def (at,aty)) -> + (separate i) ^ + ppname n ^ ": " ^ + pp ~metasenv:conjectures aty name_context ^ + ":= " ^ pp ~metasenv:conjectures + at name_context ^ " ", + (Some n)::name_context + | None -> + (separate i) ^ "_ :? _ ", None::name_context) + ) context ("",[]) + in + conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ + pp ~metasenv:conjectures t name_context ^ "\n" ^ i + ) conjectures "" ^ + "\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" ^ + "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" + + +(* MATITA NAMING CONVENTION *) + +let is_prefix prefix string = + let len = String.length prefix in + let len1 = String.length string in + if len <= len1 then + begin + let head = String.sub string 0 len in + if + (String.compare (String.lowercase head) (String.lowercase prefix)=0) then + begin + let diff = len1-len in + let tail = String.sub string len diff in + if ((diff > 0) && (String.rcontains_from tail 0 '_')) then + Some (String.sub tail 1 (diff-1)) + else Some tail + end + else None + end + else None + +let remove_prefix prefix (last,string) = + if string = "" then (last,string) + else + match is_prefix prefix string with + None -> + if last <> "" then + match is_prefix last prefix with + None -> (last,string) + | Some _ -> + (match is_prefix prefix (last^string) with + None -> (last,string) + | Some tail -> (prefix,tail)) + else (last,string) + | Some tail -> (prefix, tail) + +let legal_suffix string = + if string = "" then true else + begin + let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in + (Str.string_match legal_s string 0) && (Str.matched_string string = string) + end + +(** check if a prefix of string_name is legal for term and returns the tail. + chec_rec cannot fail: at worst it return string_name. + The algorithm is greedy, but last contains the last name matched, providing + a one slot buffer. + string_name is here a pair (last,string_name).*) + +let rec check_rec ctx string_name = + function + | Cic.Rel m -> + (match List.nth ctx (m-1) with + Cic.Name name -> + remove_prefix name string_name + | Cic.Anonymous -> string_name) + | Cic.Meta _ -> string_name + | Cic.Sort sort -> remove_prefix (ppsort sort) string_name + | Cic.Implicit _ -> string_name + | Cic.Cast (te,ty) -> check_rec ctx string_name te + | Cic.Prod (name,so,dest) -> + let l_string_name = check_rec ctx string_name so in + check_rec (name::ctx) string_name dest + | Cic.Lambda (name,so,dest) -> + let string_name = + match name with + Cic.Anonymous -> string_name + | Cic.Name name -> remove_prefix name string_name in + let l_string_name = check_rec ctx string_name so in + check_rec (name::ctx) l_string_name dest + | Cic.LetIn (name,so,_,dest) -> + let string_name = check_rec ctx string_name so in + check_rec (name::ctx) string_name dest + | Cic.Appl l -> + List.fold_left (check_rec ctx) string_name l + | Cic.Var (uri,exp_named_subst) -> + let name = UriManager.name_of_uri uri in + remove_prefix name string_name + | Cic.Const (uri,exp_named_subst) -> + let name = UriManager.name_of_uri uri in + remove_prefix name string_name + | Cic.MutInd (uri,_,exp_named_subst) -> + let name = UriManager.name_of_uri uri in + remove_prefix name string_name + | Cic.MutConstruct (uri,n,m,exp_named_subst) -> + let name = + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + Cic.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cons) = get_nth dl (n+1) in + let (id,_) = get_nth cons m in + id + | _ -> assert false) in + remove_prefix name string_name + | Cic.MutCase (_,_,_,te,pl) -> + let string_name = remove_prefix "match" string_name in + let string_name = check_rec ctx string_name te in + List.fold_right (fun t s -> check_rec ctx s t) pl string_name + | Cic.Fix (_,fl) -> + let string_name = remove_prefix "fix" string_name in + let names = List.map (fun (name,_,_,_) -> name) fl in + let onames = + List.rev (List.map (function name -> Cic.Name name) names) + in + List.fold_right + (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name + | Cic.CoFix (_,fl) -> + let string_name = remove_prefix "cofix" string_name in + let names = List.map (fun (name,_,_) -> name) fl in + let onames = + List.rev (List.map (function name -> Cic.Name name) names) + in + List.fold_right + (fun (_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name + +let check_name ?(allow_suffix=false) ctx name term = + let (_,tail) = check_rec ctx ("",name) term in + if (not allow_suffix) then (String.length tail = 0) + else legal_suffix tail + +let check_elim ctx conclusion_name = + let elim = Str.regexp "_elim\\|_case" in + if (Str.string_match elim conclusion_name 0) then + let len = String.length conclusion_name in + let tail = String.sub conclusion_name 5 (len-5) in + legal_suffix tail + else false + +let rec check_names ctx hyp_names conclusion_name t = + match t with + | Cic.Prod (name,s,t) -> + (match hyp_names with + [] -> check_names (name::ctx) hyp_names conclusion_name t + | hd::tl -> + if check_name ctx hd s then + check_names (name::ctx) tl conclusion_name t + else + check_names (name::ctx) hyp_names conclusion_name t) + | Cic.Appl ((Cic.Rel n)::args) -> + (match hyp_names with + | [] -> + (check_name ~allow_suffix:true ctx conclusion_name t) || + (check_elim ctx conclusion_name) + | [what_to_elim] -> + (* what to elim could be an argument + of the predicate: e.g. leb_elim *) + let (last,tail) = + List.fold_left (check_rec ctx) ("",what_to_elim) args in + (tail = "" && check_elim ctx conclusion_name) + | _ -> false) + | Cic.MutCase (_,_,Cic.Lambda(name,so,ty),te,_) -> + (match hyp_names with + | [] -> + (match is_prefix "match" conclusion_name with + None -> check_name ~allow_suffix:true ctx conclusion_name t + | Some tail -> check_name ~allow_suffix:true ctx tail t) + | [what_to_match] -> + (* what to match could be the term te or its type so; in this case the + conclusion name should match ty *) + check_name ~allow_suffix:true (name::ctx) conclusion_name ty && + (check_name ctx what_to_match te || check_name ctx what_to_match so) + | _ -> false) + | _ -> + hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t + +let check name term = + let names = Str.split (Str.regexp_string "_to_") name in + let hyp_names,conclusion_name = + match List.rev names with + [] -> assert false + | hd::tl -> + let elim = Str.regexp "_elim\\|_case" in + let len = String.length hd in + try + let pos = Str.search_backward elim hd len in + let hyp = String.sub hd 0 pos in + let concl = String.sub hd pos (len-pos) in + List.rev (hyp::tl),concl + with Not_found -> (List.rev tl),hd in + check_names [] hyp_names conclusion_name term +;; + +