-requires="helm-lexicon helm-grafite ulex08 helm-ng_disambiguation helm-ng_library"
+requires="helm-grafite ulex08 helm-ng_disambiguation helm-ng_library helm-content_pres"
version="0.0.1"
archive(byte)="grafite_parser.cma"
archive(native)="grafite_parser.cmxa"
+++ /dev/null
-requires="helm-content_pres helm-ng_library camlp5.gramlib"
-version="0.0.1"
-archive(byte)="lexicon.cma"
-archive(native)="lexicon.cmxa"
-requires="helm-library helm-content helm-ng_refiner"
+requires="helm-library helm-ng_library helm-grafite helm-content helm-ng_refiner"
version="0.0.1"
archive(byte)="ng_cic_content.cma"
archive(native)="ng_cic_content.cmxa"
-requires="helm-ng_refiner helm-ng_cic_content helm-ng_disambiguation helm-ng_paramodulation"
+requires="helm-ng_refiner helm-registry helm-library"
version="0.0.1"
archive(byte)="ng_library.cma"
archive(native)="ng_library.cmxa"
-requires="helm-ng_disambiguation helm-lexicon helm-grafite_parser helm-ng_paramodulation"
+requires="helm-ng_disambiguation helm-grafite_parser helm-ng_paramodulation"
version="0.0.1"
archive(byte)="ng_tactics.cma"
archive(native)="ng_tactics.cmxa"
content \
grafite \
ng_refiner \
+ ng_library \
ng_cic_content \
disambiguation \
ng_disambiguation \
ng_paramodulation \
- ng_library \
content_pres \
- lexicon \
grafite_parser \
ng_tactics \
grafite_engine \
content.cmi:
-notationUtil.cmi:
-notationEnv.cmi:
-notationPp.cmi:
-interpretations.cmi: notationPt.cmx
+notationUtil.cmi: notationPt.cmx
+notationEnv.cmi: notationPt.cmx
+notationPp.cmi: notationPt.cmx notationEnv.cmi
notationPt.cmo:
notationPt.cmx:
content.cmo: content.cmi
notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi
notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
-interpretations.cmo: notationUtil.cmi notationPt.cmx interpretations.cmi
-interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi
cicNotationPres.cmi: mpresentation.cmi box.cmi
-content2pres.cmi: cicNotationPres.cmi
-sequent2pres.cmi: cicNotationPres.cmi
+content2pres.cmi: termContentPres.cmi cicNotationPres.cmi
+sequent2pres.cmi: termContentPres.cmi cicNotationPres.cmi
renderingAttrs.cmo: renderingAttrs.cmi
renderingAttrs.cmx: renderingAttrs.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
trie.cmi:
discrimination_tree.cmi:
hTopoSort.cmi:
-refCounter.cmi:
graphvizPp.cmi:
componentsConf.cmo: componentsConf.cmi
componentsConf.cmx: componentsConf.cmi
discrimination_tree.cmx: trie.cmx discrimination_tree.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
-refCounter.cmo: refCounter.cmi
-refCounter.cmx: refCounter.cmi
graphvizPp.cmo: graphvizPp.cmi
graphvizPp.cmx: graphvizPp.cmi
grafiteAstPp.cmi: grafiteAst.cmx
-grafiteMarshal.cmi: grafiteAst.cmx
grafiteAst.cmo:
grafiteAst.cmx:
grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
-grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi
-grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi
grafiteTypes.cmi:
-grafiteSync.cmi: grafiteTypes.cmi
nCicCoercDeclaration.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
grafiteTypes.cmx: grafiteTypes.cmi
-grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi
-grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi
nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
-grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi grafiteSync.cmi \
+grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \
grafiteEngine.cmi
-grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx grafiteSync.cmx \
+grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \
grafiteEngine.cmi
dependenciesParser.cmi:
grafiteParser.cmi:
-grafiteDisambiguate.cmi:
print_grammar.cmi: grafiteParser.cmi
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
print_grammar.cmo: print_grammar.cmi
print_grammar.cmx: print_grammar.cmi
+++ /dev/null
-grafiteDisambiguate.cmi:
-lexiconSync.cmi: grafiteDisambiguate.cmi
-grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
-lexiconSync.cmo: grafiteDisambiguate.cmi lexiconSync.cmi
-lexiconSync.cmx: grafiteDisambiguate.cmx lexiconSync.cmi
+++ /dev/null
-lexiconAstPp.cmi: lexiconAst.cmx
-lexiconMarshal.cmi: lexiconAst.cmx
-cicNotation.cmi: lexiconAst.cmx
-lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi
-lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx
-lexiconAst.cmo:
-lexiconAst.cmx:
-lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi
-lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
-lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi
-lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi
-cicNotation.cmo: lexiconAst.cmx cicNotation.cmi
-cicNotation.cmx: lexiconAst.cmx cicNotation.cmi
-lexiconEngine.cmo: lexiconMarshal.cmi lexiconAstPp.cmi lexiconAst.cmx \
- cicNotation.cmi lexiconEngine.cmi
-lexiconEngine.cmx: lexiconMarshal.cmx lexiconAstPp.cmx lexiconAst.cmx \
- cicNotation.cmx lexiconEngine.cmi
-lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmx cicNotation.cmi \
- lexiconSync.cmi
-lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \
- lexiconSync.cmi
+++ /dev/null
-PACKAGE = lexicon
-PREDICATES =
-
-INTERFACE_FILES = \
- grafiteDisambiguate.mli \
- $(NULL)
-IMPLEMENTATION_FILES = \
- $(INTERFACE_FILES:%.mli=%.ml)
-
-
-include ../../Makefile.defs
-include ../Makefile.common
+++ /dev/null
-(*
- *
- * 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$ *)
-
-type db = {
- aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
- new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
-}
-
-let initial_status = {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- new_aliases = []
-}
-
-class type g_status =
- object
- inherit Interpretations.g_status
- method disambiguate_db: db
- end
-
-class status =
- object (self)
- inherit Interpretations.status
- val disambiguate_db = initial_status
- method disambiguate_db = disambiguate_db
- method set_disambiguate_db v = {< disambiguate_db = v >}
- method set_disambiguate_status
- : 'status. #g_status as 'status -> 'self
- = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
- end
-
-let eval_with_new_aliases status f =
- let status =
- status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
- new_aliases,res
-;;
-
-let dump_aliases out msg status =
- out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
- DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
- status#disambiguate_db.aliases
-
-let set_proof_aliases status ~implicit_aliases mode new_aliases =
- if mode = GrafiteAst.WithoutPreferences then
- status
- else
- (* MATITA 1.0
- let new_commands =
- List.map
- (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
- in *)
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status#disambiguate_db.aliases new_aliases in
- let multi_aliases =
- List.fold_left (fun acc (d,c) ->
- DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
- d c acc)
- status#disambiguate_db.multi_aliases new_aliases
- in
- let new_status =
- {multi_aliases = multi_aliases ;
- aliases = aliases;
- new_aliases =
- (if implicit_aliases then new_aliases else []) @
- status#disambiguate_db.new_aliases}
- in
- status#set_disambiguate_db new_status
-
-exception BaseUriNotSetYet
-
-let singleton msg = function
- | [x], _ -> x
- | l, _ ->
- let debug =
- Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
- msg (List.length l)
- in
- prerr_endline debug; assert false
-
-let __Implicit = "__Implicit__"
-let __Closed_Implicit = "__Closed_Implicit__"
-
-let ncic_mk_choice status = function
- | GrafiteAst.Symbol_alias (name, _, dsc) ->
- if name = __Implicit then
- dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
- else if name = __Closed_Implicit then
- dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
- else
- DisambiguateChoices.lookup_symbol_by_dsc status
- ~mk_implicit:(function
- | true -> NCic.Implicit `Closed
- | false -> NCic.Implicit `Term)
- ~mk_appl:(function
- (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_nref:(fun nref -> NCic.Const nref)
- name dsc
- | GrafiteAst.Number_alias (_, dsc) ->
- 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)
- | GrafiteAst.Ident_alias (name, uri) ->
- uri, `Sym_interp
- (fun l->assert(l = []);
- let nref = NReference.reference_of_string uri in
- NCic.Const nref)
-;;
-
-
-let mk_implicit b =
- match b with
- | false ->
- GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
- | true ->
- GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
-;;
-
-let nlookup_in_library
- interactive_user_uri_choice input_or_locate_uri item
-=
- match item with
- | DisambiguateTypes.Id id ->
- (try
- let references = NCicLibrary.resolve id in
- List.map
- (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
- ) references
- with
- NCicEnvironment.ObjectNotFound _ -> [])
- | _ -> []
-;;
-
-let fix_instance item l =
- match item with
- DisambiguateTypes.Symbol (_,n) ->
- List.map
- (function
- GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
- | _ -> assert false
- ) l
- | DisambiguateTypes.Num n ->
- List.map
- (function
- GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
- | _ -> assert false
- ) l
- | DisambiguateTypes.Id _ -> l
-;;
-
-
-let disambiguate_nterm estatus expty context metasenv subst thing
-=
- let diff, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~expty
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
- ~lookup_in_library:nlookup_in_library
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~description_of_alias:GrafiteAst.description_of_alias
- ~context ~metasenv ~subst thing)
- in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
- diff
- in
- metasenv, subst, estatus, cic
-;;
-
-
-type pattern =
- NotationPt.term Disambiguate.disambiguator_input option *
- (string * NCic.term) list * NCic.term option
-
-let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
- let interp path = NCicDisambiguate.disambiguate_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 x -> Some (text,prefix_len,x)
- in
- (wanted, hyp_paths, goal_path)
-;;
-
-let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
- | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
- | `Normalize
- | `Simpl
- | `Unfold None
- | `Whd as kind -> kind
-;;
-
-let disambiguate_auto_params
- disambiguate_term metasenv context (oterms, params)
-=
- match oterms with
- | None -> metasenv, (None, params)
- | Some terms ->
- let metasenv, terms =
- List.fold_right
- (fun t (metasenv, terms) ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv,t::terms) terms (metasenv, [])
- in
- metasenv, (Some terms, params)
-;;
-
-let disambiguate_just disambiguate_term context metasenv =
- function
- `Term t ->
- let metasenv,t = disambiguate_term context metasenv t in
- metasenv, `Term t
- | `Auto params ->
- let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
- context params
- in
- metasenv, `Auto params
-;;
-
-let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
- let uri =
- let baseuri =
- match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
- in
- let name =
- match obj with
- | NotationPt.Inductive (_,(name,_,_,_)::_)
- | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | NotationPt.Inductive _ -> assert false
- in
- NUri.uri_of_string (baseuri ^ "/" ^ name)
- in
- let diff, _, _, cic =
- singleton "third"
- (NCicDisambiguate.disambiguate_obj
- ~lookup_in_library:nlookup_in_library
- ~description_of_alias:GrafiteAst.description_of_alias
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~uri
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
- (text,prefix_len,obj)) in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
- diff
- in
- estatus, cic
-;;
-
-let disambiguate_cic_appl_pattern status args =
- let rec disambiguate =
- function
- NotationPt.ApplPattern l ->
- NotationPt.ApplPattern (List.map disambiguate l)
- | NotationPt.VarPattern id
- when not
- (List.exists
- (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
- ->
- let item = DisambiguateTypes.Id id in
- begin
- try
- match
- DisambiguateTypes.Environment.find item
- status#disambiguate_db.aliases
- with
- GrafiteAst.Ident_alias (_, uri) ->
- NotationPt.NRefPattern (NReference.reference_of_string uri)
- | _ -> assert false
- with Not_found ->
- prerr_endline
- ("LexiconEngine.eval_command: domain item not found: " ^
- (DisambiguateTypes.string_of_domain_item item));
- dump_aliases prerr_endline "" status;
- raise
- (Failure
- ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
- end
- | p -> p
- in
- disambiguate
-;;
-
-let add_aliases_for_objs status =
- List.fold_left
- (fun status nref ->
- let references = NCicLibrary.aliases_of nref in
- let new_env =
- List.map
- (fun u ->
- let name = NCicPp.r2s true u in
- DisambiguateTypes.Id name,
- GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
- ) references
- in
- set_proof_aliases status ~implicit_aliases:false
- GrafiteAst.WithPreferences new_env
- ) status
+++ /dev/null
-(* Copyright (C) 2004-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/
- *)
-
-type db
-
-class type g_status =
- object
- inherit Interpretations.g_status
- method disambiguate_db: db
- end
-
-class status :
- object ('self)
- inherit g_status
- inherit Interpretations.status
- method set_disambiguate_db: db -> 'self
- method set_disambiguate_status: #g_status -> 'self
- end
-
-val eval_with_new_aliases:
- #status as 'status -> ('status -> 'a) ->
- (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
-
-val set_proof_aliases:
- #status as 'status ->
- implicit_aliases:bool -> (* implicit ones are made explicit *)
- GrafiteAst.inclusion_mode ->
- (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
-
-val add_aliases_for_objs: #status as 'status -> NUri.uri list -> 'status
-
-(* args: print function, message (may be empty), status *)
-val dump_aliases: (string -> unit) -> string -> #status -> unit
-
-exception BaseUriNotSetYet
-
-val disambiguate_nterm :
- #status as 'status ->
- NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
- NotationPt.term Disambiguate.disambiguator_input ->
- NCic.metasenv * NCic.substitution * 'status * NCic.term
-
-val disambiguate_nobj :
- #status as 'status -> ?baseuri:string ->
- (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
- 'status * NCic.obj
-
-type pattern =
- NotationPt.term Disambiguate.disambiguator_input option *
- (string * NCic.term) list * NCic.term option
-
-val disambiguate_npattern:
- GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
-
-val disambiguate_cic_appl_pattern:
- #status ->
- NotationPt.argument_pattern list ->
- NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern
ncic2astMatcher.cmi:
-nTermCicContent.cmi:
+interpretations.cmi:
ncic2astMatcher.cmo: ncic2astMatcher.cmi
ncic2astMatcher.cmx: ncic2astMatcher.cmi
-nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi
-nTermCicContent.cmx: ncic2astMatcher.cmx nTermCicContent.cmi
+interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
+interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi
+disambiguateChoices.cmi:
nCicDisambiguate.cmi:
+nnumber_notation.cmi:
+grafiteDisambiguate.cmi:
disambiguateChoices.cmo: disambiguateChoices.cmi
disambiguateChoices.cmx: disambiguateChoices.cmi
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
-nnumber_notation.cmo: disambiguateChoices.cmi
-nnumber_notation.cmx: disambiguateChoices.cmx
+nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi
+nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi
+grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
+ grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \
+ grafiteDisambiguate.cmi
+disambiguateChoices.cmi:
nCicDisambiguate.cmi:
+nnumber_notation.cmi:
+grafiteDisambiguate.cmi:
+disambiguateChoices.cmo: disambiguateChoices.cmi
+disambiguateChoices.cmx: disambiguateChoices.cmi
nCicDisambiguate.cmo: nCicDisambiguate.cmi
nCicDisambiguate.cmx: nCicDisambiguate.cmi
-nnumber_notation.cmo:
-nnumber_notation.cmx:
+nnumber_notation.cmo: disambiguateChoices.cmi nnumber_notation.cmi
+nnumber_notation.cmx: disambiguateChoices.cmx nnumber_notation.cmi
+grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
+ grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \
+ grafiteDisambiguate.cmi
PACKAGE = ng_disambiguation
PREDICATES =
-INTERFACE_FILES = nCicDisambiguate.mli
+INTERFACE_FILES = \
+ disambiguateChoices.mli \
+ nCicDisambiguate.mli \
+ nnumber_notation.mli \
+ grafiteDisambiguate.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ $(INTERFACE_FILES:%.mli=%.ml)
-IMPLEMENTATION_FILES = \
- disambiguateChoices.ml \
- $(INTERFACE_FILES:%.mli=%.ml) nnumber_notation.ml
-EXTRA_OBJECTS_TO_INSTALL =
-EXTRA_OBJECTS_TO_CLEAN =
-%.cmo: OCAMLOPTIONS += -w Ae
-%.cmi: OCAMLOPTIONS += -w Ae
-%.cmx: OCAMLOPTIONS += -w Ae
-
-all:
-%: %.ml $(PACKAGE).cma
- $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $<
-all.opt opt:
-%.opt: %.ml $(PACKAGE).cmxa
- $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $<
-
-depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES)
- ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml
- cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot .
- for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot
- echo "}" >> depend.dot
- cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot .
- cat depend.dot
- tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot .
- cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot .
- echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot
- cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot .
- echo "NCicLibrary [ style=dashed ];" >> depend.dot
- echo "NCicPp [ style=dashed ];" >> depend.dot
- echo "}" >> depend.dot
- cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot .
-
-depend.png depend.eps: depend.dot
- dot -Tpng > depend.png < depend.dot
- dot -Tps > depend.eps < depend.dot
include ../../Makefile.defs
include ../Makefile.common
-
-OCAMLARCHIVEOPTIONS += -linkall
--- /dev/null
+(*
+ *
+ * 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$ *)
+
+type db = {
+ aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t;
+ multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t;
+ new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list
+}
+
+let initial_status = {
+ aliases = DisambiguateTypes.Environment.empty;
+ multi_aliases = DisambiguateTypes.Environment.empty;
+ new_aliases = []
+}
+
+class type g_status =
+ object
+ inherit Interpretations.g_status
+ method disambiguate_db: db
+ end
+
+class status =
+ object (self)
+ inherit Interpretations.status
+ val disambiguate_db = initial_status
+ method disambiguate_db = disambiguate_db
+ method set_disambiguate_db v = {< disambiguate_db = v >}
+ method set_disambiguate_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
+ end
+
+let eval_with_new_aliases status f =
+ let status =
+ status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
+ let res = f status in
+ let new_aliases = status#disambiguate_db.new_aliases in
+ new_aliases,res
+;;
+
+let dump_aliases out msg status =
+ out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
+ DisambiguateTypes.Environment.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
+ status#disambiguate_db.aliases
+
+let set_proof_aliases status ~implicit_aliases mode new_aliases =
+ if mode = GrafiteAst.WithoutPreferences then
+ status
+ else
+ (* MATITA 1.0
+ let new_commands =
+ List.map
+ (fun _,alias -> GrafiteAst.Alias (HExtlib.dummy_floc, alias)) new_aliases
+ in *)
+ let aliases =
+ List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
+ status#disambiguate_db.aliases new_aliases in
+ let multi_aliases =
+ List.fold_left (fun acc (d,c) ->
+ DisambiguateTypes.Environment.cons GrafiteAst.description_of_alias
+ d c acc)
+ status#disambiguate_db.multi_aliases new_aliases
+ in
+ let new_status =
+ {multi_aliases = multi_aliases ;
+ aliases = aliases;
+ new_aliases =
+ (if implicit_aliases then new_aliases else []) @
+ status#disambiguate_db.new_aliases}
+ in
+ status#set_disambiguate_db new_status
+
+exception BaseUriNotSetYet
+
+let singleton msg = function
+ | [x], _ -> x
+ | l, _ ->
+ let debug =
+ Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
+ msg (List.length l)
+ in
+ prerr_endline debug; assert false
+
+let __Implicit = "__Implicit__"
+let __Closed_Implicit = "__Closed_Implicit__"
+
+let ncic_mk_choice status = function
+ | GrafiteAst.Symbol_alias (name, _, dsc) ->
+ if name = __Implicit then
+ dsc, `Sym_interp (fun _ -> NCic.Implicit `Term)
+ else if name = __Closed_Implicit then
+ dsc, `Sym_interp (fun _ -> NCic.Implicit `Closed)
+ else
+ DisambiguateChoices.lookup_symbol_by_dsc status
+ ~mk_implicit:(function
+ | true -> NCic.Implicit `Closed
+ | false -> NCic.Implicit `Term)
+ ~mk_appl:(function
+ (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
+ ~term_of_nref:(fun nref -> NCic.Const nref)
+ name dsc
+ | GrafiteAst.Number_alias (_, dsc) ->
+ 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)
+ | GrafiteAst.Ident_alias (name, uri) ->
+ uri, `Sym_interp
+ (fun l->assert(l = []);
+ let nref = NReference.reference_of_string uri in
+ NCic.Const nref)
+;;
+
+
+let mk_implicit b =
+ match b with
+ | false ->
+ GrafiteAst.Symbol_alias (__Implicit,-1,"Fake Implicit")
+ | true ->
+ GrafiteAst.Symbol_alias (__Closed_Implicit,-1,"Fake Closed Implicit")
+;;
+
+let nlookup_in_library
+ interactive_user_uri_choice input_or_locate_uri item
+=
+ match item with
+ | DisambiguateTypes.Id id ->
+ (try
+ let references = NCicLibrary.resolve id in
+ List.map
+ (fun u -> GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
+ ) references
+ with
+ NCicEnvironment.ObjectNotFound _ -> [])
+ | _ -> []
+;;
+
+let fix_instance item l =
+ match item with
+ DisambiguateTypes.Symbol (_,n) ->
+ List.map
+ (function
+ GrafiteAst.Symbol_alias (s,_,d) -> GrafiteAst.Symbol_alias (s,n,d)
+ | _ -> assert false
+ ) l
+ | DisambiguateTypes.Num n ->
+ List.map
+ (function
+ GrafiteAst.Number_alias (_,d) -> GrafiteAst.Number_alias (n,d)
+ | _ -> assert false
+ ) l
+ | DisambiguateTypes.Id _ -> l
+;;
+
+
+let disambiguate_nterm estatus expty context metasenv subst thing
+=
+ let diff, metasenv, subst, cic =
+ singleton "first"
+ (NCicDisambiguate.disambiguate_term
+ ~rdb:estatus
+ ~aliases:estatus#disambiguate_db.aliases
+ ~expty
+ ~universe:(Some estatus#disambiguate_db.multi_aliases)
+ ~lookup_in_library:nlookup_in_library
+ ~mk_choice:(ncic_mk_choice estatus)
+ ~mk_implicit ~fix_instance
+ ~description_of_alias:GrafiteAst.description_of_alias
+ ~context ~metasenv ~subst thing)
+ in
+ let estatus =
+ set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+ diff
+ in
+ metasenv, subst, estatus, cic
+;;
+
+
+type pattern =
+ NotationPt.term Disambiguate.disambiguator_input option *
+ (string * NCic.term) list * NCic.term option
+
+let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+ let interp path = NCicDisambiguate.disambiguate_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 x -> Some (text,prefix_len,x)
+ in
+ (wanted, hyp_paths, goal_path)
+;;
+
+let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
+ | `Unfold (Some t) -> assert false (* MATITA 1.0 *)
+ | `Normalize
+ | `Simpl
+ | `Unfold None
+ | `Whd as kind -> kind
+;;
+
+let disambiguate_auto_params
+ disambiguate_term metasenv context (oterms, params)
+=
+ match oterms with
+ | None -> metasenv, (None, params)
+ | Some terms ->
+ let metasenv, terms =
+ List.fold_right
+ (fun t (metasenv, terms) ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,t::terms) terms (metasenv, [])
+ in
+ metasenv, (Some terms, params)
+;;
+
+let disambiguate_just disambiguate_term context metasenv =
+ function
+ `Term t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv, `Term t
+ | `Auto params ->
+ let metasenv,params = disambiguate_auto_params disambiguate_term metasenv
+ context params
+ in
+ metasenv, `Auto params
+;;
+
+let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
+ let uri =
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | NotationPt.Inductive (_,(name,_,_,_)::_)
+ | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Inductive _ -> assert false
+ in
+ NUri.uri_of_string (baseuri ^ "/" ^ name)
+ in
+ let diff, _, _, cic =
+ singleton "third"
+ (NCicDisambiguate.disambiguate_obj
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:GrafiteAst.description_of_alias
+ ~mk_choice:(ncic_mk_choice estatus)
+ ~mk_implicit ~fix_instance
+ ~uri
+ ~rdb:estatus
+ ~aliases:estatus#disambiguate_db.aliases
+ ~universe:(Some estatus#disambiguate_db.multi_aliases)
+ (text,prefix_len,obj)) in
+ let estatus =
+ set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+ diff
+ in
+ estatus, cic
+;;
+
+let disambiguate_cic_appl_pattern status args =
+ let rec disambiguate =
+ function
+ NotationPt.ApplPattern l ->
+ NotationPt.ApplPattern (List.map disambiguate l)
+ | NotationPt.VarPattern id
+ when not
+ (List.exists
+ (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
+ ->
+ let item = DisambiguateTypes.Id id in
+ begin
+ try
+ match
+ DisambiguateTypes.Environment.find item
+ status#disambiguate_db.aliases
+ with
+ GrafiteAst.Ident_alias (_, uri) ->
+ NotationPt.NRefPattern (NReference.reference_of_string uri)
+ | _ -> assert false
+ with Not_found ->
+ prerr_endline
+ ("LexiconEngine.eval_command: domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item));
+ dump_aliases prerr_endline "" status;
+ raise
+ (Failure
+ ((DisambiguateTypes.string_of_domain_item item) ^ " not found"))
+ end
+ | p -> p
+ in
+ disambiguate
+;;
+
+let add_aliases_for_objs status =
+ List.fold_left
+ (fun status nref ->
+ let references = NCicLibrary.aliases_of nref in
+ let new_env =
+ List.map
+ (fun u ->
+ let name = NCicPp.r2s true u in
+ DisambiguateTypes.Id name,
+ GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
+ ) references
+ in
+ set_proof_aliases status ~implicit_aliases:false
+ GrafiteAst.WithPreferences new_env
+ ) status
--- /dev/null
+(* Copyright (C) 2004-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/
+ *)
+
+type db
+
+class type g_status =
+ object
+ inherit Interpretations.g_status
+ method disambiguate_db: db
+ end
+
+class status :
+ object ('self)
+ inherit g_status
+ inherit Interpretations.status
+ method set_disambiguate_db: db -> 'self
+ method set_disambiguate_status: #g_status -> 'self
+ end
+
+val eval_with_new_aliases:
+ #status as 'status -> ('status -> 'a) ->
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
+
+val set_proof_aliases:
+ #status as 'status ->
+ implicit_aliases:bool -> (* implicit ones are made explicit *)
+ GrafiteAst.inclusion_mode ->
+ (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
+
+val add_aliases_for_objs: #status as 'status -> NUri.uri list -> 'status
+
+(* args: print function, message (may be empty), status *)
+val dump_aliases: (string -> unit) -> string -> #status -> unit
+
+exception BaseUriNotSetYet
+
+val disambiguate_nterm :
+ #status as 'status ->
+ NCic.term option -> NCic.context -> NCic.metasenv -> NCic.substitution ->
+ NotationPt.term Disambiguate.disambiguator_input ->
+ NCic.metasenv * NCic.substitution * 'status * NCic.term
+
+val disambiguate_nobj :
+ #status as 'status -> ?baseuri:string ->
+ (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input ->
+ 'status * NCic.obj
+
+type pattern =
+ NotationPt.term Disambiguate.disambiguator_input option *
+ (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+ GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+
+val disambiguate_cic_appl_pattern:
+ #status ->
+ NotationPt.argument_pattern list ->
+ NotationPt.cic_appl_pattern -> NotationPt.cic_appl_pattern
--- /dev/null
+(* Copyright (C) 2004, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id: number_notation.ml 9771 2009-05-14 13:43:55Z fguidi $ *)
+
+(* Works by side-effects only *)
nCicMetaSubst.cmi:
nCicUnifHint.cmi:
nCicCoercion.cmi: nCicUnifHint.cmi
-nRstatus.cmi: nCicCoercion.cmi
nCicRefineUtil.cmi:
-nCicUnification.cmi: nRstatus.cmi
-nCicRefiner.cmi: nRstatus.cmi
+nCicUnification.cmi: nCicCoercion.cmi
+nCicRefiner.cmi: nCicCoercion.cmi
nDiscriminationTree.cmo: nDiscriminationTree.cmi
nDiscriminationTree.cmx: nDiscriminationTree.cmi
nCicMetaSubst.cmo: nCicMetaSubst.cmi
nCicCoercion.cmi
nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
nCicCoercion.cmi
-nRstatus.cmo: nCicCoercion.cmi nRstatus.cmi
-nRstatus.cmx: nCicCoercion.cmx nRstatus.cmi
nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi
nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
nCicTacReduction.cmi:
nTacStatus.cmi: continuationals.cmi
nCicElim.cmi:
-nTactics.cmi: nTacStatus.cmi continuationals.cmi
+nTactics.cmi: nTacStatus.cmi
nnAuto.cmi: nTacStatus.cmi
nDestructTac.cmi: nTacStatus.cmi
nInversion.cmi: nTacStatus.cmi
projects / helm.git / commitdiff