- 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 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