From d284dd23d0e12a62a001d3473eadf4942d12ffaa Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 11:36:04 +0000 Subject: [PATCH] - cic almost not used --- matita/components/cic/.depend | 3 - matita/components/cic/.depend.opt | 3 - matita/components/cic/Makefile | 5 +- matita/components/cic/cic.ml | 6 - matita/components/cic/cicPp.ml | 538 ---------- matita/components/cic/cicPp.mli | 55 - matita/components/cic/cicUniv.ml | 941 ------------------ matita/components/cic/cicUniv.mli | 160 --- matita/components/cic/cicUtil.ml | 54 - matita/components/cic/cicUtil.mli | 28 - matita/components/content/notationPp.ml | 2 - matita/components/content/notationPt.ml | 3 +- .../content_pres/cicNotationParser.ml | 2 - .../grafite_engine/grafiteEngine.ml | 10 +- .../grafite_engine/grafiteEngine.mli | 4 +- .../grafite_parser/grafiteDisambiguate.ml | 4 - .../grafite_parser/grafiteDisambiguate.mli | 4 - .../ng_cic_content/nTermCicContent.ml | 14 - .../ng_disambiguation/disambiguateChoices.ml | 8 - .../ng_disambiguation/disambiguateChoices.mli | 3 - .../ng_disambiguation/nCicDisambiguate.ml | 4 - matita/components/ng_refiner/check.ml | 320 ------ matita/components/ng_refiner/rt.ml | 42 - 23 files changed, 7 insertions(+), 2206 deletions(-) delete mode 100644 matita/components/cic/cicPp.ml delete mode 100644 matita/components/cic/cicPp.mli delete mode 100644 matita/components/cic/cicUniv.ml delete mode 100644 matita/components/cic/cicUniv.mli delete mode 100644 matita/components/cic/cicUtil.ml delete mode 100644 matita/components/cic/cicUtil.mli delete mode 100644 matita/components/ng_refiner/check.ml delete mode 100644 matita/components/ng_refiner/rt.ml diff --git a/matita/components/cic/.depend b/matita/components/cic/.depend index cabb8d5d1..2ba6ab8fd 100644 --- a/matita/components/cic/.depend +++ b/matita/components/cic/.depend @@ -1,11 +1,8 @@ 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 diff --git a/matita/components/cic/.depend.opt b/matita/components/cic/.depend.opt index 296da325d..34fcd83c2 100644 --- a/matita/components/cic/.depend.opt +++ b/matita/components/cic/.depend.opt @@ -1,11 +1,8 @@ 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 diff --git a/matita/components/cic/Makefile b/matita/components/cic/Makefile index 297d41d20..09b39139b 100644 --- a/matita/components/cic/Makefile +++ b/matita/components/cic/Makefile @@ -1,10 +1,7 @@ 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 diff --git a/matita/components/cic/cic.ml b/matita/components/cic/cic.ml index 9a4f4b0de..012f52eea 100644 --- a/matita/components/cic/cic.ml +++ b/matita/components/cic/cic.ml @@ -48,8 +48,6 @@ type implicit_annotation = [ `Closed | `Type | `Hole ] type sort = Prop | Set - | Type of CicUniv.universe - | CProp of CicUniv.universe type name = | Name of string @@ -221,10 +219,6 @@ and annhypothesis = 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 diff --git a/matita/components/cic/cicPp.ml b/matita/components/cic/cicPp.ml deleted file mode 100644 index 931a98135..000000000 --- a/matita/components/cic/cicPp.ml +++ /dev/null @@ -1,538 +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 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 -;; - - diff --git a/matita/components/cic/cicPp.mli b/matita/components/cic/cicPp.mli deleted file mode 100644 index e898c352d..000000000 --- a/matita/components/cic/cicPp.mli +++ /dev/null @@ -1,55 +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 *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 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 diff --git a/matita/components/cic/cicUniv.ml b/matita/components/cic/cicUniv.ml deleted file mode 100644 index 58dc5cd6c..000000000 --- a/matita/components/cic/cicUniv.ml +++ /dev/null @@ -1,941 +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 *) -(* *) -(* Enrico Tassi *) -(* 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 - - -(*****************************************************************************) -(** _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'' (* ) *) -;; - - - -(*****************************************************************************) -(** 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 "\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 - - -(*****************************************************************************) -(** 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 *) diff --git a/matita/components/cic/cicUniv.mli b/matita/components/cic/cicUniv.mli deleted file mode 100644 index 8a24614c2..000000000 --- a/matita/components/cic/cicUniv.mli +++ /dev/null @@ -1,160 +0,0 @@ -(* 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 diff --git a/matita/components/cic/cicUtil.ml b/matita/components/cic/cicUtil.ml deleted file mode 100644 index e600b5388..000000000 --- a/matita/components/cic/cicUtil.ml +++ /dev/null @@ -1,54 +0,0 @@ -(* 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) diff --git a/matita/components/cic/cicUtil.mli b/matita/components/cic/cicUtil.mli deleted file mode 100644 index 3a3e155a5..000000000 --- a/matita/components/cic/cicUtil.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* 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 *) diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml index a101747df..30abf348e 100644 --- a/matita/components/content/notationPp.ml +++ b/matita/components/content/notationPp.ml @@ -154,8 +154,6 @@ let rec pp_term ?(pp_parens = true) t = | 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 diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml index 731a2ba74..90990300a 100644 --- a/matita/components/content/notationPt.ml +++ b/matita/components/content/notationPt.ml @@ -29,8 +29,7 @@ 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 diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 18c52b7cf..2d52f0b89 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -582,9 +582,7 @@ EXTEND [ "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: [ diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 6ebeb2842..6dd087d78 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -30,7 +30,7 @@ exception Drop 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 @@ -57,7 +57,7 @@ type eval_ast = 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 -> @@ -97,7 +97,7 @@ type 'a eval_executable = 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 -> @@ -108,10 +108,6 @@ type 'a eval_executable = 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 ;; diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index dbb462d65..dd3216412 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -27,7 +27,7 @@ exception Drop 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 @@ -41,7 +41,7 @@ val eval_ast : 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 -> diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index c23e5acff..bd633d5d2 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -32,10 +32,6 @@ type tactic = 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, _ -> diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 7590699f9..4392de870 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -30,10 +30,6 @@ type tactic = 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 -> diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index 18685f35b..dbd6523cf 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -43,12 +43,6 @@ type term_info = { 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 = @@ -340,14 +334,6 @@ in ;; (* -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; diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 6c335ab64..dfddae59b 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -88,11 +88,3 @@ let lookup_symbol_by_dsc ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref symbol (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) -;; diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli index 4e9807932..f96d90459 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.mli +++ b/matita/components/ng_disambiguation/disambiguateChoices.mli @@ -57,9 +57,6 @@ val lookup_symbol_by_dsc: 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) -> diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 2c5b06394..f3341a5f7 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -352,14 +352,10 @@ let interpretate_term_and_interpretate_term_option | 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 []) diff --git a/matita/components/ng_refiner/check.ml b/matita/components/ng_refiner/check.ml deleted file mode 100644 index 4cb188170..000000000 --- a/matita/components/ng_refiner/check.ml +++ /dev/null @@ -1,320 +0,0 @@ -(* - ||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; -;; diff --git a/matita/components/ng_refiner/rt.ml b/matita/components/ng_refiner/rt.ml deleted file mode 100644 index 997bc2e3c..000000000 --- a/matita/components/ng_refiner/rt.ml +++ /dev/null @@ -1,42 +0,0 @@ -(* - ||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; -;; -- 2.39.2