]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicPp.ml
- renamed ocaml/ to components/
[helm.git] / helm / ocaml / cic_proof_checking / cicPp.ml
diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
deleted file mode 100644 (file)
index 9541345..0000000
+++ /dev/null
@@ -1,480 +0,0 @@
-(* 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
-;;
-
-