cicUniv.cmi:
-cicUtil.cmi: cic.cmo
cicPp.cmi: cic.cmo
cic.cmo: cicUniv.cmi
cic.cmx: cicUniv.cmx
cicUniv.cmo: cicUniv.cmi
cicUniv.cmx: cicUniv.cmi
-cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi
-cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi
cicPp.cmo: cic.cmo cicPp.cmi
cicPp.cmx: cic.cmx cicPp.cmi
cicUniv.cmi:
-cicUtil.cmi: cic.cmx
cicPp.cmi: cic.cmx
cic.cmo: cicUniv.cmi
cic.cmx: cicUniv.cmx
cicUniv.cmo: cicUniv.cmi
cicUniv.cmx: cicUniv.cmi
-cicUtil.cmo: cicUniv.cmi cic.cmx cicUtil.cmi
-cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi
cicPp.cmo: cic.cmx cicPp.cmi
cicPp.cmx: cic.cmx cicPp.cmi
PACKAGE = cic
PREDICATES =
-INTERFACE_FILES = \
- cicUniv.mli \
- cicUtil.mli \
- cicPp.mli
+INTERFACE_FILES =
IMPLEMENTATION_FILES = \
cic.ml $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
type sort =
Prop
| Set
- | Type of CicUniv.universe
- | CProp of CicUniv.universe
type name =
| Name of string
and anncontext = annhypothesis list
;;
-type lazy_term =
- context -> metasenv -> CicUniv.universe_graph ->
- term * metasenv * CicUniv.universe_graph
-
type anntarget =
Object of annobj (* if annobj is a Constant, this is its type *)
| ConstantBody of annobj
+++ /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 pp ?metasenv =
-let rec pp t l =
- assert false (* MATITA 1.0
- 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) ->
- (match metasenv with
- None ->
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
- "]"
- | Some metasenv ->
- try
- let _,context,_ = CicUtil.lookup_meta n metasenv in
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev
- (List.map2
- (fun x y ->
- match x,y with
- _, None
- | None, _ -> "_"
- | Some _, Some t -> pp t l
- ) context l1)) ^
- "]"
- with
- CicUtil.Meta_not_found _
- | Invalid_argument _ ->
- "???" ^ (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 -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
- | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ 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,ty,t) ->
- " let " ^ ppname b ^ ": " ^ pp ty l ^ " \\def " ^ pp s l ^ " in " ^ 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
- Sys.Break as exn -> raise exn
- | _ -> 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
- Sys.Break as exn -> raise exn
- | _ ->
- UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
- string_of_int n2
- )
- | C.MutCase (uri,n1,ty,te,patterns) ->
- let connames_and_argsno =
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- C.InductiveDefinition (dl,_,paramsno,_) ->
- let (_,_,_,cons) = get_nth dl (n1+1) in
- List.map
- (fun (id,ty) ->
- (* this is just an approximation since we do not have
- reduction yet! *)
- let rec count_prods toskip =
- function
- C.Prod (_,_,bo) when toskip > 0 ->
- count_prods (toskip - 1) bo
- | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
- | _ -> 0
- in
- id, count_prods paramsno ty
- ) cons
- | _ -> raise CicPpInternalError
- )
- in
- let connames_and_argsno_and_patterns =
- let rec combine =
- function
- [],[] -> []
- | [],l -> List.map (fun x -> "???",0,Some x) l
- | l,[] -> List.map (fun (x,no) -> x,no,None) l
- | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
- in
- combine (connames_and_argsno,patterns)
- in
- "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
- (String.concat "\n | "
- (List.map
- (fun (x,argsno,y) ->
- let rec aux argsno l =
- function
- Cic.Lambda (name,ty,bo) when argsno > 0 ->
- let args,res = aux (argsno - 1) (Some name::l) bo in
- ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
- ":" ^ pp ty l ^ ")")::args, res
- | t when argsno = 0 -> [],pp t l
- | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
- in
- let pattern,body =
- match y with
- None -> x,""
- | Some y when argsno = 0 -> x,pp y l
- | Some y ->
- let args,body = aux argsno l y in
- "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
- in
- pattern ^ " => " ^ body
- ) connames_and_argsno_and_patterns)) ^
- "\n]"
- | 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
- ) ^ "]"
- *)
-in
- pp
-;;
-
-let ppterm ?metasenv t =
- pp ?metasenv 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 ?metasenv ?(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 ?metasenv t name_context), (Some n)::name_context
- | Some (n,Cic.Def (bo,ty)) ->
- Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
- (pp ?metasenv ty name_context)
- (pp ?metasenv 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 ~metasenv:conjectures at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def (at,aty)) ->
- (separate i) ^
- ppname n ^ ": " ^
- pp ~metasenv:conjectures aty name_context ^
- ":= " ^ pp ~metasenv:conjectures
- at name_context ^ " ",
- (Some n)::name_context
- | None ->
- (separate i) ^ "_ :? _ ", None::name_context)
- ) context ("",[])
- in
- conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
- pp ~metasenv:conjectures t name_context ^ "\n" ^ i
- ) conjectures "" ^
- "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
- pp ~metasenv:conjectures 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 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 =
- assert false (*
- 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) l_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 string_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 string_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 string_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
-;;
-
-
+++ /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 *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 24/01/2000 *)
-(* *)
-(* 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 *)
-(* *)
-(*****************************************************************************)
-
-(* ppobj obj returns a string with describing the cic object obj in a syntax*)
-(* similar to the one used by Coq *)
-val ppobj : Cic.obj -> string
-
-val ppterm : ?metasenv:Cic.metasenv -> Cic.term -> string
-
-val ppcontext : ?metasenv:Cic.metasenv -> ?sep:string -> Cic.context -> string
-
-(* Required only by the topLevel. It is the generalization of ppterm to *)
-(* work with environments. *)
-val pp : ?metasenv:Cic.metasenv -> Cic.term -> (Cic.name option) list -> string
-
-val ppname : Cic.name -> string
-
-val ppsort: Cic.sort -> string
-
-val check: string -> Cic.term -> bool
+++ /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 *)
-(* *)
-(* Enrico Tassi <tassi@cs.unibo.it> *)
-(* 23/04/2004 *)
-(* *)
-(* This module implements the aciclic graph of universes. *)
-(* *)
-(*****************************************************************************)
-
-(* $Id$ *)
-
-(*****************************************************************************)
-(** open **)
-(*****************************************************************************)
-
-open Printf
-
-(*****************************************************************************)
-(** Types and default values **)
-(*****************************************************************************)
-
-
-type universe = int * UriManager.uri option
-
-let eq u1 u2 =
- match u1,u2 with
- | (id1, Some uri1),(id2, Some uri2) ->
- id1 = id2 && UriManager.eq uri1 uri2
- | (id1, None),(id2, None) -> id1 = id2
- | _ -> false
-
-let compare (id1, uri1) (id2, uri2) =
- let cmp = id1 - id2 in
- if cmp = 0 then
- match uri1,uri2 with
- | None, None -> 0
- | Some _, None -> 1
- | None, Some _ -> ~-1
- | Some uri1, Some uri2 -> UriManager.compare uri1 uri2
- else
- cmp
-
-module UniverseType = struct
- type t = universe
- let compare = compare
-end
-
-module SOF = Set.Make(UniverseType)
-
-type entry = {
- eq_closure : SOF.t;
- ge_closure : SOF.t;
- gt_closure : SOF.t;
- in_gegt_of : SOF.t;
- one_s_eq : SOF.t;
- one_s_ge : SOF.t;
- one_s_gt : SOF.t;
-}
-
-module MAL = Map.Make(UniverseType)
-
-type arc_type = GE | GT | EQ
-
-type bag = entry MAL.t
-
-let empty_entry = {
- eq_closure=SOF.empty;
- ge_closure=SOF.empty;
- gt_closure=SOF.empty;
- in_gegt_of=SOF.empty;
- one_s_eq=SOF.empty;
- one_s_ge=SOF.empty;
- one_s_gt=SOF.empty;
-}
-let empty_bag = MAL.empty
-
-let are_set_eq s1 s2 =
- SOF.equal s1 s2
-
-let are_entry_eq v1 v2 =
- (are_set_eq v1.gt_closure v2.gt_closure ) &&
- (are_set_eq v1.ge_closure v2.ge_closure ) &&
- (are_set_eq v1.eq_closure v2.eq_closure ) &&
- (*(are_set_eq v1.in_gegt_of v2.in_gegt_of ) &&*)
- (are_set_eq v1.one_s_ge v2.one_s_ge ) &&
- (are_set_eq v1.one_s_gt v2.one_s_gt ) &&
- (are_set_eq v1.one_s_eq v2.one_s_eq )
-
-let are_ugraph_eq = MAL.equal are_entry_eq
-
-(*****************************************************************************)
-(** Pretty printings **)
-(*****************************************************************************)
-
-let string_of_universe (i,u) =
- match u with
- Some u ->
- "(" ^ ((string_of_int i) ^ "," ^ (UriManager.string_of_uri u) ^ ")")
- | None -> "(" ^ (string_of_int i) ^ ",None)"
-
-let string_of_universe_set l =
- SOF.fold (fun x s -> s ^ (string_of_universe x) ^ " ") l ""
-
-let string_of_node n =
- "{"^
- "eq_c: " ^ (string_of_universe_set n.eq_closure) ^ "; " ^
- "ge_c: " ^ (string_of_universe_set n.ge_closure) ^ "; " ^
- "gt_c: " ^ (string_of_universe_set n.gt_closure) ^ "; " ^
- "i_gegt: " ^ (string_of_universe_set n.in_gegt_of) ^ "}\n"
-
-let string_of_arc (a,u,v) =
- (string_of_universe u) ^ " " ^ a ^ " " ^ (string_of_universe v)
-
-let string_of_mal m =
- let rc = ref "" in
- MAL.iter (fun k v ->
- rc := !rc ^ sprintf "%s --> %s" (string_of_universe k)
- (string_of_node v)) m;
- !rc
-
-let string_of_bag b =
- string_of_mal b
-
-(*****************************************************************************)
-(** Helpers **)
-(*****************************************************************************)
-
-(* find the repr *)
-let repr u m =
- try
- MAL.find u m
- with
- Not_found -> empty_entry
-
-(* FIXME: May be faster if we make it by hand *)
-let merge_closures f nodes m =
- SOF.fold (fun x i -> SOF.union (f (repr x m)) i ) nodes SOF.empty
-
-\f
-(*****************************************************************************)
-(** _fats implementation **)
-(*****************************************************************************)
-
-let rec closure_of_fast ru m =
- let eq_c = closure_eq_fast ru m in
- let ge_c = closure_ge_fast ru m in
- let gt_c = closure_gt_fast ru m in
- {
- eq_closure = eq_c;
- ge_closure = ge_c;
- gt_closure = gt_c;
- in_gegt_of = ru.in_gegt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = ru.one_s_gt
- }
-
-and closure_eq_fast ru m =
- let eq_c =
- let j = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.eq_closure) j m in
- let one_step_eq = ru.one_s_eq in
- (SOF.union one_step_eq _Uj)
- in
- eq_c
-
-and closure_ge_fast ru m =
- let ge_c =
- let j = SOF.union ru.one_s_ge (SOF.union ru.one_s_gt ru.one_s_eq) in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Ux = j in
- (SOF.union _Uj _Ux)
- in
- ge_c
-
-and closure_gt_fast ru m =
- let gt_c =
- let j = ru.one_s_gt in
- let k = ru.one_s_ge in
- let l = ru.one_s_eq in
- let _Uj = merge_closures (fun x -> x.ge_closure) j m in
- let _Uk = merge_closures (fun x -> x.gt_closure) k m in
- let _Ul = merge_closures (fun x -> x.gt_closure) l m in
- let one_step_gt = ru.one_s_gt in
- (SOF.union (SOF.union (SOF.union _Ul one_step_gt) _Uk) _Uj)
- in
- gt_c
-
-and print_rec_status u ru =
- print_endline ("Aggiusto " ^ (string_of_universe u) ^
- "e ottengo questa chiusura\n " ^ (string_of_node ru))
-
-and adjust_fast_aux adjusted u m =
- if SOF.mem u adjusted then m, adjusted else
- let adjusted = SOF.add u adjusted in
- let ru = repr u m in
- let gt_c = closure_gt_fast ru m in
- let ge_c = closure_ge_fast ru m in
- let eq_c = closure_eq_fast ru m in
- let changed_eq = not (are_set_eq eq_c ru.eq_closure) in
- let changed_gegt =
- (not (are_set_eq gt_c ru.gt_closure)) ||
- (not (are_set_eq ge_c ru.ge_closure))
- in
- if ((not changed_gegt) && (not changed_eq)) then
- m, adjusted
- else
- begin
- let ru' = {
- eq_closure = eq_c;
- ge_closure = ge_c;
- gt_closure = gt_c;
- in_gegt_of = ru.in_gegt_of;
- one_s_eq = ru.one_s_eq;
- one_s_ge = ru.one_s_ge;
- one_s_gt = ru.one_s_gt}
- in
- let m = MAL.add u ru' m in
- let m, adjusted =
- SOF.fold (fun x (m,adjusted) -> MAL.add x ru' m, SOF.add x adjusted)
- (SOF.diff ru'.eq_closure adjusted)
- (m,adjusted)
- in
- let m, adjusted =
- SOF.fold (fun x (m,adjusted) -> adjust_fast_aux adjusted x m)
- (SOF.diff ru'.in_gegt_of adjusted)
- (m,adjusted)
- in
- m, adjusted
- end
-
-(*
-and profiler_adj = HExtlib.profile "CicUniv.adjust_fast"
-and adjust_fast x y = profiler_adj.HExtlib.profile (adjust_fast_aux x) y
-*)
-and adjust_fast x y =
- fst(adjust_fast_aux SOF.empty x y)
-
-and add_gt_arc_fast u v m =
- let ru = repr u m in
- if SOF.mem v ru.gt_closure then m else
- let ru' = {ru with one_s_gt = SOF.add v ru.one_s_gt} in
- let m' = MAL.add u ru' m in
- let rv = repr v m' in
- let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
- let m'' = MAL.add v rv' m' in
- adjust_fast u m''
-
-and add_ge_arc_fast u v m =
- let ru = repr u m in
- if SOF.mem v ru.ge_closure then m else
- let ru' = { ru with one_s_ge = SOF.add v ru.one_s_ge} in
- let m' = MAL.add u ru' m in
- let rv = repr v m' in
- let rv' = {rv with in_gegt_of = SOF.add u rv.in_gegt_of} in
- let m'' = MAL.add v rv' m' in
- adjust_fast u m''
-
-and add_eq_arc_fast u v m =
- let ru = repr u m in
- if SOF.mem v ru.eq_closure then m else
- let rv = repr v m in
- let ru' = {ru with one_s_eq = SOF.add v ru.one_s_eq} in
- (*TESI: let ru' = {ru' with in_gegt_of = SOF.add v ru.in_gegt_of} in *)
- let m' = MAL.add u ru' m in
- let rv' = {rv with one_s_eq = SOF.add u rv.one_s_eq} in
- (*TESI: let rv' = {rv' with in_gegt_of = SOF.add u rv.in_gegt_of} in *)
- let m'' = MAL.add v rv' m' in
- adjust_fast v (*(adjust_fast u*) m'' (* ) *)
-;;
-
-\f
-
-(*****************************************************************************)
-(** Other real code **)
-(*****************************************************************************)
-
-exception UniverseInconsistency of string Lazy.t
-
-let error arc node1 closure_type node2 closure =
- let s =
- lazy
- ("\n ===== Universe Inconsistency detected =====\n\n" ^
- " Unable to add\n" ^
- "\t" ^ (string_of_arc arc) ^ "\n" ^
- " cause\n" ^
- "\t" ^ (string_of_universe node1) ^ "\n" ^
- " is in the " ^ closure_type ^ " closure\n" ^
- "\t{" ^ (string_of_universe_set closure) ^ "}\n" ^
- " of\n" ^
- "\t" ^ (string_of_universe node2) ^ "\n\n" ^
- " ===== Universe Inconsistency detected =====\n") in
-(* prerr_endline (Lazy.force s); *)
- raise (UniverseInconsistency s)
-
-
-let fill_empty_nodes_with_uri (g, already_contained,o) l uri =
- let fill_empty_universe u =
- match u with
- (i,None) -> (i,Some uri)
- | (i,Some _) as u -> u
- in
- let fill_empty_set s =
- SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
- in
- let fill_empty_entry e = {
- eq_closure = (fill_empty_set e.eq_closure) ;
- ge_closure = (fill_empty_set e.ge_closure) ;
- gt_closure = (fill_empty_set e.gt_closure) ;
- in_gegt_of = (fill_empty_set e.in_gegt_of) ;
- one_s_eq = (fill_empty_set e.one_s_eq) ;
- one_s_ge = (fill_empty_set e.one_s_ge) ;
- one_s_gt = (fill_empty_set e.one_s_gt) ;
- } in
- let m = g in
- let m' = MAL.fold (
- fun k v m ->
- MAL.add (fill_empty_universe k) (fill_empty_entry v) m) m MAL.empty
- in
- let l' = List.map fill_empty_universe l in
- (m', already_contained,o),l'
-
-
-(*****************************************************************************)
-(** World interface **)
-(*****************************************************************************)
-
-type universe_graph = bag * UriManager.UriSet.t * bool
-(* the graph , the cache of already merged ugraphs, oblivion? *)
-
-let empty_ugraph = empty_bag, UriManager.UriSet.empty, false
-let oblivion_ugraph = empty_bag, UriManager.UriSet.empty, true
-(* FG: default choice for a ugraph ??? *)
-let default_ugraph = oblivion_ugraph
-
-let current_index_anon = ref (-1)
-let current_index_named = ref (-1)
-
-let restart_numbering () = current_index_named := (-1)
-
-let fresh ?uri ?id () =
- let i =
- match uri,id with
- | None,None ->
- current_index_anon := !current_index_anon + 1;
- !current_index_anon
- | None, Some _ -> assert false
- | Some _, None ->
- current_index_named := !current_index_named + 1;
- !current_index_named
- | Some _, Some id -> id
- in
- (i,uri)
-
-let name_universe u uri =
- match u with
- | (i, None) -> (i, Some uri)
- | u -> u
-;;
-
-let print_ugraph (g, _, o) =
- if o then prerr_endline "oblivion universe" else
- prerr_endline (string_of_bag g)
-
-let add_eq u v b =
- (* should we check to no add twice the same?? *)
- let m = b in
- let ru = repr u m in
- if SOF.mem v ru.gt_closure then
- error ("EQ",u,v) v "GT" u ru.gt_closure
- else
- begin
- let rv = repr v m in
- if SOF.mem u rv.gt_closure then
- error ("EQ",u,v) u "GT" v rv.gt_closure
- else
- add_eq_arc_fast u v b
- end
-
-let add_ge u v b =
- (* should we check to no add twice the same?? *)
- let m = b in
- let rv = repr v m in
- if SOF.mem u rv.gt_closure then
- error ("GE",u,v) u "GT" v rv.gt_closure
- else
- add_ge_arc_fast u v b
-
-let add_gt u v b =
- (* should we check to no add twice the same?? *)
- (*
- FIXME : check the thesis... no need to check GT and EQ closure since the
- GE is a superset of both
- *)
- let m = b in
- let rv = repr v m in
-
- if u = v then
- error ("GT",u,v) u "==" v SOF.empty
- else
-
- (*if SOF.mem u rv.gt_closure then
- error ("GT",u,v) u "GT" v rv.gt_closure
- else
- begin*)
- if SOF.mem u rv.ge_closure then
- error ("GT",u,v) u "GE" v rv.ge_closure
- else
-(* begin
- if SOF.mem u rv.eq_closure then
- error ("GT",u,v) u "EQ" v rv.eq_closure
- else*)
- add_gt_arc_fast u v b
-(* end
- end*)
-
-(*****************************************************************************)
-(** START: Decomment this for performance comparisons **)
-(*****************************************************************************)
-
-let add_eq u v (b,already_contained,oblivion) =
- if oblivion then (b,already_contained,oblivion) else
- let rc = add_eq u v b in
- rc,already_contained,false
-
-let add_ge u v (b,already_contained,oblivion) =
- if oblivion then (b,already_contained,oblivion) else
- let rc = add_ge u v b in
- rc,already_contained,false
-
-let add_gt u v (b,already_contained,oblivion) =
- if oblivion then (b,already_contained,oblivion) else
- let rc = add_gt u v b in
- rc,already_contained,false
-
-(* profiling code *)
-let profiler_eq = HExtlib.profile "CicUniv.add_eq"
-let profiler_ge = HExtlib.profile "CicUniv.add_ge"
-let profiler_gt = HExtlib.profile "CicUniv.add_gt"
-let add_gt u v b =
- profiler_gt.HExtlib.profile (fun _ -> add_gt u v b) ()
-let add_ge u v b =
- profiler_ge.HExtlib.profile (fun _ -> add_ge u v b) ()
-let add_eq u v b =
- profiler_eq.HExtlib.profile (fun _ -> add_eq u v b) ()
-
-
-(* ugly *)
-let rank = ref MAL.empty;;
-
-let do_rank (b,_,_) =
- let keys =
- MAL.fold
- (fun k v acc ->
- SOF.union acc (SOF.union (SOF.singleton k)
- (SOF.union v.eq_closure (SOF.union v.gt_closure v.ge_closure))))
- b SOF.empty
- in
- let keys = SOF.elements keys in
- let rec aux cache l =
- match l with
- | [] -> -1,cache
- | x::tl when List.mem_assoc x cache ->
- let height = List.assoc x cache in
- let rest, cache = aux cache tl in
- max rest height, cache
- | x::tl ->
- let sons = SOF.elements (repr x b).gt_closure in
- let height,cache = aux cache sons in
- let height = height + 1 in
- let cache = (x,height) :: cache in
- let rest, cache = aux cache tl in
- max height rest, cache
- in
- let _, cache = aux [] keys in
- rank := List.fold_left (fun m (k,v) -> MAL.add k v m) MAL.empty cache;
- let res = ref [] in
- let resk = ref [] in
- MAL.iter
- (fun k v ->
- if not (List.mem v !res) then res := v::!res;
- resk := k :: !resk) !rank;
- !res, !resk
-;;
-
-let get_rank u =
- try MAL.find u !rank
- with Not_found -> 0
- (* if the universe is not in the graph it means there are
- * no contraints on it! thus it can be freely set to Type0 *)
-;;
-
-(*****************************************************************************)
-(** END: Decomment this for performance comparisons **)
-(*****************************************************************************)
-
-(* TODO: uncomment l to gain a small speedup *)
-let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment(*,l*)) =
- let merge_brutal (u,a,_) v =
-(* prerr_endline ("merging graph: "^UriManager.string_of_uri
- * uri_of_increment); *)
- let m1 = u in
- let m2 = v in
- MAL.fold (
- fun k v x ->
- (SOF.fold (
- fun u x ->
- let m = add_gt k u x in m)
- (SOF.union v.one_s_gt v.gt_closure)
- (SOF.fold (
- fun u x ->
- let m = add_ge k u x in m)
- (SOF.union v.one_s_ge v.ge_closure)
- (SOF.fold (
- fun u x ->
- let m = add_eq k u x in m)
- (SOF.union v.one_s_eq v.eq_closure) x)))
- ) m1 m2
- in
- let base, already_contained, oblivion = base_ugraph in
- let inc,_,oblivion2 = increment in
- if oblivion then
- base_ugraph
- else if oblivion2 then
- increment
- else if MAL.is_empty base then
- increment
- else if
- MAL.is_empty inc ||
- UriManager.UriSet.mem uri_of_increment already_contained
- then
- base_ugraph
- else
- (fun (x,_,_) -> x) (merge_brutal increment base_ugraph),
-(*
- List.fold_right UriManager.UriSet.add
- (List.map (fun (_,x) -> HExtlib.unopt x) l)
-*)
- (UriManager.UriSet.add uri_of_increment already_contained), false
-
-(* profiling code; WARNING: the time spent during profiling can be
- greater than the profiled time
-let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs"
-let merge_ugraphs ~base_ugraph ~increment =
- profiler_merge.HExtlib.profile
- (fun _ -> merge_ugraphs ~base_ugraph ~increment) ()
-*)
-
-(*****************************************************************************)
-(** Xml sesialization and parsing **)
-(*****************************************************************************)
-
-let xml_of_universe name u =
- match u with
- | (i,Some u) ->
- Xml.xml_empty name [
- None,"id",(string_of_int i) ;
- None,"uri",(UriManager.string_of_uri u)]
- | (_,None) ->
- raise (Failure "we can serialize only universes with uri")
-
-let xml_of_set s =
- let l =
- List.map (xml_of_universe "node") (SOF.elements s)
- in
- List.fold_left (fun s x -> [< s ; x >] ) [<>] l
-
-let xml_of_entry_content e =
- let stream_of_field f name =
- let eq_c = xml_of_set f in
- if eq_c != [<>] then
- Xml.xml_nempty name [] eq_c
- else
- [<>]
- in
- [<
- (stream_of_field e.eq_closure "eq_closure");
- (stream_of_field e.gt_closure "gt_closure");
- (stream_of_field e.ge_closure "ge_closure");
- (stream_of_field e.in_gegt_of "in_gegt_of");
- (stream_of_field e.one_s_eq "one_s_eq");
- (stream_of_field e.one_s_gt "one_s_gt");
- (stream_of_field e.one_s_ge "one_s_ge")
- >]
-
-let xml_of_entry u e =
- let (i,u') = u in
- let u'' =
- match u' with
- Some x -> x
- | None ->
- raise (Failure "we can serialize only universes (entry) with uri")
- in
- let ent = Xml.xml_nempty "entry" [
- None,"id",(string_of_int i) ;
- None,"uri",(UriManager.string_of_uri u'')] in
- let content = xml_of_entry_content e in
- ent content
-
-let write_xml_of_ugraph filename (m,_,_) l =
- let tokens =
- [<
- Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
- Xml.xml_nempty "ugraph" []
- ([< (MAL.fold ( fun k v s -> [< s ; (xml_of_entry k v) >]) m [<>]) ;
- (List.fold_left
- (fun s u -> [< s ; xml_of_universe "owned_node" u >]) [<>] l) >])>]
- in
- Xml.pp ~gzip:true tokens (Some filename)
-
-let univno = fst
-let univuri = function
- | _,None -> UriManager.uri_of_string "cic:/fake.con"
- | _,Some u -> u
-
-
-let rec clean_ugraph m already_contained f =
- let m' =
- MAL.fold (fun k v x -> if (f k) then MAL.add k v x else x ) m MAL.empty in
- let m'' = MAL.fold (fun k v x ->
- let v' = {
- eq_closure = SOF.filter f v.eq_closure;
- ge_closure = SOF.filter f v.ge_closure;
- gt_closure = SOF.filter f v.gt_closure;
- in_gegt_of = SOF.filter f v.in_gegt_of;
- one_s_eq = SOF.filter f v.one_s_eq;
- one_s_ge = SOF.filter f v.one_s_ge;
- one_s_gt = SOF.filter f v.one_s_gt
- } in
- MAL.add k v' x ) m' MAL.empty in
- let e_l =
- MAL.fold (fun k v l -> if v = empty_entry && not(f k) then
- begin
- SOF.add k l end else l) m'' SOF.empty
- in
- if not (SOF.is_empty e_l) then
- clean_ugraph
- m'' already_contained (fun u -> (f u) && not (SOF.mem u e_l))
- else
- MAL.fold
- (fun k v x -> if v <> empty_entry then MAL.add k v x else x)
- m'' MAL.empty,
- already_contained
-
-let clean_ugraph (m,a,o) l =
- assert(not o);
- let l = List.fold_right SOF.add l SOF.empty in
- let m, a = clean_ugraph m a (fun u -> SOF.mem u l) in
- m, a, o
-
-let assigner_of =
- function
- "ge_closure" -> (fun e u->{e with ge_closure=SOF.add u e.ge_closure})
- | "gt_closure" -> (fun e u->{e with gt_closure=SOF.add u e.gt_closure})
- | "eq_closure" -> (fun e u->{e with eq_closure=SOF.add u e.eq_closure})
- | "in_gegt_of" -> (fun e u->{e with in_gegt_of =SOF.add u e.in_gegt_of})
- | "one_s_ge" -> (fun e u->{e with one_s_ge =SOF.add u e.one_s_ge})
- | "one_s_gt" -> (fun e u->{e with one_s_gt =SOF.add u e.one_s_gt})
- | "one_s_eq" -> (fun e u->{e with one_s_eq =SOF.add u e.one_s_eq})
- | s -> raise (Failure ("unsupported tag " ^ s))
-;;
-
-let cb_factory m l =
- let module XPP = XmlPushParser in
- let current_node = ref (0,None) in
- let current_entry = ref empty_entry in
- let current_assign = ref (assigner_of "in_gegt_of") in
- { XPP.default_callbacks with
- XPP.end_element = Some( fun name ->
- match name with
- | "entry" ->
- m := MAL.add !current_node !current_entry !m;
- current_entry := empty_entry
- | _ -> ()
- );
- XPP.start_element = Some( fun name attlist ->
- match name with
- | "ugraph" -> ()
- | "entry" ->
- let id = List.assoc "id" attlist in
- let uri = List.assoc "uri" attlist in
- current_node := (int_of_string id,Some (UriManager.uri_of_string uri))
- | "node" ->
- let id = int_of_string (List.assoc "id" attlist) in
- let uri = List.assoc "uri" attlist in
- current_entry := !current_assign !current_entry
- (id,Some (UriManager.uri_of_string uri))
- | "owned_node" ->
- let id = int_of_string (List.assoc "id" attlist) in
- let uri = List.assoc "uri" attlist in
- l := (id,Some (UriManager.uri_of_string uri)) :: !l
- | s -> current_assign := assigner_of s
- )
- }
-;;
-
-let ugraph_and_univlist_of_xml filename =
- let module XPP = XmlPushParser in
- let result_map = ref MAL.empty in
- let result_list = ref [] in
- let cb = cb_factory result_map result_list in
- let xml_parser = XPP.create_parser cb in
- let xml_source = `Gzip_file filename in
- (try XPP.parse xml_parser xml_source
- with (XPP.Parse_error err) as exn -> raise exn);
- (!result_map,UriManager.UriSet.empty,false), !result_list
-
-\f
-(*****************************************************************************)
-(** the main, only for testing **)
-(*****************************************************************************)
-
-(*
-
-type arc = Ge | Gt | Eq ;;
-
-let randomize_actionlist n m =
- let ge_percent = 0.7 in
- let gt_percent = 0.15 in
- let random_step () =
- let node1 = Random.int m in
- let node2 = Random.int m in
- let op =
- let r = Random.float 1.0 in
- if r < ge_percent then
- Ge
- else (if r < (ge_percent +. gt_percent) then
- Gt
- else
- Eq)
- in
- op,node1,node2
- in
- let rec aux n =
- match n with
- 0 -> []
- | n -> (random_step ())::(aux (n-1))
- in
- aux n
-
-let print_action_list l =
- let string_of_step (op,node1,node2) =
- (match op with
- Ge -> "Ge"
- | Gt -> "Gt"
- | Eq -> "Eq") ^
- "," ^ (string_of_int node1) ^ "," ^ (string_of_int node2)
- in
- let rec aux l =
- match l with
- [] -> "]"
- | a::tl ->
- ";" ^ (string_of_step a) ^ (aux tl)
- in
- let body = aux l in
- let l_body = (String.length body) - 1 in
- prerr_endline ("[" ^ (String.sub body 1 l_body))
-
-let debug = false
-let d_print_endline = if debug then print_endline else ignore
-let d_print_ugraph = if debug then print_ugraph else ignore
-
-let _ =
- (if Array.length Sys.argv < 2 then
- prerr_endline ("Usage " ^ Sys.argv.(0) ^ " max_edges max_nodes"));
- Random.self_init ();
- let max_edges = int_of_string Sys.argv.(1) in
- let max_nodes = int_of_string Sys.argv.(2) in
- let action_listR = randomize_actionlist max_edges max_nodes in
-
- let action_list = [Ge,1,4;Ge,2,6;Ge,1,1;Eq,6,4;Gt,6,3] in
- let action_list = action_listR in
-
- print_action_list action_list;
- let prform_step ?(fast=false) (t,u,v) g =
- let f,str =
- match t with
- Ge -> add_ge,">="
- | Gt -> add_gt,">"
- | Eq -> add_eq,"="
- in
- d_print_endline (
- "Aggiungo " ^
- (string_of_int u) ^
- " " ^ str ^ " " ^
- (string_of_int v));
- let g' = f ~fast (u,None) (v,None) g in
- (*print_ugraph g' ;*)
- g'
- in
- let fail = ref false in
- let time1 = Unix.gettimeofday () in
- let n_safe = ref 0 in
- let g_safe =
- try
- d_print_endline "SAFE";
- List.fold_left (
- fun g e ->
- n_safe := !n_safe + 1;
- prform_step e g
- ) empty_ugraph action_list
- with
- UniverseInconsistency s -> fail:=true;empty_bag
- in
- let time2 = Unix.gettimeofday () in
- d_print_ugraph g_safe;
- let time3 = Unix.gettimeofday () in
- let n_test = ref 0 in
- let g_test =
- try
- d_print_endline "FAST";
- List.fold_left (
- fun g e ->
- n_test := !n_test + 1;
- prform_step ~fast:true e g
- ) empty_ugraph action_list
- with
- UniverseInconsistency s -> empty_bag
- in
- let time4 = Unix.gettimeofday () in
- d_print_ugraph g_test;
- if are_ugraph_eq g_safe g_test && !n_test = !n_safe then
- begin
- let num_eq =
- List.fold_left (
- fun s (e,_,_) ->
- if e = Eq then s+1 else s
- ) 0 action_list
- in
- let num_gt =
- List.fold_left (
- fun s (e,_,_) ->
- if e = Gt then s+1 else s
- ) 0 action_list
- in
- let num_ge = max_edges - num_gt - num_eq in
- let time_fast = (time4 -. time3) in
- let time_safe = (time2 -. time1) in
- let gap = ((time_safe -. time_fast) *. 100.0) /. time_safe in
- let fail = if !fail then 1 else 0 in
- print_endline
- (sprintf
- "OK %d safe %1.4f fast %1.4f %% %1.2f #eq %d #gt %d #ge %d %d"
- fail time_safe time_fast gap num_eq num_gt num_ge !n_safe);
- exit 0
- end
- else
- begin
- print_endline "FAIL";
- print_ugraph g_safe;
- print_ugraph g_test;
- exit 1
- end
-;;
-
- *)
-
-let recons_univ u =
- match u with
- | i, None -> u
- | i, Some uri ->
- i, Some (UriManager.uri_of_string (UriManager.string_of_uri uri))
-
-let recons_entry entry =
- let recons_set set =
- SOF.fold (fun univ set -> SOF.add (recons_univ univ) set) set SOF.empty
- in
- {
- eq_closure = recons_set entry.eq_closure;
- ge_closure = recons_set entry.ge_closure;
- gt_closure = recons_set entry.gt_closure;
- in_gegt_of = recons_set entry.in_gegt_of;
- one_s_eq = recons_set entry.one_s_eq;
- one_s_ge = recons_set entry.one_s_ge;
- one_s_gt = recons_set entry.one_s_gt;
- }
-
-let recons_graph (graph,uriset,o) =
- MAL.fold
- (fun universe entry map ->
- MAL.add (recons_univ universe) (recons_entry entry) map)
- graph
- MAL.empty,
- UriManager.UriSet.fold
- (fun u acc ->
- UriManager.UriSet.add
- (UriManager.uri_of_string (UriManager.string_of_uri u)) acc)
- uriset UriManager.UriSet.empty, o
-
-let assert_univ u =
- match u with
- | (_,None) ->
- raise (UniverseInconsistency (lazy "This universe graph has a hole"))
- | _ -> ()
-
-let assert_univs_have_uri (graph,_,_) univlist =
- let assert_set s =
- SOF.iter (fun u -> assert_univ u) s
- in
- let assert_entry e =
- assert_set e.eq_closure;
- assert_set e.ge_closure;
- assert_set e.gt_closure;
- assert_set e.in_gegt_of;
- assert_set e.one_s_eq;
- assert_set e.one_s_ge;
- assert_set e.one_s_gt;
- in
- MAL.iter (fun k v -> assert_univ k; assert_entry v)graph;
- List.iter assert_univ univlist
-
-let is_anon = function (_,None) -> true | _ -> false
-
-(* EOF *)
+++ /dev/null
-(* Copyright (C) 2004, 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://helm.cs.unibo.it/
- *)
-
-
-(*
- The strings contains an unreadable message
-*)
-exception UniverseInconsistency of string Lazy.t
-
-(*
- Cic.Type of universe
-*)
-type universe
-
-(*
- Opaque data structure you will use to store constraints
-*)
-type universe_graph
-
-(*
- returns a fresh universe
-*)
-val fresh:
- ?uri:UriManager.uri ->
- ?id:int ->
- unit ->
- universe
-
- (* names a universe if unnamed *)
-val name_universe: universe -> UriManager.uri -> universe
-
-(*
- really useful at the begin and in all the functions that don't care
- of universes
-*)
-val empty_ugraph: universe_graph
-
-(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
-val oblivion_ugraph: universe_graph
-
-(* one of the previous two, no set to empty_ugraph *)
-val default_ugraph: universe_graph
-
-
-(*
- These are the real functions to add eq/ge/gt constraints
- to the passed graph, returning an updated graph or raising
- UniverseInconsistency
-*)
-val add_eq:
- universe -> universe -> universe_graph -> universe_graph
-val add_ge:
- universe -> universe -> universe_graph -> universe_graph
-val add_gt:
- universe -> universe -> universe_graph -> universe_graph
-
-val do_rank: universe_graph -> int list * universe list
-val get_rank: universe -> int
-
-(*
- debug function to print the graph to standard error
-*)
-val print_ugraph:
- universe_graph -> unit
-
-(*
- does what expected, but I don't remember why this was exported
-*)
-val string_of_universe:
- universe -> string
-
-(*
- given the list of visible universes (see universes_of_obj) returns a
- cleaned graph (cleaned from the not visible nodes)
-*)
-val clean_ugraph:
- universe_graph -> universe list -> universe_graph
-
-(*
- Since fresh() can't add the right uri to each node, you
- must fill empty nodes with the uri before you serialize the graph to xml
-
- these empty nodes are also filled in the universe list
-*)
-val fill_empty_nodes_with_uri:
- universe_graph -> universe list -> UriManager.uri ->
- universe_graph * universe list
-
-(*
- makes a union.
- TODO:
- - remember already merged uri so that we completely skip already merged
- graphs, this may include a dependecy graph (not merge a subpart of an
- already merged graph)
-*)
-val merge_ugraphs:
- base_ugraph:universe_graph ->
- increment:(universe_graph * UriManager.uri) -> universe_graph
-
-(*
- ugraph to xml file and viceversa
-*)
-val write_xml_of_ugraph:
- string -> universe_graph -> universe list -> unit
-
-(*
- given a filename parses the xml and returns the data structure
-*)
-val ugraph_and_univlist_of_xml:
- string -> universe_graph * universe list
-val restart_numbering:
- unit -> unit
-
-(*
- returns the universe number (used to save it do xml)
-*)
-val univno: universe -> int
-val univuri: universe -> UriManager.uri
-
- (** re-hash-cons URIs contained in the given universe so that phisicaly
- * equality could be enforced. Mainly used by
- * CicEnvironment.restore_from_channel *)
-val recons_graph: universe_graph -> universe_graph
-
- (** re-hash-cons a single universe *)
-val recons_univ: universe -> universe
-
- (** consistency check that should be done before committin the graph to the
- * cache *)
-val assert_univs_have_uri: universe_graph -> universe list-> unit
-
- (** asserts the universe is named *)
-val assert_univ: universe -> unit
-
-val compare: universe -> universe -> int
-val eq: universe -> universe -> bool
-
-val is_anon: universe -> bool
+++ /dev/null
-(* Copyright (C) 2004, 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://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-module C = Cic
-
-let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
-let slash_RE = Str.regexp "/"
-
-let term_of_uri uri =
- let s = UriManager.string_of_uri uri in
- try
- (if UriManager.uri_is_con uri then
- C.Const (uri, [])
- else if UriManager.uri_is_var uri then
- C.Var (uri, [])
- else if not (Str.string_match xpointer_RE s 0) then
- raise (UriManager.IllFormedUri s)
- else
- let (baseuri,xpointer) = (Str.matched_group 1 s, Str.matched_group 2 s) in
- let baseuri = UriManager.uri_of_string baseuri in
- (match Str.split slash_RE xpointer with
- | [_; tyno] -> C.MutInd (baseuri, int_of_string tyno - 1, [])
- | [_; tyno; consno] ->
- C.MutConstruct
- (baseuri, int_of_string tyno - 1, int_of_string consno, [])
- | _ -> raise Exit))
- with
- | Exit
- | Failure _
- | Not_found -> raise (UriManager.IllFormedUri s)
+++ /dev/null
-(* Copyright (C) 2004, 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://helm.cs.unibo.it/
- *)
-
-(** conversions between terms which are fully representable as uris (Var, Const,
- * Mutind, and MutConstruct) and corresponding tree representations *)
-val term_of_uri: UriManager.uri -> Cic.term (** @raise UriManager.IllFormedUri *)
| Ast.Num (num, _) -> num
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
- | Ast.Sort (`Type _) -> "Type"
- | Ast.Sort (`CProp _)-> "CProp"
| Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
| Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
| Ast.Symbol (name, _) -> "'" ^ name
type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of
-CicUniv.universe | `NType of string |`NCProp of string]
+type sort_kind = [ `Prop | `Set | `NType of string |`NCProp of string]
type fold_kind = [ `Left | `Right ]
type location = Stdpp.location
[ "Prop" -> `Prop
| "Set" -> `Set
| "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
- | "Type" -> `Type (CicUniv.fresh ())
| "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
- | "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
disambiguate_macro:
(GrafiteTypes.status ->
(('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
disambiguate_macro:
(GrafiteTypes.status ->
(('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
options ->
GrafiteTypes.status ->
type 'a eval_from_moo =
{ efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
-let coercion_moo_statement_of (uri,arity, saturations,_) =
- GrafiteAst.Coercion
- (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
-
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
;;
exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+ (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
disambiguate_macro:
(GrafiteTypes.status ->
(('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro) ->
+ Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
NotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactic
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
let singleton msg = function
| [x], _ -> x
| l, _ ->
NotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactic
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
val disambiguate_command:
LexiconEngine.status as 'status ->
?baseuri:string ->
{ sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
uri: (Cic.id, UriManager.uri) Hashtbl.t;
}
-
-let get_types uri =
- let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
- match o with
- | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno
- | _ -> assert false
*)
let idref register_ref =
;;
(*
-let ast_of_acic ~output_type id_to_sort annterm =
- debug_print (lazy ("ast_of_acic <- "
- ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
- let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
- let ast = ast_of_acic1 ~output_type term_info annterm in
- debug_print (lazy ("ast_of_acic -> " ^ NotationPp.pp_term ast));
- ast, term_info.uri
-
let fresh_id =
fun () ->
incr counter;
(List.find (fun (dsc', _, _) -> dsc = dsc') interpretations)
with Interpretations.Interpretation_not_found | Not_found ->
raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc)))
-
-let cic_lookup_symbol_by_dsc = lookup_symbol_by_dsc
- ~mk_implicit:(function
- | true -> Cic.Implicit (Some `Type)
- | false -> Cic.Implicit None)
- ~mk_appl:(function (Cic.Appl l)::tl -> Cic.Appl (l@tl) | l -> Cic.Appl l)
- ~term_of_uri:CicUtil.term_of_uri ~term_of_nref:(fun _ -> assert false)
-;;
term_of_nref: (NReference.reference -> 'term) ->
string -> string -> 'term codomain_item
-val cic_lookup_symbol_by_dsc:
- string -> string -> Cic.term codomain_item
-
val mk_choice:
mk_appl: ('term list -> 'term) ->
mk_implicit: (bool -> 'term) ->
| NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
| NotationPt.Sort `Set -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
- | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
- [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
| NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
[`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
| NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
[`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
- | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
- [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
| NotationPt.Symbol (symbol, instance) ->
Disambiguate.resolve ~env ~mk_choice
(Symbol (symbol, instance)) (`Args [])
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id$ *)
-
-let debug = true
-let ignore_exc = false
-let rank_all_dependencies = false
-let trust_environment = false
-let print_object = false
-
-let indent = ref 0;;
-
-let load_graph, get_graph =
- let oldg = ref CicUniv.empty_ugraph in
- (function uri ->
- let _,g = CicEnvironment.get_obj !oldg uri in
- oldg := g),
- (function _ -> !oldg)
-;;
-
-let logger =
- let do_indent () = String.make !indent ' ' in
- (function
- | `Start_type_checking s ->
- if debug then
- prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s);
- incr indent
- | `Type_checking_completed s ->
- decr indent;
- if debug then
- prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
- | `Type_checking_interrupted s ->
- decr indent;
- if debug then
- prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
- | `Type_checking_failed s ->
- decr indent;
- if debug then
- prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
- | `Trust_obj s ->
- if debug then
- prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
-;;
-
-let mk_type n =
- if n = 0 then
- [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
- else
- [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
-;;
-let mk_cprop n =
- if n = 0 then
- [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
- else
- [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
-;;
-
-
-let _ =
- Sys.catch_break true;
- let do_old_logging = ref true in
- HelmLogger.register_log_callback
- (fun ?append_NL html_msg ->
- if !do_old_logging then
- prerr_endline (HelmLogger.string_of_html_msg html_msg));
- CicParser.impredicative_set := false;
- NCicTypeChecker.set_logger logger;
- Helm_registry.load_from "conf.xml";
- let alluris =
- try
- let s = Sys.argv.(1) in
- if s = "-alluris" then
- begin
- let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in
- let uris = Http_getter.getalluris () in
- let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
- let oc = open_out "alluris.txt" in
- List.iter (fun s -> output_string oc (s^"\n")) alluris;
- close_out oc;
- []
- end
- else [s]
- with Invalid_argument _ ->
- let r = ref [] in
- let ic = open_in "alluris.txt" in
- try while true do r := input_line ic :: !r; done; []
- with _ -> List.rev !r
- in
- let alluris =
- HExtlib.filter_map
- (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris
- in
- (* brutal *)
- prerr_endline "computing graphs to load...";
- let roots_alluris =
- if not rank_all_dependencies then
- alluris
- else (
- let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in
- MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
- let uniq l =
- HExtlib.list_uniq (List.sort UriManager.compare l) in
- let who_uses u =
- uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri)
- (MetadataDeps.inverse_deps ~dbd u)) in
- let rec fix acc l =
- let acc, todo =
- List.fold_left (fun (acc,todo) x ->
- let w = who_uses x in
- if w = [] then (x::acc,todo) else (acc,uniq (todo@w)))
- (acc,[]) l
- in
- if todo = [] then uniq acc else fix acc todo
- in
- fix [] alluris)
- in
- prerr_endline "generating Coq graphs...";
- CicEnvironment.set_trust (fun _ -> trust_environment);
- List.iter
- (fun u ->
- prerr_endline (" - " ^ UriManager.string_of_uri u);
- try
- ignore(CicTypeChecker.typecheck u);
- with
- | CicTypeChecker.AssertFailure s
- | CicTypeChecker.TypeCheckerFailure s ->
- prerr_endline (Lazy.force s);
- assert false
- ) roots_alluris;
- prerr_endline "loading...";
- List.iter
- (fun u ->
- prerr_endline (" - "^UriManager.string_of_uri u);
- try load_graph u with exn -> ())
- roots_alluris;
- prerr_endline "finished....";
- let lll, uuu =(CicUniv.do_rank (get_graph ())) in
- let lll = List.sort compare lll in
- List.iter (fun k ->
- prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu;
- let _ =
- try
- let rec aux = function
- | a::(b::_ as tl) ->
- NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
- NCicEnvironment.add_lt_constraint (mk_cprop a) (mk_cprop b);
- aux tl
- | _ -> ()
- in
- aux lll
- with NCicEnvironment.BadConstraint s as e ->
- prerr_endline (Lazy.force s); raise e
- in
- prerr_endline "ranked....";
- prerr_endline (NCicEnvironment.pp_constraints ());
-(*
- let [_,type0_uri] = mk_type 0 in
- let [_,type1_uri] = mk_type 1 in
- let [_,type2_uri] = mk_type 2 in
- prerr_endline
- ("Min:" ^
- (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with
- | None -> "NO SUP"
- | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]
- (NCic.Sort (NCic.Type t))));
-*)
- HExtlib.profiling_enabled := false;
- List.iter (fun uu ->
- let uu= OCic2NCic.nuri_of_ouri uu in
- indent := 0;
- let o = NCicLibrary.get_obj uu in
- if print_object then prerr_endline (NCicPp.ppobj o);
- try
- NCicEnvironment.check_and_add_obj o
- with
- | NCicTypeChecker.AssertFailure s
- | NCicTypeChecker.TypeCheckerFailure s
- | NCicEnvironment.ObjectNotFound s
- | NCicEnvironment.BadConstraint s
- | NCicEnvironment.BadDependency (s,_) as e ->
- prerr_endline ("######### " ^ Lazy.force s);
- if not ignore_exc then raise e
- )
- alluris;
- NCicEnvironment.invalidate ();
- Gc.compact ();
- HExtlib.profiling_enabled := true;
- NCicTypeChecker.set_logger (fun _ -> ());
- do_old_logging := false;
- prerr_endline "typechecking, first with the new and then with the old kernel";
- List.iter
- (fun u ->
- let u = OCic2NCic.nuri_of_ouri u in
- indent := 0;
- match NCicLibrary.get_obj u with
- | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
- let rec intros = function
- | NCic.Prod (name, s, t) ->
- let ctx, t = intros t in
- ctx @ [(name, (NCic.Decl s))] , t
- | t -> [], t
- in
- let rec perforate ctx metasenv = function
- | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
- when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
- let metasenv, ty = perforate ctx metasenv ty in
- let a,_,b,_ =
- NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
- | t ->
- NCicUntrusted.map_term_fold_a
- (fun e ctx -> e::ctx) ctx perforate metasenv t
- in
- let rec curryfy ctx = function
- | NCic.Lambda (name, (NCic.Sort _ as s), tgt) ->
- NCic.Lambda (name, s, curryfy ((name,NCic.Decl s) :: ctx) tgt)
- | NCic.Lambda (name, s, tgt) ->
- let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
- NCic.Lambda (name, NCic.Implicit `Type, tgt)
- | t ->
- NCicUtils.map
- (fun e ctx -> e::ctx) ctx curryfy t
- in
-(*
- let ctx, pty = intros ty in
- let metasenv, pty = perforate ctx [] pty in
-*)
-(*
- let sty, metasenv, _ =
- NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
- in
-*)
-(* let ctx, ty = intros ty in *)
-(*
- let left, right =
- match NCicReduction.whd ~delta:max_int ctx pty with
- | NCic.Appl [eq;t;a;b] -> a, b
- | _-> assert false
- in
-*)
-
-(*
- let whd ty =
- match ty with
- | NCic.Appl [eq;t;a;b] ->
- NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
- | t -> NCicReduction.whd ~delta:0 ctx t
- in
-*)
-(*
- prerr_endline
- (Printf.sprintf "%s == %s"
- (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
- (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
-*)
- prerr_endline ("start: " ^ NUri.string_of_uri u);
- let bo = curryfy [] bo in
- (try
- let rdb = new NRstatus.status in
- let metasenv, subst, bo, infty =
- NCicRefiner.typeof rdb [] [] [] bo None
- in
- let metasenv, subst =
- try
- NCicUnification.unify rdb metasenv subst [] infty ty
- with
- | NCicUnification.Uncertain msg
- | NCicUnification.UnificationFailure msg
- | NCicMetaSubst.MetaSubstFailure msg ->
- prerr_endline (Lazy.force msg);
- metasenv, subst
- | Sys.Break -> metasenv, subst
- in
- if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
- then
- prerr_endline ("OK: " ^ NUri.string_of_uri u)
- else
- (
- let ctx = [] in
- let right = infty in
- let left = ty in
-
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
- prerr_endline
- (Printf.sprintf
- ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^
- "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
- "TERMS:\n%s\n==\n%s\n")
- (NCicPp.ppsubst ~metasenv subst)
- (NCicPp.ppmetasenv ~subst metasenv)
- (NCicPp.ppcontext ~metasenv ~subst ctx)
- (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
- (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
- (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
- (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
- (*let inferred_ty =
- NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
- in*)
- with
- | Sys.Break -> ()
- | NCicRefiner.RefineFailure msg
- | NCicRefiner.Uncertain msg ->
- let _, msg = Lazy.force msg in
- prerr_endline msg;
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
- | e ->
- prerr_endline (Printexc.to_string e);
- prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
- )
- | _ -> ())
- alluris;
-;;
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ *)
-
-(* $Id$ *)
-
-let _ =
- Helm_registry.load_from "conf.xml";
- CicParser.impredicative_set := false;
- let u = UriManager.uri_of_string Sys.argv.(1) in
- let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
- prerr_endline "VECCHIO";
- prerr_endline (CicPp.ppobj o);
- let l = OCic2NCic.convert_obj u o in
- prerr_endline "OGGETTI:.........................................";
- List.iter (fun o -> prerr_endline (NCicPp.ppobj o)) l;
- prerr_endline "/OGGETTI:.........................................";
- let objs =
- List.flatten
- (List.map NCic2OCic.convert_nobj l) in
- List.iter
- (fun (u,o) ->
- prerr_endline ("round trip: " ^ UriManager.string_of_uri u);
- prerr_endline (CicPp.ppobj o);
- prerr_endline "tipo.......";
- try CicTypeChecker.typecheck_obj u o
- with
- CicTypeChecker.TypeCheckerFailure s
- | CicTypeChecker.AssertFailure s ->
- prerr_endline (Lazy.force s)
- | CicEnvironment.Object_not_found uri ->
- prerr_endline
- ("CicEnvironment: Object not found " ^ UriManager.string_of_uri uri))
- objs;
-;;
projects / helm.git / commitdiff