From 179cb3108e88369d855ba0088084be285fb19fdc Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 5 Oct 2010 16:45:05 +0000 Subject: [PATCH] whelp and cic disambiguation removed --- matita/components/METAS/meta.helm-lexicon.src | 2 +- .../METAS/meta.helm-ng_disambiguation.src | 2 +- .../components/METAS/meta.helm-ng_kernel.src | 2 +- matita/components/METAS/meta.helm-tactics.src | 2 +- matita/components/METAS/meta.helm-whelp.src | 4 - matita/components/Makefile | 2 - matita/components/cic_disambiguation/.depend | 8 - .../components/cic_disambiguation/.depend.opt | 8 - matita/components/cic_disambiguation/Makefile | 20 - .../cic_disambiguation/cicDisambiguate.ml | 685 ----------------- .../cic_disambiguation/cicDisambiguate.mli | 74 -- .../cic_disambiguation/doc/precedence.txt | 32 - .../cic_disambiguation/number_notation.ml | 78 -- .../cic_disambiguation/tests/aliases.txt | 6 - .../cic_disambiguation/tests/eq.txt | 1 - .../cic_disambiguation/tests/match.txt | 49 -- .../grafite_engine/grafiteEngine.ml | 63 +- .../grafite_parser/grafiteDisambiguate.ml | 695 +----------------- .../grafite_parser/grafiteDisambiguate.mli | 14 - matita/components/ng_disambiguation/.depend | 2 + matita/components/ng_disambiguation/Makefile | 1 + .../disambiguateChoices.ml | 0 .../disambiguateChoices.mli | 0 matita/components/tactics/fwdSimplTactic.ml | 2 + matita/components/whelp/.depend | 6 - matita/components/whelp/.depend.opt | 6 - matita/components/whelp/Makefile | 11 - matita/components/whelp/fwdQueries.ml | 115 --- matita/components/whelp/fwdQueries.mli | 28 - matita/components/whelp/whelp.ml | 232 ------ matita/components/whelp/whelp.mli | 30 - matita/configure.ac | 1 - matita/matita/matitaEngine.ml | 23 +- 33 files changed, 26 insertions(+), 2178 deletions(-) delete mode 100644 matita/components/METAS/meta.helm-whelp.src delete mode 100644 matita/components/cic_disambiguation/.depend delete mode 100644 matita/components/cic_disambiguation/.depend.opt delete mode 100644 matita/components/cic_disambiguation/Makefile delete mode 100644 matita/components/cic_disambiguation/cicDisambiguate.ml delete mode 100644 matita/components/cic_disambiguation/cicDisambiguate.mli delete mode 100644 matita/components/cic_disambiguation/doc/precedence.txt delete mode 100644 matita/components/cic_disambiguation/number_notation.ml delete mode 100644 matita/components/cic_disambiguation/tests/aliases.txt delete mode 100644 matita/components/cic_disambiguation/tests/eq.txt delete mode 100644 matita/components/cic_disambiguation/tests/match.txt rename matita/components/{cic_disambiguation => ng_disambiguation}/disambiguateChoices.ml (100%) rename matita/components/{cic_disambiguation => ng_disambiguation}/disambiguateChoices.mli (100%) delete mode 100644 matita/components/whelp/.depend delete mode 100644 matita/components/whelp/.depend.opt delete mode 100644 matita/components/whelp/Makefile delete mode 100644 matita/components/whelp/fwdQueries.ml delete mode 100644 matita/components/whelp/fwdQueries.mli delete mode 100644 matita/components/whelp/whelp.ml delete mode 100644 matita/components/whelp/whelp.mli diff --git a/matita/components/METAS/meta.helm-lexicon.src b/matita/components/METAS/meta.helm-lexicon.src index a98593133..0842312ec 100644 --- a/matita/components/METAS/meta.helm-lexicon.src +++ b/matita/components/METAS/meta.helm-lexicon.src @@ -1,4 +1,4 @@ -requires="helm-content_pres helm-ng_library helm-cic_disambiguation camlp5.gramlib" +requires="helm-content_pres helm-ng_library camlp5.gramlib" version="0.0.1" archive(byte)="lexicon.cma" archive(native)="lexicon.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_disambiguation.src b/matita/components/METAS/meta.helm-ng_disambiguation.src index 7693d8f3c..7910e8dff 100644 --- a/matita/components/METAS/meta.helm-ng_disambiguation.src +++ b/matita/components/METAS/meta.helm-ng_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-whelp helm-acic_content helm-ng_refiner helm-disambiguation helm-cic_disambiguation" +requires="helm-acic_content helm-ng_refiner helm-disambiguation" version="0.0.1" archive(byte)="ng_disambiguation.cma" archive(native)="ng_disambiguation.cmxa" diff --git a/matita/components/METAS/meta.helm-ng_kernel.src b/matita/components/METAS/meta.helm-ng_kernel.src index acf5aab9e..b5402e3fa 100644 --- a/matita/components/METAS/meta.helm-ng_kernel.src +++ b/matita/components/METAS/meta.helm-ng_kernel.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking helm-library helm-metadata" +requires="helm-cic_proof_checking helm-library" version="0.0.1" archive(byte)="ng_kernel.cma" archive(native)="ng_kernel.cmxa" diff --git a/matita/components/METAS/meta.helm-tactics.src b/matita/components/METAS/meta.helm-tactics.src index 5f620680a..1eee28f6a 100644 --- a/matita/components/METAS/meta.helm-tactics.src +++ b/matita/components/METAS/meta.helm-tactics.src @@ -1,4 +1,4 @@ -requires="helm-extlib helm-cic_proof_checking helm-cic_unification helm-whelp" +requires="helm-extlib helm-cic_proof_checking helm-cic_unification" version="0.0.1" archive(byte)="tactics.cma" archive(native)="tactics.cmxa" diff --git a/matita/components/METAS/meta.helm-whelp.src b/matita/components/METAS/meta.helm-whelp.src deleted file mode 100644 index 20ea84329..000000000 --- a/matita/components/METAS/meta.helm-whelp.src +++ /dev/null @@ -1,4 +0,0 @@ -requires="helm-metadata" -version="0.0.1" -archive(byte)="whelp.cma" -archive(native)="whelp.cmxa" diff --git a/matita/components/Makefile b/matita/components/Makefile index 02125883f..db866c9c4 100644 --- a/matita/components/Makefile +++ b/matita/components/Makefile @@ -27,11 +27,9 @@ MODULES = \ acic_content \ grafite \ cic_unification \ - whelp \ tactics \ acic_procedural \ disambiguation \ - cic_disambiguation \ ng_kernel \ ng_refiner \ ng_disambiguation \ diff --git a/matita/components/cic_disambiguation/.depend b/matita/components/cic_disambiguation/.depend deleted file mode 100644 index a9ae65a5e..000000000 --- a/matita/components/cic_disambiguation/.depend +++ /dev/null @@ -1,8 +0,0 @@ -cicDisambiguate.cmi: -disambiguateChoices.cmi: -cicDisambiguate.cmo: cicDisambiguate.cmi -cicDisambiguate.cmx: cicDisambiguate.cmi -disambiguateChoices.cmo: disambiguateChoices.cmi -disambiguateChoices.cmx: disambiguateChoices.cmi -number_notation.cmo: disambiguateChoices.cmi -number_notation.cmx: disambiguateChoices.cmx diff --git a/matita/components/cic_disambiguation/.depend.opt b/matita/components/cic_disambiguation/.depend.opt deleted file mode 100644 index a9ae65a5e..000000000 --- a/matita/components/cic_disambiguation/.depend.opt +++ /dev/null @@ -1,8 +0,0 @@ -cicDisambiguate.cmi: -disambiguateChoices.cmi: -cicDisambiguate.cmo: cicDisambiguate.cmi -cicDisambiguate.cmx: cicDisambiguate.cmi -disambiguateChoices.cmo: disambiguateChoices.cmi -disambiguateChoices.cmx: disambiguateChoices.cmi -number_notation.cmo: disambiguateChoices.cmi -number_notation.cmx: disambiguateChoices.cmx diff --git a/matita/components/cic_disambiguation/Makefile b/matita/components/cic_disambiguation/Makefile deleted file mode 100644 index 2fb5de515..000000000 --- a/matita/components/cic_disambiguation/Makefile +++ /dev/null @@ -1,20 +0,0 @@ -PACKAGE = cic_disambiguation -NOTATIONS = number -INTERFACE_FILES = \ - cicDisambiguate.mli \ - disambiguateChoices.mli -IMPLEMENTATION_FILES = \ - $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ - $(patsubst %,%_notation.ml,$(NOTATIONS)) - -all: - -clean: -distclean: - rm -f macro_table.dump - -include ../../Makefile.defs -include ../Makefile.common - -OCAMLARCHIVEOPTIONS += -linkall - diff --git a/matita/components/cic_disambiguation/cicDisambiguate.ml b/matita/components/cic_disambiguation/cicDisambiguate.ml deleted file mode 100644 index 8f8bba7d8..000000000 --- a/matita/components/cic_disambiguation/cicDisambiguate.ml +++ /dev/null @@ -1,685 +0,0 @@ -(* -Copyright (C) 1999-2006, 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 this program; if not, write to the Free Software -Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA -02110-1301 USA. - -For details, see the HELM web site: http://helm.cs.unibo.it/ -*) - -open Printf -module Ast = CicNotationPt - -let debug = false -let debug_print s = if debug then prerr_endline (Lazy.force s) else () - -let rec string_context_of_context = - List.map - (function - | Cic.Name n -> Some n - | Cic.Anonymous -> Some "_") -;; - -let refine_term metasenv subst context uri ~use_coercions - term expty ugraph ~localization_tbl = -(* if benchmark then incr actual_refinements; *) - assert (uri=None); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term))); - let saved_use_coercions = !CicRefine.insert_coercions in - try - CicRefine.insert_coercions := use_coercions; - let term = - match expty with - | None -> term - | Some ty -> Cic.Cast(term,ty) - in - let term', _, metasenv',ugraph1 = - CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl - in - let term' = - match expty, term' with - | None,_ -> term' - | Some _,Cic.Cast (term',_) -> term' - | _ -> assert false - in - CicRefine.insert_coercions := saved_use_coercions; - (Disambiguate.Ok (term', metasenv',[],ugraph1)) - with - exn -> - CicRefine.insert_coercions := saved_use_coercions; - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ; - Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (Lazy.force msg))); - Disambiguate.Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn - -let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph - ~localization_tbl = - assert (context = []); - assert (metasenv = []); - assert (subst = []); - debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ; - let saved_use_coercions = !CicRefine.insert_coercions in - try - CicRefine.insert_coercions := use_coercions; - let obj', metasenv,ugraph = - CicRefine.typecheck metasenv uri obj ~localization_tbl - in - CicRefine.insert_coercions := saved_use_coercions; - (Disambiguate.Ok (obj', metasenv,[],ugraph)) - with - exn -> - CicRefine.insert_coercions := saved_use_coercions; - let rec process_exn loc = - function - HExtlib.Localized (loc,exn) -> process_exn loc exn - | CicRefine.Uncertain msg -> - debug_print (lazy ("UNCERTAIN!!! [" ^ - (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ; - Disambiguate.Uncertain (lazy (loc,Lazy.force msg)) - | CicRefine.RefineFailure msg -> - debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (Lazy.force msg))) ; - Disambiguate.Ko (lazy (loc,Lazy.force msg)) - | exn -> raise exn - in - process_exn Stdpp.dummy_loc exn -;; - -let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri - ~is_path ast ~localization_tbl ~obj_context -= - (* create_dummy_ids shouldbe used only for interpretating patterns *) - assert (uri = None); - let rec aux ~localize loc context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> - let res = aux ~localize loc context term in - if localize then Cic.CicHash.add localization_tbl res loc; - res - | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term - | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> - let cic_args = List.map (aux ~localize loc context) args in - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args) - | CicNotationPt.Appl terms -> - Cic.Appl (List.map (aux ~localize loc context) terms) - | CicNotationPt.Binder (binder_kind, (var, typ), body) -> - let cic_type = aux_option ~localize loc context (Some `Type) typ in - let cic_name = CicNotationUtil.cic_name_of_name var in - let cic_body = aux ~localize loc (cic_name :: context) body in - (match binder_kind with - | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) - | `Pi - | `Forall -> Cic.Prod (cic_name, cic_type, cic_body) - | `Exists -> - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Symbol ("exists", 0)) - (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ])) - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let cic_term = aux ~localize loc context term in - let cic_outtype = aux_option ~localize loc context None outtype in - let do_branch ((head, _, args), term) = - let rec do_branch' context = function - | [] -> aux ~localize loc context term - | (name, typ) :: tl -> - let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_body = do_branch' (cic_name :: context) tl in - let typ = - match typ with - | None -> Cic.Implicit (Some `Type) - | Some typ -> aux ~localize loc context typ - in - Cic.Lambda (cic_name, typ, cic_body) - in - do_branch' context args - in - let indtype_uri, indtype_no = - if create_dummy_ids then - (UriManager.uri_of_string "cic:/fake_indty.con", 0) - else - match indty_ident with - | Some (indty_ident, _) -> - (match - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Id indty_ident) (`Args []) - with - | Cic.MutInd (uri, tyno, _) -> (uri, tyno) - | Cic.Implicit _ -> - raise (Disambiguate.Try_again - (lazy "The type of the term to be matched - is still unknown")) - | _ -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!")))) - | None -> - let rec fst_constructor = - function - (Ast.Pattern (head, _, _), _) :: _ -> head - | (Ast.Wildcard, _) :: tl -> fst_constructor tl - | [] -> raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))) - in - (match Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Id (fst_constructor branches)) - (`Args []) with - | Cic.MutConstruct (indtype_uri, indtype_no, _, _) -> - (indtype_uri, indtype_no) - | Cic.Implicit _ -> - raise (Disambiguate.Try_again (lazy "The type of the term to be matched - is still unknown")) - | _ -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!")))) - in - let branches = - if create_dummy_ids then - List.map - (function - Ast.Wildcard,term -> ("wildcard",None,[]), term - | Ast.Pattern _,_ -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\""))) - ) branches - else - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with - Cic.InductiveDefinition (il,_,leftsno,_) -> - let _,_,_,cl = - try - List.nth il indtype_no - with _ -> assert false - in - let rec count_prod t = - match CicReduction.whd [] t with - Cic.Prod (_, _, t) -> 1 + (count_prod t) - | _ -> 0 - in - let rec sort branches cl = - match cl with - [] -> - let rec analyze unused unrecognized useless = - function - [] -> - if unrecognized != [] then - raise (DisambiguateTypes.Invalid_choice - (lazy (loc, - ("Unrecognized constructors: " ^ - String.concat " " unrecognized)))) - else if useless > 0 then - raise (DisambiguateTypes.Invalid_choice - (lazy (loc, - ("The last " ^ string_of_int useless ^ - "case" ^ if useless > 1 then "s are" else " is" ^ - " unused")))) - else - [] - | (Ast.Wildcard,_)::tl when not unused -> - analyze true unrecognized useless tl - | (Ast.Pattern (head,_,_),_)::tl when not unused -> - analyze unused (head::unrecognized) useless tl - | _::tl -> analyze unused unrecognized (useless + 1) tl - in - analyze false [] 0 branches - | (name,ty)::cltl -> - let rec find_and_remove = - function - [] -> - raise - (DisambiguateTypes.Invalid_choice - (lazy (loc, ("Missing case: " ^ name)))) - | ((Ast.Wildcard, _) as branch :: _) as branches -> - branch, branches - | (Ast.Pattern (name',_,_),_) as branch :: tl - when name = name' -> - branch,tl - | branch::tl -> - let found,rest = find_and_remove tl in - found, branch::rest - in - let branch,tl = find_and_remove branches in - match branch with - Ast.Pattern (name,y,args),term -> - if List.length args = count_prod ty - leftsno then - ((name,y,args),term)::sort tl cltl - else - raise - (DisambiguateTypes.Invalid_choice - (lazy (loc,"Wrong number of arguments for " ^ - name))) - | Ast.Wildcard,term -> - let rec mk_lambdas = - function - 0 -> term - | n -> - CicNotationPt.Binder - (`Lambda, (CicNotationPt.Ident ("_", None), None), - mk_lambdas (n - 1)) - in - (("wildcard",None,[]), - mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl - in - sort branches cl - | _ -> assert false - in - Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, - (List.map do_branch branches)) - | CicNotationPt.Cast (t1, t2) -> - let cic_t1 = aux ~localize loc context t1 in - let cic_t2 = aux ~localize loc context t2 in - Cic.Cast (cic_t1, cic_t2) - | CicNotationPt.LetIn ((name, typ), def, body) -> - let cic_def = aux ~localize loc context def in - let cic_name = CicNotationUtil.cic_name_of_name name in - let cic_typ = - match typ with - | None -> Cic.Implicit (Some `Type) - | Some t -> aux ~localize loc context t - in - let cic_body = aux ~localize loc (cic_name :: context) body in - Cic.LetIn (cic_name, cic_def, cic_typ, cic_body) - | CicNotationPt.LetRec (kind, defs, body) -> - let context' = - List.fold_left - (fun acc (_, (name, _), _, _) -> - CicNotationUtil.cic_name_of_name name :: acc) - context defs - in - let cic_body = - let unlocalized_body = aux ~localize:false loc context' body in - match unlocalized_body with - Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n - | Cic.Appl (Cic.Rel n::l) when n <= List.length defs -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] (List.length defs) t - in - assert (subst=[]); - assert (metasenv=[]); - t') l - in - (* We can avoid the LetIn. But maybe we need to recompute l' - so that it is localized *) - if localize then - match body with - CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> - (* since we avoid the letin, the context has no - * recfuns in it *) - let l' = List.map (aux ~localize loc context) l in - `AvoidLetIn (n,l') - | _ -> assert false - else - `AvoidLetIn (n,l') - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body) - | _ -> - if localize then - `AddLetIn (aux ~localize loc context' body) - else - `AddLetIn unlocalized_body - in - let inductiveFuns = - List.map - (fun (params, (name, typ), body, decr_idx) -> - let add_binders kind t = - List.fold_right - (fun var t -> CicNotationPt.Binder (kind, var, t)) params t - in - let cic_body = - aux ~localize loc context' (add_binders `Lambda body) in - let typ = - match typ with - Some typ -> typ - | None-> CicNotationPt.Implicit `JustOne in - let cic_type = - aux_option ~localize loc context (Some `Type) - (Some (add_binders `Pi typ)) in - let name = - match CicNotationUtil.cic_name_of_name name with - | Cic.Anonymous -> - CicNotationPt.fail loc - "Recursive functions cannot be anonymous" - | Cic.Name name -> name - in - (name, decr_idx, cic_type, cic_body)) - defs - in - let fix_or_cofix n = - match kind with - `Inductive -> Cic.Fix (n,inductiveFuns) - | `CoInductive -> - let coinductiveFuns = - List.map - (fun (name, _, typ, body) -> name, typ, body) - inductiveFuns - in - Cic.CoFix (n,coinductiveFuns) - in - let counter = ref ~-1 in - let build_term funs (var,_,ty,_) t = - incr counter; - Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t) - in - (match cic_body with - `AvoidLetInNoAppl n -> - let n' = List.length inductiveFuns - n in - fix_or_cofix n' - | `AvoidLetIn (n,l) -> - let n' = List.length inductiveFuns - n in - Cic.Appl (fix_or_cofix n'::l) - | `AddLetIn cic_body -> - List.fold_right (build_term inductiveFuns) inductiveFuns - cic_body) - | CicNotationPt.Ident _ - | CicNotationPt.Uri _ - | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed - | CicNotationPt.NCic _ -> assert false - | CicNotationPt.NRef _ -> assert false - | CicNotationPt.Ident (name,subst) - | CicNotationPt.Uri (name, subst) as ast -> - let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in - (try - if is_uri ast then raise Not_found;(* don't search the env for URIs *) - let index = - Disambiguate.find_in_context name (string_context_of_context context) - in - if subst <> None then - CicNotationPt.fail loc "Explicit substitutions not allowed here"; - Cic.Rel index - with Not_found -> - let cic = - if is_uri ast then (* we have the URI, build the term out of it *) - try - CicUtil.term_of_uri (UriManager.uri_of_string name) - with UriManager.IllFormedUri _ -> - CicNotationPt.fail loc "Ill formed URI" - else - try - List.assoc name obj_context - with - Not_found -> - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Id name) (`Args []) - in - let mk_subst uris = - let ids_to_uris = - List.map (fun uri -> UriManager.name_of_uri uri, uri) uris - in - (match subst with - | Some subst -> - List.map - (fun (s, term) -> - (try - List.assoc s ids_to_uris, aux ~localize loc context term - with Not_found -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))) - subst - | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) - in - (try - match cic with - | Cic.Const (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.Const (uri, mk_subst uris) - | Cic.Var (uri, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.Var (uri, mk_subst uris) - | Cic.MutInd (uri, i, []) -> - (try - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.MutInd (uri, i, mk_subst uris) - with - CicEnvironment.Object_not_found _ -> - (* if we are here it is probably the case that during the - definition of a mutual inductive type we have met an - occurrence of the type in one of its constructors. - However, the inductive type is not yet in the environment - *) - (*here the explicit_named_substituion is assumed to be of length 0 *) - Cic.MutInd (uri,i,[])) - | Cic.MutConstruct (uri, i, j, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.MutConstruct (uri, i, j, mk_subst uris) - | Cic.Meta _ | Cic.Implicit _ as t -> -(* - debug_print (lazy (sprintf - "Warning: %s must be instantiated with _[%s] but we do not enforce it" - (CicPp.ppterm t) - (String.concat "; " - (List.map - (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term) - subst)))); -*) - t - | _ -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?"))) - with - CicEnvironment.CircularDependency _ -> - raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment"))))) - | CicNotationPt.Implicit `Vector -> assert false - | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None - | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole) - | CicNotationPt.Num (num, i) -> - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Num i) (`Num_arg num) - | CicNotationPt.Meta (index, subst) -> - let cic_subst = - List.map - (function - None -> None - | Some term -> Some (aux ~localize loc context term)) - subst - in - Cic.Meta (index, cic_subst) - | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop - | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set - | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u) - | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) - | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ())) - | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u) - | CicNotationPt.Symbol (symbol, instance) -> - Disambiguate.resolve ~mk_choice ~env - (DisambiguateTypes.Symbol (symbol, instance)) (`Args []) - | CicNotationPt.Variable _ - | CicNotationPt.Magic _ - | CicNotationPt.Layout _ - | CicNotationPt.Literal _ -> assert false (* god bless Bologna *) - and aux_option ~localize loc context annotation = function - | None -> Cic.Implicit annotation - | Some term -> aux ~localize loc context term - in - aux ~localize:true HExtlib.dummy_floc context ast - -let interpretate_path ~context path = - let localization_tbl = Cic.CicHash.create 23 in - (* here we are throwing away useful localization informations!!! *) - fst ( - interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true - ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true - path ~localization_tbl ~obj_context:[], localization_tbl) - -let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj - ~localization_tbl -= - assert (context = []); - assert (is_path = false); - let interpretate_term ?(obj_context=[]) = - interpretate_term ~mk_choice ~localization_tbl ~obj_context in - match obj with - | CicNotationPt.Inductive (params,tyl) -> - let uri = match uri with Some uri -> uri | None -> assert false in - let context,params = - let context,res = - List.fold_left - (fun (context,res) (name,t) -> - let t = - match t with - None -> CicNotationPt.Implicit `JustOne - | Some t -> t in - let name = CicNotationUtil.cic_name_of_name name in - name::context,(name, interpretate_term context env None false t)::res - ) ([],[]) params - in - context,List.rev res in - let add_params = - List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let obj_context = - snd ( - List.fold_left - (*here the explicit_named_substituion is assumed to be of length 0 *) - (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res) - (0,[]) tyl) in - let tyl = - List.map - (fun (name,b,ty,cl) -> - let ty' = add_params (interpretate_term context env None false ty) in - let cl' = - List.map - (fun (name,ty) -> - let ty' = - add_params - (interpretate_term ~obj_context ~context ~env ~uri:None - ~is_path:false ty) - in - name,ty' - ) cl - in - name,b,ty',cl' - ) tyl - in - Cic.InductiveDefinition (tyl,[],List.length params,[]) - | CicNotationPt.Record (params,name,ty,fields) -> - let uri = match uri with Some uri -> uri | None -> assert false in - let context,params = - let context,res = - List.fold_left - (fun (context,res) (name,t) -> - let t = - match t with - None -> CicNotationPt.Implicit `JustOne - | Some t -> t in - let name = CicNotationUtil.cic_name_of_name name in - name::context,(name, interpretate_term context env None false t)::res - ) ([],[]) params - in - context,List.rev res in - let add_params = - List.fold_right - (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let ty' = add_params (interpretate_term context env None false ty) in - let fields' = - snd ( - List.fold_left - (fun (context,res) (name,ty,_coercion,arity) -> - let context' = Cic.Name name :: context in - context',(name,interpretate_term context env None false ty)::res - ) (context,[]) fields) in - let concl = - (*here the explicit_named_substituion is assumed to be of length 0 *) - let mutind = Cic.MutInd (uri,0,[]) in - if params = [] then mutind - else - Cic.Appl - (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in - let con = - List.fold_left - (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) - concl fields' in - let con' = add_params con in - let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in - Cic.InductiveDefinition - (tyl,[],List.length params,[`Class (`Record field_names)]) - | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) -> - let attrs = [`Flavour flavour] in - let ty' = interpretate_term [] env None false ty in - (match bo,flavour with - None,`Axiom -> - Cic.Constant (name,None,ty',[],attrs) - | Some bo,`Axiom -> assert false - | None,_ -> - Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs) - | Some bo,_ -> - let bo' = Some (interpretate_term [] env None false bo) in - Cic.Constant (name,bo',ty',[],attrs)) -;; - -let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri - ~is_path ast ~localization_tbl -= - let context = - List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context - in - interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path - ast ~localization_tbl ~obj_context:[] -;; - -let string_context_of_context = - List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some - (Cic.Anonymous,_) -> Some "_");; - -let disambiguate_term ~context ~metasenv ~subst ~expty - ?(initial_ugraph = CicUniv.oblivion_ugraph) - ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice - ~aliases ~universe ~lookup_in_library (text,prefix_len,term) -= - let mk_localization_tbl x = Cic.CicHash.create x in - MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst - ~initial_ugraph ~aliases ~string_context_of_context - ~universe ~lookup_in_library ~mk_implicit ~description_of_alias - ~fix_instance - ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:Disambiguate.domain_of_term - ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice) - ~refine_thing:refine_term (text,prefix_len,term) - ~mk_localization_tbl - ~expty - ~freshen_thing:CicNotationUtil.freshen_term - ~passes:(MultiPassDisambiguator.passes ()) - -let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice - ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) -= - let mk_localization_tbl x = Cic.CicHash.create x in - MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri ~string_context_of_context - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) - ~domain_of_thing:Disambiguate.domain_of_obj - ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance - ~initial_ugraph:CicUniv.empty_ugraph - ~interpretate_thing:(interpretate_obj ~mk_choice) - ~refine_thing:refine_obj - ~mk_localization_tbl - ~expty:None - ~passes:(MultiPassDisambiguator.passes ()) - ~freshen_thing:CicNotationUtil.freshen_obj - (text,prefix_len,obj) diff --git a/matita/components/cic_disambiguation/cicDisambiguate.mli b/matita/components/cic_disambiguation/cicDisambiguate.mli deleted file mode 100644 index 52919dfa1..000000000 --- a/matita/components/cic_disambiguation/cicDisambiguate.mli +++ /dev/null @@ -1,74 +0,0 @@ -(* - * -Copyright (C) 1999-2006, 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 this program; if not, write to the Free Software -Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA -02110-1301 USA. - -For details, see the HELM web site: http://helm.cs.unibo.it/ -*) - -val interpretate_path : - context:Cic.name list -> CicNotationPt.term -> Cic.term - -val disambiguate_term : - context:Cic.context -> - metasenv:Cic.metasenv -> - subst:Cic.substitution -> - expty:Cic.term option -> - ?initial_ugraph:CicUniv.universe_graph -> - mk_implicit:(bool -> 'alias) -> - description_of_alias:('alias -> string) -> - fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> - aliases:'alias DisambiguateTypes.Environment.t -> - universe:'alias list DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'alias list) -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * 'alias) list * - Cic.metasenv * - Cic.substitution * - Cic.term* - CicUniv.universe_graph) list * - bool - -val disambiguate_obj : - mk_implicit:(bool -> 'alias) -> - description_of_alias:('alias -> string) -> - fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) -> - mk_choice:('alias -> Cic.term DisambiguateTypes.codomain_item) -> - aliases:'alias DisambiguateTypes.Environment.t -> - universe:'alias list DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'alias list) -> - uri:UriManager.uri option -> (* required only for inductive types *) - CicNotationPt.term CicNotationPt.obj Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * 'alias) list * - Cic.metasenv * - Cic.substitution * - Cic.obj * - CicUniv.universe_graph) list * - bool diff --git a/matita/components/cic_disambiguation/doc/precedence.txt b/matita/components/cic_disambiguation/doc/precedence.txt deleted file mode 100644 index 09efea853..000000000 --- a/matita/components/cic_disambiguation/doc/precedence.txt +++ /dev/null @@ -1,32 +0,0 @@ - -Input Should be parsed as Derived constraint - on precedence --------------------------------------------------------------------------------- -\lambda x.x y \lambda x.(x y) lambda > apply -S x = y (= (S x) y) apply > infix operators -\forall x.x=x (\forall x.(= x x)) infix operators > binders -\lambda x.x \to x \lambda. (x \to x) \to > \lambda --------------------------------------------------------------------------------- - -Precedence total order: - - apply > infix operators > to > binders - -where binders are all binders except lambda (i.e. \forall, \pi, \exists) - -to test: - -./test_parser term << EOT - \lambda x.x y - S x = y - \forall x.x=x - \lambda x.x \to x -EOT - -should respond with: - - \lambda x.(x y) - (eq (S x) y) - \forall x.(eq x x) - \lambda x.(x \to x) - diff --git a/matita/components/cic_disambiguation/number_notation.ml b/matita/components/cic_disambiguation/number_notation.ml deleted file mode 100644 index c41a9aab0..000000000 --- a/matita/components/cic_disambiguation/number_notation.ml +++ /dev/null @@ -1,78 +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 -module Obj = LibraryObjects -module DT = DisambiguateTypes - -let error msg = - raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg))) - -let build_nat o s str = - let n = int_of_string str in - if n < 0 then error (str ^ " is not a valid natural number number") else - let rec aux n = if n = 0 then o () else s (aux (pred n)) in - aux n - -let interp_natural_number num = - let nat_URI = match Obj.nat_URI () with - | Some uri -> uri - | None -> error "no default natural numbers" - in - let o () = C.MutConstruct (nat_URI,0,1,[]) in - let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in - build_nat o s num - -let _ = - DisambiguateChoices.add_num_choice - ("natural number", `Num_interp interp_natural_number); - DisambiguateChoices.add_num_choice - ("Coq natural number", - `Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num))); - DisambiguateChoices.add_num_choice - ("real number", - `Num_interp (fun num -> HelmLibraryObjects.build_real (int_of_string num))); - DisambiguateChoices.add_num_choice - ("binary positive number", - `Num_interp (fun num -> - let num = int_of_string num in - if num = 0 then - error "0 is not a valid positive number" - else - HelmLibraryObjects.build_bin_pos num)); - DisambiguateChoices.add_num_choice - ("binary integer number", - `Num_interp (fun num -> - let num = int_of_string num in - if num = 0 then - HelmLibraryObjects.BinInt.z0 - else if num > 0 then - Cic.Appl [ - HelmLibraryObjects.BinInt.zpos; - HelmLibraryObjects.build_bin_pos num ] - else - assert false)) diff --git a/matita/components/cic_disambiguation/tests/aliases.txt b/matita/components/cic_disambiguation/tests/aliases.txt deleted file mode 100644 index 12b09fff1..000000000 --- a/matita/components/cic_disambiguation/tests/aliases.txt +++ /dev/null @@ -1,6 +0,0 @@ -alias id foo = cic:/a.con -alias id bar = cic:/b.con -alias symbol "plus" (instance 0) = "real plus" -alias symbol "plus" (instance 1) = "natural plus" -alias num (instance 0) = "real number" -alias num (instance 1) = "natural number" diff --git a/matita/components/cic_disambiguation/tests/eq.txt b/matita/components/cic_disambiguation/tests/eq.txt deleted file mode 100644 index 6a826fc71..000000000 --- a/matita/components/cic_disambiguation/tests/eq.txt +++ /dev/null @@ -1 +0,0 @@ -\forall n. \forall m. n + m = n diff --git a/matita/components/cic_disambiguation/tests/match.txt b/matita/components/cic_disambiguation/tests/match.txt deleted file mode 100644 index 87bb0159b..000000000 --- a/matita/components/cic_disambiguation/tests/match.txt +++ /dev/null @@ -1,49 +0,0 @@ -[\lambda x:nat. - [\lambda y:nat. Set] - match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]] -match (S O):nat with -[ O \Rightarrow O -| (S x) \Rightarrow false ] - -[\lambda z:nat. \lambda h:(le O z). (eq nat O O)] -match (le_n O): le with -[ le_n \Rightarrow (refl_equal nat O) -| (le_S x y) \Rightarrow (refl_equal nat O) ] - -[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))] -match (le_n (plus (plus O O) (plus O O))): le with -[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) -| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ] - -(* -[\lambda z:nat. \lambda h:(le 1 z). (le 0 z)] -match (le_S 2 (le_n 1)): le with -[ le_n \Rightarrow (le_S 1 (le_n 0)) -| (le_S x y) \Rightarrow y ] -*) - -[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))] -match (le_S 0 0 (le_n 0)): le with -[ le_n \Rightarrow (le_S 0 0 (le_n 0)) -| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ] - - -[\lambda x:bool. nat] -match true:bool with -[ true \Rightarrow O -| false \Rightarrow (S O) ] - -[\lambda x:nat. nat] -match O:nat with -[ O \Rightarrow O -| (S x) \Rightarrow (S (S x)) ] - -[\lambda x:list. list] -match nil:list with -[ nil \Rightarrow nil -| (cons x y) \Rightarrow (cons x y) ] - -\lambda x:False. - [\lambda h:False. True] - match x:False with [] - diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 976b25b55..ee030a215 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -1231,68 +1231,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status, `Old [] (*CSC: TO BE FIXED *) | GrafiteAst.Set (loc, name, value) -> status, `Old [] (* GrafiteTypes.set_option status name value,[] *) - | GrafiteAst.Obj (loc,obj) -> - let ext,name = - match obj with - Cic.Constant (name,_,_,_,_) - | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name - | Cic.InductiveDefinition (types,_,_,_) -> - ".ind", - (match types with (name,_,_,_)::_ -> name | _ -> assert false) - | _ -> assert false in - let buri = status#baseuri in - let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in - let obj = CicRefine.pack_coercion_obj obj in - let metasenv = GrafiteTypes.get_proof_metasenv status in - match obj with - | Cic.CurrentProof (_,metasenv',bo,ty,_, attrs) -> - let name = UriManager.name_of_uri uri in - if not(CicPp.check name ty) then - HLog.warn ("Bad name: " ^ name); - if opts.do_heavy_checks then - begin - let dbd = LibraryDb.instance () in - let similar = Whelp.match_term ~dbd ty in - let similar_len = List.length similar in - if similar_len> 30 then - (HLog.message - ("Duplicate check will compare your theorem with " ^ - string_of_int similar_len ^ - " theorems, this may take a while.")); - let convertible = - List.filter ( - fun u -> - let t = CicUtil.term_of_uri u in - let ty',g = - CicTypeChecker.type_of_aux' - metasenv' [] t CicUniv.oblivion_ugraph - in - fst(CicReduction.are_convertible [] ty' ty g)) - similar - in - (match convertible with - | [] -> () - | x::_ -> - HLog.warn - ("Theorem already proved: " ^ UriManager.string_of_uri x ^ - "\nPlease use a variant.")); - end; - let _subst = [] in - let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in - let initial_stack = Continuationals.Stack.of_metasenv metasenv' in - status#set_proof_status - (GrafiteTypes.Incomplete_proof - { GrafiteTypes.proof = initial_proof; stack = initial_stack }), - `Old [] - | _ -> - if metasenv <> [] then - raise (GrafiteTypes.Command_error ( - "metasenv not empty while giving a definition with body: " ^ - CicMetaSubst.ppmetasenv [] metasenv)); - let status, lemmas = add_obj uri obj status in - let status,new_lemmas = add_coercions_of_lemmas lemmas status in - status#set_proof_status GrafiteTypes.No_proof, - `Old (uri::new_lemmas@lemmas) + | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false in match status#proof_status with GrafiteTypes.Intermediate _ -> diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index cfb85d239..eb9f33f51 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -48,21 +48,6 @@ let singleton msg = function let __Implicit = "__Implicit__" let __Closed_Implicit = "__Closed_Implicit__" -let cic_mk_choice = function - | LexiconAst.Symbol_alias (name, _, dsc) -> - if name = __Implicit then - dsc, `Sym_interp (fun _ -> Cic.Implicit None) - else if name = __Closed_Implicit then - dsc, `Sym_interp (fun _ -> Cic.Implicit (Some `Closed)) - else - DisambiguateChoices.cic_lookup_symbol_by_dsc name dsc - | LexiconAst.Number_alias (_, dsc) -> - DisambiguateChoices.lookup_num_by_dsc dsc - | LexiconAst.Ident_alias (name, uri) -> - uri, `Sym_interp - (fun l->assert(l = []);CicUtil.term_of_uri (UriManager.uri_of_string uri)) -;; - let ncic_mk_choice = function | LexiconAst.Symbol_alias (name, _, dsc) -> if name = __Implicit then @@ -76,23 +61,13 @@ let ncic_mk_choice = function | false -> NCic.Implicit `Term) ~mk_appl:(function (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l) - ~term_of_uri:(fun uri -> - fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri))) + ~term_of_uri:(fun _ -> assert false) ~term_of_nref:(fun nref -> NCic.Const nref) name dsc | LexiconAst.Number_alias (_, dsc) -> - (try - let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in - desc, `Num_interp - (fun num -> match f with `Num_interp f -> f num | _ -> assert false) - with - DisambiguateChoices.Choice_not_found _ -> - let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in - desc, `Num_interp - (fun num -> - fst (OCic2NCic.convert_term - (UriManager.uri_of_string "cic:/xxx/x.con") - (match f with `Num_interp f -> f num | _ -> assert false)))) + let desc,f = DisambiguateChoices.nlookup_num_by_dsc dsc in + desc, `Num_interp + (fun num -> match f with `Num_interp f -> f num | _ -> assert false) | LexiconAst.Ident_alias (name, uri) -> uri, `Sym_interp (fun l->assert(l = []); @@ -114,56 +89,6 @@ let mk_implicit b = LexiconAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit") ;; -let lookup_in_library - interactive_user_uri_choice input_or_locate_uri item -= - let mk_ident_alias id u = - LexiconAst.Ident_alias (id,UriManager.string_of_uri u) - in - let mk_num_alias instance = - List.map - (fun dsc,_ -> LexiconAst.Number_alias (instance,dsc)) - (DisambiguateChoices.lookup_num_choices()) - in - let mk_symbol_alias symb ino (dsc, _,_) = - LexiconAst.Symbol_alias (symb,ino,dsc) - in - let dbd = LibraryDb.instance () in - let choices_of_id id = - let uris = Whelp.locate ~dbd id in - match uris with - | [] -> - (match - (input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") - ?id:(Some id) ()) - with - | None -> [] - | Some uri -> [uri]) - | [uri] -> [uri] - | _ -> - interactive_user_uri_choice ~selection_mode:`MULTIPLE - ?ok:(Some "Try selected.") - ?enable_button_for_non_vars:(Some true) - ~title:"Ambiguous input." - ~msg: ("Ambiguous input \"" ^ id ^ - "\". Please, choose one or more interpretations:") - ~id - uris - in - match item with - | DisambiguateTypes.Id id -> - let uris = choices_of_id id in - List.map (mk_ident_alias id) uris - | DisambiguateTypes.Symbol (symb, ino) -> - (try - List.map (mk_symbol_alias symb ino) - (TermAcicContent.lookup_interpretations symb) - with - TermAcicContent.Interpretation_not_found -> []) - | DisambiguateTypes.Num instance -> mk_num_alias instance -;; - let nlookup_in_library interactive_user_uri_choice input_or_locate_uri item = @@ -173,12 +98,10 @@ let nlookup_in_library let references = NCicLibrary.resolve id in List.map (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u) - ) references @ - lookup_in_library interactive_user_uri_choice input_or_locate_uri item + ) references with - NCicEnvironment.ObjectNotFound _ -> - lookup_in_library interactive_user_uri_choice input_or_locate_uri item) - | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item + NCicEnvironment.ObjectNotFound _ -> []) + | _ -> [] ;; let fix_instance item l = @@ -199,26 +122,6 @@ let fix_instance item l = ;; - (** @param term not meaningful when context is given *) -let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv -term = - let lexicon_status = !lexicon_status_ref in - let (diff, metasenv, subst, cic, _) = - singleton "first" - (CicDisambiguate.disambiguate_term - ~aliases:lexicon_status#lstatus.LexiconEngine.aliases - ~expty ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) - ~lookup_in_library - ~mk_choice:cic_mk_choice - ~mk_implicit ~fix_instance - ~description_of_alias:LexiconAst.description_of_alias - ~context ~metasenv ~subst:[] (text,prefix_len,term)) - in - let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - lexicon_status_ref := lexicon_status; - metasenv,(*subst,*) cic -;; - let disambiguate_nterm expty estatus context metasenv subst thing = let diff, metasenv, subst, cic = @@ -239,48 +142,6 @@ let disambiguate_nterm expty estatus context metasenv subst thing ;; - (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term - * rationale: lazy_term will be invoked in different context to obtain a term, - * each invocation will disambiguate the term and can add aliases. Once all - * disambiguations have been performed, the first returned function can be - * used to obtain the resulting aliases *) -let disambiguate_lazy_term expty text prefix_len lexicon_status_ref term = - (fun context metasenv ugraph -> - let lexicon_status = !lexicon_status_ref in - let (diff, metasenv, _, cic, ugraph) = - singleton "second" - (CicDisambiguate.disambiguate_term - ~lookup_in_library - ~mk_choice:cic_mk_choice - ~mk_implicit ~fix_instance - ~description_of_alias:LexiconAst.description_of_alias - ~initial_ugraph:ugraph ~aliases:lexicon_status#lstatus.LexiconEngine.aliases - ~universe:(Some lexicon_status#lstatus.LexiconEngine.multi_aliases) - ~context ~metasenv ~subst:[] - (text,prefix_len,term) ~expty) in - let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in - lexicon_status_ref := lexicon_status; - cic, metasenv, ugraph) -;; - -let disambiguate_pattern - text prefix_len lexicon_status_ref (wanted, hyp_paths, goal_path) -= - let interp path =CicDisambiguate.interpretate_path [] path in - let goal_path = HExtlib.map_option interp goal_path in - let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - let wanted = - match wanted with - None -> None - | Some wanted -> - let wanted = - disambiguate_lazy_term None text prefix_len lexicon_status_ref wanted - in - Some wanted - in - (wanted, hyp_paths, goal_path) -;; - type pattern = CicNotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option @@ -296,10 +157,7 @@ let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = ;; let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function - | `Unfold (Some t) -> - let t = - disambiguate_lazy_term None text prefix_len lexicon_status_ref t in - `Unfold (Some t) + | `Unfold (Some t) -> assert false (* MATITA 1.0 *) | `Normalize | `Simpl | `Unfold None @@ -333,461 +191,6 @@ let disambiguate_just disambiguate_term context metasenv = metasenv, `Auto params ;; -let rec disambiguate_tactic - lexicon_status_ref context metasenv goal (text,prefix_len,tactic) -= - let disambiguate_term_hint = - let _,_,expty = - List.find (fun (x,_,_) -> Some x = goal) metasenv - in - disambiguate_term (Some expty) text prefix_len lexicon_status_ref in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref in - let disambiguate_pattern = - disambiguate_pattern text prefix_len lexicon_status_ref in - let disambiguate_reduction_kind = - disambiguate_reduction_kind text prefix_len lexicon_status_ref in - let disambiguate_lazy_term = - disambiguate_lazy_term None text prefix_len lexicon_status_ref in - let disambiguate_tactic metasenv tac = - disambiguate_tactic lexicon_status_ref context metasenv goal (text,prefix_len,tac) - in - let disambiguate_auto_params m p = - disambiguate_auto_params disambiguate_term m context p - in - match tactic with - (* Higher order tactics *) - | GrafiteAst.Progress (loc,tac) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,GrafiteAst.Progress (loc,tac) - | GrafiteAst.Solve (loc,tacl) -> - let metasenv,tacl = - List.fold_right - (fun tac (metasenv,tacl) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,tac::tacl - ) tacl (metasenv,[]) - in - metasenv,GrafiteAst.Solve (loc,tacl) - | GrafiteAst.Try (loc,tac) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,GrafiteAst.Try (loc,tac) - | GrafiteAst.First (loc,tacl) -> - let metasenv,tacl = - List.fold_right - (fun tac (metasenv,tacl) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,tac::tacl - ) tacl (metasenv,[]) - in - metasenv,GrafiteAst.First (loc,tacl) - | GrafiteAst.Seq (loc,tacl) -> - let metasenv,tacl = - List.fold_right - (fun tac (metasenv,tacl) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,tac::tacl - ) tacl (metasenv,[]) - in - metasenv,GrafiteAst.Seq (loc,tacl) - | GrafiteAst.Repeat (loc,tac) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,GrafiteAst.Repeat (loc,tac) - | GrafiteAst.Do (loc,n,tac) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,GrafiteAst.Do (loc,n,tac) - | GrafiteAst.Then (loc,tac,tacl) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - let metasenv,tacl = - List.fold_right - (fun tac (metasenv,tacl) -> - let metasenv,tac = disambiguate_tactic metasenv tac in - metasenv,tac::tacl - ) tacl (metasenv,[]) - in - metasenv,GrafiteAst.Then (loc,tac,tacl) - (* First order tactics *) - | GrafiteAst.Absurd (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Absurd (loc, cic) - | GrafiteAst.Apply (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Apply (loc, cic) - | GrafiteAst.ApplyRule (loc, term) -> - let metasenv,cic = disambiguate_term_hint context metasenv term in - metasenv,GrafiteAst.ApplyRule (loc, cic) - | GrafiteAst.ApplyP (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.ApplyP (loc, cic) - | GrafiteAst.ApplyS (loc, term, params) -> - let metasenv, params = disambiguate_auto_params metasenv params in - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.ApplyS (loc, cic, params) - | GrafiteAst.Assumption loc -> - metasenv,GrafiteAst.Assumption loc - | GrafiteAst.AutoBatch (loc,params) -> - let metasenv, params = disambiguate_auto_params metasenv params in - metasenv,GrafiteAst.AutoBatch (loc,params) - | GrafiteAst.Cases (loc, what, pattern, idents) -> - let metasenv,what = disambiguate_term context metasenv what in - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Cases (loc, what, pattern, idents) - | GrafiteAst.Change (loc, pattern, with_what) -> - let with_what = disambiguate_lazy_term with_what in - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Change (loc, pattern, with_what) - | GrafiteAst.Clear (loc,id) -> - metasenv,GrafiteAst.Clear (loc,id) - | GrafiteAst.ClearBody (loc,id) -> - metasenv,GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compose (loc, t1, t2, times, spec) -> - let metasenv,t1 = disambiguate_term context metasenv t1 in - let metasenv,t2 = - match t2 with - | None -> metasenv, None - | Some t2 -> - let m, t2 = disambiguate_term context metasenv t2 in - m, Some t2 - in - metasenv, GrafiteAst.Compose (loc, t1, t2, times, spec) - | GrafiteAst.Constructor (loc,n) -> - metasenv,GrafiteAst.Constructor (loc,n) - | GrafiteAst.Contradiction loc -> - metasenv,GrafiteAst.Contradiction loc - | GrafiteAst.Cut (loc, ident, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.Decompose (loc, names) -> - metasenv,GrafiteAst.Decompose (loc, names) - | GrafiteAst.Demodulate (loc, params) -> - let metasenv, params = disambiguate_auto_params metasenv params in - metasenv,GrafiteAst.Demodulate (loc, params) - | GrafiteAst.Destruct (loc, Some terms) -> - let map term (metasenv, terms) = - let metasenv, term = disambiguate_term context metasenv term in - metasenv, term :: terms - in - let metasenv, terms = List.fold_right map terms (metasenv, []) in - metasenv, GrafiteAst.Destruct(loc, Some terms) - | GrafiteAst.Destruct (loc, None) -> - metasenv,GrafiteAst.Destruct(loc,None) - | GrafiteAst.Exact (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Exact (loc, cic) - | GrafiteAst.Elim (loc, what, Some using, pattern, specs) -> - let metasenv,what = disambiguate_term context metasenv what in - let metasenv,using = disambiguate_term context metasenv using in - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs) - | GrafiteAst.Elim (loc, what, None, pattern, specs) -> - let metasenv,what = disambiguate_term context metasenv what in - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs) - | GrafiteAst.ElimType (loc, what, Some using, specs) -> - let metasenv,what = disambiguate_term context metasenv what in - let metasenv,using = disambiguate_term context metasenv using in - metasenv,GrafiteAst.ElimType (loc, what, Some using, specs) - | GrafiteAst.ElimType (loc, what, None, specs) -> - let metasenv,what = disambiguate_term context metasenv what in - metasenv,GrafiteAst.ElimType (loc, what, None, specs) - | GrafiteAst.Exists loc -> - metasenv,GrafiteAst.Exists loc - | GrafiteAst.Fail loc -> - metasenv,GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,red_kind, term, pattern) -> - let pattern = disambiguate_pattern pattern in - let term = disambiguate_lazy_term term in - let red_kind = disambiguate_reduction_kind red_kind in - metasenv,GrafiteAst.Fold (loc, red_kind, term, pattern) - | GrafiteAst.FwdSimpl (loc, hyp, names) -> - metasenv,GrafiteAst.FwdSimpl (loc, hyp, names) - | GrafiteAst.Fourier loc -> - metasenv,GrafiteAst.Fourier loc - | GrafiteAst.Generalize (loc,pattern,ident) -> - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Generalize (loc,pattern,ident) - | GrafiteAst.IdTac loc -> - metasenv,GrafiteAst.IdTac loc - | GrafiteAst.Intros (loc, specs) -> - metasenv,GrafiteAst.Intros (loc, specs) - | GrafiteAst.Inversion (loc, term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Inversion (loc, term) - | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) -> - let f term (metasenv, to_what) = - let metasenv, term = disambiguate_term context metasenv term in - metasenv, term :: to_what - in - let metasenv, to_what = List.fold_right f to_what (metasenv, []) in - let metasenv, what = disambiguate_term context metasenv what in - metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) - | GrafiteAst.Left loc -> - metasenv,GrafiteAst.Left loc - | GrafiteAst.LetIn (loc, term, name) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, red_kind, pattern) -> - let pattern = disambiguate_pattern pattern in - let red_kind = disambiguate_reduction_kind red_kind in - metasenv,GrafiteAst.Reduce(loc, red_kind, pattern) - | GrafiteAst.Reflexivity loc -> - metasenv,GrafiteAst.Reflexivity loc - | GrafiteAst.Replace (loc, pattern, with_what) -> - let pattern = disambiguate_pattern pattern in - let with_what = disambiguate_lazy_term with_what in - metasenv,GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern, names) -> - let metasenv,term = disambiguate_term context metasenv t in - let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names) - | GrafiteAst.Right loc -> - metasenv,GrafiteAst.Right loc - | GrafiteAst.Ring loc -> - metasenv,GrafiteAst.Ring loc - | GrafiteAst.Split loc -> - metasenv,GrafiteAst.Split loc - | GrafiteAst.Symmetry loc -> - metasenv,GrafiteAst.Symmetry loc - | GrafiteAst.Transitivity (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Transitivity (loc, cic) - (* Nuovi casi *) - | GrafiteAst.Assume (loc, id, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Assume (loc, id, cic) - | GrafiteAst.Suppose (loc, term, id, term') -> - let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = - match term' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.Suppose (loc, cic, id, cic') - | GrafiteAst.Bydone (loc,just) -> - let metasenv,just = - disambiguate_just disambiguate_term context metasenv just - in - metasenv,GrafiteAst.Bydone (loc, just) - | GrafiteAst.We_need_to_prove (loc,term,id,term') -> - let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = - match term' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic') - | GrafiteAst.By_just_we_proved (loc,just,term',id,term'') -> - let metasenv,just = - disambiguate_just disambiguate_term context metasenv just in - let metasenv,cic' = disambiguate_term context metasenv term' in - let metasenv,cic'' = - match term'' with - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in - metasenv,GrafiteAst.By_just_we_proved (loc,just,cic',id,cic'') - | GrafiteAst.We_proceed_by_cases_on (loc, term, term') -> - let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = disambiguate_term context metasenv term' in - metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic') - | GrafiteAst.We_proceed_by_induction_on (loc, term, term') -> - let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = disambiguate_term context metasenv term' in - metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic') - | GrafiteAst.Byinduction (loc, term, id) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Byinduction(loc, cic, id) - | GrafiteAst.Thesisbecomes (loc, term) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Thesisbecomes (loc, cic) - | GrafiteAst.ExistsElim (loc, just, id1, term1, id2, term2) -> - let metasenv,just = - disambiguate_just disambiguate_term context metasenv just in - let metasenv,cic' = disambiguate_term context metasenv term1 in - let cic''= disambiguate_lazy_term term2 in - metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'') - | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) -> - let metasenv,just = - disambiguate_just disambiguate_term context metasenv just in - let metasenv,cic'= disambiguate_term context metasenv term1 in - let metasenv,cic''= disambiguate_term context metasenv term2 in - metasenv,GrafiteAst.AndElim(loc, just, id, cic', id1, cic'') - | GrafiteAst.Case (loc, id, params) -> - let metasenv,params' = - List.fold_right - (fun (id,term) (metasenv,params) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,(id,cic)::params - ) params (metasenv,[]) - in - metasenv,GrafiteAst.Case(loc, id, params') - | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) -> - let metasenv,cic = - match term1 with - None -> metasenv,None - | Some (start,t) -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some (start,t) in - let metasenv,cic'= disambiguate_term context metasenv term2 in - let metasenv,cic'' = - match term3 with - | `SolveWith term -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv, `SolveWith term - | `Auto params -> - let metasenv, params = disambiguate_auto_params metasenv params in - metasenv,`Auto params - | `Term t -> - let metasenv,t = disambiguate_term context metasenv t in - metasenv,`Term t - | `Proof as t -> metasenv,t in - metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) - -let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = - let uri = - let baseuri = - match baseuri with Some x -> x | None -> raise BaseUriNotSetYet - in - let name = - match obj with - | CicNotationPt.Inductive (_,(name,_,_,_)::_) - | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" - | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" - | CicNotationPt.Inductive _ -> assert false - in - UriManager.uri_of_string (baseuri ^ "/" ^ name) - in -(* - let _try_new cic = - (NCicLibrary.clear_cache (); - NCicEnvironment.invalidate (); - OCic2NCic.clear (); - let graph = - match cic with - | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) -> - let _, ugraph = - CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph - in - ugraph - | Some (Cic.Constant (_,_, ty,_,_)) -> - let _, ugraph = - CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph - in - ugraph - | _ -> CicUniv.empty_ugraph - in - -(* - prerr_endline "PRIMA COERCIONS"; - let _,l = CicUniv.do_rank graph in - List.iter (fun k -> - prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int - (CicUniv.get_rank k))) l; -*) - - let graph = - List.fold_left - (fun graph (_,_,l) -> - List.fold_left - (fun graph (uri,_,_) -> - let _,g = CicTypeChecker.typecheck uri in - CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri)) - graph l) - graph (CoercDb.to_list (CoercDb.dump ())) - in - ignore(CicUniv.do_rank graph); - - -(* - prerr_endline "DOPO COERCIONS"; - let _,l = CicUniv.do_rank graph in - List.iter (fun k -> - prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int - (CicUniv.get_rank k))) l; -*) - - - prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE"; - let time = Unix.gettimeofday () in - (try - (match - NCicDisambiguate.disambiguate_obj - ~rdb:estatus - ~lookup_in_library:nlookup_in_library - ~description_of_alias:LexiconAst.description_of_alias - ~mk_choice:ncic_mk_choice - ~mk_implicit - ~uri:(OCic2NCic.nuri_of_ouri uri) - ~aliases:estatus#lstatus.LexiconEngine.aliases - ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) - (text,prefix_len,obj) - with - | [_,_,_,obj],_ -> - let time = Unix.gettimeofday () -. time in -(* NCicTypeChecker.typecheck_obj obj; *) - prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time); -(* - let obj = - let u,i,m,_,o = obj in - u,i,m,[],o - in -*) - prerr_endline (NCicPp.ppobj obj) - | _ -> - prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! ")) - with - | MultiPassDisambiguator.DisambiguationError (_,s) -> - prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE (" - ^UriManager.string_of_uri uri^ - "):\n" ^ - String.concat "\n" - (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s))) -(* | exn -> prerr_endline (Printexc.to_string exn) *) - ) - ) - in -*) - - - try -(* let time = Unix.gettimeofday () in *) - - - let (diff, metasenv, _, cic, _) = - singleton "third" - (CicDisambiguate.disambiguate_obj - ~lookup_in_library - ~mk_choice:cic_mk_choice - ~mk_implicit ~fix_instance - ~description_of_alias:LexiconAst.description_of_alias - ~aliases:estatus#lstatus.LexiconEngine.aliases - ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases) - ~uri:(Some uri) - (text,prefix_len,obj)) - in - - -(* - let time = Unix.gettimeofday () -. time in - prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^ - UriManager.string_of_uri uri ^"): " ^ string_of_float time); -*) -(* try_new (Some cic); *) - - - let estatus = LexiconEngine.set_proof_aliases estatus diff in - estatus, metasenv, cic - - with - | Sys.Break as exn -> raise exn - | exn -> -(* try_new None; *) - raise exn -;; - let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = let uri = let baseuri = @@ -817,44 +220,16 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = let estatus = LexiconEngine.set_proof_aliases estatus diff in estatus, cic ;; - let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= match cmd with - | GrafiteAst.Index(loc,key,uri) -> - let lexicon_status_ref = ref estatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let disambiguate_term_option metasenv = - function - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term metasenv t in - metasenv, Some t - in - let metasenv,key = disambiguate_term_option metasenv key in - !lexicon_status_ref,metasenv,GrafiteAst.Index(loc,key,uri) + | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false | GrafiteAst.Select (loc,uri) -> estatus, metasenv, GrafiteAst.Select(loc,uri) | GrafiteAst.Pump(loc,i) -> estatus, metasenv, GrafiteAst.Pump(loc,i) - | GrafiteAst.PreferCoercion (loc,t) -> - let lexicon_status_ref = ref estatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.PreferCoercion (loc,t) - | GrafiteAst.Coercion (loc,t,b,a,s) -> - let lexicon_status_ref = ref estatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let metasenv,t = disambiguate_term metasenv t in - !lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s) - | GrafiteAst.Inverter (loc,n,indty,params) -> - let lexicon_status_ref = ref estatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let metasenv,indty = disambiguate_term metasenv indty in - !lexicon_status_ref, metasenv, GrafiteAst.Inverter (loc,n,indty,params) + | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false + | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false + | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ @@ -862,47 +237,5 @@ let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)= | GrafiteAst.Qed _ | GrafiteAst.Set _ as cmd -> estatus,metasenv,cmd - | GrafiteAst.Obj (loc,obj) -> - let estatus,metasenv,obj = - disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj)in - estatus, metasenv, GrafiteAst.Obj (loc,obj) - | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> - let lexicon_status_ref = ref estatus in - let disambiguate_term = - disambiguate_term None text prefix_len lexicon_status_ref [] in - let disambiguate_term_option metasenv = - function - None -> metasenv,None - | Some t -> - let metasenv,t = disambiguate_term metasenv t in - metasenv, Some t - in - let metasenv,a = disambiguate_term metasenv a in - let metasenv,aeq = disambiguate_term metasenv aeq in - let metasenv,refl = disambiguate_term_option metasenv refl in - let metasenv,sym = disambiguate_term_option metasenv sym in - let metasenv,trans = disambiguate_term_option metasenv trans in - !lexicon_status_ref, metasenv, - GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) - -let disambiguate_macro - lexicon_status_ref metasenv context (text,prefix_len, macro) -= - let disambiguate_term = disambiguate_term None text prefix_len lexicon_status_ref in - let disambiguate_reduction_kind = - disambiguate_reduction_kind text prefix_len lexicon_status_ref in - match macro with - | GrafiteAst.Check (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Check (loc,term) - | GrafiteAst.Eval (loc,kind,term) -> - let metasenv, term = disambiguate_term context metasenv term in - let kind = disambiguate_reduction_kind kind in - metasenv,GrafiteAst.Eval (loc,kind,term) - | GrafiteAst.AutoInteractive (loc, params) -> - let metasenv, params = - disambiguate_auto_params disambiguate_term metasenv context params in - metasenv, GrafiteAst.AutoInteractive (loc, params) - | GrafiteAst.Hint _ - | GrafiteAst.Inline _ as macro -> - metasenv,macro + | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false + | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 6565a4d9f..e17769ec9 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -34,13 +34,6 @@ type lazy_tactic = (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic -val disambiguate_tactic: - LexiconEngine.status ref -> - Cic.context -> - Cic.metasenv -> int option -> - tactic Disambiguate.disambiguator_input -> - Cic.metasenv * lazy_tactic - val disambiguate_command: LexiconEngine.status as 'status -> ?baseuri:string -> @@ -48,13 +41,6 @@ val disambiguate_command: ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> 'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command -val disambiguate_macro: - LexiconEngine.status ref -> - Cic.metasenv -> - Cic.context -> - ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input -> - Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro - val disambiguate_nterm : NCic.term option -> (#NEstatus.status as 'status) -> diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend index f2694c199..3630ffef3 100644 --- a/matita/components/ng_disambiguation/.depend +++ b/matita/components/ng_disambiguation/.depend @@ -1,4 +1,6 @@ nCicDisambiguate.cmi: +disambiguateChoices.cmo: disambiguateChoices.cmi +disambiguateChoices.cmx: disambiguateChoices.cmi nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi nnumber_notation.cmo: diff --git a/matita/components/ng_disambiguation/Makefile b/matita/components/ng_disambiguation/Makefile index 7c747df48..ad6a6de80 100644 --- a/matita/components/ng_disambiguation/Makefile +++ b/matita/components/ng_disambiguation/Makefile @@ -4,6 +4,7 @@ PREDICATES = INTERFACE_FILES = nCicDisambiguate.mli IMPLEMENTATION_FILES = \ + disambiguateChoices.ml \ $(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/matita/components/cic_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml similarity index 100% rename from matita/components/cic_disambiguation/disambiguateChoices.ml rename to matita/components/ng_disambiguation/disambiguateChoices.ml diff --git a/matita/components/cic_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli similarity index 100% rename from matita/components/cic_disambiguation/disambiguateChoices.mli rename to matita/components/ng_disambiguation/disambiguateChoices.mli diff --git a/matita/components/tactics/fwdSimplTactic.ml b/matita/components/tactics/fwdSimplTactic.ml index 10df83c5d..087e4b3f5 100644 --- a/matita/components/tactics/fwdSimplTactic.ml +++ b/matita/components/tactics/fwdSimplTactic.ml @@ -154,6 +154,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub let fwd_simpl_tac ?(mk_fresh_name_callback = FNG.mk_fresh_name ~subst:[]) ~dbd hyp = +assert false (* MATITA 1.0 let lapply_tac to_what lemma = lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma in @@ -171,3 +172,4 @@ let fwd_simpl_tac PET.apply_tactic tac status in PET.mk_tactic fwd_simpl_tac + *) diff --git a/matita/components/whelp/.depend b/matita/components/whelp/.depend deleted file mode 100644 index 65dc07955..000000000 --- a/matita/components/whelp/.depend +++ /dev/null @@ -1,6 +0,0 @@ -whelp.cmi: -fwdQueries.cmi: -whelp.cmo: whelp.cmi -whelp.cmx: whelp.cmi -fwdQueries.cmo: fwdQueries.cmi -fwdQueries.cmx: fwdQueries.cmi diff --git a/matita/components/whelp/.depend.opt b/matita/components/whelp/.depend.opt deleted file mode 100644 index 65dc07955..000000000 --- a/matita/components/whelp/.depend.opt +++ /dev/null @@ -1,6 +0,0 @@ -whelp.cmi: -fwdQueries.cmi: -whelp.cmo: whelp.cmi -whelp.cmx: whelp.cmi -fwdQueries.cmo: fwdQueries.cmi -fwdQueries.cmx: fwdQueries.cmi diff --git a/matita/components/whelp/Makefile b/matita/components/whelp/Makefile deleted file mode 100644 index 6d8d3958f..000000000 --- a/matita/components/whelp/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -PACKAGE = whelp - -INTERFACE_FILES = \ - whelp.mli \ - fwdQueries.mli \ - $(NULL) - -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) - -include ../../Makefile.defs -include ../Makefile.common diff --git a/matita/components/whelp/fwdQueries.ml b/matita/components/whelp/fwdQueries.ml deleted file mode 100644 index 5453c544e..000000000 --- a/matita/components/whelp/fwdQueries.ml +++ /dev/null @@ -1,115 +0,0 @@ -(* Copyright (C) 2005, 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$ *) - -(* fwd_simpl ****************************************************************) - -let rec filter_map_n f n = function - | [] -> [] - | hd :: tl -> - match f n hd with - | None -> filter_map_n f (succ n) tl - | Some hd -> hd :: filter_map_n f (succ n) tl - -let get_uri t = - let aux = function - | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl) - | hd -> Some (CicUtil.uri_of_term hd, []) - in - try aux t with - | Invalid_argument "uri_of_term" -> None - -let get_metadata t = - let f n t = - match get_uri t with - | None -> None - | Some (uri, _) -> Some (n, uri) - in - match get_uri t with - | None -> None - | Some (uri, args) -> Some (uri, filter_map_n f 1 args) - -let debug_metadata = function - | None -> () - | Some (outer, inners) -> - let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in - Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer); - List.iter f inners; prerr_newline () - -let fwd_simpl ~dbd t = - let map inners row = - match row.(0), row.(1), row.(2) with - | Some source, Some inner, Some index -> - source, - List.mem - (int_of_string index, (UriManager.uri_of_string inner)) inners - | _ -> "", false - in - let rec rank ranks (source, ok) = - match ranks, ok with - | [], false -> [source, 0] - | [], true -> [source, 1] - | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl - | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl - | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl - | hd :: tl, _ -> hd :: rank tl (source, ok) - in - let compare (_, x) (_, y) = compare x y in - let filter n (uri, rank) = - if rank > 0 then Some (UriManager.uri_of_string uri) else None - in - let metadata = get_metadata t in debug_metadata metadata; - match metadata with - | None -> [] - | Some (outer, inners) -> - let select = "source, h_inner, h_index" in - let from = "genLemma" in - let where = - Printf.sprintf "h_outer = \"%s\"" - (HSql.escape HSql.Library dbd (UriManager.string_of_uri outer)) in - let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in - let result = HSql.exec HSql.Library dbd query in - let lemmas = HSql.map ~f:(map inners) result in - let ranked = List.fold_left rank [] lemmas in - let ordered = List.rev (List.fast_sort compare ranked) in - filter_map_n filter 0 ordered - -(* get_decomposables ********************************************************) - -let decomposables ~dbd = - let map row = match row.(0) with - | None -> None - | Some str -> - match CicUtil.term_of_uri (UriManager.uri_of_string str) with - | Cic.MutInd (uri, typeno, _) -> Some (uri, Some typeno) - | Cic.Const (uri, _) -> Some (uri, None) - | _ -> - raise (UriManager.IllFormedUri str) - in - let select, from = "source", "decomposables" in - let query = Printf.sprintf "SELECT %s FROM %s" select from in - let decomposables = HSql.map ~f:map (HSql.exec HSql.Library dbd query) in - filter_map_n (fun _ x -> x) 0 decomposables diff --git a/matita/components/whelp/fwdQueries.mli b/matita/components/whelp/fwdQueries.mli deleted file mode 100644 index 3e4936dec..000000000 --- a/matita/components/whelp/fwdQueries.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - -val fwd_simpl: dbd:HSql.dbd -> Cic.term -> UriManager.uri list -val decomposables: dbd:HSql.dbd -> (UriManager.uri * int option) list - diff --git a/matita/components/whelp/whelp.ml b/matita/components/whelp/whelp.ml deleted file mode 100644 index ef544f850..000000000 --- a/matita/components/whelp/whelp.ml +++ /dev/null @@ -1,232 +0,0 @@ -(* Copyright (C) 2005, 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$ *) - -open Printf - -let nonvar uri = not (UriManager.uri_is_var uri) - - (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for - * the "like" operator (which uses '%' and '_'). Does not support escaping. *) -let sqlpat_of_shellglob = - let star_RE, qmark_RE, percent_RE, uscore_RE = - Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" - in - fun shellglob -> - Pcre.replace ~rex:star_RE ~templ:"%" - (Pcre.replace ~rex:qmark_RE ~templ:"_" - (Pcre.replace ~rex:percent_RE ~templ:"\\%" - (Pcre.replace ~rex:uscore_RE ~templ:"\\_" - shellglob))) - -let locate ~(dbd:HSql.dbd) ?(vars = false) pat = - let escape dbtype dbd s = HSql.escape dbtype dbd s in - let sql_pat = sqlpat_of_shellglob pat in - let query dbtype tbl = - sprintf - ("SELECT source FROM %s WHERE value LIKE \"%s\" " - ^^ HSql.escape_string_for_like dbtype dbd) - tbl (escape dbtype dbd sql_pat) - in - let tbls = - [HSql.User, MetadataTypes.name_tbl (); - HSql.Library, MetadataTypes.library_name_tbl; - HSql.Legacy, MetadataTypes.library_name_tbl] - in - let map cols = - match cols.(0) with - | Some s -> UriManager.uri_of_string s | _ -> assert false - in - let result = - List.fold_left - (fun acc (dbtype,tbl) -> - acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl))) - [] tbls - in - List.filter nonvar result - -let match_term ~(dbd:HSql.dbd) ty = -(* debug_print (lazy (CicPp.ppterm ty)); *) - let metadata = MetadataExtractor.compute ~body:None ~ty in - let constants_no = - MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty) - in - let full_card, diff = - if CicUtil.is_meta_closed ty then - Some (MetadataConstraints.Eq constants_no), None - else - let diff_no = - let (hyp_constants, concl_constants) = - (* collect different constants in hypotheses and conclusions *) - List.fold_left - (fun ((hyp, concl) as acc) metadata -> - match (metadata: MetadataTypes.metadata) with - | `Sort _ | `Rel _ -> acc - | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) - when not (List.mem uri concl) -> (hyp, uri :: concl) - | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) - when not (List.mem uri hyp) -> (uri :: hyp, concl) - | `Obj _ -> acc) - ([], []) - metadata - in - List.length hyp_constants - List.length concl_constants - in - let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in - let diff = - if MetadataExtractor.IntSet.equal concl_metas hyp_metas then - Some (MetadataConstraints.Eq diff_no) - else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then - Some (MetadataConstraints.Gt (diff_no - 1)) - else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then - Some (MetadataConstraints.Lt (diff_no + 1)) - else - None - in - None, diff - in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - MetadataConstraints.at_least ~dbd ?full_card ?diff constraints - -let fill_with_dummy_constants t = - let rec aux i types = - function - Cic.Lambda (n,s,t) -> - let dummy_uri = - UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in - (aux (i+1) (s::types) - (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) - | t -> t,types - in - let t,types = aux 0 [] t in - t, List.rev types - -let instance ~dbd t = - let t',types = fill_with_dummy_constants t in - let metadata = MetadataExtractor.compute ~body:None ~ty:t' in -(* List.iter - (fun x -> - debug_print - (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) - metadata; *) - let no_concl = MetadataDb.count_distinct `Conclusion metadata in - let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in - let no_full = MetadataDb.count_distinct `Statement metadata in - let is_dummy = function - | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy" - | _ -> true - in - let rec look_for_dummy_main = function - | [] -> None - | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ - when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> - let s = UriManager.string_of_uri s in - let len = String.length s in - let dummy_index = int_of_string (String.sub s 11 (len-15)) in - let dummy_type = List.nth types dummy_index in - Some (d,dummy_type) - | _::l -> look_for_dummy_main l - in - match (look_for_dummy_main metadata) with - | None-> -(* debug_print (lazy "Caso None"); *) - (* no dummy in main position *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff - constraints - | Some (depth, dummy_type) -> -(* debug_print - (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *) - (* a dummy in main position *) - let metadata_for_dummy_type = - MetadataExtractor.compute ~body:None ~ty:dummy_type in - (* Let us skip this for the moment - let main_of_dummy_type = - look_for_dummy_main metadata_for_dummy_type in *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let metadata_for_dummy_type = - List.filter is_dummy metadata_for_dummy_type in - let metadata_for_dummy_type, depth' = - (* depth' = the depth of the A -> A -> Prop *) - List.fold_left (fun (acc,dep) c -> - match c with - | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type - in - let constraints_for_dummy_type = - List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in - (* start with the dummy constant in main conlusion *) - let from = ["refObj as table0"] in (* XXX table hardcoded *) - let where = - [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; - sprintf "table0.h_depth >= %d" depth] in - let (n,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:2) - (2,from,where) constraints in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - let (n,from,where) = - MetadataConstraints.add_all_constr - (n,from,where) concl_card full_card diff in - (* join with the constraints over the type of the constant *) - let where = - (sprintf "table0.h_occurrence = table%d.source" n)::where in - let where = - sprintf "table0.h_depth - table%d.h_depth = %d" - n (depth - depth')::where - in - (* XXX performed only in library and legacy not user *) - let (m,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:n) - (n,from,where) constraints_for_dummy_type - in - MetadataConstraints.exec HSql.Library ~dbd (m,from,where) - @ - MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where) - -let elim ~dbd uri = - let constraints = - [`Rel [`MainConclusion None]; - `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]); - `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); - `Obj (uri,[`InHypothesis]); - ] - in - MetadataConstraints.at_least ~rating:`Hits ~dbd constraints - diff --git a/matita/components/whelp/whelp.mli b/matita/components/whelp/whelp.mli deleted file mode 100644 index 80c4d6522..000000000 --- a/matita/components/whelp/whelp.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* Copyright (C) 2005, 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/ - *) - -val locate: dbd:HSql.dbd -> ?vars:bool -> string -> UriManager.uri list -val elim: dbd:HSql.dbd -> UriManager.uri -> UriManager.uri list -val instance: dbd:HSql.dbd -> Cic.term -> UriManager.uri list -val match_term: dbd:HSql.dbd -> Cic.term -> UriManager.uri list - diff --git a/matita/configure.ac b/matita/configure.ac index bc655aae3..aa3d1b49a 100644 --- a/matita/configure.ac +++ b/matita/configure.ac @@ -73,7 +73,6 @@ zip \ FINDLIB_COMREQUIRES="\ helm-disambiguation \ -helm-cic_disambiguation \ helm-grafite \ helm-grafite_engine \ helm-tptp_grafite \ diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index c13004c24..c96132b8a 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -30,16 +30,6 @@ module G = GrafiteAst let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; -let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal tac = - let metasenv,tac = - GrafiteDisambiguate.disambiguate_tactic - lexicon_status_ref - (GrafiteTypes.get_proof_context grafite_status goal) - (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal) - tac - in - GrafiteTypes.set_metasenv metasenv grafite_status,tac - let disambiguate_command lexicon_status_ref grafite_status cmd = let baseuri = grafite_status#baseuri in let lexicon_status,metasenv,cmd = @@ -49,15 +39,6 @@ let disambiguate_command lexicon_status_ref grafite_status cmd = lexicon_status_ref := lexicon_status; GrafiteTypes.set_metasenv metasenv grafite_status,cmd -let disambiguate_macro lexicon_status_ref grafite_status macro context = - let metasenv,macro = - GrafiteDisambiguate.disambiguate_macro - lexicon_status_ref - (GrafiteTypes.get_proof_metasenv grafite_status) - context macro - in - GrafiteTypes.set_metasenv metasenv grafite_status,macro - let eval_macro_screenshot (status : GrafiteTypes.status) name = let _,_,metasenv,subst,_ = status#obj in let sequent = List.hd metasenv in @@ -89,9 +70,9 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = status, `Old [] | ast -> GrafiteEngine.eval_ast - ~disambiguate_tactic:(disambiguate_tactic text prefix_len lexicon_status_ref) + ~disambiguate_tactic:((* MATITA 1.0*) fun _ -> assert false) ~disambiguate_command:(disambiguate_command lexicon_status_ref) - ~disambiguate_macro:(disambiguate_macro lexicon_status_ref) + ~disambiguate_macro:((* MATITA 1.0*) fun _ -> assert false) ?do_heavy_checks status (text,prefix_len,ast) in let new_status = -- 2.39.2