libraries-complete.ps
.dep.dot
.alldep.dot
+.clustersdep.dot
+.extdep.dot
+libraries-clusters.ps
+libraries-ext.ps
-requires="helm-content_pres"
+requires="helm-cic"
version="0.0.1"
archive(byte)="grafite.cma"
archive(native)="grafite.cmxa"
+++ /dev/null
-requires="helm-library helm-grafite helm-tactics helm-cic_disambiguation"
-version="0.0.1"
-archive(byte)="grafite2.cma"
-archive(native)="grafite2.cmxa"
-linkopts=""
--- /dev/null
+requires="helm-library helm-grafite helm-tactics"
+version="0.0.1"
+archive(byte)="grafite_engine.cma"
+archive(native)="grafite_engine.cmxa"
+linkopts=""
-requires="helm-grafite2 ulex"
+requires="helm-lexicon helm-grafite ulex"
version="0.0.1"
archive(byte)="grafite_parser.cma"
archive(native)="grafite_parser.cmxa"
--- /dev/null
+requires="helm-content_pres helm-cic_disambiguation camlp4.gramlib"
+version="0.0.1"
+archive(byte)="lexicon.cma"
+archive(native)="lexicon.cmxa"
tactics \
paramodulation \
cic_disambiguation \
- grafite2 \
+ lexicon \
+ grafite_engine \
grafite_parser \
$(NULL)
.extdep.dot: .dep.dot
./patch_deps.sh $< $@
+.clustersdep.dot: .dep.dot
+ USE_CLUSTERS=yes ./patch_deps.sh $< $@
libraries.ps: .dep.dot
dot -Tps -o $@ $<
libraries-ext.ps: .extdep.dot
dot -Tps -o $@ $<
+libraries-clusters.ps: .clustersdep.dot
+ dot -Tps -o $@ $<
libraries-complete.ps: .alldep.dot
dot -Tps -o $@ $<
+ps: libraries.ps libraries-ext.ps libraries-clusters.ps
+
tags: TAGS
.PHONY: TAGS
TAGS:
and anncontext = annhypothesis list
;;
+type lazy_term =
+ context -> metasenv -> CicUniv.universe_graph ->
+ term * metasenv * CicUniv.universe_graph
+
type anntarget =
Object of annobj (* if annobj is a Constant, this is its type *)
| ConstantBody of annobj
| None -> Cic.Implicit annotation
| Some term -> aux ~localize loc context term
in
- aux ~localize:true dummy_floc context ast
+ aux ~localize:true HExtlib.dummy_floc context ast
let interpretate_path ~context path =
let localization_tbl = Cic.CicHash.create 23 in
(* "aux" keeps domain in reverse order and doesn't care about duplicates.
* Domain item more in deep in the list will be processed first.
*)
-let rec domain_rev_of_term ?(loc = dummy_floc) context = function
+let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
domain_rev_of_term ~loc context term
| CicNotationPt.AttributedTerm (_, term) ->
let string_of_domain dom =
String.concat "; " (List.map string_of_domain_item dom)
-
-let floc_of_loc (loc_begin, loc_end) =
- let floc_begin =
- { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
- Lexing.pos_cnum = loc_begin }
- in
- let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
- (floc_begin, floc_end)
-
-let dummy_floc = floc_of_loc (-1, -1)
-
| Comment of CicNotationPt.location * string
type script = CicNotationPt.location * script_entry list
*)
-
-val dummy_floc: Lexing.position * Lexing.position
-
style = "filled";
color = "white"
acic_content;
- cic_acic;
cic_disambiguation;
content_pres;
- grafite;
+ grafite_parser;
+ lexicon;
}
subgraph cluster_partially {
label = "Partially specified terms";
cic_unification;
tactics;
paramodulation;
+ grafite;
+ grafite_engine;
}
subgraph cluster_fully {
label = "Fully specified terms";
metadata;
urimanager;
whelp;
+ library;
+ cic_acic;
}
subgraph cluster_utilities {
label = "Utilities";
hgdome;
hmysql;
registry;
-// utf8_macros;
+ utf8_macros;
xml;
+ logger;
}
Matita -> hgdome;
ProofChecker -> cic_proof_checking;
Uwobo -> content_pres;
- Whelp -> cic_disambiguation;
- Whelp -> content_pres;
+ Whelp -> grafite_parser;
| { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
(loc_begin, loc_end)
+let floc_of_loc (loc_begin, loc_end) =
+ let floc_begin =
+ { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
+ Lexing.pos_cnum = loc_begin }
+ in
+ let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
+ (floc_begin, floc_end)
+
+let dummy_floc = floc_of_loc (-1, -1)
+
let raise_localized_exception ~offset floc exn =
let (x, y) = loc_of_floc floc in
let x = offset + x in
exception Localized of Token.flocation * exn
val loc_of_floc: Token.flocation -> int * int
+val floc_of_loc: int * int -> Token.flocation
+
+val dummy_floc: Lexing.position * Lexing.position
val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a
grafiteAstPp.cmi: grafiteAst.cmo
-cicNotation.cmi: grafiteAst.cmo
grafiteMarshal.cmi: grafiteAst.cmo
grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
-cicNotation.cmo: grafiteAst.cmo cicNotation.cmi
-cicNotation.cmx: grafiteAst.cmx cicNotation.cmi
grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi
grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi
INTERFACE_FILES = \
grafiteAstPp.mli \
- cicNotation.mli \
grafiteMarshal.mli \
$(NULL)
IMPLEMENTATION_FILES = \
+++ /dev/null
-(* 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/
- *)
-
-open GrafiteAst
-
-type notation_id =
- | RuleId of CicNotationParser.rule_id
- | InterpretationId of TermAcicContent.interpretation_id
- | PrettyPrinterId of TermContentPres.pretty_printer_id
-
-let process_notation st =
- match st with
- | Notation (loc, dir, l1, associativity, precedence, l2) ->
- let rule_id =
- if dir <> Some `RightToLeft then
- [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity
- (fun env loc ->
- CicNotationPt.AttributedTerm
- (`Loc loc,TermContentPres.instantiate_level2 env l2))) ]
- else
- []
- in
- let pp_id =
- if dir <> Some `LeftToRight then
- [ PrettyPrinterId
- (TermContentPres.add_pretty_printer ?precedence ?associativity
- l2 l1) ]
- else
- []
- in
- st, rule_id @ pp_id
- | Interpretation (loc, dsc, l2, l3) ->
- let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
- st, [ InterpretationId interp_id ]
- | st -> st, []
-
-let remove_notation = function
- | RuleId id -> CicNotationParser.delete id
- | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
- | InterpretationId id -> TermAcicContent.remove_interpretation id
-
-let get_all_notations () =
- List.map
- (fun (interp_id, dsc) ->
- InterpretationId interp_id, "interpretation: " ^ dsc)
- (TermAcicContent.get_all_interpretations ())
-
-let get_active_notations () =
- List.map (fun id -> InterpretationId id)
- (TermAcicContent.get_active_interpretations ())
-
-let set_active_notations ids =
- let interp_ids =
- HExtlib.filter_map
- (function InterpretationId interp_id -> Some interp_id | _ -> None)
- ids
- in
- TermAcicContent.set_active_interpretations interp_ids
-
+++ /dev/null
-(* 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/
- *)
-
-type notation_id
-
-val process_notation:
- 'obj GrafiteAst.command -> 'obj GrafiteAst.command * notation_id list
-
-val remove_notation: notation_id -> unit
-
-(** {2 Notation enabling/disabling}
- * Right now, only disabling of notation during pretty printing is supporting.
- * If it is useful to disable it also for the input phase is still to be
- * understood ... *)
-
-val get_all_notations: unit -> (notation_id * string) list (* id, dsc *)
-val get_active_notations: unit -> notation_id list
-val set_active_notations: notation_id list -> unit
-
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = CicNotationPt.location
+type loc = Token.flocation
type ('term, 'lazy_term, 'ident) pattern =
'lazy_term option * ('ident * 'term) list * 'term option
| Search_pat of loc * search_kind * string (* searches with string pattern *)
| Search_term of loc * search_kind * 'term (* searches with term pattern *)
-type alias_spec =
- | Ident_alias of string * string (* identifier, uri *)
- | Symbol_alias of string * int * string (* name, instance no, description *)
- | Number_alias of int * string (* instance no, description *)
-
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
let magic = 5
| Set of loc * string * string
| Drop of loc
| Qed of loc
- (** name.
- * Name is needed when theorem was started without providing a name
- *)
| Coercion of loc * UriManager.uri * bool (* add composites *)
- | Alias of loc * alias_spec
- (** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
- int * CicNotationPt.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * CicNotationPt.argument_pattern list) *
- CicNotationPt.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
- (* DEBUGGING *)
- | Dump of loc (* dump grammar on stdout *)
- (* DEBUGGING *)
- | Render of loc * UriManager.uri (* render library object *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
type ('term, 'lazy_term, 'reduction, 'ident) tactical =
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
| Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
| Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
-
- (* statements meaningful for matitadep *)
-type dependency =
- | IncludeDep of string
- | BaseuriDep of string
- | UriDep of UriManager.uri
-
| Print (_, name) -> sprintf "Print \"%s\"" name
| Quit _ -> "Quit"
-let pp_alias = function
- | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
- | Symbol_alias (symb, instance, desc) ->
- sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
- symb instance desc
- | Number_alias (instance,desc) ->
- sprintf "alias num (instance %d) = \"%s\"" instance desc
-
-let pp_argument_pattern = function
- | CicNotationPt.IdentArg (eta_depth, name) ->
- let eta_buf = Buffer.create 5 in
- for i = 1 to eta_depth do
- Buffer.add_string eta_buf "\\eta."
- done;
- sprintf "%s%s" (Buffer.contents eta_buf) name
-
-let pp_l1_pattern = CicNotationPp.pp_term
-let pp_l2_pattern = CicNotationPp.pp_term
-
let pp_associativity = function
| Gramext.LeftA -> "left associative"
| Gramext.RightA -> "right associative"
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
-let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
- sprintf "interpretation \"%s\" '%s %s = %s"
- dsc symbol
- (String.concat " " (List.map pp_argument_pattern arg_patterns))
- (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
-
let pp_default what uris =
sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
-let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
- sprintf "notation %s\"%s\" %s %s for %s"
- (pp_dir_opt dir_opt)
- (pp_l1_pattern l1_pattern)
- (pp_associativity assoc)
- (pp_precedence prec)
- (pp_l2_pattern l2_pattern)
-
let pp_coercion uri do_composites =
sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
(if do_composites then "compounds" else "no compounds")
| Drop _ -> "drop"
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
| Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
- | Alias (_,s) -> pp_alias s
| Obj (_,obj) -> obj_pp obj
| Default (_,what,uris) ->
pp_default what uris
- | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
- pp_interpretation dsc symbol arg_patterns cic_appl_pattern
- | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
- pp_notation dir_opt l1_pattern assoc prec l2_pattern
- | Render _
- | Dump _ -> assert false (* ZACK: debugging *)
let rec pp_tactical ~term_pp ~lazy_term_pp =
let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
function
| Executable (_, ex) -> pp_executable ~lazy_term_pp ~term_pp ~obj_pp ex
| Comment (_, c) -> pp_comment ~term_pp ~lazy_term_pp ~obj_pp c
-
-let pp_dependency = function
- | IncludeDep str -> "include \"" ^ str ^ "\""
- | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
- | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
-
val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string
val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
-val pp_alias: GrafiteAst.alias_spec -> string
-val pp_dependency: GrafiteAst.dependency -> string
-
val pp_comment:
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
| GrafiteAst.Default (loc, name, uris) ->
let uris = List.map rehash_uri uris in
GrafiteAst.Default (loc, name, uris)
- | GrafiteAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
- let rec aux =
- function
- | CicNotationPt.UriPattern uri ->
- CicNotationPt.UriPattern (rehash_uri uri)
- | CicNotationPt.ApplPattern args ->
- CicNotationPt.ApplPattern (List.map aux args)
- | CicNotationPt.VarPattern _
- | CicNotationPt.ImplicitPattern as pat -> pat
- in
- let appl_pattern = aux cic_appl_pattern in
- GrafiteAst.Interpretation (loc, dsc, args, appl_pattern)
| GrafiteAst.Coercion (loc, uri, close) ->
GrafiteAst.Coercion (loc, rehash_uri uri, close)
- | GrafiteAst.Notation _
- | GrafiteAst.Alias _ as cmd -> cmd
| cmd ->
prerr_endline "Found a command not expected in a .moo:";
let obj_pp _ = assert false in
-matitaSync.cmi: grafiteTypes.cmi
+grafiteSync.cmi: grafiteTypes.cmi
grafiteEngine.cmi: grafiteTypes.cmi
grafiteTypes.cmo: grafiteTypes.cmi
grafiteTypes.cmx: grafiteTypes.cmi
-disambiguatePp.cmo: disambiguatePp.cmi
-disambiguatePp.cmx: disambiguatePp.cmi
-matitaSync.cmo: grafiteTypes.cmi disambiguatePp.cmi matitaSync.cmi
-matitaSync.cmx: grafiteTypes.cmx disambiguatePp.cmx matitaSync.cmi
+grafiteSync.cmo: grafiteTypes.cmi grafiteSync.cmi
+grafiteSync.cmx: grafiteTypes.cmx grafiteSync.cmi
grafiteMisc.cmo: grafiteMisc.cmi
grafiteMisc.cmx: grafiteMisc.cmi
-grafiteEngine.cmo: matitaSync.cmi grafiteTypes.cmi grafiteMisc.cmi \
- grafiteEngine.cmi
-grafiteEngine.cmx: matitaSync.cmx grafiteTypes.cmx grafiteMisc.cmx \
- grafiteEngine.cmi
+grafiteEngine.cmo: grafiteTypes.cmi grafiteMisc.cmi grafiteEngine.cmi
+grafiteEngine.cmx: grafiteTypes.cmx grafiteMisc.cmx grafiteEngine.cmi
INTERFACE_FILES = \
grafiteTypes.mli \
- disambiguatePp.mli \
- matitaSync.mli \
+ grafiteSync.mli \
grafiteMisc.mli \
grafiteEngine.mli \
$(NULL)
+++ /dev/null
-(* 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/
- *)
-
-open DisambiguateTypes
-
-let alias_of_domain_and_codomain_items domain_item (dsc,_) =
- match domain_item with
- Id id -> GrafiteAst.Ident_alias (id, dsc)
- | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
- | Num i -> GrafiteAst.Number_alias (i, dsc)
-
-let aliases_of_environment env =
- Environment.fold
- (fun domain_item codomain_item acc ->
- alias_of_domain_and_codomain_items domain_item codomain_item::acc
- ) env []
-
-let aliases_of_domain_and_codomain_items_list l =
- List.fold_left
- (fun acc (domain_item,codomain_item) ->
- alias_of_domain_and_codomain_items domain_item codomain_item::acc
- ) [] l
-
-let pp_environment env =
- let aliases = aliases_of_environment env in
- let strings =
- List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases
- in
- String.concat "\n" (List.sort compare strings)
+++ /dev/null
-(* 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 aliases_of_domain_and_codomain_items_list:
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
- GrafiteAst.alias_spec list
-
-val pp_environment: DisambiguateTypes.environment -> string
+++ /dev/null
-(* 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/
- *)
-
-exception Drop
-exception IncludedFileNotCompiled of string (* file name *)
-exception MetadataNotFound of string (* file name *)
-
-type options = {
- do_heavy_checks: bool ;
- clean_baseuri: bool
-}
-
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
- * names as long as they are available, then it fallbacks to name generation
- * using FreshNamesGenerator module *)
-let namer_of names =
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-let tactic_of_ast ast =
- let module PET = ProofEngineTypes in
- match ast with
- | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
- | GrafiteAst.Apply (_, term) -> Tactics.apply term
- | GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
- ~dbd:(LibraryDb.instance ()) ()
- | GrafiteAst.Change (_, pattern, with_what) ->
- Tactics.change ~pattern with_what
- | GrafiteAst.Clear (_,id) -> Tactics.clear id
- | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
- | GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
- | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
- | GrafiteAst.Cut (_, ident, term) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
- | GrafiteAst.Decompose (_, types, what, names) ->
- let to_type = function
- | GrafiteAst.Type (uri, typeno) -> uri, typeno
- | GrafiteAst.Ident _ -> assert false
- in
- let user_types = List.rev_map to_type types in
- let dbd = LibraryDb.instance () in
- let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
- | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
- | GrafiteAst.Elim (_, what, using, depth, names) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- what
- | GrafiteAst.ElimType (_, what, using, depth, names) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- what
- | GrafiteAst.Exact (_, term) -> Tactics.exact term
- | GrafiteAst.Exists _ -> Tactics.exists
- | GrafiteAst.Fail _ -> Tactics.fail
- | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
- let reduction =
- match reduction_kind with
- | `Normalize ->
- PET.const_lazy_reduction
- (CicReduction.normalize ~delta:false ~subst:[])
- | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
- | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
- | `Unfold None ->
- PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
- | `Unfold (Some lazy_term) ->
- (fun context metasenv ugraph ->
- let what, metasenv, ugraph = lazy_term context metasenv ugraph in
- ProofEngineReduction.unfold ~what, metasenv, ugraph)
- | `Whd ->
- PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[])
- in
- Tactics.fold ~reduction ~term ~pattern
- | GrafiteAst.Fourier _ -> Tactics.fourier
- | GrafiteAst.FwdSimpl (_, hyp, names) ->
- Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
- ~dbd:(LibraryDb.instance ()) hyp
- | GrafiteAst.Generalize (_,pattern,ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
- | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
- | GrafiteAst.IdTac _ -> Tactics.id
- | GrafiteAst.Injection (_,term) -> Tactics.injection term
- | GrafiteAst.Intros (_, None, names) ->
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.Intros (_, Some num, names) ->
- PrimitiveTactics.intros_tac ~howmany:num
- ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.Inversion (_, term) ->
- Tactics.inversion term
- | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
- ~to_what what
- | GrafiteAst.Left _ -> Tactics.left
- | GrafiteAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
- (match reduction_kind with
- | `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
- | `Simpl -> Tactics.simpl ~pattern
- | `Unfold what -> Tactics.unfold ~pattern what
- | `Whd -> Tactics.whd ~pattern)
- | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
- | GrafiteAst.Replace (_, pattern, with_what) ->
- Tactics.replace ~pattern ~with_what
- | GrafiteAst.Rewrite (_, direction, t, pattern) ->
- EqualityTactics.rewrite_tac ~direction ~pattern t
- | GrafiteAst.Right _ -> Tactics.right
- | GrafiteAst.Ring _ -> Tactics.ring
- | GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Symmetry _ -> Tactics.symmetry
- | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
-
-(* maybe we only need special cases for apply and goal *)
-let classify_tactic tactic =
- match tactic with
- (* tactics that can't close the goal (return a goal we want to "select") *)
- | GrafiteAst.Rewrite _
- | GrafiteAst.Split _
- | GrafiteAst.Replace _
- | GrafiteAst.Reduce _
- | GrafiteAst.Injection _
- | GrafiteAst.IdTac _
- | GrafiteAst.Generalize _
- | GrafiteAst.Elim _
- | GrafiteAst.Cut _
- | GrafiteAst.Decompose _ -> true, true
- (* tactics we don't want to reorder goals. I think only Goal needs this. *)
- | GrafiteAst.Goal _ -> false, true
- (* tactics like apply *)
- | _ -> true, false
-
-let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
- let module PEH = ProofEngineHelpers in
-(* let print_m name metasenv =
- prerr_endline (">>>>> " ^ name);
- prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)
- in *)
- (* phase one calculates:
- * new_goals_from_refine: goals added by refine
- * head_goal: the first goal opened by ythe tactic
- * other_goals: other goals opened by the tactic
- *)
- let new_goals_from_refine = PEH.compare_metasenvs start refine in
- let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
- let head_goal, other_goals, goals =
- match goals with
- | [] -> None,[],goals
- | hd::tl ->
- (* assert (List.mem hd new_goals_from_tactic);
- * invalidato dalla goal_tac
- * *)
- Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
- hd) goals
- in
- let produced_goals =
- match head_goal with
- | None -> new_goals_from_refine @ other_goals
- | Some x -> x :: new_goals_from_refine @ other_goals
- in
- (* extract the metas generated by refine and tactic *)
- let metas_for_tactic_head =
- match head_goal with
- | None -> []
- | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
- let metas_for_tactic_goals =
- List.map
- (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
- goals
- in
- let metas_for_refine_goals =
- List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
- let produced_metas, goals =
- let produced_metas =
- if always_opens_a_goal then
- metas_for_tactic_head @ metas_for_refine_goals @
- metas_for_tactic_goals
- else begin
-(* print_m "metas_for_refine_goals" metas_for_refine_goals;
- print_m "metas_for_tactic_head" metas_for_tactic_head;
- print_m "metas_for_tactic_goals" metas_for_tactic_goals; *)
- metas_for_refine_goals @ metas_for_tactic_head @
- metas_for_tactic_goals
- end
- in
- let goals = List.map (fun (metano, _, _) -> metano) produced_metas in
- produced_metas, goals
- in
- (* residual metas, preserving the original order *)
- let before, after =
- let rec split e =
- function
- | [] -> [],[]
- | (metano, _, _) :: tl when metano = e ->
- [], List.map (fun (x,_,_) -> x) tl
- | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
- in
- let find n metasenv =
- try
- Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
- with Not_found -> None
- in
- let extract l =
- List.fold_right
- (fun n acc ->
- match find n tactic with
- | Some x -> x::acc
- | None -> acc
- ) l [] in
- let before_l, after_l = split current_goal start in
- let before_l =
- List.filter (fun x -> not (List.mem x produced_goals)) before_l in
- let after_l =
- List.filter (fun x -> not (List.mem x produced_goals)) after_l in
- let before = extract before_l in
- let after = extract after_l in
- before, after
- in
-(* |+ DEBUG CODE +|
- print_m "BEGIN" start;
- prerr_endline ("goal was: " ^ string_of_int current_goal);
- prerr_endline ("and metas from refine are:");
- List.iter
- (fun t -> prerr_string (" " ^ string_of_int t))
- new_goals_from_refine;
- prerr_endline "";
- print_m "before" before;
- print_m "metas_for_tactic_head" metas_for_tactic_head;
- print_m "metas_for_refine_goals" metas_for_refine_goals;
- print_m "metas_for_tactic_goals" metas_for_tactic_goals;
- print_m "produced_metas" produced_metas;
- print_m "after" after;
-|+ FINE DEBUG CODE +| *)
- before @ produced_metas @ after, goals
-
-let apply_tactic ~disambiguate_tactic tactic (status, goal) =
-(* prerr_endline "apply_tactic"; *)
-(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *)
- let starting_metasenv = GrafiteTypes.get_proof_metasenv status in
- let before = List.map (fun g, _, _ -> g) starting_metasenv in
-(* prerr_endline "disambiguate"; *)
- let status_ref, tactic = disambiguate_tactic status goal tactic in
- let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv !status_ref in
- let proof = GrafiteTypes.get_current_proof !status_ref in
- let proof_status = proof, goal in
- let needs_reordering, always_opens_a_goal = classify_tactic tactic in
- let tactic = tactic_of_ast tactic in
- (* apply tactic will change the status pointed by status_ref ... *)
-(* prerr_endline "apply_tactic bassa"; *)
- let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
- let after = ProofEngineTypes.goals_of_proof proof in
- let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
-(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before));
-prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after));
-prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *)
-(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals));
-prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *)
- let proof, opened_goals =
- if needs_reordering then begin
- let uri, metasenv_after_tactic, t, ty = proof in
-(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *)
- let reordered_metasenv, opened_goals =
- reorder_metasenv
- starting_metasenv
- metasenv_after_refinement metasenv_after_tactic
- opened goal always_opens_a_goal
- in
- let proof' = uri, reordered_metasenv, t, ty in
-(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *)
- proof', opened_goals
- end
- else
- proof, opened_goals
- in
- let incomplete_proof =
- match !status_ref.GrafiteTypes.proof_status with
- | GrafiteTypes.Incomplete_proof p -> p
- | _ -> assert false
- in
- { !status_ref with GrafiteTypes.proof_status =
- GrafiteTypes.Incomplete_proof
- { incomplete_proof with GrafiteTypes.proof = proof } },
- opened_goals, closed_goals
-
-type eval_ast =
- {ea_go:
- 'term 'lazy_term 'reduction 'obj 'ident.
- baseuri_of_script:(string -> string) ->
- disambiguate_tactic:
- (GrafiteTypes.status ->
- ProofEngineTypes.goal ->
- ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
- GrafiteTypes.status ref *
- (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
-
- disambiguate_command:
- (GrafiteTypes.status ->
- 'obj GrafiteAst.command ->
- GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
-
- ?do_heavy_checks:bool ->
- ?clean_baseuri:bool ->
- GrafiteTypes.status ->
- ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
- GrafiteTypes.status
- }
-
-type 'a eval_command =
- {ec_go: 'term 'obj.
- baseuri_of_script:(string -> string) ->
- disambiguate_command:
- (GrafiteTypes.status ->
- 'obj GrafiteAst.command ->
- GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
- options -> GrafiteTypes.status -> 'obj GrafiteAst.command ->
- GrafiteTypes.status
- }
-
-type 'a eval_executable =
- {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
- baseuri_of_script:(string -> string) ->
- disambiguate_tactic:
- (GrafiteTypes.status ->
- ProofEngineTypes.goal ->
- ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
- GrafiteTypes.status ref *
- (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
-
- disambiguate_command:
- (GrafiteTypes.status ->
- 'obj GrafiteAst.command ->
- GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
-
- options ->
- GrafiteTypes.status ->
- ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code -> GrafiteTypes.status
- }
-
-type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit }
-
-let coercion_moo_statement_of uri =
- GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, uri, false)
-
-let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
- let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
- let moo_content = coercion_moo_statement_of uri in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
- let status = MatitaSync.add_coercion status uri compounds in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
-
-let eval_tactical ~disambiguate_tactic status tac =
- let apply_tactic = apply_tactic ~disambiguate_tactic in
- let module MatitaStatus =
- struct
- type input_status = GrafiteTypes.status * ProofEngineTypes.goal
-
- type output_status =
- GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
-
- type tactic = input_status -> output_status
-
- let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc)
- let mk_tactic tac = tac
- let apply_tactic tac = tac
- let goals (_, opened, closed) = opened, closed
- let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
- let get_stack (status, _) = GrafiteTypes.get_stack status
-
- let set_stack stack (status, opened, closed) =
- GrafiteTypes.set_stack stack status, opened, closed
-
- let inject (status, _) = (status, [], [])
- let focus goal (status, _, _) = (status, goal)
- end
- in
- let module MatitaTacticals = Tacticals.Make (MatitaStatus) in
- let rec tactical_of_ast l tac =
- match tac with
- | GrafiteAst.Tactic (loc, tactic) ->
- MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
- | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- assert (l > 0);
- MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
- | GrafiteAst.Do (loc, n, tactical) ->
- MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Repeat (loc, tactical) ->
- MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- assert (l > 0);
- MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
- ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
- | GrafiteAst.First (loc, tacticals) ->
- MatitaTacticals.first
- ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
- | GrafiteAst.Try (loc, tactical) ->
- MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Solve (loc, tacticals) ->
- MatitaTacticals.solve_tactics
- ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
-
- | GrafiteAst.Skip loc -> MatitaTacticals.skip
- | GrafiteAst.Dot loc -> MatitaTacticals.dot
- | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
- | GrafiteAst.Branch loc -> MatitaTacticals.branch
- | GrafiteAst.Shift loc -> MatitaTacticals.shift
- | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
- | GrafiteAst.Merge loc -> MatitaTacticals.merge
- | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
- | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
- in
- let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
- let status = (* is proof completed? *)
- match status.GrafiteTypes.proof_status with
- | GrafiteTypes.Incomplete_proof
- { GrafiteTypes.stack = stack; proof = proof }
- when Continuationals.Stack.is_empty stack ->
- { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof }
- | _ -> status
- in
- status
-
-let eval_comment status c = status
-
-(* since the record syntax allows to declare coercions, we have to put this
- * information inside the moo *)
-let add_coercions_of_record_to_moo obj lemmas status =
- let attributes = CicUtil.attributes_of_obj obj in
- let is_record = function `Class (`Record att) -> Some att | _-> None in
- match HExtlib.list_findopt is_record attributes with
- | None -> status
- | Some fields ->
- let is_a_coercion uri =
- try
- let obj,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
- let attrs = CicUtil.attributes_of_obj obj in
- List.mem (`Class `Projection) attrs
- with Not_found -> assert false
- in
- (* looking at the fields we can know the 'wanted' coercions, but not the
- * actually generated ones. So, only the intersection between the wanted
- * and the actual should be in the moo as coercion, while everithing in
- * lemmas should go as aliases *)
- let wanted_coercions =
- HExtlib.filter_map
- (function
- | (name,true) ->
- Some
- (UriManager.uri_of_string
- (GrafiteTypes.qualify status name ^ ".con"))
- | _ -> None)
- fields
- in
- prerr_endline "wanted coercions:";
- List.iter
- (fun u -> prerr_endline (UriManager.string_of_uri u))
- wanted_coercions;
- let coercions, moo_content =
- List.split
- (HExtlib.filter_map
- (fun uri ->
- let is_a_wanted_coercion =
- List.exists (UriManager.eq uri) wanted_coercions in
- if is_a_coercion uri && is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of uri)
- else
- None)
- lemmas)
- in
- List.iter
- (fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions;
- let status = GrafiteTypes.add_moo_content moo_content status in
- List.fold_left
- (fun status uri ->
- MatitaSync.add_coercion status uri [])
- status coercions
-
-let add_obj uri obj status =
- let basedir = Helm_registry.get "matita.basedir" in
- let lemmas = LibrarySync.add_obj uri obj basedir in
- let status =
- {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects} in
- let status = MatitaSync.add_obj uri obj lemmas status in
- status, lemmas
-
-let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd ->
- let status,cmd = disambiguate_command status cmd in
- let cmd,notation_ids' = CicNotation.process_notation cmd in
- let status =
- { status with
- GrafiteTypes.notation_ids =
- notation_ids' @ status.GrafiteTypes.notation_ids } in
- let basedir = Helm_registry.get "matita.basedir" in
- match cmd with
- | GrafiteAst.Default (loc, what, uris) as cmd ->
- LibraryObjects.set_default what uris;
- GrafiteTypes.add_moo_content [cmd] status
- | GrafiteAst.Include (loc, path) ->
- let baseuri = baseuri_of_script path in
- let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
- let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists moopath) then
- raise (IncludedFileNotCompiled moopath);
- let status =
- if Helm_registry.get_bool "db.nodb" then
- if not (Sys.file_exists metadatapath) then
- raise (MetadataNotFound metadatapath)
- else
- GrafiteTypes.add_metadata
- (LibraryNoDb.load_metadata ~fname:metadatapath) status
- else
- status
- in
- let status = ref status in
- eval_from_moo.efm_go status moopath;
- !status
- | GrafiteAst.Set (loc, name, value) ->
- let status =
- if name = "baseuri" then begin
- let value =
- let v = Http_getter_misc.strip_trailing_slash value in
- try
- ignore (String.index v ' ');
- raise (GrafiteTypes.Command_error "baseuri can't contain spaces")
- with Not_found -> v
- in
- if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
- HLog.warn ("baseuri " ^ value ^ " is not empty");
- HLog.message ("cleaning baseuri " ^ value);
- LibraryClean.clean_baseuris ~basedir [value]
- end;
- GrafiteTypes.add_metadata [LibraryNoDb.Baseuri value] status
- end else
- status
- in
- GrafiteTypes.set_option status name value
- | GrafiteAst.Drop loc -> raise Drop
- | GrafiteAst.Qed loc ->
- let uri, metasenv, bo, ty =
- match status.GrafiteTypes.proof_status with
- | GrafiteTypes.Proof (Some uri, metasenv, body, ty) ->
- uri, metasenv, body, ty
- | GrafiteTypes.Proof (None, metasenv, body, ty) ->
- raise (GrafiteTypes.Command_error
- ("Someone allows to start a theorem without giving the "^
- "name/uri. This should be fixed!"))
- | _->
- raise
- (GrafiteTypes.Command_error "You can't Qed an incomplete theorem")
- in
- if metasenv <> [] then
- raise
- (GrafiteTypes.Command_error
- "Proof not completed! metasenv is not empty!");
- let name = UriManager.name_of_uri uri in
- let obj = Cic.Constant (name,Some bo,ty,[],[]) in
- let status, _lemmas = add_obj uri obj status in
- (* should we assert lemmas = [] ? *)
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
- | GrafiteAst.Coercion (loc, uri, add_composites) ->
- eval_coercion status ~add_composites uri
- | GrafiteAst.Alias (loc, spec) ->
- let diff =
- (*CSC: Warning: this code should be factorized with the corresponding
- code in DisambiguatePp *)
- match spec with
- | GrafiteAst.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id id,
- (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
- | GrafiteAst.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),
- DisambiguateChoices.lookup_symbol_by_dsc symb desc]
- | GrafiteAst.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,
- DisambiguateChoices.lookup_num_by_dsc desc]
- in
- MatitaSync.set_proof_aliases status diff
- | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
- | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *)
- | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
- let status = GrafiteTypes.add_moo_content [stm] status in
- let uris =
- List.map
- (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
- (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
- in
- let diff =
- [DisambiguateTypes.Symbol (symbol, 0),
- DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
- in
- let status = MatitaSync.set_proof_aliases status diff in
- let status = GrafiteTypes.add_metadata uris status in
- status
- | GrafiteAst.Notation _ as stm -> GrafiteTypes.add_moo_content [stm] status
- | 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 uri =
- UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext)
- in
- let metasenv = GrafiteTypes.get_proof_metasenv status in
- match obj with
- | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
- let name = UriManager.name_of_uri uri in
- if not(CicPp.check name ty) then
- HLog.error ("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.empty_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;
- assert (metasenv = metasenv');
- let goalno =
- match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false
- in
- let initial_proof = (Some uri, metasenv, bo, ty) in
- let initial_stack = Continuationals.Stack.of_metasenv metasenv in
- { status with GrafiteTypes.proof_status =
- GrafiteTypes.Incomplete_proof
- { GrafiteTypes.proof = initial_proof; stack = initial_stack } }
- | _ ->
- 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 = add_coercions_of_record_to_moo obj lemmas status in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
-
-} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex ->
- match ex with
- | GrafiteAst.Tactical (_, tac, None) ->
- eval_tactical ~disambiguate_tactic status tac
- | GrafiteAst.Tactical (_, tac, Some punct) ->
- let status = eval_tactical ~disambiguate_tactic status tac in
- eval_tactical ~disambiguate_tactic status punct
- | GrafiteAst.Command (_, cmd) ->
- eval_command.ec_go ~baseuri_of_script ~disambiguate_command
- opts status cmd
- | GrafiteAst.Macro (_, mac) ->
-(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
- raise (Command_error
- (Printf.sprintf "The macro %s can't be in a script"
- (GrafiteAstPp.pp_macro_ast mac)))
-*) assert false
-
-} and eval_from_moo = {efm_go = fun status fname ->
- let ast_of_cmd cmd =
- GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
- GrafiteAst.Command (DisambiguateTypes.dummy_floc,
- cmd))
- in
- let moo = GrafiteMarshal.load_moo fname in
- List.iter
- (fun ast ->
- let ast = ast_of_cmd ast in
- status :=
- eval_ast.ea_go
- ~baseuri_of_script:(fun _ -> assert false)
- ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
- ~disambiguate_command:(fun status cmd -> status,cmd)
- !status ast)
- moo
-} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic
- ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
- st
-->
- let opts = {
- do_heavy_checks = do_heavy_checks ;
- clean_baseuri = clean_baseuri }
- in
- match st with
- | GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic
- ~disambiguate_command opts status ex
- | GrafiteAst.Comment (_,c) -> eval_comment status c
-}
-
-let eval_ast = eval_ast.ea_go
+++ /dev/null
-(* 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/
- *)
-
-exception Drop
-exception IncludedFileNotCompiled of string
-
-val eval_ast :
- baseuri_of_script:(string -> string) ->
-
- disambiguate_tactic:
- (GrafiteTypes.status ->
- ProofEngineTypes.goal ->
- ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
- GrafiteTypes.status ref *
- (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
-
- disambiguate_command:
- (GrafiteTypes.status ->
- 'obj GrafiteAst.command ->
- GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
-
- ?do_heavy_checks:bool ->
- ?clean_baseuri:bool ->
- GrafiteTypes.status ->
- ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
- GrafiteTypes.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/
- *)
-
-let is_empty buri =
- List.for_all
- (function
- Http_getter_types.Ls_section _ -> true
- | Http_getter_types.Ls_object _ -> false)
- (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
+++ /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/
- *)
-
- (** check whether no objects are defined below a given baseuri *)
-val is_empty: string -> bool
+++ /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/
- *)
-
-exception Option_error of string * string
-exception Statement_error of string
-exception Command_error of string
-
-let command_error msg = raise (Command_error msg)
-
-type incomplete_proof = {
- proof: ProofEngineTypes.proof;
- stack: Continuationals.Stack.t;
-}
-
-type proof_status =
- | No_proof
- | Incomplete_proof of incomplete_proof
- | Proof of ProofEngineTypes.proof
- | Intermediate of Cic.metasenv
- (* Status in which the proof could be while it is being processed by the
- * engine. No status entering/exiting the engine could be in it. *)
-
-module StringMap = Map.Make (String)
-type option_value =
- | String of string
- | Int of int
-type options = option_value StringMap.t
-let no_options = StringMap.empty
-
-type status = {
- aliases: DisambiguateTypes.environment;
- multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: GrafiteMarshal.moo;
- metadata: LibraryNoDb.metadata list;
- proof_status: proof_status;
- options: options;
- objects: UriManager.uri list;
- coercions: UriManager.uri list;
- notation_ids: CicNotation.notation_id list;
-}
-
-let get_current_proof status =
- match status.proof_status with
- | Incomplete_proof { proof = p } -> p
- | _ -> raise (Statement_error "no ongoing proof")
-
-let get_proof_metasenv status =
- match status.proof_status with
- | No_proof -> []
- | Proof (_, metasenv, _, _)
- | Incomplete_proof { proof = (_, metasenv, _, _) }
- | Intermediate metasenv ->
- metasenv
-
-let get_stack status =
- match status.proof_status with
- | Incomplete_proof p -> p.stack
- | Proof _ -> Continuationals.Stack.empty
- | _ -> assert false
-
-let set_stack stack status =
- match status.proof_status with
- | Incomplete_proof p ->
- { status with proof_status = Incomplete_proof { p with stack = stack } }
- | Proof _ ->
- assert (Continuationals.Stack.is_empty stack);
- status
- | _ -> assert false
-
-let set_metasenv metasenv status =
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
- Incomplete_proof
- { incomplete_proof with proof = (uri, metasenv, proof, ty) }
- | Intermediate _ -> Intermediate metasenv
- | Proof _ -> assert false
- in
- { status with proof_status = proof_status }
-
-let get_proof_context status goal =
- match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _) } ->
- let (_, context, _) = CicUtil.lookup_meta goal metasenv in
- context
- | _ -> []
-
-let get_proof_conclusion status goal =
- match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _) } ->
- let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
- conclusion
- | _ -> raise (Statement_error "no ongoing proof")
-
-let add_moo_content cmds status =
- let content = status.moo_content_rev in
- let content' =
- List.fold_right
- (fun cmd acc ->
-(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
- match cmd with
- | GrafiteAst.Interpretation _
- | GrafiteAst.Default _ ->
- if List.mem cmd content then acc
- else cmd :: acc
- | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
- cmd :: (List.filter ((<>) cmd) acc)
- | _ -> cmd :: acc)
- cmds content
- in
-(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
- GrafiteAstPp.pp_command content')); *)
- { status with moo_content_rev = content' }
-
-let get_option status name =
- try
- StringMap.find name status.options
- with Not_found -> raise (Option_error (name, "not found"))
-
-let set_option status name value =
- let mangle_dir s =
- let s = Str.global_replace (Str.regexp "//+") "/" s in
- let s = Str.global_replace (Str.regexp "/$") "" s in
- s
- in
- let types = [ "baseuri", (`String, mangle_dir); ] in
- let ty_and_mangler =
- try
- List.assoc name types
- with Not_found ->
- command_error (Printf.sprintf "Unknown option \"%s\"" name)
- in
- let value =
- match ty_and_mangler with
- | `String, f -> String (f value)
- | `Int, f ->
- (try
- Int (int_of_string (f value))
- with Failure _ ->
- command_error (Printf.sprintf "Not an integer value \"%s\"" value))
- in
- if StringMap.mem name status.options && name = "baseuri" then
- command_error "Redefinition of 'baseuri' is forbidden."
- else
- { status with options = StringMap.add name value status.options }
-
-
-let get_string_option status name =
- match get_option status name with
- | String s -> s
- | _ -> raise (Option_error (name, "not a string value"))
-
-let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
-
-let add_metadata new_metadata status =
- if Helm_registry.get_bool "db.nodb" then
- let metadata = status.metadata in
- let metadata' =
- List.fold_left
- (fun acc m ->
- match m with
- | LibraryNoDb.Dependency buri ->
- let is_self = (* self dependency *)
- try
- get_string_option status "baseuri" = buri
- with Option_error _ -> false (* baseuri not yet set *)
- in
- if is_self (* duplicate *)
- || List.exists (LibraryNoDb.eq_metadata m) metadata
- then acc
- else m :: acc
- | _ -> m :: acc)
- metadata new_metadata
- in
- { status with metadata = metadata' }
- else
- status
-
-let dump_status status =
- HLog.message "status.aliases:\n";
- HLog.message "status.proof_status:";
- HLog.message
- (match status.proof_status with
- | No_proof -> "no proof\n"
- | Incomplete_proof _ -> "incomplete proof\n"
- | Proof _ -> "proof\n"
- | Intermediate _ -> "Intermediate\n");
- HLog.message "status.options\n";
- StringMap.iter (fun k v ->
- let v =
- match v with
- | String s -> s
- | Int i -> string_of_int i
- in
- HLog.message (k ^ "::=" ^ v)) status.options;
- HLog.message "status.coercions\n";
- HLog.message "status.objects:\n";
- List.iter
- (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects
+++ /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/
- *)
-
-exception Option_error of string * string
-exception Statement_error of string
-exception Command_error of string
-
-type incomplete_proof = {
- proof: ProofEngineTypes.proof;
- stack: Continuationals.Stack.t;
-}
-
-type proof_status =
- No_proof
- | Incomplete_proof of incomplete_proof
- | Proof of ProofEngineTypes.proof
- | Intermediate of Cic.metasenv
-
-type option_value =
- | String of string
- | Int of int
-type options
-val no_options: options
-
-type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: GrafiteMarshal.moo;
- metadata: LibraryNoDb.metadata list;
- proof_status: proof_status; (** logical status *)
- options: options;
- objects: UriManager.uri list; (** in-scope objects *)
- coercions: UriManager.uri list; (** defined coercions *)
- notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
-}
-
-val dump_status : status -> unit
-
- (** list is not reversed, head command will be the first emitted *)
-val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
-val add_metadata: LibraryNoDb.metadata list -> status -> status
-
-val get_option : status -> string -> option_value
-val get_string_option : status -> string -> string
-val set_option : status -> string -> string -> status
-
-val qualify: status -> string -> string
-
-val get_current_proof: status -> ProofEngineTypes.proof
-val get_proof_metasenv: status -> Cic.metasenv
-val get_stack: status -> Continuationals.Stack.t
-val get_proof_context : status -> int -> Cic.context
-val get_proof_conclusion : status -> int -> Cic.term
-
-val set_stack: Continuationals.Stack.t -> status -> status
-val set_metasenv: Cic.metasenv -> status -> 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/
- *)
-
-open Printf
-
-open GrafiteTypes
-
-let alias_diff ~from status =
- let module Map = DisambiguateTypes.Environment in
- Map.fold
- (fun domain_item (description1,_ as codomain_item) acc ->
- try
- let description2,_ = Map.find domain_item from.aliases in
- if description1 <> description2 then
- (domain_item,codomain_item)::acc
- else
- acc
- with
- Not_found ->
- (domain_item,codomain_item)::acc)
- status.aliases []
-
-let alias_diff =
- let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
-
-let set_proof_aliases status new_aliases =
- let commands_of_aliases =
- List.map
- (fun alias -> GrafiteAst.Alias (DisambiguateTypes.dummy_floc, alias))
- in
- let deps_of_aliases =
- HExtlib.filter_map
- (function
- | GrafiteAst.Ident_alias (_, suri) ->
- let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
- Some (LibraryNoDb.Dependency buri)
- | _ -> None)
- in
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status.aliases new_aliases in
- let multi_aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
- status.multi_aliases new_aliases in
- let new_status =
- { status with multi_aliases = multi_aliases ; aliases = aliases}
- in
- if new_aliases = [] then
- new_status
- else
- let aliases =
- DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
- in
- let status = add_moo_content (commands_of_aliases aliases) new_status in
- let status = add_metadata (deps_of_aliases aliases) status in
- status
-
-(** given a uri and a type list (the contructors types) builds a list of pairs
- * (name,uri) that is used to generate automatic aliases **)
-let extract_alias types uri =
- fst(List.fold_left (
- fun (acc,i) (name, _, _, cl) ->
- (name, UriManager.uri_of_uriref uri i None) ::
- (fst(List.fold_left (
- fun (acc,j) (name,_) ->
- (((name,UriManager.uri_of_uriref uri i
- (Some j)) :: acc) , j+1)
- ) (acc,1) cl)),i+1
- ) ([],0) types)
-
-let build_aliases =
- List.map
- (fun (name,uri) ->
- DisambiguateTypes.Id name,
- (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
-
-let add_aliases_for_inductive_def status types uri =
- let aliases = build_aliases (extract_alias types uri) in
- set_proof_aliases status aliases
-
-let add_alias_for_constant status uri =
- let name = UriManager.name_of_uri uri in
- let new_env = build_aliases [(name,uri)] in
- set_proof_aliases status new_env
-
-let add_aliases_for_object status uri =
- function
- Cic.InductiveDefinition (types,_,_,_) ->
- add_aliases_for_inductive_def status types uri
- | Cic.Constant _ -> add_alias_for_constant status uri
- | Cic.Variable _
- | Cic.CurrentProof _ -> assert false
-
-let add_obj uri obj lemmas status =
- List.fold_left add_alias_for_constant
- (add_aliases_for_object status uri obj) lemmas
-
-let add_obj =
- let profiler = HExtlib.profile "add_obj" in
- fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
-
-let add_coercion status uri compounds =
- let status = {status with coercions = uri :: status.coercions} in
- List.fold_left add_alias_for_constant status compounds
-
-module OrderedUri =
-struct
- type t = UriManager.uri * string
- let compare (u1, _) (u2, _) = UriManager.compare u1 u2
-end
-
-module OrderedId =
-struct
- type t = CicNotation.notation_id
- let compare = Pervasives.compare
-end
-
-module UriSet = Set.Make (OrderedUri)
-module IdSet = Set.Make (OrderedId)
-
- (** @return l2 \ l1 *)
-let uri_list_diff l2 l1 =
- let module S = UriManager.UriSet in
- let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
- let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
- let diff = S.diff s2 s1 in
- S.fold (fun uri uris -> uri :: uris) diff []
-
- (** @return l2 \ l1 *)
-let id_list_diff l2 l1 =
- let module S = IdSet in
- let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
- let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
- let diff = S.diff s2 s1 in
- S.fold (fun uri uris -> uri :: uris) diff []
-
-let time_travel ~present ~past =
- let objs_to_remove = uri_list_diff present.objects past.objects in
- let coercions_to_remove = uri_list_diff present.coercions past.coercions in
- let notation_to_remove =
- id_list_diff present.notation_ids past.notation_ids
- in
- let debug_list = ref [] in
- List.iter
- (fun uri -> LibrarySync.remove_coercion uri)
- coercions_to_remove;
- List.iter LibrarySync.remove_obj objs_to_remove;
- List.iter CicNotation.remove_notation notation_to_remove
-
-let init () =
- LibrarySync.remove_all_coercions ();
- LibraryObjects.reset_defaults ();
- {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- moo_content_rev = [];
- metadata = [];
- proof_status = No_proof;
- options = no_options;
- objects = [];
- coercions = [];
- notation_ids = [];
- }
-
-
+++ /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/
- *)
-
-val add_obj:
- UriManager.uri -> Cic.obj -> UriManager.uri list ->
- GrafiteTypes.status -> GrafiteTypes.status
-
-val add_coercion:
- GrafiteTypes.status -> UriManager.uri -> UriManager.uri list ->
- GrafiteTypes.status
-
-val time_travel:
- present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
-
- (** perform a diff between the aliases contained in two statuses, assuming
- * that the second one can only have more aliases than the first one
- * @return the list of aliases that should be added to aliases of from in
- * order to be equal to aliases of the second argument *)
-val alias_diff:
- from:GrafiteTypes.status -> GrafiteTypes.status ->
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
-
- (** set the proof aliases enriching the moo_content *)
-val set_proof_aliases :
- GrafiteTypes.status ->
- (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
- GrafiteTypes.status
-
- (* also resets the imperative part of the status *)
-val init: unit -> GrafiteTypes.status
-
-
--- /dev/null
+*.cm[iaox]
+*.cmxa
+test_dep
+test_parser
+print_grammar
--- /dev/null
+grafiteSync.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
+grafiteMisc.cmo: grafiteMisc.cmi
+grafiteMisc.cmx: grafiteMisc.cmi
+grafiteEngine.cmo: grafiteTypes.cmi grafiteSync.cmi grafiteMisc.cmi \
+ grafiteEngine.cmi
+grafiteEngine.cmx: grafiteTypes.cmx grafiteSync.cmx grafiteMisc.cmx \
+ grafiteEngine.cmi
--- /dev/null
+PACKAGE = grafite_engine
+PREDICATES =
+
+INTERFACE_FILES = \
+ grafiteTypes.mli \
+ grafiteSync.mli \
+ grafiteMisc.mli \
+ grafiteEngine.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+
+include ../Makefile.common
--- /dev/null
+(* 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/
+ *)
+
+exception Drop
+exception IncludedFileNotCompiled of string (* file name *)
+
+type options = {
+ do_heavy_checks: bool ;
+ clean_baseuri: bool
+}
+
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+ * names as long as they are available, then it fallbacks to name generation
+ * using FreshNamesGenerator module *)
+let namer_of names =
+ let len = List.length names in
+ let count = ref 0 in
+ fun metasenv context name ~typ ->
+ if !count < len then begin
+ let name = Cic.Name (List.nth names !count) in
+ incr count;
+ name
+ end else
+ FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
+
+let tactic_of_ast ast =
+ let module PET = ProofEngineTypes in
+ match ast with
+ | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
+ | GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.Assumption _ -> Tactics.assumption
+ | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
+ AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
+ ~dbd:(LibraryDb.instance ()) ()
+ | GrafiteAst.Change (_, pattern, with_what) ->
+ Tactics.change ~pattern with_what
+ | GrafiteAst.Clear (_,id) -> Tactics.clear id
+ | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
+ | GrafiteAst.Contradiction _ -> Tactics.contradiction
+ | GrafiteAst.Compare (_, term) -> Tactics.compare term
+ | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
+ | GrafiteAst.Cut (_, ident, term) ->
+ let names = match ident with None -> [] | Some id -> [id] in
+ Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
+ | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
+ | GrafiteAst.Decompose (_, types, what, names) ->
+ let to_type = function
+ | GrafiteAst.Type (uri, typeno) -> uri, typeno
+ | GrafiteAst.Ident _ -> assert false
+ in
+ let user_types = List.rev_map to_type types in
+ let dbd = LibraryDb.instance () in
+ let mk_fresh_name_callback = namer_of names in
+ Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+ | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
+ | GrafiteAst.Elim (_, what, using, depth, names) ->
+ Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+ what
+ | GrafiteAst.ElimType (_, what, using, depth, names) ->
+ Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
+ what
+ | GrafiteAst.Exact (_, term) -> Tactics.exact term
+ | GrafiteAst.Exists _ -> Tactics.exists
+ | GrafiteAst.Fail _ -> Tactics.fail
+ | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
+ let reduction =
+ match reduction_kind with
+ | `Normalize ->
+ PET.const_lazy_reduction
+ (CicReduction.normalize ~delta:false ~subst:[])
+ | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
+ | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
+ | `Unfold None ->
+ PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
+ | `Unfold (Some lazy_term) ->
+ (fun context metasenv ugraph ->
+ let what, metasenv, ugraph = lazy_term context metasenv ugraph in
+ ProofEngineReduction.unfold ~what, metasenv, ugraph)
+ | `Whd ->
+ PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[])
+ in
+ Tactics.fold ~reduction ~term ~pattern
+ | GrafiteAst.Fourier _ -> Tactics.fourier
+ | GrafiteAst.FwdSimpl (_, hyp, names) ->
+ Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
+ ~dbd:(LibraryDb.instance ()) hyp
+ | GrafiteAst.Generalize (_,pattern,ident) ->
+ let names = match ident with None -> [] | Some id -> [id] in
+ Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
+ | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
+ | GrafiteAst.IdTac _ -> Tactics.id
+ | GrafiteAst.Injection (_,term) -> Tactics.injection term
+ | GrafiteAst.Intros (_, None, names) ->
+ PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
+ | GrafiteAst.Intros (_, Some num, names) ->
+ PrimitiveTactics.intros_tac ~howmany:num
+ ~mk_fresh_name_callback:(namer_of names) ()
+ | GrafiteAst.Inversion (_, term) ->
+ Tactics.inversion term
+ | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+ let names = match ident with None -> [] | Some id -> [id] in
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
+ ~to_what what
+ | GrafiteAst.Left _ -> Tactics.left
+ | GrafiteAst.LetIn (loc,term,name) ->
+ Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
+ | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
+ (match reduction_kind with
+ | `Normalize -> Tactics.normalize ~pattern
+ | `Reduce -> Tactics.reduce ~pattern
+ | `Simpl -> Tactics.simpl ~pattern
+ | `Unfold what -> Tactics.unfold ~pattern what
+ | `Whd -> Tactics.whd ~pattern)
+ | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
+ | GrafiteAst.Replace (_, pattern, with_what) ->
+ Tactics.replace ~pattern ~with_what
+ | GrafiteAst.Rewrite (_, direction, t, pattern) ->
+ EqualityTactics.rewrite_tac ~direction ~pattern t
+ | GrafiteAst.Right _ -> Tactics.right
+ | GrafiteAst.Ring _ -> Tactics.ring
+ | GrafiteAst.Split _ -> Tactics.split
+ | GrafiteAst.Symmetry _ -> Tactics.symmetry
+ | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+
+(* maybe we only need special cases for apply and goal *)
+let classify_tactic tactic =
+ match tactic with
+ (* tactics that can't close the goal (return a goal we want to "select") *)
+ | GrafiteAst.Rewrite _
+ | GrafiteAst.Split _
+ | GrafiteAst.Replace _
+ | GrafiteAst.Reduce _
+ | GrafiteAst.Injection _
+ | GrafiteAst.IdTac _
+ | GrafiteAst.Generalize _
+ | GrafiteAst.Elim _
+ | GrafiteAst.Cut _
+ | GrafiteAst.Decompose _ -> true, true
+ (* tactics we don't want to reorder goals. I think only Goal needs this. *)
+ | GrafiteAst.Goal _ -> false, true
+ (* tactics like apply *)
+ | _ -> true, false
+
+let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
+ let module PEH = ProofEngineHelpers in
+(* let print_m name metasenv =
+ prerr_endline (">>>>> " ^ name);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)
+ in *)
+ (* phase one calculates:
+ * new_goals_from_refine: goals added by refine
+ * head_goal: the first goal opened by ythe tactic
+ * other_goals: other goals opened by the tactic
+ *)
+ let new_goals_from_refine = PEH.compare_metasenvs start refine in
+ let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
+ let head_goal, other_goals, goals =
+ match goals with
+ | [] -> None,[],goals
+ | hd::tl ->
+ (* assert (List.mem hd new_goals_from_tactic);
+ * invalidato dalla goal_tac
+ * *)
+ Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
+ hd) goals
+ in
+ let produced_goals =
+ match head_goal with
+ | None -> new_goals_from_refine @ other_goals
+ | Some x -> x :: new_goals_from_refine @ other_goals
+ in
+ (* extract the metas generated by refine and tactic *)
+ let metas_for_tactic_head =
+ match head_goal with
+ | None -> []
+ | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
+ let metas_for_tactic_goals =
+ List.map
+ (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
+ goals
+ in
+ let metas_for_refine_goals =
+ List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
+ let produced_metas, goals =
+ let produced_metas =
+ if always_opens_a_goal then
+ metas_for_tactic_head @ metas_for_refine_goals @
+ metas_for_tactic_goals
+ else begin
+(* print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals; *)
+ metas_for_refine_goals @ metas_for_tactic_head @
+ metas_for_tactic_goals
+ end
+ in
+ let goals = List.map (fun (metano, _, _) -> metano) produced_metas in
+ produced_metas, goals
+ in
+ (* residual metas, preserving the original order *)
+ let before, after =
+ let rec split e =
+ function
+ | [] -> [],[]
+ | (metano, _, _) :: tl when metano = e ->
+ [], List.map (fun (x,_,_) -> x) tl
+ | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
+ in
+ let find n metasenv =
+ try
+ Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
+ with Not_found -> None
+ in
+ let extract l =
+ List.fold_right
+ (fun n acc ->
+ match find n tactic with
+ | Some x -> x::acc
+ | None -> acc
+ ) l [] in
+ let before_l, after_l = split current_goal start in
+ let before_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) before_l in
+ let after_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) after_l in
+ let before = extract before_l in
+ let after = extract after_l in
+ before, after
+ in
+(* |+ DEBUG CODE +|
+ print_m "BEGIN" start;
+ prerr_endline ("goal was: " ^ string_of_int current_goal);
+ prerr_endline ("and metas from refine are:");
+ List.iter
+ (fun t -> prerr_string (" " ^ string_of_int t))
+ new_goals_from_refine;
+ prerr_endline "";
+ print_m "before" before;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals;
+ print_m "produced_metas" produced_metas;
+ print_m "after" after;
+|+ FINE DEBUG CODE +| *)
+ before @ produced_metas @ after, goals
+
+let apply_tactic ~disambiguate_tactic tactic (status, goal) =
+(* prerr_endline "apply_tactic"; *)
+(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *)
+ let starting_metasenv = GrafiteTypes.get_proof_metasenv status in
+ let before = List.map (fun g, _, _ -> g) starting_metasenv in
+(* prerr_endline "disambiguate"; *)
+ let status, tactic = disambiguate_tactic status goal tactic in
+ let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in
+ let proof = GrafiteTypes.get_current_proof status in
+ let proof_status = proof, goal in
+ let needs_reordering, always_opens_a_goal = classify_tactic tactic in
+ let tactic = tactic_of_ast tactic in
+ (* apply tactic will change the lexicon_status ... *)
+(* prerr_endline "apply_tactic bassa"; *)
+ let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
+ let after = ProofEngineTypes.goals_of_proof proof in
+ let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
+(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before));
+prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after));
+prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *)
+(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals));
+prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *)
+ let proof, opened_goals =
+ if needs_reordering then begin
+ let uri, metasenv_after_tactic, t, ty = proof in
+(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *)
+ let reordered_metasenv, opened_goals =
+ reorder_metasenv
+ starting_metasenv
+ metasenv_after_refinement metasenv_after_tactic
+ opened goal always_opens_a_goal
+ in
+ let proof' = uri, reordered_metasenv, t, ty in
+(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *)
+ proof', opened_goals
+ end
+ else
+ proof, opened_goals
+ in
+ let incomplete_proof =
+ match status.GrafiteTypes.proof_status with
+ | GrafiteTypes.Incomplete_proof p -> p
+ | _ -> assert false
+ in
+ { status with GrafiteTypes.proof_status =
+ GrafiteTypes.Incomplete_proof
+ { incomplete_proof with GrafiteTypes.proof = proof } },
+ opened_goals, closed_goals
+
+type eval_ast =
+ {ea_go:
+ 'term 'lazy_term 'reduction 'obj 'ident.
+ disambiguate_tactic:
+ (GrafiteTypes.status ->
+ ProofEngineTypes.goal ->
+ ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
+ GrafiteTypes.status *
+ (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
+
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+
+ ?do_heavy_checks:bool ->
+ ?clean_baseuri:bool ->
+ GrafiteTypes.status ->
+ ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
+ GrafiteTypes.status * UriManager.uri list
+ }
+
+type 'a eval_command =
+ {ec_go: 'term 'obj.
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ options -> GrafiteTypes.status -> 'obj GrafiteAst.command ->
+ GrafiteTypes.status * UriManager.uri list
+ }
+
+type 'a eval_executable =
+ {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
+ disambiguate_tactic:
+ (GrafiteTypes.status ->
+ ProofEngineTypes.goal ->
+ ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
+ GrafiteTypes.status *
+ (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
+
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+
+ options ->
+ GrafiteTypes.status ->
+ ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code ->
+ GrafiteTypes.status * UriManager.uri list
+ }
+
+type 'a eval_from_moo =
+ { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status }
+
+let coercion_moo_statement_of uri =
+ GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+
+let eval_coercion status ~add_composites uri =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let status,compounds =
+ GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+ let moo_content = coercion_moo_statement_of uri in
+ let status = GrafiteTypes.add_moo_content [moo_content] status in
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ compounds
+
+let eval_tactical ~disambiguate_tactic status tac =
+ let apply_tactic = apply_tactic ~disambiguate_tactic in
+ let module MatitaStatus =
+ struct
+ type input_status = GrafiteTypes.status * ProofEngineTypes.goal
+
+ type output_status =
+ GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
+
+ type tactic = input_status -> output_status
+
+ let id_tactic = apply_tactic (GrafiteAst.IdTac HExtlib.dummy_floc)
+ let mk_tactic tac = tac
+ let apply_tactic tac = tac
+ let goals (_, opened, closed) = opened, closed
+ let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
+ let get_stack (status, _) = GrafiteTypes.get_stack status
+
+ let set_stack stack (status, opened, closed) =
+ GrafiteTypes.set_stack stack status, opened, closed
+
+ let inject (status, _) = (status, [], [])
+ let focus goal (status, _, _) = (status, goal)
+ end
+ in
+ let module MatitaTacticals = Tacticals.Make (MatitaStatus) in
+ let rec tactical_of_ast l tac =
+ match tac with
+ | GrafiteAst.Tactic (loc, tactic) ->
+ MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
+ | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
+ assert (l > 0);
+ MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
+ | GrafiteAst.Do (loc, n, tactical) ->
+ MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Repeat (loc, tactical) ->
+ MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
+ assert (l > 0);
+ MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
+ ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
+ | GrafiteAst.First (loc, tacticals) ->
+ MatitaTacticals.first
+ ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
+ | GrafiteAst.Try (loc, tactical) ->
+ MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Solve (loc, tacticals) ->
+ MatitaTacticals.solve_tactics
+ ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
+
+ | GrafiteAst.Skip loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ in
+ let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
+ let status = (* is proof completed? *)
+ match status.GrafiteTypes.proof_status with
+ | GrafiteTypes.Incomplete_proof
+ { GrafiteTypes.stack = stack; proof = proof }
+ when Continuationals.Stack.is_empty stack ->
+ { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof }
+ | _ -> status
+ in
+ status
+
+let eval_comment status c = status
+
+(* since the record syntax allows to declare coercions, we have to put this
+ * information inside the moo *)
+let add_coercions_of_record_to_moo obj lemmas status =
+ let attributes = CicUtil.attributes_of_obj obj in
+ let is_record = function `Class (`Record att) -> Some att | _-> None in
+ match HExtlib.list_findopt is_record attributes with
+ | None -> status,[]
+ | Some fields ->
+ let is_a_coercion uri =
+ try
+ let obj,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let attrs = CicUtil.attributes_of_obj obj in
+ List.mem (`Class `Projection) attrs
+ with Not_found -> assert false
+ in
+ (* looking at the fields we can know the 'wanted' coercions, but not the
+ * actually generated ones. So, only the intersection between the wanted
+ * and the actual should be in the moo as coercion, while everithing in
+ * lemmas should go as aliases *)
+ let wanted_coercions =
+ HExtlib.filter_map
+ (function
+ | (name,true) ->
+ Some
+ (UriManager.uri_of_string
+ (GrafiteTypes.qualify status name ^ ".con"))
+ | _ -> None)
+ fields
+ in
+ prerr_endline "wanted coercions:";
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ wanted_coercions;
+ let coercions, moo_content =
+ List.split
+ (HExtlib.filter_map
+ (fun uri ->
+ let is_a_wanted_coercion =
+ List.exists (UriManager.eq uri) wanted_coercions in
+ if is_a_coercion uri && is_a_wanted_coercion then
+ Some (uri, coercion_moo_statement_of uri)
+ else
+ None)
+ lemmas)
+ in
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ coercions;
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ let basedir = Helm_registry.get "matita.basedir" in
+ List.fold_left
+ (fun (status,lemmas) uri ->
+ let status,new_lemmas =
+ GrafiteSync.add_coercion ~basedir ~add_composites:true status uri
+ in
+ status,new_lemmas@lemmas
+ ) (status,[]) coercions
+
+let add_obj uri obj status =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ status, lemmas
+
+let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
+ let status,cmd = disambiguate_command status cmd in
+ let basedir = Helm_registry.get "matita.basedir" in
+ let status,uris =
+ match cmd with
+ | GrafiteAst.Default (loc, what, uris) as cmd ->
+ LibraryObjects.set_default what uris;
+ GrafiteTypes.add_moo_content [cmd] status,[]
+ | GrafiteAst.Include (loc, baseuri) ->
+ let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
+ if not (Sys.file_exists moopath) then
+ raise (IncludedFileNotCompiled moopath);
+ let status = eval_from_moo.efm_go status moopath in
+ status,[]
+ | GrafiteAst.Set (loc, name, value) ->
+ if name = "baseuri" then begin
+ let value =
+ let v = Http_getter_misc.strip_trailing_slash value in
+ try
+ ignore (String.index v ' ');
+ raise (GrafiteTypes.Command_error "baseuri can't contain spaces")
+ with Not_found -> v
+ in
+ if not (GrafiteMisc.is_empty value) && opts.clean_baseuri then begin
+ HLog.warn ("baseuri " ^ value ^ " is not empty");
+ HLog.message ("cleaning baseuri " ^ value);
+ LibraryClean.clean_baseuris ~basedir [value];
+ end;
+ end;
+ GrafiteTypes.set_option status name value,[]
+ | GrafiteAst.Drop loc -> raise Drop
+ | GrafiteAst.Qed loc ->
+ let uri, metasenv, bo, ty =
+ match status.GrafiteTypes.proof_status with
+ | GrafiteTypes.Proof (Some uri, metasenv, body, ty) ->
+ uri, metasenv, body, ty
+ | GrafiteTypes.Proof (None, metasenv, body, ty) ->
+ raise (GrafiteTypes.Command_error
+ ("Someone allows to start a theorem without giving the "^
+ "name/uri. This should be fixed!"))
+ | _->
+ raise
+ (GrafiteTypes.Command_error "You can't Qed an incomplete theorem")
+ in
+ if metasenv <> [] then
+ raise
+ (GrafiteTypes.Command_error
+ "Proof not completed! metasenv is not empty!");
+ let name = UriManager.name_of_uri uri in
+ let obj = Cic.Constant (name,Some bo,ty,[],[]) in
+ let status, lemmas = add_obj uri obj status in
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ uri::lemmas
+ | GrafiteAst.Coercion (loc, uri, add_composites) ->
+ eval_coercion status ~add_composites uri
+ | 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 uri =
+ UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext)
+ in
+ let metasenv = GrafiteTypes.get_proof_metasenv status in
+ match obj with
+ | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
+ let name = UriManager.name_of_uri uri in
+ if not(CicPp.check name ty) then
+ HLog.error ("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.empty_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;
+ assert (metasenv = metasenv');
+ let goalno =
+ match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false
+ in
+ let initial_proof = (Some uri, metasenv, bo, ty) in
+ let initial_stack = Continuationals.Stack.of_metasenv metasenv in
+ { status with GrafiteTypes.proof_status =
+ GrafiteTypes.Incomplete_proof
+ { GrafiteTypes.proof = initial_proof; stack = initial_stack } },
+ []
+ | _ ->
+ 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_record_to_moo obj lemmas status
+ in
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+ uri::new_lemmas@lemmas
+ in
+ match status.GrafiteTypes.proof_status with
+ GrafiteTypes.Intermediate _ ->
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
+ | _ -> status,uris
+
+} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+ match ex with
+ | GrafiteAst.Tactical (_, tac, None) ->
+ eval_tactical ~disambiguate_tactic status tac,[]
+ | GrafiteAst.Tactical (_, tac, Some punct) ->
+ let status = eval_tactical ~disambiguate_tactic status tac in
+ eval_tactical ~disambiguate_tactic status punct,[]
+ | GrafiteAst.Command (_, cmd) ->
+ eval_command.ec_go ~disambiguate_command opts status cmd
+ | GrafiteAst.Macro (_, mac) ->
+(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
+ raise (Command_error
+ (Printf.sprintf "The macro %s can't be in a script"
+ (GrafiteAstPp.pp_macro_ast mac)))
+*) assert false
+
+} and eval_from_moo = {efm_go = fun status fname ->
+ let ast_of_cmd cmd =
+ GrafiteAst.Executable (HExtlib.dummy_floc,
+ GrafiteAst.Command (HExtlib.dummy_floc,
+ cmd))
+ in
+ let moo = GrafiteMarshal.load_moo fname in
+ List.fold_left
+ (fun status ast ->
+ let ast = ast_of_cmd ast in
+ let status,lemmas =
+ eval_ast.ea_go
+ ~disambiguate_tactic:(fun status _ tactic -> status,tactic)
+ ~disambiguate_command:(fun status cmd -> status,cmd)
+ status ast
+ in
+ assert (lemmas=[]);
+ status)
+ status moo
+} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+ st
+->
+ let opts = {
+ do_heavy_checks = do_heavy_checks ;
+ clean_baseuri = clean_baseuri }
+ in
+ match st with
+ | GrafiteAst.Executable (_,ex) ->
+ eval_executable.ee_go ~disambiguate_tactic
+ ~disambiguate_command opts status ex
+ | GrafiteAst.Comment (_,c) -> eval_comment status c,[]
+}
+
+let eval_ast = eval_ast.ea_go
--- /dev/null
+(* 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/
+ *)
+
+exception Drop
+exception IncludedFileNotCompiled of string
+
+val eval_ast :
+ disambiguate_tactic:
+ (GrafiteTypes.status ->
+ ProofEngineTypes.goal ->
+ ('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic ->
+ GrafiteTypes.status *
+ (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
+
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+
+ ?do_heavy_checks:bool ->
+ ?clean_baseuri:bool ->
+ GrafiteTypes.status ->
+ ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
+ (* the new status and generated objects, if any *)
+ GrafiteTypes.status * UriManager.uri list
--- /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/
+ *)
+
+let is_empty buri =
+ List.for_all
+ (function
+ Http_getter_types.Ls_section _ -> true
+ | Http_getter_types.Ls_object _ -> false)
+ (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
--- /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/
+ *)
+
+ (** check whether no objects are defined below a given baseuri *)
+val is_empty: string -> bool
--- /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/
+ *)
+
+open Printf
+
+let add_obj ~basedir uri obj status =
+ let lemmas = LibrarySync.add_obj uri obj basedir in
+ {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
+ lemmas
+
+let add_coercion ~basedir ~add_composites status uri =
+ let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
+ {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
+ compounds
+
+module OrderedUri =
+struct
+ type t = UriManager.uri * string
+ let compare (u1, _) (u2, _) = UriManager.compare u1 u2
+end
+
+module UriSet = Set.Make (OrderedUri)
+
+ (** @return l2 \ l1 *)
+let uri_list_diff l2 l1 =
+ let module S = UriManager.UriSet in
+ let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+ let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+ let diff = S.diff s2 s1 in
+ S.fold (fun uri uris -> uri :: uris) diff []
+
+let time_travel ~present ~past =
+ let objs_to_remove =
+ uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
+ let coercions_to_remove =
+ uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions
+ in
+ List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
+ List.iter LibrarySync.remove_obj objs_to_remove
+
+let init () =
+ LibrarySync.remove_all_coercions ();
+ LibraryObjects.reset_defaults ();
+ {
+ GrafiteTypes.moo_content_rev = [];
+ proof_status = GrafiteTypes.No_proof;
+ options = GrafiteTypes.no_options;
+ objects = [];
+ coercions = [];
+ }
--- /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/
+ *)
+
+val add_obj:
+ basedir:string -> UriManager.uri -> Cic.obj -> GrafiteTypes.status ->
+ GrafiteTypes.status * UriManager.uri list
+
+val add_coercion:
+ basedir:string -> add_composites:bool -> GrafiteTypes.status ->
+ UriManager.uri -> GrafiteTypes.status * UriManager.uri list
+
+val time_travel:
+ present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
+
+ (* also resets the imperative part of the status *)
+val init: unit -> GrafiteTypes.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/
+ *)
+
+exception Option_error of string * string
+exception Statement_error of string
+exception Command_error of string
+
+let command_error msg = raise (Command_error msg)
+
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
+type proof_status =
+ | No_proof
+ | Incomplete_proof of incomplete_proof
+ | Proof of ProofEngineTypes.proof
+ | Intermediate of Cic.metasenv
+ (* Status in which the proof could be while it is being processed by the
+ * engine. No status entering/exiting the engine could be in it. *)
+
+module StringMap = Map.Make (String)
+type option_value =
+ | String of string
+ | Int of int
+type options = option_value StringMap.t
+let no_options = StringMap.empty
+
+type status = {
+ moo_content_rev: GrafiteMarshal.moo;
+ proof_status: proof_status;
+ options: options;
+ objects: UriManager.uri list;
+ coercions: UriManager.uri list;
+}
+
+let get_current_proof status =
+ match status.proof_status with
+ | Incomplete_proof { proof = p } -> p
+ | _ -> raise (Statement_error "no ongoing proof")
+
+let get_proof_metasenv status =
+ match status.proof_status with
+ | No_proof -> []
+ | Proof (_, metasenv, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _) }
+ | Intermediate metasenv ->
+ metasenv
+
+let get_stack status =
+ match status.proof_status with
+ | Incomplete_proof p -> p.stack
+ | Proof _ -> Continuationals.Stack.empty
+ | _ -> assert false
+
+let set_stack stack status =
+ match status.proof_status with
+ | Incomplete_proof p ->
+ { status with proof_status = Incomplete_proof { p with stack = stack } }
+ | Proof _ ->
+ assert (Continuationals.Stack.is_empty stack);
+ status
+ | _ -> assert false
+
+let set_metasenv metasenv status =
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) ->
+ Incomplete_proof
+ { incomplete_proof with proof = (uri, metasenv, proof, ty) }
+ | Intermediate _ -> Intermediate metasenv
+ | Proof (_, metasenv', _, _) ->
+ assert (metasenv = metasenv');
+ status.proof_status
+ in
+ { status with proof_status = proof_status }
+
+let get_proof_context status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
+ context
+ | _ -> []
+
+let get_proof_conclusion status goal =
+ match status.proof_status with
+ | Incomplete_proof { proof = (_, metasenv, _, _) } ->
+ let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
+ conclusion
+ | _ -> raise (Statement_error "no ongoing proof")
+
+let add_moo_content cmds status =
+ let content = status.moo_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc ->
+(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+ match cmd with
+ | GrafiteAst.Default _ ->
+ if List.mem cmd content then acc
+ else cmd :: acc
+ | _ -> cmd :: acc)
+ cmds content
+ in
+(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
+ GrafiteAstPp.pp_command content')); *)
+ { status with moo_content_rev = content' }
+
+let get_option status name =
+ try
+ StringMap.find name status.options
+ with Not_found -> raise (Option_error (name, "not found"))
+
+let set_option status name value =
+ let mangle_dir s =
+ let s = Str.global_replace (Str.regexp "//+") "/" s in
+ let s = Str.global_replace (Str.regexp "/$") "" s in
+ s
+ in
+ let types = [ "baseuri", (`String, mangle_dir); ] in
+ let ty_and_mangler =
+ try
+ List.assoc name types
+ with Not_found ->
+ command_error (Printf.sprintf "Unknown option \"%s\"" name)
+ in
+ let value =
+ match ty_and_mangler with
+ | `String, f -> String (f value)
+ | `Int, f ->
+ (try
+ Int (int_of_string (f value))
+ with Failure _ ->
+ command_error (Printf.sprintf "Not an integer value \"%s\"" value))
+ in
+ if StringMap.mem name status.options && name = "baseuri" then
+ command_error "Redefinition of 'baseuri' is forbidden."
+ else
+ { status with options = StringMap.add name value status.options }
+
+
+let get_string_option status name =
+ match get_option status name with
+ | String s -> s
+ | _ -> raise (Option_error (name, "not a string value"))
+
+let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
+
+let dump_status status =
+ HLog.message "status.aliases:\n";
+ HLog.message "status.proof_status:";
+ HLog.message
+ (match status.proof_status with
+ | No_proof -> "no proof\n"
+ | Incomplete_proof _ -> "incomplete proof\n"
+ | Proof _ -> "proof\n"
+ | Intermediate _ -> "Intermediate\n");
+ HLog.message "status.options\n";
+ StringMap.iter (fun k v ->
+ let v =
+ match v with
+ | String s -> s
+ | Int i -> string_of_int i
+ in
+ HLog.message (k ^ "::=" ^ v)) status.options;
+ HLog.message "status.coercions\n";
+ HLog.message "status.objects:\n";
+ List.iter
+ (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects
--- /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/
+ *)
+
+exception Option_error of string * string
+exception Statement_error of string
+exception Command_error of string
+
+type incomplete_proof = {
+ proof: ProofEngineTypes.proof;
+ stack: Continuationals.Stack.t;
+}
+
+type proof_status =
+ No_proof
+ | Incomplete_proof of incomplete_proof
+ | Proof of ProofEngineTypes.proof
+ | Intermediate of Cic.metasenv
+
+type option_value =
+ | String of string
+ | Int of int
+type options
+val no_options: options
+
+type status = {
+ moo_content_rev: GrafiteMarshal.moo;
+ proof_status: proof_status; (** logical status *)
+ options: options;
+ objects: UriManager.uri list; (** in-scope objects *)
+ coercions: UriManager.uri list; (** defined coercions *)
+}
+
+val dump_status : status -> unit
+
+ (** list is not reversed, head command will be the first emitted *)
+val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
+
+val get_option : status -> string -> option_value
+val get_string_option : status -> string -> string
+val set_option : status -> string -> string -> status
+
+val qualify: status -> string -> string
+
+val get_current_proof: status -> ProofEngineTypes.proof
+val get_proof_metasenv: status -> Cic.metasenv
+val get_stack: status -> Continuationals.Stack.t
+val get_proof_context : status -> int -> Cic.context
+val get_proof_conclusion : status -> int -> Cic.term
+
+val set_stack: Continuationals.Stack.t -> status -> status
+val set_metasenv: Cic.metasenv -> status -> status
-grafiteParser.cmo: grafiteParser.cmi
-grafiteParser.cmx: grafiteParser.cmi
+dependenciesParser.cmo: dependenciesParser.cmi
+dependenciesParser.cmx: dependenciesParser.cmi
+grafiteParser.cmo: dependenciesParser.cmi grafiteParser.cmi
+grafiteParser.cmx: dependenciesParser.cmx grafiteParser.cmi
cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
-matitaDisambiguator.cmo: matitaDisambiguator.cmi
-matitaDisambiguator.cmx: matitaDisambiguator.cmi
-grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi
-grafiteParserMisc.cmo: grafiteParser.cmi grafiteParserMisc.cmi
-grafiteParserMisc.cmx: grafiteParser.cmx grafiteParserMisc.cmi
+grafiteDisambiguator.cmo: grafiteDisambiguator.cmi
+grafiteDisambiguator.cmx: grafiteDisambiguator.cmi
+grafiteDisambiguate.cmo: grafiteDisambiguator.cmi grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: grafiteDisambiguator.cmx grafiteDisambiguate.cmi
PREDICATES =
INTERFACE_FILES = \
+ dependenciesParser.mli \
grafiteParser.mli \
cicNotation2.mli \
- matitaDisambiguator.mli \
+ grafiteDisambiguator.mli \
grafiteDisambiguate.mli \
- grafiteParserMisc.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
* http://helm.cs.unibo.it/
*)
-let load_notation fname =
+let load_notation ~include_paths fname =
let ic = open_in fname in
let lexbuf = Ulexing.from_utf8_channel ic in
+ let status = ref LexiconSync.init in
try
- while true do
- match GrafiteParser.parse_statement lexbuf with
- | GrafiteAst.Executable (_, GrafiteAst.Command (_, cmd)) ->
- ignore (CicNotation.process_notation cmd)
- | _ -> ()
- done
- with End_of_file -> close_in ic
-
-let parse_environment str =
- let stream = Ulexing.from_utf8_string str in
- let environment = ref DisambiguateTypes.Environment.empty in
- let multiple_environment = ref DisambiguateTypes.Environment.empty in
- try
- while true do
- let alias =
- match GrafiteParser.parse_statement stream with
- GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
- -> alias
- | _ -> assert false in
- let key,value =
- (*CSC: Warning: this code should be factorized with the corresponding
- code in MatitaEngine *)
- match alias with
- GrafiteAst.Ident_alias (id,uri) ->
- DisambiguateTypes.Id id,
- (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
- | GrafiteAst.Symbol_alias (symb,instance,desc) ->
- DisambiguateTypes.Symbol (symb,instance),
- DisambiguateChoices.lookup_symbol_by_dsc symb desc
- | GrafiteAst.Number_alias (instance,desc) ->
- DisambiguateTypes.Num instance,
- DisambiguateChoices.lookup_num_by_dsc desc
- in
- environment := DisambiguateTypes.Environment.add key value !environment;
- multiple_environment := DisambiguateTypes.Environment.cons key value !multiple_environment;
- done;
- assert false
- with End_of_file ->
- !environment, !multiple_environment
+ while true do
+ status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)
+ done;
+ assert false
+ with End_of_file -> close_in ic; !status
+let parse_environment ~include_paths str =
+ let lexbuf = Ulexing.from_utf8_string str in
+ let status = ref LexiconSync.init in
+ try
+ while true do
+ status := fst (GrafiteParser.parse_statement ~include_paths lexbuf !status)
+ done;
+ assert false
+ with End_of_file ->
+ !status.LexiconEngine.aliases,
+ !status.LexiconEngine.multi_aliases
* http://helm.cs.unibo.it/
*)
+(** Note: notation is also loaded, but it cannot be undone since the
+ notation_ids part of the status is thrown away;
+ so far this function is useful only in Whelp *)
val parse_environment:
- string ->
- DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
+ include_paths:string list ->
+ string ->
+ DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
(** @param fname file from which load notation *)
-val load_notation: string -> unit
+val load_notation: include_paths:string list -> string -> LexiconEngine.status
--- /dev/null
+(* 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/
+ *)
+
+exception UnableToInclude of string
+
+ (* statements meaningful for matitadep *)
+type dependency =
+ | IncludeDep of string
+ | BaseuriDep of string
+ | UriDep of UriManager.uri
+
+let pp_dependency = function
+ | IncludeDep str -> "include \"" ^ str ^ "\""
+ | BaseuriDep str -> "set \"baseuri\" \"" ^ str ^ "\""
+ | UriDep uri -> "uri \"" ^ UriManager.string_of_uri uri ^ "\""
+
+let parse_dependencies lexbuf =
+ let tok_stream,_ =
+ CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
+ in
+ let rec parse acc =
+ (parser
+ | [< '("URI", u) >] ->
+ parse (UriDep (UriManager.uri_of_string u) :: acc)
+ | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
+ parse (IncludeDep fname :: acc)
+ | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
+ parse (BaseuriDep baseuri :: acc)
+ | [< '("EOI", _) >] -> acc
+ | [< 'tok >] -> parse acc
+ | [< >] -> acc) tok_stream
+ in
+ List.rev (parse [])
+
+let make_absolute paths path =
+ let rec aux = function
+ | [] -> ignore (Unix.stat path); path
+ | p :: tl ->
+ let path = p ^ "/" ^ path in
+ try
+ ignore (Unix.stat path); path
+ with Unix.Unix_error _ -> aux tl
+ in
+ try
+ aux paths
+ with Unix.Unix_error _ -> raise (UnableToInclude path)
+;;
+
+let baseuri_of_script ~include_paths file =
+ let file = make_absolute include_paths file in
+ let ic = open_in file in
+ let istream = Ulexing.from_utf8_channel ic in
+ let rec find_baseuri =
+ function
+ [] -> failwith ("No baseuri defined in " ^ file)
+ | BaseuriDep s::_ -> s
+ | _::tl -> find_baseuri tl in
+ let buri = find_baseuri (parse_dependencies istream) in
+ let uri = Http_getter_misc.strip_trailing_slash buri in
+ if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
+ HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(Http_getter.resolve uri)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri
--- /dev/null
+(* 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/
+ *)
+
+exception UnableToInclude of string
+
+ (* statements meaningful for matitadep *)
+type dependency =
+ | IncludeDep of string
+ | BaseuriDep of string
+ | UriDep of UriManager.uri
+
+val pp_dependency: dependency -> string
+
+ (** @raise End_of_file *)
+val parse_dependencies: Ulexing.lexbuf -> dependency list
+
+val baseuri_of_script : include_paths:string list -> string -> string
* http://helm.cs.unibo.it/
*)
-open GrafiteTypes
+exception BaseUriNotSetYet
let singleton = function
| [x], _ -> x
| _ -> assert false
(** @param term not meaningful when context is given *)
-let disambiguate_term ?context status_ref goal term =
- let status = !status_ref in
- let context =
- match context with
- | Some c -> c
- | None -> GrafiteTypes.get_proof_context status goal
- in
+let disambiguate_term lexicon_status_ref context metasenv term =
+ let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context ~metasenv:(GrafiteTypes.get_proof_metasenv status) term)
+ (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv term)
in
- let status = GrafiteTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status diff in
- status_ref := status;
- cic
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
+ metasenv,cic
(** 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 status_ref term =
+let disambiguate_lazy_term lexicon_status_ref term =
(fun context metasenv ugraph ->
- let status = !status_ref in
+ let lexicon_status = !lexicon_status_ref in
let (diff, metasenv, cic, ugraph) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
- ~initial_ugraph:ugraph ~aliases:status.aliases
- ~universe:(Some status.multi_aliases) ~context ~metasenv term)
- in
- let status = GrafiteTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status diff in
- status_ref := status;
+ (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
+ ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~context ~metasenv
+ term) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status_ref := lexicon_status;
cic, metasenv, ugraph)
-let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
+let disambiguate_pattern lexicon_status_ref (wanted, hyp_paths, goal_path) =
let interp path = Disambiguate.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
match wanted with
None -> None
| Some wanted ->
- let wanted = disambiguate_lazy_term status_ref wanted in
+ let wanted = disambiguate_lazy_term lexicon_status_ref wanted in
Some wanted
in
(wanted, hyp_paths, goal_path)
-let disambiguate_reduction_kind aliases_ref = function
+let disambiguate_reduction_kind lexicon_status_ref = function
| `Unfold (Some t) ->
- let t = disambiguate_lazy_term aliases_ref t in
+ let t = disambiguate_lazy_term lexicon_status_ref t in
`Unfold (Some t)
| `Normalize
| `Reduce
| `Unfold None
| `Whd as kind -> kind
-let disambiguate_tactic status goal tactic =
- let status_ref = ref status in
- let tactic =
- match tactic with
+let disambiguate_tactic lexicon_status_ref context metasenv tactic =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+ let disambiguate_pattern = disambiguate_pattern lexicon_status_ref in
+ let disambiguate_reduction_kind = disambiguate_reduction_kind lexicon_status_ref in
+ let disambiguate_lazy_term = disambiguate_lazy_term lexicon_status_ref in
+ match tactic with
| GrafiteAst.Absurd (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Absurd (loc, cic)
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Absurd (loc, cic)
| GrafiteAst.Apply (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.Assumption loc ->
+ metasenv,GrafiteAst.Assumption loc
| GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
- GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+ metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
| GrafiteAst.Change (loc, pattern, with_what) ->
- let with_what = disambiguate_lazy_term status_ref with_what in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+ 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.Compare (loc,term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Compare (loc,term)
- | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Compare (loc,term)
+ | GrafiteAst.Constructor (loc,n) ->
+ metasenv,GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc ->
+ metasenv,GrafiteAst.Contradiction loc
| GrafiteAst.Cut (loc, ident, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.DecideEquality loc ->
+ metasenv,GrafiteAst.DecideEquality loc
| GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate types = function
+ let disambiguate (metasenv,types) = function
| GrafiteAst.Type _ -> assert false
| GrafiteAst.Ident id ->
- (match disambiguate_term status_ref goal
- (CicNotationPt.Ident (id, None))
- with
- | Cic.MutInd (uri, tyno, _) ->
- (GrafiteAst.Type (uri, tyno) :: types)
- | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
+ (match
+ disambiguate_term context metasenv
+ (CicNotationPt.Ident(id, None))
+ with
+ | metasenv,Cic.MutInd (uri, tyno, _) ->
+ metasenv,(GrafiteAst.Type (uri, tyno) :: types)
+ | _ ->
+ raise (GrafiteDisambiguator.DisambiguationError
+ (0,[[None,lazy "Decompose works only on inductive types"]])))
+ in
+ let metasenv,types =
+ List.fold_left disambiguate (metasenv,[]) types
in
- let types = List.fold_left disambiguate [] types in
- GrafiteAst.Decompose (loc, types, what, names)
+ metasenv,GrafiteAst.Decompose (loc, types, what, names)
| GrafiteAst.Discriminate (loc,term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Discriminate(loc,term)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Discriminate(loc,term)
| GrafiteAst.Exact (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Exact (loc, cic)
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Exact (loc, cic)
| GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ let metasenv,what = disambiguate_term context metasenv what in
+ let metasenv,using = disambiguate_term context metasenv using in
+ metasenv,GrafiteAst.Elim (loc, what, Some using, depth, idents)
| GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.Elim (loc, what, None, depth, idents)
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.Elim (loc, what, None, depth, idents)
| GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ 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, depth, idents)
| GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.ElimType (loc, what, None, depth, idents)
- | GrafiteAst.Exists loc -> GrafiteAst.Exists loc
- | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | 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 status_ref pattern in
- let term = disambiguate_lazy_term status_ref term in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- 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) ->
- GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+ metasenv,GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc ->
+ metasenv,GrafiteAst.Fourier loc
| GrafiteAst.Generalize (loc,pattern,ident) ->
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
- | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Generalize (loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) ->
+ metasenv,GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc ->
+ metasenv,GrafiteAst.IdTac loc
| GrafiteAst.Injection (loc, term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Injection (loc,term)
- | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) ->
+ metasenv,GrafiteAst.Intros (loc, num, names)
| GrafiteAst.Inversion (loc, term) ->
- let term = disambiguate_term status_ref goal term in
- GrafiteAst.Inversion (loc, term)
+ let metasenv,term = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Inversion (loc, term)
| GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
let f term to_what =
- let term = disambiguate_term status_ref goal term in
+ let metasenv,term = disambiguate_term context metasenv term in
term :: to_what
in
let to_what = List.fold_right f to_what [] in
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.LApply (loc, depth, to_what, what, ident)
- | GrafiteAst.Left loc -> GrafiteAst.Left loc
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc ->
+ metasenv,GrafiteAst.Left loc
| GrafiteAst.LetIn (loc, term, name) ->
- let term = disambiguate_term status_ref goal term in
- 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 status_ref pattern in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- GrafiteAst.Reduce(loc, red_kind, pattern)
- | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+ 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 status_ref pattern in
- let with_what = disambiguate_lazy_term status_ref with_what in
- 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) ->
- let term = disambiguate_term status_ref goal t in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+ let metasenv,term = disambiguate_term context metasenv t in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | 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 cic = disambiguate_term status_ref goal term in
- GrafiteAst.Transitivity (loc, cic)
- in
- status_ref, tactic
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Transitivity (loc, cic)
-let disambiguate_obj status obj =
+let disambiguate_obj lexicon_status ~baseuri metasenv obj =
let uri =
match obj with
| CicNotationPt.Inductive (_,(name,_,_,_)::_)
| CicNotationPt.Record (_,name,_,_) ->
- Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind"))
+ (match baseuri with
+ | Some baseuri ->
+ Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
+ | None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
- in
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof _
- | Proof _ ->
- raise (GrafiteTypes.Command_error "imbricated proofs not allowed")
- | Intermediate _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status diff in
- status, cic
+ (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri obj) in
+ let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
+ lexicon_status, metasenv, cic
-let disambiguate_command status =
+let disambiguate_command lexicon_status ~baseuri metasenv =
function
- | GrafiteAst.Alias _
| GrafiteAst.Coercion _
| GrafiteAst.Default _
| GrafiteAst.Drop _
- | GrafiteAst.Dump _
| GrafiteAst.Include _
- | GrafiteAst.Interpretation _
- | GrafiteAst.Notation _
| GrafiteAst.Qed _
- | GrafiteAst.Render _
| GrafiteAst.Set _ as cmd ->
- status,cmd
+ lexicon_status,metasenv,cmd
| GrafiteAst.Obj (loc,obj) ->
- let status,obj = disambiguate_obj status obj in
- status, GrafiteAst.Obj (loc,obj)
-
+ let lexicon_status,metasenv,obj =
+ disambiguate_obj lexicon_status ~baseuri metasenv obj in
+ lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
* http://helm.cs.unibo.it/
*)
+exception BaseUriNotSetYet
+
val disambiguate_tactic:
- GrafiteTypes.status ->
- ProofEngineTypes.goal ->
+ LexiconEngine.status ref ->
+ Cic.context ->
+ Cic.metasenv ->
(CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic ->
- GrafiteTypes.status ref *
- (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
+ Cic.metasenv *
+ (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic
val disambiguate_command:
- GrafiteTypes.status ->
+ LexiconEngine.status ->
+ baseuri:string option ->
+ Cic.metasenv ->
CicNotationPt.obj GrafiteAst.command ->
- GrafiteTypes.status * Cic.obj GrafiteAst.command
-
+ LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command
--- /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/
+ *)
+
+open Printf
+
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int * (Token.flocation option * string Lazy.t) list list
+ (** parameters are: option name, error message *)
+exception Unbound_identifier of string
+
+type choose_uris_callback =
+ id:string -> UriManager.uri list -> UriManager.uri list
+
+type choose_interp_callback = (string * string) list list -> int list
+
+let mono_uris_callback ~id =
+ if Helm_registry.get_bool "matita.auto_disambiguation" then
+ function l -> l
+ else
+ raise Ambiguous_input
+
+let mono_interp_callback _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+module Callbacks =
+ struct
+ let interactive_user_uri_choice ~selection_mode ?ok
+ ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
+ !_choose_uris_callback ~id uris
+
+ let interactive_interpretation_choice interp =
+ !_choose_interp_callback interp
+
+ let input_or_locate_uri ~(title:string) ?id =
+ (* Zack: I try to avoid using this callback. I therefore assume that
+ * the presence of an identifier that can't be resolved via "locate"
+ * query is a syntax error *)
+ let msg = match id with Some id -> id | _ -> "_" in
+ raise (Unbound_identifier msg)
+ end
+
+module Disambiguator = Disambiguate.Make (Callbacks)
+
+(* implement module's API *)
+
+let disambiguate_thing ~aliases ~universe
+ ~(f:?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b)
+ ~(drop_aliases: 'b -> 'b)
+ ~(drop_aliases_and_clear_diff: 'b -> 'b)
+ (thing: 'a)
+=
+ assert (universe <> None);
+ let library = false, DisambiguateTypes.Environment.empty, None in
+ let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+ let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+ let passes = (* <fresh_instances?, aliases, coercions?> *)
+ [ (false, mono_aliases, false);
+ (false, multi_aliases, false);
+ (true, mono_aliases, false);
+ (true, multi_aliases, false);
+ (true, mono_aliases, true);
+ (true, multi_aliases, true);
+ (true, library, true);
+ ]
+ in
+ let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
+ CicRefine.insert_coercions := insert_coercions;
+ f ~fresh_instances ~aliases ~universe thing
+ in
+ let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
+ if use_mono_aliases && not instances then
+ drop_aliases res
+ else if user_asked then
+ drop_aliases res (* one shot aliases *)
+ else
+ drop_aliases_and_clear_diff res
+ in
+ let rec aux errors =
+ function
+ | [ pass ] ->
+ (try
+ set_aliases pass (try_pass pass)
+ with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+ raise (DisambiguationError (offset, errors @ [newerrors])))
+ | hd :: tl ->
+ (try
+ set_aliases hd (try_pass hd)
+ with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
+ aux (errors @ [newerrors]) tl)
+ | [] -> assert false
+ in
+ let saved_insert_coercions = !CicRefine.insert_coercions in
+ try
+ let res = aux [] passes in
+ CicRefine.insert_coercions := saved_insert_coercions;
+ res
+ with exn ->
+ CicRefine.insert_coercions := saved_insert_coercions;
+ raise exn
+
+type disambiguator_thing =
+ { do_it :
+ 'a 'b.
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ f:(?fresh_instances:bool ->
+ aliases:DisambiguateTypes.environment ->
+ universe:DisambiguateTypes.multiple_environment option ->
+ 'a -> 'b * bool) ->
+ drop_aliases:('b * bool -> 'b * bool) ->
+ drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
+ }
+
+let disambiguate_thing =
+ let profiler = HExtlib.profile "disambiguate_thing" in
+ { do_it =
+ fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
+ -> profiler.HExtlib.profile
+ (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff) thing
+ }
+
+let drop_aliases (choices, user_asked) =
+ (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
+ user_asked
+
+let drop_aliases_and_clear_diff (choices, user_asked) =
+ (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
+ user_asked
+
+let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
+ ~aliases ~universe term
+ =
+ assert (fresh_instances = None);
+ let f =
+ Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+ in
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff term
+
+let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+ assert (fresh_instances = None);
+ let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+ disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
+ ~drop_aliases_and_clear_diff obj
--- /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/
+ *)
+
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+ * compiler) *)
+exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int * (Token.flocation option * string Lazy.t) list list
+
+type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
+type choose_interp_callback = (string * string) list list -> int list
+
+val set_choose_uris_callback: choose_uris_callback -> unit
+val set_choose_interp_callback: choose_interp_callback -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_uris_callback if not set otherwise with set_choose_uris_callback
+ * above *)
+val mono_uris_callback: choose_uris_callback
+
+(** @raise Ambiguous_input if called, default value for internal
+ * choose_interp_callback if not set otherwise with set_choose_interp_callback
+ * above *)
+val mono_interp_callback: choose_interp_callback
+
+(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
+
+include Disambiguate.Disambiguator
module Ast = CicNotationPt
+type 'a localized_option =
+ LSome of 'a
+ | LNone of Token.flocation
+
type statement =
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
- GrafiteAst.statement
+ include_paths:string list ->
+ LexiconEngine.status ->
+ LexiconEngine.status *
+ (CicNotationPt.term, CicNotationPt.term,
+ CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+ GrafiteAst.statement localized_option
let grammar = CicNotationParser.level2_ast_grammar
if (try ignore (UriManager.uri_of_string uri); true
with UriManager.IllFormedUri _ -> false)
then
- GrafiteAst.Ident_alias (id, uri)
+ LexiconAst.Ident_alias (id, uri)
else
raise
(HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
let instance =
match instance with Some i -> i | None -> 0
in
- GrafiteAst.Symbol_alias (symbol, instance, dsc)
+ LexiconAst.Symbol_alias (symbol, instance, dsc)
| IDENT "num";
instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
SYMBOL "="; dsc = QSTRING ->
let instance =
match instance with Some i -> i | None -> 0
in
- GrafiteAst.Number_alias (instance, dsc)
+ LexiconAst.Number_alias (instance, dsc)
]
];
argument: [
(s, args, t)
]
];
- command: [ [
+
+ include_command: [ [
+ IDENT "include" ; path = QSTRING -> loc,path
+ ]];
+
+ grafite_command: [ [
IDENT "set"; n = QSTRING; v = QSTRING ->
GrafiteAst.Set (loc, n, v)
| IDENT "drop" -> GrafiteAst.Drop loc
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
| IDENT "coercion" ; suri = URI ->
GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
- | IDENT "alias" ; spec = alias_spec ->
- GrafiteAst.Alias (loc, spec)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
- | IDENT "include" ; path = QSTRING ->
- GrafiteAst.Include (loc,path)
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
GrafiteAst.Default (loc,what,uris)
+ ]];
+ lexicon_command: [ [
+ IDENT "alias" ; spec = alias_spec ->
+ LexiconAst.Alias (loc, spec)
| IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
- GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
+ LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
| IDENT "interpretation"; id = QSTRING;
(symbol, args, l3) = interpretation ->
- GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
-
- | IDENT "dump" -> GrafiteAst.Dump loc
- | IDENT "render"; u = URI ->
- GrafiteAst.Render (loc, UriManager.uri_of_string u)
+ LexiconAst.Interpretation (loc, id, (symbol, args), l3)
]];
executable: [
- [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
+ [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
| tac = tactical; punct = punctuation_tactical ->
GrafiteAst.Tactical (loc, tac, Some punct)
| punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
]
];
statement: [
- [ ex = executable -> GrafiteAst.Executable (loc,ex)
- | com = comment -> GrafiteAst.Comment (loc, com)
+ [ ex = executable ->
+ fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+ | com = comment ->
+ fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+ | (iloc,fname) = include_command ; SYMBOL "." ->
+ fun ~include_paths status ->
+ let path = DependenciesParser.baseuri_of_script ~include_paths fname in
+ let status =
+ LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+ in
+ status,
+ LSome
+ (GrafiteAst.Executable
+ (loc,GrafiteAst.Command
+ (loc,GrafiteAst.Include (iloc,path))))
+ | scom = lexicon_command ; SYMBOL "." ->
+ fun ~include_paths status ->
+ let status = LexiconEngine.eval_command status scom in
+ status,LNone loc
| EOI -> raise End_of_file
]
];
let parse_statement lexbuf =
exc_located_wrapper
(fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
-
-let parse_dependencies lexbuf =
- let tok_stream,_ =
- CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf)
- in
- let rec parse acc =
- (parser
- | [< '("URI", u) >] ->
- parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc)
- | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
- parse (GrafiteAst.IncludeDep fname :: acc)
- | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
- parse (GrafiteAst.BaseuriDep baseuri :: acc)
- | [< '("EOI", _) >] -> acc
- | [< 'tok >] -> parse acc
- | [< >] -> acc) tok_stream
- in
- List.rev (parse [])
-
* http://helm.cs.unibo.it/
*)
+type 'a localized_option =
+ LSome of 'a
+ | LNone of Token.flocation
+
type statement =
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
- GrafiteAst.statement
+ include_paths:string list ->
+ LexiconEngine.status ->
+ LexiconEngine.status *
+ (CicNotationPt.term, CicNotationPt.term,
+ CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+ GrafiteAst.statement localized_option
val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *)
- (** @raise End_of_file *)
-val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list
-
val statement: statement Grammar.Entry.e
+++ /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/
- *)
-
-exception UnableToInclude of string
-
-let baseuri_of_baseuri_decl st =
- match st with
- | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
- Some buri
- | _ -> None
-
-let make_absolute paths path =
- let rec aux = function
- | [] -> ignore (Unix.stat path); path
- | p :: tl ->
- let path = p ^ "/" ^ path in
- try
- ignore (Unix.stat path); path
- with Unix.Unix_error _ -> aux tl
- in
- try
- aux paths
- with Unix.Unix_error _ -> raise (UnableToInclude path)
-;;
-
-let baseuri_of_script ~include_paths file =
- let file = make_absolute include_paths file in
- let uri = ref None in
- let ic = open_in file in
- let istream = Ulexing.from_utf8_channel ic in
- (try
- while true do
- try
- let stm = GrafiteParser.parse_statement istream in
- match baseuri_of_baseuri_decl stm with
- | Some buri ->
- let u = Http_getter_misc.strip_trailing_slash buri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
- (try
- ignore(Http_getter.resolve u)
- with
- | Http_getter_types.Unresolvable_URI _ ->
- HLog.error (file ^ " sets an unresolvable baseuri: "^buri)
- | Http_getter_types.Key_not_found _ -> ());
- uri := Some u;
- raise End_of_file
- | None -> ()
- with
- CicNotationParser.Parse_error err ->
- HLog.error ("Unable to parse: " ^ file);
- HLog.error ("Parse error: " ^ err);
- ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
+++ /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/
- *)
-
-exception UnableToInclude of string
-
-val baseuri_of_baseuri_decl :
- ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
- string option
-
-val baseuri_of_script : include_paths:string list -> string -> string
+++ /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/
- *)
-
-open Printf
-
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
- (** parameters are: option name, error message *)
-exception Unbound_identifier of string
-
-type choose_uris_callback =
- id:string -> UriManager.uri list -> UriManager.uri list
-
-type choose_interp_callback = (string * string) list list -> int list
-
-let mono_uris_callback ~id =
- if Helm_registry.get_bool "matita.auto_disambiguation" then
- function l -> l
- else
- raise Ambiguous_input
-
-let mono_interp_callback _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
- struct
- let interactive_user_uri_choice ~selection_mode ?ok
- ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
- !_choose_uris_callback ~id uris
-
- let interactive_interpretation_choice interp =
- !_choose_interp_callback interp
-
- let input_or_locate_uri ~(title:string) ?id =
- (* Zack: I try to avoid using this callback. I therefore assume that
- * the presence of an identifier that can't be resolved via "locate"
- * query is a syntax error *)
- let msg = match id with Some id -> id | _ -> "_" in
- raise (Unbound_identifier msg)
- end
-
-module Disambiguator = Disambiguate.Make (Callbacks)
-
-(* implement module's API *)
-
-let disambiguate_thing ~aliases ~universe
- ~(f:?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
- 'a -> 'b)
- ~(drop_aliases: 'b -> 'b)
- ~(drop_aliases_and_clear_diff: 'b -> 'b)
- (thing: 'a)
-=
- assert (universe <> None);
- let library = false, DisambiguateTypes.Environment.empty, None in
- let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
- let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
- let passes = (* <fresh_instances?, aliases, coercions?> *)
- [ (false, mono_aliases, false);
- (false, multi_aliases, false);
- (true, mono_aliases, false);
- (true, multi_aliases, false);
- (true, mono_aliases, true);
- (true, multi_aliases, true);
- (true, library, true);
- ]
- in
- let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
- CicRefine.insert_coercions := insert_coercions;
- f ~fresh_instances ~aliases ~universe thing
- in
- let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
- if use_mono_aliases && not instances then
- drop_aliases res
- else if user_asked then
- drop_aliases res (* one shot aliases *)
- else
- drop_aliases_and_clear_diff res
- in
- let rec aux errors =
- function
- | [ pass ] ->
- (try
- set_aliases pass (try_pass pass)
- with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
- raise (DisambiguationError (offset, errors @ [newerrors])))
- | hd :: tl ->
- (try
- set_aliases hd (try_pass hd)
- with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
- aux (errors @ [newerrors]) tl)
- | [] -> assert false
- in
- let saved_insert_coercions = !CicRefine.insert_coercions in
- try
- let res = aux [] passes in
- CicRefine.insert_coercions := saved_insert_coercions;
- res
- with exn ->
- CicRefine.insert_coercions := saved_insert_coercions;
- raise exn
-
-type disambiguator_thing =
- { do_it :
- 'a 'b.
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
- f:(?fresh_instances:bool ->
- aliases:DisambiguateTypes.environment ->
- universe:DisambiguateTypes.multiple_environment option ->
- 'a -> 'b * bool) ->
- drop_aliases:('b * bool -> 'b * bool) ->
- drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
- }
-
-let disambiguate_thing =
- let profiler = HExtlib.profile "disambiguate_thing" in
- { do_it =
- fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
- -> profiler.HExtlib.profile
- (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff) thing
- }
-
-let drop_aliases (choices, user_asked) =
- (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
- user_asked
-
-let drop_aliases_and_clear_diff (choices, user_asked) =
- (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
- user_asked
-
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
- ~aliases ~universe term
- =
- assert (fresh_instances = None);
- let f =
- Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
- in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff term
-
-let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
- assert (fresh_instances = None);
- let f = Disambiguator.disambiguate_obj ~dbd ~uri in
- disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
- ~drop_aliases_and_clear_diff obj
+++ /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/
- *)
-
-(** raised when ambiguous input is found but not expected (e.g. in the batch
- * compiler) *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
-exception DisambiguationError of
- int * (Token.flocation option * string Lazy.t) list list
-
-type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
-type choose_interp_callback = (string * string) list list -> int list
-
-val set_choose_uris_callback: choose_uris_callback -> unit
-val set_choose_interp_callback: choose_interp_callback -> unit
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_uris_callback if not set otherwise with set_choose_uris_callback
- * above *)
-val mono_uris_callback: choose_uris_callback
-
-(** @raise Ambiguous_input if called, default value for internal
- * choose_interp_callback if not set otherwise with set_choose_interp_callback
- * above *)
-val mono_interp_callback: choose_interp_callback
-
-(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *)
-
-include Disambiguate.Disambiguator
in
Arg.parse [] open_file usage;
let deps =
- GrafiteParser.parse_dependencies (Ulexing.from_utf8_channel !ic)
+ DependenciesParser.parse_dependencies (Ulexing.from_utf8_channel !ic)
in
- List.iter (fun dep -> print_endline (GrafiteAstPp.pp_dependency dep)) deps
+ List.iter (fun dep -> print_endline (DependenciesParser.pp_dependency dep)) deps
let char_count = ref 0 in
let module P = CicNotationPt in
let module G = GrafiteAst in
+ let status =
+ ref
+ (CicNotation2.load_notation
+ ~include_paths:[] (Helm_registry.get "notation.core_file"))
+ in
try
while true do
try
- let statement = GrafiteParser.parse_statement istream in
- let floc = extract_loc statement in
- let (_, y) = HExtlib.loc_of_floc floc in
- char_count := y + !char_count;
- match statement with
-(* | G.Executable (_, G.Macro (_, G.Check (_,
- P.AttributedTerm (_, P.Ident _)))) ->
- prerr_endline "mega hack";
- (match !last_rule_id with
- | None -> ()
- | Some id ->
- prerr_endline "removing last notation rule ...";
- CicNotationParser.delete id) *)
- | G.Executable (_, G.Macro (_, G.Check (_, t))) ->
- prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t));
- let t' = TermContentPres.pp_ast t in
- prerr_endline (sprintf "rendered ast: %s"
- (CicNotationPp.pp_term t'));
- let tbl = Hashtbl.create 0 in
- dump_xml t' tbl "out.xml"
- | G.Executable (_, G.Command (_,
- G.Notation (_, dir, l1, associativity, precedence, l2))) ->
- prerr_endline "notation";
- prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1));
- prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2));
- prerr_endline (sprintf "prec: %s" (pp_precedence precedence));
- prerr_endline (sprintf "assoc: %s" (pp_associativity associativity));
- let keywords = CicNotationUtil.keywords_of_term l1 in
- if keywords <> [] then
- prerr_endline (sprintf "keywords: %s"
- (String.concat " " keywords));
- if dir <> Some `RightToLeft then
- ignore
- (CicNotationParser.extend l1 ?precedence ?associativity
- (fun env loc -> TermContentPres.instantiate_level2 env l2));
-(* last_rule_id := Some rule_id; *)
- if dir <> Some `LeftToRight then
- ignore (TermContentPres.add_pretty_printer
- ?precedence ?associativity l2 l1)
- | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) ->
- prerr_endline "interpretation";
- prerr_endline (sprintf "dsc: %s" id);
- ignore (TermAcicContent.add_interpretation id l2 l3);
- flush stdout
- | G.Executable (_, G.Command (_, G.Dump _)) ->
- CicNotationParser.print_l2_pattern (); print_newline ()
- | G.Executable (_, G.Command (_, G.Render (_, uri))) ->
- let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- let annobj, _, _, id_to_sort, _, _, _ =
- Cic2acic.acic_object_of_cic_object obj
- in
- let annterm =
- match annobj with
- | Cic.AConstant (_, _, _, _, ty, _, _)
- | Cic.AVariable (_, _, _, ty, _, _) -> ty
- | _ -> assert false
- in
- let t, id_to_uri =
- TermAcicContent.ast_of_acic id_to_sort annterm
- in
- prerr_endline "Raw AST";
- prerr_endline (CicNotationPp.pp_term t);
- let t' = TermContentPres.pp_ast t in
- prerr_endline "Rendered AST";
- prerr_endline (CicNotationPp.pp_term t');
- dump_xml t' id_to_uri "out.xml"
- | _ -> prerr_endline "Unsupported statement"
+ match
+ GrafiteParser.parse_statement ~include_paths:[] istream !status
+ with
+ newstatus, GrafiteParser.LNone _ -> status := newstatus
+ | newstatus, GrafiteParser.LSome statement ->
+ status := newstatus;
+ let floc = extract_loc statement in
+ let (_, y) = HExtlib.loc_of_floc floc in
+ char_count := y + !char_count;
+ match statement with
+ (* | G.Executable (_, G.Macro (_, G.Check (_,
+ P.AttributedTerm (_, P.Ident _)))) ->
+ prerr_endline "mega hack";
+ (match !last_rule_id with
+ | None -> ()
+ | Some id ->
+ prerr_endline "removing last notation rule ...";
+ CicNotationParser.delete id) *)
+ | G.Executable (_, G.Macro (_, G.Check (_, t))) ->
+ prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t));
+ let t' = TermContentPres.pp_ast t in
+ prerr_endline (sprintf "rendered ast: %s"
+ (CicNotationPp.pp_term t'));
+ let tbl = Hashtbl.create 0 in
+ dump_xml t' tbl "out.xml"
+ | statement ->
+ prerr_endline
+ ("Unsupported statement: " ^
+ GrafiteAstPp.pp_statement
+ ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:(fun _ -> "_lazy_term_here_")
+ ~obj_pp:(fun _ -> "_obj_here_")
+ statement)
with
| End_of_file -> raise End_of_file
| HExtlib.Localized (floc,CicNotationParser.Parse_error msg) ->
let usage = "" in
Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage;
print_endline "Loading builtin notation ...";
- CicNotation2.load_notation (Helm_registry.get "notation.core_file");
print_endline "done.";
flush stdout;
process_stream (Ulexing.from_utf8_channel stdin)
--- /dev/null
+*.cmi
+*.cma
+*.cmo
+*.cmx
+*.cmxa
+*.o
+*.a
--- /dev/null
+lexiconAstPp.cmi: lexiconAst.cmo
+disambiguatePp.cmi: lexiconAst.cmo
+lexiconMarshal.cmi: lexiconAst.cmo
+cicNotation.cmi: lexiconAst.cmo
+lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi
+lexiconSync.cmi: lexiconEngine.cmi
+lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi
+lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi
+disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmo disambiguatePp.cmi
+disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi
+lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi
+lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi
+cicNotation.cmo: lexiconAst.cmo cicNotation.cmi
+cicNotation.cmx: lexiconAst.cmx cicNotation.cmi
+lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo disambiguatePp.cmi \
+ cicNotation.cmi lexiconEngine.cmi
+lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \
+ cicNotation.cmx lexiconEngine.cmi
+lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi
+lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi
--- /dev/null
+PACKAGE = lexicon
+PREDICATES =
+
+INTERFACE_FILES = \
+ lexiconAstPp.mli \
+ disambiguatePp.mli \
+ lexiconMarshal.mli \
+ cicNotation.mli \
+ lexiconEngine.mli \
+ lexiconSync.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ lexiconAst.ml \
+ $(INTERFACE_FILES:%.mli=%.ml)
+
+
+include ../Makefile.common
--- /dev/null
+(* 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/
+ *)
+
+open LexiconAst
+
+type notation_id =
+ | RuleId of CicNotationParser.rule_id
+ | InterpretationId of TermAcicContent.interpretation_id
+ | PrettyPrinterId of TermContentPres.pretty_printer_id
+
+let process_notation st =
+ match st with
+ | Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let rule_id =
+ if dir <> Some `RightToLeft then
+ [ RuleId (CicNotationParser.extend l1 ?precedence ?associativity
+ (fun env loc ->
+ CicNotationPt.AttributedTerm
+ (`Loc loc,TermContentPres.instantiate_level2 env l2))) ]
+ else
+ []
+ in
+ let pp_id =
+ if dir <> Some `LeftToRight then
+ [ PrettyPrinterId
+ (TermContentPres.add_pretty_printer ?precedence ?associativity
+ l2 l1) ]
+ else
+ []
+ in
+ rule_id @ pp_id
+ | Interpretation (loc, dsc, l2, l3) ->
+ let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
+ [InterpretationId interp_id]
+ | st -> []
+
+let remove_notation = function
+ | RuleId id -> CicNotationParser.delete id
+ | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
+ | InterpretationId id -> TermAcicContent.remove_interpretation id
+
+let get_all_notations () =
+ List.map
+ (fun (interp_id, dsc) ->
+ InterpretationId interp_id, "interpretation: " ^ dsc)
+ (TermAcicContent.get_all_interpretations ())
+
+let get_active_notations () =
+ List.map (fun id -> InterpretationId id)
+ (TermAcicContent.get_active_interpretations ())
+
+let set_active_notations ids =
+ let interp_ids =
+ HExtlib.filter_map
+ (function InterpretationId interp_id -> Some interp_id | _ -> None)
+ ids
+ in
+ TermAcicContent.set_active_interpretations interp_ids
+
--- /dev/null
+(* 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/
+ *)
+
+type notation_id
+
+val process_notation: LexiconAst.command -> notation_id list
+
+val remove_notation: notation_id -> unit
+
+(** {2 Notation enabling/disabling}
+ * Right now, only disabling of notation during pretty printing is supporting.
+ * If it is useful to disable it also for the input phase is still to be
+ * understood ... *)
+
+val get_all_notations: unit -> (notation_id * string) list (* id, dsc *)
+val get_active_notations: unit -> notation_id list
+val set_active_notations: notation_id list -> unit
+
--- /dev/null
+(* 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/
+ *)
+
+open DisambiguateTypes
+
+let alias_of_domain_and_codomain_items domain_item (dsc,_) =
+ match domain_item with
+ Id id -> LexiconAst.Ident_alias (id, dsc)
+ | Symbol (symb, i) -> LexiconAst.Symbol_alias (symb, i, dsc)
+ | Num i -> LexiconAst.Number_alias (i, dsc)
+
+let aliases_of_environment env =
+ Environment.fold
+ (fun domain_item codomain_item acc ->
+ alias_of_domain_and_codomain_items domain_item codomain_item::acc
+ ) env []
+
+let aliases_of_domain_and_codomain_items_list l =
+ List.fold_left
+ (fun acc (domain_item,codomain_item) ->
+ alias_of_domain_and_codomain_items domain_item codomain_item::acc
+ ) [] l
+
+let pp_environment env =
+ let aliases = aliases_of_environment env in
+ let strings =
+ List.map (fun alias -> LexiconAstPp.pp_alias alias ^ ".") aliases
+ in
+ String.concat "\n" (List.sort compare strings)
--- /dev/null
+(* 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 aliases_of_domain_and_codomain_items_list:
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
+ LexiconAst.alias_spec list
+
+val pp_environment: DisambiguateTypes.environment -> string
--- /dev/null
+(* 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/
+ *)
+
+type direction = [ `LeftToRight | `RightToLeft ]
+
+type loc = Token.flocation
+
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
+(** To be increased each time the command type below changes, used for "safe"
+ * marshalling *)
+let magic = 5
+
+type command =
+ | Include of loc * string
+ | Alias of loc * alias_spec
+ (** parameters, name, type, fields *)
+ | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
+ int * CicNotationPt.term
+ (* direction, l1 pattern, associativity, precedence, l2 pattern *)
+ | Interpretation of loc *
+ string * (string * CicNotationPt.argument_pattern list) *
+ CicNotationPt.cic_appl_pattern
+ (* description (i.e. id), symbol, arg pattern, appl pattern *)
+
+(* composed magic: term + command magics. No need to change this value *)
+let magic = magic + 10000 * CicNotationPt.magic
+
--- /dev/null
+(* 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/
+ *)
+
+open Printf
+
+open LexiconAst
+
+let pp_l1_pattern = CicNotationPp.pp_term
+let pp_l2_pattern = CicNotationPp.pp_term
+
+let pp_alias = function
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+ | Symbol_alias (symb, instance, desc) ->
+ sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
+ symb instance desc
+ | Number_alias (instance,desc) ->
+ sprintf "alias num (instance %d) = \"%s\"" instance desc
+
+let pp_associativity = function
+ | Gramext.LeftA -> "left associative"
+ | Gramext.RightA -> "right associative"
+ | Gramext.NonA -> "non associative"
+
+let pp_precedence i = sprintf "with precedence %d" i
+
+let pp_argument_pattern = function
+ | CicNotationPt.IdentArg (eta_depth, name) ->
+ let eta_buf = Buffer.create 5 in
+ for i = 1 to eta_depth do
+ Buffer.add_string eta_buf "\\eta."
+ done;
+ sprintf "%s%s" (Buffer.contents eta_buf) name
+
+let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
+ sprintf "interpretation \"%s\" '%s %s = %s"
+ dsc symbol
+ (String.concat " " (List.map pp_argument_pattern arg_patterns))
+ (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
+
+let pp_dir_opt = function
+ | None -> ""
+ | Some `LeftToRight -> "> "
+ | Some `RightToLeft -> "< "
+
+let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
+ sprintf "notation %s\"%s\" %s %s for %s"
+ (pp_dir_opt dir_opt)
+ (pp_l1_pattern l1_pattern)
+ (pp_associativity assoc)
+ (pp_precedence prec)
+ (pp_l2_pattern l2_pattern)
+
+let pp_command = function
+ | Include (_,path) -> "include " ^ path
+ | Alias (_,s) -> pp_alias s
+ | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
+ pp_interpretation dsc symbol arg_patterns cic_appl_pattern
+ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+ pp_notation dir_opt l1_pattern assoc prec l2_pattern
+
--- /dev/null
+(* 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 pp_command: LexiconAst.command -> string
+
+val pp_alias: LexiconAst.alias_spec -> string
+
--- /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/
+ *)
+
+exception IncludedFileNotCompiled of string (* file name *)
+exception MetadataNotFound of string (* file name *)
+
+type status = {
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ lexicon_content_rev: LexiconMarshal.lexicon;
+ notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
+ metadata: LibraryNoDb.metadata list;
+}
+
+let add_lexicon_content cmds status =
+ let content = status.lexicon_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc -> cmd :: (List.filter ((<>) cmd) acc))
+ cmds content
+ in
+(* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map
+ LexiconAstPp.pp_command content')); *)
+ { status with lexicon_content_rev = content' }
+
+let add_metadata new_metadata status =
+ if Helm_registry.get_bool "db.nodb" then
+ let metadata = status.metadata in
+ let metadata' =
+ List.fold_left
+ (fun acc m ->
+ match m with
+ | LibraryNoDb.Dependency buri ->
+ if List.exists (LibraryNoDb.eq_metadata m) metadata
+ then acc
+ else m :: acc
+ | _ -> m :: acc)
+ metadata new_metadata
+ in
+ { status with metadata = metadata' }
+ else
+ status
+
+let set_proof_aliases status new_aliases =
+ let commands_of_aliases =
+ List.map
+ (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
+ in
+ let deps_of_aliases =
+ HExtlib.filter_map
+ (function
+ | LexiconAst.Ident_alias (_, suri) ->
+ let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+ Some (LibraryNoDb.Dependency buri)
+ | _ -> None)
+ in
+ let aliases =
+ List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
+ status.aliases new_aliases in
+ let multi_aliases =
+ List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
+ status.multi_aliases new_aliases in
+ let new_status =
+ { status with multi_aliases = multi_aliases ; aliases = aliases}
+ in
+ if new_aliases = [] then
+ new_status
+ else
+ let aliases =
+ DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+ in
+ let status = add_lexicon_content (commands_of_aliases aliases) new_status in
+ let status = add_metadata (deps_of_aliases aliases) status in
+ status
+
+let rec eval_command status cmd =
+ let notation_ids' = CicNotation.process_notation cmd in
+ let status =
+ { status with notation_ids = notation_ids' @ status.notation_ids } in
+ let basedir = Helm_registry.get "matita.basedir" in
+ match cmd with
+ | LexiconAst.Include (loc, baseuri) ->
+ let lexiconpath = LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in
+ if not (Sys.file_exists lexiconpath) then
+ raise (IncludedFileNotCompiled lexiconpath);
+ let lexicon = LexiconMarshal.load_lexicon lexiconpath in
+ let status = List.fold_left eval_command status lexicon in
+ if Helm_registry.get_bool "db.nodb" then
+ let metadatapath = baseuri ^ ".metadata" in
+ if not (Sys.file_exists metadatapath) then
+ raise (MetadataNotFound metadatapath)
+ else
+ add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
+ else
+ status
+ | LexiconAst.Alias (loc, spec) ->
+ let diff =
+ (*CSC: Warning: this code should be factorized with the corresponding
+ code in DisambiguatePp *)
+ match spec with
+ | LexiconAst.Ident_alias (id,uri) ->
+ [DisambiguateTypes.Id id,
+ (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
+ | LexiconAst.Symbol_alias (symb, instance, desc) ->
+ [DisambiguateTypes.Symbol (symb,instance),
+ DisambiguateChoices.lookup_symbol_by_dsc symb desc]
+ | LexiconAst.Number_alias (instance,desc) ->
+ [DisambiguateTypes.Num instance,
+ DisambiguateChoices.lookup_num_by_dsc desc]
+ in
+ set_proof_aliases status diff
+ | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+ let status = add_lexicon_content [stm] status in
+ let uris =
+ List.map
+ (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
+ (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
+ in
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0),
+ DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
+ in
+ let status = set_proof_aliases status diff in
+ let status = add_metadata uris status in
+ status
+ | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] 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 status = {
+ aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ lexicon_content_rev: LexiconMarshal.lexicon;
+ notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
+ metadata: LibraryNoDb.metadata list;
+}
+
+val eval_command : status -> LexiconAst.command -> status
+
+val set_proof_aliases:
+ status ->
+ (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list ->
+ status
--- /dev/null
+(* 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/
+ *)
+
+exception Checksum_failure of string
+exception Corrupt_lexicon of string
+exception Version_mismatch of string
+
+type lexicon = LexiconAst.command list
+
+let marshal_flags = []
+
+let rehash_cmd_uris =
+ let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
+ function
+ | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
+ let rec aux =
+ function
+ | CicNotationPt.UriPattern uri ->
+ CicNotationPt.UriPattern (rehash_uri uri)
+ | CicNotationPt.ApplPattern args ->
+ CicNotationPt.ApplPattern (List.map aux args)
+ | CicNotationPt.VarPattern _
+ | CicNotationPt.ImplicitPattern as pat -> pat
+ in
+ let appl_pattern = aux cic_appl_pattern in
+ LexiconAst.Interpretation (loc, dsc, args, appl_pattern)
+ | LexiconAst.Notation _
+ | LexiconAst.Alias _ as cmd -> cmd
+ | cmd ->
+ prerr_endline "Found a command not expected in a .lexicon:";
+ prerr_endline (LexiconAstPp.pp_command cmd);
+ assert false
+
+(** .lexicon file format
+ * - an integer -- magic number -- denoting the version of the dumped data
+ * structure. Different magic numbers stand for incompatible data structures
+ * - an integer -- checksum -- denoting the hash value (computed with
+ * Hashtbl.hash) of the string representation of the dumped data structur
+ * - marshalled data: list of LexiconAst.command
+ *)
+
+let save_lexicon ~fname lexicon =
+ let ensure_path_exists path =
+ let dir = Filename.dirname path in
+ HExtlib.mkdir dir
+ in
+ ensure_path_exists fname;
+ let oc = open_out fname in
+ let marshalled = Marshal.to_string (List.rev lexicon) marshal_flags in
+ let checksum = Hashtbl.hash marshalled in
+ output_binary_int oc LexiconAst.magic;
+ output_binary_int oc checksum;
+ output_string oc marshalled;
+ close_out oc
+
+let load_lexicon ~fname =
+ let ic = open_in fname in
+ HExtlib.finally
+ (fun () -> close_in ic)
+ (fun () ->
+ try
+ let lexicon_magic = input_binary_int ic in
+ if lexicon_magic <> LexiconAst.magic then raise (Version_mismatch fname);
+ let lexicon_checksum = input_binary_int ic in
+ let marshalled = HExtlib.input_all ic in
+ let checksum = Hashtbl.hash marshalled in
+ if checksum <> lexicon_checksum then raise (Checksum_failure fname);
+ let (lexicon:lexicon) =
+ Marshal.from_string marshalled 0
+ in
+ List.map rehash_cmd_uris lexicon
+ with End_of_file -> raise (Corrupt_lexicon fname))
+ ()
+
--- /dev/null
+(* 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/
+ *)
+
+ (** name of the corrupt .lexicon file *)
+exception Checksum_failure of string
+exception Corrupt_lexicon of string
+exception Version_mismatch of string
+
+type lexicon = LexiconAst.command list
+
+val save_lexicon: fname:string -> lexicon -> unit
+
+ (** @raise Corrupt_lexicon *)
+val load_lexicon: fname:string -> lexicon
+
--- /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/
+ *)
+
+let alias_diff ~from status =
+ let module Map = DisambiguateTypes.Environment in
+ Map.fold
+ (fun domain_item (description1,_ as codomain_item) acc ->
+ try
+ let description2,_ = Map.find domain_item from.LexiconEngine.aliases in
+ if description1 <> description2 then
+ (domain_item,codomain_item)::acc
+ else
+ acc
+ with
+ Not_found ->
+ (domain_item,codomain_item)::acc)
+ status.LexiconEngine.aliases []
+
+let alias_diff =
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
+
+(** given a uri and a type list (the contructors types) builds a list of pairs
+ * (name,uri) that is used to generate automatic aliases **)
+let extract_alias types uri =
+ fst(List.fold_left (
+ fun (acc,i) (name, _, _, cl) ->
+ (name, UriManager.uri_of_uriref uri i None) ::
+ (fst(List.fold_left (
+ fun (acc,j) (name,_) ->
+ (((name,UriManager.uri_of_uriref uri i
+ (Some j)) :: acc) , j+1)
+ ) (acc,1) cl)),i+1
+ ) ([],0) types)
+
+let build_aliases =
+ List.map
+ (fun (name,uri) ->
+ DisambiguateTypes.Id name,
+ (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
+
+let add_aliases_for_inductive_def status types uri =
+ let aliases = build_aliases (extract_alias types uri) in
+ LexiconEngine.set_proof_aliases status aliases
+
+let add_alias_for_constant status uri =
+ let name = UriManager.name_of_uri uri in
+ let new_env = build_aliases [(name,uri)] in
+ LexiconEngine.set_proof_aliases status new_env
+
+let add_aliases_for_object status uri =
+ function
+ Cic.InductiveDefinition (types,_,_,_) ->
+ add_aliases_for_inductive_def status types uri
+ | Cic.Constant _ -> add_alias_for_constant status uri
+ | Cic.Variable _
+ | Cic.CurrentProof _ -> assert false
+
+let add_aliases_for_objs =
+ List.fold_left
+ (fun status uri ->
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ add_aliases_for_object status uri obj)
+
+module OrderedId =
+struct
+ type t = CicNotation.notation_id
+ let compare = Pervasives.compare
+end
+
+module IdSet = Set.Make (OrderedId)
+
+ (** @return l2 \ l1 *)
+let id_list_diff l2 l1 =
+ let module S = IdSet in
+ let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
+ let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
+ let diff = S.diff s2 s1 in
+ S.fold (fun uri uris -> uri :: uris) diff []
+
+let time_travel ~present ~past =
+ let notation_to_remove =
+ id_list_diff present.LexiconEngine.notation_ids
+ past.LexiconEngine.notation_ids
+ in
+ List.iter CicNotation.remove_notation notation_to_remove
+
+let init =
+ {
+ LexiconEngine.aliases = DisambiguateTypes.Environment.empty;
+ multi_aliases = DisambiguateTypes.Environment.empty;
+ lexicon_content_rev = [];
+ notation_ids = [];
+ metadata = [];
+ }
--- /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/
+ *)
+
+val add_aliases_for_objs:
+ LexiconEngine.status -> UriManager.uri list -> LexiconEngine.status
+
+val time_travel:
+ present:LexiconEngine.status -> past:LexiconEngine.status -> unit
+
+ (** perform a diff between the aliases contained in two statuses, assuming
+ * that the second one can only have more aliases than the first one
+ * @return the list of aliases that should be added to aliases of from in
+ * order to be equal to aliases of the second argument *)
+val alias_diff:
+ from:LexiconEngine.status -> LexiconEngine.status ->
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list
+
+val init: LexiconEngine.status
String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
)
-let close_nodb buris =
+let close_nodb ~basedir buris =
let rev_deps = Hashtbl.create 97 in
let all_moos =
HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
List.iter
(fun path ->
let metadata = LibraryNoDb.load_metadata ~fname:path in
- let baseuri_of_current_moo =
- let rec aux = function
- | [] -> assert false
- | LibraryNoDb.Baseuri buri::_ -> buri
- | _ :: tl -> aux tl
- in
- aux metadata
+ let baseuri_of_current_moo =
+ let dirname = Filename.chop_extension (Filename.dirname path) in
+ let basedirlen = String.length basedir in
+ assert (String.sub dirname 0 basedirlen = basedir);
+ "cic:" ^
+ String.sub dirname basedirlen (String.length dirname - basedirlen) ^
+ Filename.basename path
in
let deps =
HExtlib.filter_map
- (function
- | LibraryNoDb.Dependency buri -> Some buri
- | _ -> None )
+ (function LibraryNoDb.Dependency buri -> Some buri)
metadata
in
List.iter
List.iter debug_prerr buris;
let l =
if Helm_registry.get_bool "db.nodb" then
- close_nodb buris
+ close_nodb ~basedir buris
else
close_db [] buris
in
List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
List.iter
(fun buri ->
- HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri))
+ HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri);
+ HExtlib.safe_remove (LibraryMisc.metadata_file_of_baseuri basedir buri);
+ HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri basedir buri))
(HExtlib.list_uniq (List.fast_sort Pervasives.compare
(List.map (UriManager.buri_of_uri) l)));
List.iter
let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
path ^ ".moo"
+let lexicon_file_of_baseuri ~basedir ~baseuri =
+ let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
+ path ^ ".lexicon"
+
let metadata_file_of_baseuri ~basedir ~baseuri =
let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
path ^ ".metadata"
*)
val obj_file_of_baseuri: basedir:string -> baseuri:string -> string
+val lexicon_file_of_baseuri: basedir:string -> baseuri:string -> string
val metadata_file_of_baseuri: basedir:string -> baseuri:string -> string
-
type metadata =
| Dependency of string (* baseuri without trailing slash *)
- | Baseuri of string
let eq_metadata (m1:metadata) (m2:metadata) = m1 = m2
*)
let save_metadata ~fname metadata =
- let oc = open_out fname in
- let marshalled = Marshal.to_string metadata marshal_flags in
- let checksum = Hashtbl.hash marshalled in
- output_binary_int oc magic;
- output_binary_int oc checksum;
- output_string oc marshalled;
- close_out oc
+ let ensure_path_exists path =
+ let dir = Filename.dirname path in
+ HExtlib.mkdir dir
+ in
+ ensure_path_exists fname;
+ let oc = open_out fname in
+ let marshalled = Marshal.to_string metadata marshal_flags in
+ let checksum = Hashtbl.hash marshalled in
+ output_binary_int oc magic;
+ output_binary_int oc checksum;
+ output_string oc marshalled;
+ close_out oc
let load_metadata ~fname =
let ic = open_in fname in
* support their format *)
type metadata =
| Dependency of string (* baseuri without trailing slash *)
- | Baseuri of string
val eq_metadata: metadata -> metadata -> bool
List.iter remove_single_obj !uris;
raise exn
-(* COERICONS ***********************************************************)
+(* COERCIONS ***********************************************************)
let remove_all_coercions () =
UriManager.UriHashtbl.clear coercion_hashtbl;
#!/bin/sh
# script args: source_file target_file
-use_clusters='yes'
+use_clusters='no'
+if [ ! -z "$USE_CLUSTERS" ]; then
+ use_clusters=$USE_CLUSTERS
+fi
# args: file snippet
# file will be modified in place
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
+tactics.cmi: proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
val replace_tac:
pattern:ProofEngineTypes.lazy_pattern ->
- with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+ with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val symmetry_tac: ProofEngineTypes.tactic
* @raise Bad_pattern
* *)
let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
- ~(pattern: (Cic.term, ProofEngineTypes.lazy_term) ProofEngineTypes.pattern)
+ ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
let find_pattern_for name =
type reduction = Cic.context -> Cic.term -> Cic.term
-type lazy_term =
- Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
- Cic.term * Cic.metasenv * CicUniv.universe_graph
-
let const_lazy_term t =
(fun _ metasenv ugraph -> t, metasenv, ugraph)
type ('term, 'lazy_term) pattern =
'lazy_term option * (string * 'term) list * 'term option
-type lazy_pattern = (Cic.term, lazy_term) pattern
+type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
let conclusion_pattern t =
let t' =
type reduction = Cic.context -> Cic.term -> Cic.term
-type lazy_term =
- Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
- Cic.term * Cic.metasenv * CicUniv.universe_graph
-
-val const_lazy_term: Cic.term -> lazy_term
+val const_lazy_term: Cic.term -> Cic.lazy_term
type lazy_reduction =
Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
type ('term, 'lazy_term) pattern =
'lazy_term option * (string * 'term) list * 'term option
-type lazy_pattern = (Cic.term, lazy_term) pattern
+type lazy_pattern = (Cic.term, Cic.lazy_term) pattern
(** conclusion_pattern [t] returns the pattern (t,[],%) *)
val conclusion_pattern : Cic.term option -> lazy_pattern
(* The default of term is the thesis of the goal to be prooved *)
val unfold_tac:
- ProofEngineTypes.lazy_term option ->
+ Cic.lazy_term option ->
pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
val change_tac:
pattern:ProofEngineTypes.lazy_pattern ->
- ProofEngineTypes.lazy_term ->
+ Cic.lazy_term ->
ProofEngineTypes.tactic
val fold_tac:
reduction:ProofEngineTypes.lazy_reduction ->
- term:ProofEngineTypes.lazy_term ->
+ term:Cic.lazy_term ->
pattern:ProofEngineTypes.lazy_pattern ->
ProofEngineTypes.tactic
?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
val change :
pattern:ProofEngineTypes.lazy_pattern ->
- ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+ Cic.lazy_term -> ProofEngineTypes.tactic
val clear : hyp:string -> ProofEngineTypes.tactic
val clearbody : hyp:string -> ProofEngineTypes.tactic
val compare : term:Cic.term -> ProofEngineTypes.tactic
val fail : ProofEngineTypes.tactic
val fold :
reduction:ProofEngineTypes.lazy_reduction ->
- term:ProofEngineTypes.lazy_term ->
+ term:Cic.lazy_term ->
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val fourier : ProofEngineTypes.tactic
val fwd_simpl :
val reflexivity : ProofEngineTypes.tactic
val replace :
pattern:ProofEngineTypes.lazy_pattern ->
- with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic
+ with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val rewrite :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
val unfold :
- ProofEngineTypes.lazy_term option ->
+ Cic.lazy_term option ->
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
projects / helm.git / commitdiff