--- /dev/null
+requires="helm-library helm-tactics helm-cic_disambiguation"
+version="0.0.1"
+archive(byte)="grafite2.cma"
+archive(native)="grafite2.cmxa"
+linkopts=""
--- /dev/null
+requires="helm-grafite2"
+version="0.0.1"
+archive(byte)="grafite_parser.cma"
+archive(native)="grafite_parser.cmxa"
+linkopts=""
cic_unification \
whelp \
tactics \
- cic_disambiguation \
paramodulation \
+ cic_disambiguation \
+ grafite2 \
+ grafite_parser \
$(NULL)
OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
* http://helm.cs.unibo.it/
*)
-module Ast = CicNotationPt
-
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = Ast.location
+type loc = CicNotationPt.location
type ('term, 'lazy_term, 'ident) pattern =
'lazy_term option * ('ident * 'term) list * 'term
| Ident of 'ident
| Type of UriManager.uri * int
-type reduction =
+type 'lazy_term reduction =
[ `Normalize
| `Reduce
| `Simpl
- | `Unfold of CicNotationPt.term option
+ | `Unfold of 'lazy_term option
| `Whd ]
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 3
+let magic = 4
type ('term,'obj) command =
| Default of loc * string * UriManager.uri list
| Alias of loc * alias_spec
(** parameters, name, type, fields *)
| Obj of loc * 'obj
- | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
- int * Ast.term
+ | 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 * Ast.argument_pattern list) *
- Ast.cic_appl_pattern
+ string * (string * CicNotationPt.argument_pattern list) *
+ CicNotationPt.cic_appl_pattern
(* description (i.e. id), symbol, arg pattern, appl pattern *)
| Metadata of loc * metadata
open GrafiteAst
-module Ast = CicNotationPt
-
let tactical_terminator = ""
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
sprintf "alias num (instance %d) = \"%s\"" instance desc
let pp_argument_pattern = function
- | Ast.IdentArg (eta_depth, name) ->
+ | 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."
*)
val pp_tactic:
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactic ->
string
val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
val pp_comment:
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
CicNotationPt.obj, string)
GrafiteAst.comment ->
string
val pp_executable:
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
CicNotationPt.obj, string)
GrafiteAst.code ->
string
val pp_statement:
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
CicNotationPt.obj, string)
GrafiteAst.statement ->
string
val pp_macro_cic: Cic.term GrafiteAst.macro -> string
val pp_tactical:
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
GrafiteAst.tactical ->
string
exception Corrupt_moo of string
exception Version_mismatch of string
-type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
+type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
let marshal_flags = []
exception Corrupt_moo of string
exception Version_mismatch of string
-type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
+type ast_command = (Cic.term, Cic.obj) GrafiteAst.command
type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
val save_moo: fname:string -> moo -> unit
module Ast = CicNotationPt
type statement =
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
CicNotationPt.obj, string)
GrafiteAst.statement
*)
type statement =
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction,
+ (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
CicNotationPt.obj, string)
GrafiteAst.statement
--- /dev/null
+*.cm[iaox]
+*.cmxa
+test_dep
+test_parser
+print_grammar
--- /dev/null
+matitaSync.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
+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
--- /dev/null
+PACKAGE = grafite2
+PREDICATES =
+
+INTERFACE_FILES = \
+ grafiteTypes.mli \
+ disambiguatePp.mli \
+ matitaSync.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/
+ *)
+
+open DisambiguateTypes
+
+let parse_environment str =
+ let stream = Ulexing.from_utf8_string str in
+ let environment = ref Environment.empty in
+ let multiple_environment = ref 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) ->
+ Id id,
+ (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+ | GrafiteAst.Symbol_alias (symb,instance,desc) ->
+ Symbol (symb,instance),
+ DisambiguateChoices.lookup_symbol_by_dsc symb desc
+ | GrafiteAst.Number_alias (instance,desc) ->
+ Num instance,
+ DisambiguateChoices.lookup_num_by_dsc desc
+ in
+ environment := Environment.add key value !environment;
+ multiple_environment := Environment.cons key value !multiple_environment;
+ done;
+ assert false
+ with End_of_file ->
+ !environment, !multiple_environment
+
+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 parse_environment:
+ string ->
+ DisambiguateTypes.environment * DisambiguateTypes.multiple_environment
+
+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 UnableToInclude of string
+exception IncludedFileNotCompiled of string
+
+type options = {
+ do_heavy_checks: bool ;
+ include_paths: string list ;
+ 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.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.
+ 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 ->
+ ('term, 'obj) GrafiteAst.command ->
+ GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+
+ ?do_heavy_checks:bool ->
+ ?include_paths:string list ->
+ ?clean_baseuri:bool ->
+ GrafiteTypes.status ->
+ ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
+ GrafiteTypes.status
+ }
+
+type 'a eval_command =
+ {ec_go: 'term 'obj.
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ ('term,'obj) GrafiteAst.command ->
+ GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+ options -> GrafiteTypes.status -> ('term,'obj) GrafiteAst.command ->
+ GrafiteTypes.status
+ }
+
+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 ref *
+ (Cic.term, ProofEngineTypes.lazy_term, ProofEngineTypes.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
+
+ disambiguate_command:
+ (GrafiteTypes.status ->
+ ('term, 'obj) GrafiteAst.command ->
+ GrafiteTypes.status * (Cic.term, 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 eval_coercion status ~add_composites coercion =
+ let uri = CicUtil.uri_of_term coercion in
+ let status = MatitaSync.add_coercion status ~add_composites uri 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 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 eval_comment status c = status
+
+let rec eval_command = {ec_go = fun ~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 absolute_path = make_absolute opts.include_paths path in
+ let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in
+ let status = ref status in
+ if not (Sys.file_exists moopath) then
+ raise (IncludedFileNotCompiled moopath);
+ eval_from_moo.efm_go status moopath;
+ !status
+ | GrafiteAst.Metadata (loc, m) ->
+ (match m with
+ | GrafiteAst.Dependency uri -> GrafiteTypes.add_moo_metadata [m] status
+ | GrafiteAst.Baseuri _ -> 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_moo_metadata [GrafiteAst.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
+ MatitaSync.add_obj uri obj
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
+ | GrafiteAst.Coercion (loc, coercion, add_composites) ->
+ eval_coercion status ~add_composites coercion
+ | 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 -> GrafiteAst.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_moo_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));
+ MatitaSync.add_obj uri obj
+ {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
+
+} 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 (DisambiguateTypes.dummy_floc,
+ GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+ (GrafiteAst.reash_cmd_uris cmd)))
+ in
+ let moo, metadata = GrafiteMarshal.load_moo fname in
+ List.iter
+ (fun ast ->
+ let ast = ast_of_cmd ast in
+ status :=
+ eval_ast.ea_go
+ ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
+ ~disambiguate_command:(fun status cmd -> status,cmd)
+ !status ast)
+ moo;
+ List.iter
+ (fun m ->
+ let ast =
+ ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
+ in
+ status :=
+ eval_ast.ea_go
+ ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
+ ~disambiguate_command:(fun status cmd -> status,cmd)
+ !status ast)
+ metadata
+
+} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
+ ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st
+->
+ let opts = {
+ do_heavy_checks = do_heavy_checks ;
+ include_paths = include_paths;
+ 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 UnableToInclude of string
+exception IncludedFileNotCompiled of string
+
+val eval_ast :
+ 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 ->
+ ('term, 'obj) GrafiteAst.command ->
+ GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+
+ ?do_heavy_checks:bool ->
+ ?include_paths:string list ->
+ ?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 ^ "/"))
+
+let baseuri_of_baseuri_decl st =
+ match st with
+ | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) ->
+ Some buri
+ | _ -> None
+
+let baseuri_of_file file =
+ 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)
+
+let obj_file_of_script ~basedir f =
+ let baseuri = baseuri_of_file f in
+ LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
--- /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 baseuri_of_baseuri_decl :
+ ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
+ string option
+
+ (** check whether no objects are defined below a given baseuri *)
+val is_empty: string -> bool
+
+val baseuri_of_file : string -> string
+
+val obj_file_of_script : basedir:string -> 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/
+ *)
+
+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;
+ 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, metadata = 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', metadata }
+
+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_moo_metadata new_metadata status =
+ let content, metadata = status.moo_content_rev in
+ let metadata' =
+ List.fold_left
+ (fun acc m ->
+ match m with
+ | GrafiteAst.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
+ || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
+ then acc
+ else m :: acc
+ | _ -> m :: acc)
+ metadata new_metadata
+ in
+ { status with moo_content_rev = content, metadata' }
+
+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;
+ 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_moo_metadata: GrafiteAst.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 (GrafiteAst.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_moo_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 status =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = LibrarySync.add_obj uri obj basedir in
+ let status = {status with objects = uri::status.objects} in
+ 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 ~add_composites uri =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in
+ let status = {status with coercions = uri :: status.coercions} in
+ let statement_of name =
+ GrafiteAst.Coercion
+ (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in
+ let moo_content = [statement_of (UriManager.name_of_uri uri)] in
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ List.fold_left add_alias_for_constant status lemmas
+
+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 -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri))
+ coercions_to_remove;
+ List.iter LibrarySync.remove_obj objs_to_remove;
+ List.iter CicNotation.remove_notation notation_to_remove
--- /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 ->
+ GrafiteTypes.status -> GrafiteTypes.status
+
+val add_coercion:
+ GrafiteTypes.status -> add_composites:bool -> UriManager.uri ->
+ 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
--- /dev/null
+*.cm[iaox]
+*.cmxa
+test_dep
+test_parser
+print_grammar
--- /dev/null
+matitaDisambiguator.cmo: matitaDisambiguator.cmi
+matitaDisambiguator.cmx: matitaDisambiguator.cmi
+grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi
+grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi
--- /dev/null
+PACKAGE = grafite_parser
+PREDICATES =
+
+INTERFACE_FILES = \
+ matitaDisambiguator.mli \
+ grafiteDisambiguate.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/
+ *)
+
+open GrafiteTypes
+
+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 (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)
+ in
+ let status = GrafiteTypes.set_metasenv metasenv status in
+ let status = MatitaSync.set_proof_aliases status diff in
+ status_ref := status;
+ 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 =
+ (fun context metasenv ugraph ->
+ let status = !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;
+ cic, metasenv, ugraph)
+
+let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
+ let interp path = Disambiguate.interpretate_path [] path in
+ let goal_path = interp goal_path in
+ let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+ let wanted =
+ match wanted with
+ None -> None
+ | Some wanted ->
+ let wanted = disambiguate_lazy_term status_ref wanted in
+ Some wanted
+ in
+ (wanted, hyp_paths ,goal_path)
+
+let disambiguate_reduction_kind aliases_ref = function
+ | `Unfold (Some t) ->
+ let t = disambiguate_lazy_term aliases_ref t in
+ `Unfold (Some t)
+ | `Normalize
+ | `Reduce
+ | `Simpl
+ | `Unfold None
+ | `Whd as kind -> kind
+
+let disambiguate_tactic status goal tactic =
+ let status_ref = ref status in
+ let tactic =
+ match tactic with
+ | GrafiteAst.Absurd (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ 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
+ | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
+ 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)
+ | 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
+ | 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
+ | GrafiteAst.Decompose (loc, types, what, names) ->
+ let disambiguate 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"]])))
+ in
+ let types = List.fold_left disambiguate [] types in
+ GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Discriminate (loc,term) ->
+ let term = disambiguate_term status_ref goal term in
+ GrafiteAst.Discriminate(loc,term)
+ | GrafiteAst.Exact (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ 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)
+ | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+ let what = disambiguate_term status_ref goal what in
+ 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)
+ | 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
+ | 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)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc -> 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
+ | 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)
+ | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term to_what =
+ let term = disambiguate_term status_ref goal 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
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let term = disambiguate_term status_ref goal term in
+ 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
+ | 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)
+ | 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
+ | GrafiteAst.Transitivity (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Transitivity (loc, cic)
+ in
+ status_ref, tactic
+
+let disambiguate_obj status obj =
+ let uri =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) ->
+ Some (UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ".ind"))
+ | 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
+
+let disambiguate_command status =
+ function
+ | GrafiteAst.Alias _
+ | GrafiteAst.Default _
+ | GrafiteAst.Drop _
+ | GrafiteAst.Dump _
+ | GrafiteAst.Include _
+ | GrafiteAst.Interpretation _
+ | GrafiteAst.Metadata _
+ | GrafiteAst.Notation _
+ | GrafiteAst.Qed _
+ | GrafiteAst.Render _
+ | GrafiteAst.Set _ as cmd ->
+ status,cmd
+ | GrafiteAst.Coercion (loc, term, add_composites) ->
+ let status_ref = ref status in
+ let term = disambiguate_term ~context:[] status_ref ~-1 term in
+ !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
+ | GrafiteAst.Obj (loc,obj) ->
+ let status,obj = disambiguate_obj status obj in
+ status, GrafiteAst.Obj (loc,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/
+ *)
+
+val disambiguate_tactic:
+ GrafiteTypes.status ->
+ ProofEngineTypes.goal ->
+ (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
+
+val disambiguate_command:
+ GrafiteTypes.status ->
+ (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command ->
+ GrafiteTypes.status * (Cic.term, 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), use_coercions) =
+ CoercDb.use_coercions := use_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_use_coercions = !CoercDb.use_coercions in
+ try
+ let res = aux [] passes in
+ CoercDb.use_coercions := saved_use_coercions;
+ res
+ with exn ->
+ CoercDb.use_coercions := saved_use_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 HGT = Http_getter_types;;
module HG = Http_getter;;
-module HGM = Http_getter_misc;;
module UM = UriManager;;
-module TA = GrafiteAst;;
let cache_of_processed_baseuri = Hashtbl.create 1024
let clean_baseuris ?(verbose=true) ~basedir buris =
Hashtbl.clear cache_of_processed_baseuri;
- let buris = List.map HGM.strip_trailing_slash buris in
+ let buris = List.map Http_getter_misc.strip_trailing_slash buris in
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
projects / helm.git / commitdiff