From c0ea287ec40615f72fec8a900ce2e9eb3d23c301 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 15 Jul 2005 11:11:42 +0000 Subject: [PATCH] New version of name checking. --- helm/ocaml/cic_proof_checking/cicPp.ml | 266 ++++++++++++++++--------- 1 file changed, 168 insertions(+), 98 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index effc8a4b5..776532852 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;; @@ -277,91 +277,129 @@ let ppsort = function (* MATITA NAMING CONVENTION *) -let check_name ctx name term = - let cut_off_name name string_name = - let len = String.length name in - let len1 = String.length string_name in - if len <= len1 then - begin - let head = String.sub string_name 0 len in - if ((String.compare head name)=0) || - ((String.compare head (String.lowercase name))=0) then - begin - let diff = len1-len in - let tail = String.sub string_name len diff in - if ((diff > 0) && (String.rcontains_from tail 0 '_')) then - String.sub tail 1 (diff-1) - else tail +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 head prefix)=0) || + ((String.compare 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 string_name - end - else string_name in - let rec check_aux ctx string_name = - function - | Cic.Rel m -> - (match List.nth ctx (m-1) with - Cic.Name name -> - cut_off_name name string_name - | Cic.Anonymous -> string_name) - | Cic.Meta _ -> string_name - | Cic.Sort sort -> cut_off_name (ppsort sort) string_name - | Cic.Implicit _ -> string_name - | Cic.Cast (te,ty) -> check_aux ctx string_name te - | Cic.Prod (name,so,dest) -> - let string_name = check_aux ctx string_name so in - check_aux (name::ctx) string_name dest - | Cic.Lambda (name,so,dest) -> - let string_name = - match name with - Cic.Anonymous -> string_name - | Cic.Name name -> cut_off_name name string_name in - let string_name = check_aux ctx string_name so in - check_aux (name::ctx) string_name dest - | Cic.LetIn (name,so,dest) -> - let string_name = check_aux ctx string_name so in - check_aux (name::ctx) string_name dest - | Cic.Appl l -> - List.fold_left (check_aux ctx) string_name l - | Cic.Var (uri,exp_named_subst) -> - let name = UriManager.name_of_uri uri in - cut_off_name name string_name - | Cic.Const (uri,exp_named_subst) -> - let name = UriManager.name_of_uri uri in - cut_off_name name string_name - | Cic.MutInd (uri,_,exp_named_subst) -> - let name = UriManager.name_of_uri uri in - cut_off_name 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 - cut_off_name name string_name - | Cic.MutCase (_,_,_,te,pl) -> - let strig_name = cut_off_name "match" string_name in - let string_name = check_aux ctx string_name te in - List.fold_right (fun t s -> check_aux ctx s t) pl string_name - | Cic.Fix (_,fl) -> - let strig_name = cut_off_name "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_aux (onames@ctx) s bo) fl string_name - | Cic.CoFix (_,fl) -> - let strig_name = cut_off_name "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_aux (onames@ctx) s bo) fl string_name - in - if (String.length (check_aux ctx name term) = 0) then true + 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 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 = @@ -374,15 +412,47 @@ let rec check_names ctx hyp_names conclusion_name t = 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 ctx conclusion_name t) + 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 -> (List.rev tl),hd in + | 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 ;; -- 2.39.2