+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(*****************************************************************************)
-(* *)
-(* 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 *)
-(* *)
-(*****************************************************************************)
-
-(* $Id$ *)
-
-exception CicPpInternalError;;
-exception NotEnoughElements;;
-
-(* Utility functions *)
-
-let ppname =
- function
- Cic.Name s -> s
- | Cic.Anonymous -> "_"
-;;
-
-(* get_nth l n returns the nth element of the list l if it exists or *)
-(* raises NotEnoughElements if l has less than n elements *)
-let rec get_nth l n =
- match (n,l) with
- (1, he::_) -> he
- | (n, he::tail) when n > 1 -> get_nth tail (n-1)
- | (_,_) -> raise NotEnoughElements
-;;
-
-(* pp t l *)
-(* pretty-prints a term t of cic in an environment l where l is a list of *)
-(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
-(* name associated to the greatest DeBrujin index in t *)
-let rec pp t l =
- let module C = Cic in
- match t with
- C.Rel n ->
- begin
- try
- (match get_nth l n with
- Some (C.Name s) -> s
- | Some C.Anonymous -> "__" ^ string_of_int n
- | None -> "_hidden_" ^ string_of_int n
- )
- with
- NotEnoughElements -> string_of_int (List.length l - n)
- end
- | C.Var (uri,exp_named_subst) ->
- UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
- | C.Meta (n,l1) ->
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
- "]"
- | C.Sort s ->
- (match s with
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | 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 ^ ":" ^ pp t l ^ ")"
- | C.Lambda (b,s,t) ->
- "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
- | C.LetIn (b,s,t) ->
- "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
- | C.Appl li ->
- "(" ^
- (List.fold_right
- (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
- li ""
- ) ^ ")"
- | C.Const (uri,exp_named_subst) ->
- UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
- | C.MutInd (uri,n,exp_named_subst) ->
- (try
- 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
- with
- _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
- )
- | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
- (try
- 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
- | _ -> raise CicPpInternalError
- with
- _ ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
- string_of_int n2
- )
- | C.MutCase (uri,n1,ty,te,patterns) ->
- let connames =
- (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 ^ " => " ^
- (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
- let names =
- List.rev (List.map (function name -> Some (C.Name name)) snames)
- in
- "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
- List.fold_right
- (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
- " : " ^ pp ty l ^ " := \n" ^
- pp bo (names@l) ^ i)
- funs "" ^
- "}\n"
- | C.CoFix (no,funs) ->
- let snames = List.map (fun (name,_,_) -> name) funs in
- let names =
- List.rev (List.map (function name -> Some (C.Name name)) snames)
- in
- "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
- List.fold_right
- (fun (name,ty,bo) i -> "\n" ^ name ^
- " : " ^ pp ty l ^ " := \n" ^
- pp bo (names@l) ^ i)
- funs "" ^
- "}\n"
-and pp_exp_named_subst exp_named_subst l =
- if exp_named_subst = [] then "" else
- "\\subst[" ^
- String.concat " ; " (
- List.map
- (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
- exp_named_subst
- ) ^ "]"
-;;
-
-let ppterm t =
- pp t []
-;;
-
-(* ppinductiveType (typename, inductive, arity, cons) *)
-(* pretty-prints a single inductive definition *)
-(* (typename, inductive, arity, cons) *)
-let ppinductiveType (typename, inductive, arity, cons) =
- (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
- pp arity [] ^ " =\n " ^
- List.fold_right
- (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^
- (if i = "" then "\n" else "\n | ") ^ i)
- cons ""
-;;
-
-let ppcontext ?(sep = "\n") context =
- let separate s = if s = "" then "" else s ^ sep in
- fst (List.fold_right
- (fun context_entry (i,name_context) ->
- match context_entry with
- Some (n,Cic.Decl t) ->
- Printf.sprintf "%s%s : %s" (separate i) (ppname n)
- (pp t name_context), (Some n)::name_context
- | Some (n,Cic.Def (bo,ty)) ->
- Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
- (match ty with
- None -> "_"
- | Some ty -> pp ty name_context)
- (pp bo name_context), (Some n)::name_context
- | None ->
- Printf.sprintf "%s_ :? _" (separate i), None::name_context
- ) context ("",[]))
-
-(* ppobj obj returns a string with describing the cic object obj in a syntax *)
-(* similar to the one used by Coq *)
-let ppobj obj =
- let module C = Cic in
- let module U = UriManager in
- match obj with
- 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, _) ->
- "Axiom " ^ name ^
- "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
- "):\n" ^ pp ty []
- | 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, _) ->
- "Current Proof of " ^ name ^
- "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
- ")" ^ ":\n" ^
- let separate s = if s = "" then "" else s ^ " ; " in
- List.fold_right
- (fun (n, context, t) i ->
- let conjectures',name_context =
- List.fold_right
- (fun context_entry (i,name_context) ->
- (match context_entry with
- Some (n,C.Decl at) ->
- (separate i) ^
- ppname n ^ ":" ^ pp at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,None)) ->
- (separate i) ^
- ppname n ^ ":= " ^ pp at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context
- | _ -> assert false)
- ) context ("",[])
- in
- conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
- pp t name_context ^ "\n" ^ i
- ) conjectures "" ^
- "\n" ^ pp value [] ^ " : " ^ pp ty []
- | 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
-;;
-
-