+
+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 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 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 =
+ 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
+;;
+
+