From 961cb1ed5a03de9083a82d613cd0176234d9bcc6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 7 Jul 2005 13:31:51 +0000 Subject: [PATCH] Check function for Matita name convention. --- helm/ocaml/cic_proof_checking/cicPp.ml | 109 ++++++++++++++++++++++++ helm/ocaml/cic_proof_checking/cicPp.mli | 1 + 2 files changed, 110 insertions(+) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index d11dc5766..7a1de4a7f 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -274,3 +274,112 @@ let ppsort = function | Cic.Type _ -> "Type" | Cic.CProp -> "CProp" + +(* 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 + 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 = 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 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) + | _ -> + hyp_names=[] && (check_name 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 + check_names [] hyp_names conclusion_name term +;; + + diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli index 22c414031..e84ae4fed 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.mli +++ b/helm/ocaml/cic_proof_checking/cicPp.mli @@ -52,3 +52,4 @@ val ppname : Cic.name -> string val ppsort: Cic.sort -> string +val check: string -> Cic.term -> bool -- 2.39.2