X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.ml;h=9242d1fedab60a2fc4630f835a6c2685234754dd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b9a5b72f478dfbad467211e3935163647711c540;hpb=cf5d6fab96c47ccb7d623d72742717d9b08bae7b;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index b9a5b72f4..9242d1fed 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -23,18 +23,18 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 24/01/2000 *) -(* *) -(* 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 *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* 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 *) +(* *) +(*****************************************************************************) exception CicPpInternalError;; exception NotEnoughElements;; @@ -85,16 +85,18 @@ let rec pp t l = (match s with C.Prop -> "Prop" | C.Set -> "Set" - | C.Type _ -> "Type" (* TASSI: universe is not explicit *) + | 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 -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l) | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")" ) - | C.Cast (v,t) -> pp v l + | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")" | C.Lambda (b,s,t) -> "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l) | C.LetIn (b,s,t) -> @@ -109,8 +111,8 @@ let rec pp t l = UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l | C.MutInd (uri,n,exp_named_subst) -> (try - match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> + 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 @@ -119,8 +121,8 @@ let rec pp t l = ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try - match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> + 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 @@ -132,16 +134,28 @@ let rec pp t l = ) | C.MutCase (uri,n1,ty,te,patterns) -> let connames = - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> + (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in List.map (fun (id,_) -> id) cons | _ -> raise CicPpInternalError ) in + let connames_and_patterns = + let rec combine = + function + [],[] -> [] + | [],l -> List.map (fun x -> "???",Some x) l + | l,[] -> List.map (fun x -> x,None) l + | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly)) + in + combine (connames,patterns) + in "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^ - List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i) - (List.combine connames patterns) "" ^ + List.fold_right + (fun (x,y) i -> "\n " ^ x ^ " => " ^ + (match y with None -> "" | Some y -> pp y l) ^ i) + connames_and_patterns "" ^ "\nend" | C.Fix (no, funs) -> let snames = List.map (fun (name,_,_,_) -> name) funs in @@ -217,21 +231,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 +273,206 @@ 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" + + +(* 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 prefix="append" then + begin + prerr_endline last; + prerr_endline string; + end; + 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 strig_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 strig_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 strig_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 = +(* prerr_endline name; + prerr_endline (ppterm 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 +;; + +