+xml2Gdome.cmo: xml2Gdome.cmi
+xml2Gdome.cmx: xml2Gdome.cmi
proofEngineHelpers.cmo: proofEngineHelpers.cmi
proofEngineHelpers.cmx: proofEngineHelpers.cmi
+proofEngineReduction.cmo: proofEngineReduction.cmi
+proofEngineReduction.cmx: proofEngineReduction.cmi
proofEngineStructuralRules.cmo: proofEngineTypes.cmo \
proofEngineStructuralRules.cmi
proofEngineStructuralRules.cmx: proofEngineTypes.cmx \
proofEngineStructuralRules.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmo
-primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmo \
+primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \
proofEngineTypes.cmo primitiveTactics.cmi
primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
proofEngineTypes.cmx primitiveTactics.cmi
proofEngineTypes.cmx ring.cmi
ring.cmi: proofEngineTypes.cmo
proofEngine.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \
- proofEngineReduction.cmo proofEngineStructuralRules.cmi \
+ proofEngineReduction.cmi proofEngineStructuralRules.cmi \
proofEngineTypes.cmo ring.cmi proofEngine.cmi
proofEngine.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \
proofEngineReduction.cmx proofEngineStructuralRules.cmx \
doubleTypeInference.cmx: doubleTypeInference.cmi
cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi
cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi
-cic2Xml.cmo: cic2acic.cmi
-cic2Xml.cmx: cic2acic.cmx
-logicalOperations.cmo: proofEngine.cmi
-logicalOperations.cmx: proofEngine.cmx
-sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmi
-sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx
+cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi
+cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi
+cic2Xml.cmi: cic2acic.cmi
+logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi
+logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi
+sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi
+sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi
mQueryGenerator.cmo: mQueryGenerator.cmi
mQueryGenerator.cmx: mQueryGenerator.cmi
-gTopLevel.cmo: cic2Xml.cmo cic2acic.cmi logicalOperations.cmo \
- mQueryGenerator.cmi proofEngine.cmi sequentPp.cmo xml2Gdome.cmo
+gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \
+ mQueryGenerator.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi
gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \
mQueryGenerator.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx
all: gTopLevel
opt: gTopLevel.opt
-DEPOBJS = xml2Gdome.ml proofEngineTypes.ml proofEngineHelpers.ml \
- proofEngineReduction.ml proofEngineStructuralRules.ml \
- proofEngineStructuralRules.mli \
+DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \
+ proofEngineReduction.ml proofEngineReduction.mli \
+ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli \
- proofEngine.ml proofEngine.mli \
+ proofEngine.ml proofEngine.mli \
doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
- cic2Xml.ml cic2acic.mli logicalOperations.ml sequentPp.ml \
- mQueryGenerator.mli mQueryGenerator.ml gTopLevel.ml
+ cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
+ logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \
+ mQueryGenerator.ml gTopLevel.ml
TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
proofEngineReduction.cmo proofEngineStructuralRules.cmo \
-
(* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
let dtdname = "http://localhost:8081/getdtd?url=cic.dtd";;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_term curi ids_to_inner_sorts =
+let print_term curi ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
exception NotImplemented;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
-let print_object curi ids_to_inner_sorts =
+let print_object curi ~ids_to_inner_sorts =
let rec aux =
let module C = Cic in
let module X = Xml in
aux
;;
-let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+let print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types =
let module C2A = Cic2acic in
let module X = Xml in
X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception ImpossiblePossible
+exception NotImplemented
+
+val print_term :
+ UriManager.uri ->
+ ids_to_inner_sorts: (string, string) Hashtbl.t ->
+ Cic.annterm -> Xml.token Stream.t
+
+val print_object :
+ UriManager.uri ->
+ ids_to_inner_sorts: (string, string) Hashtbl.t ->
+ Cic.annobj -> Xml.token Stream.t
+
+val print_inner_types :
+ UriManager.uri ->
+ ids_to_inner_sorts: (string, string) Hashtbl.t ->
+ ids_to_inner_types: (string, Cic2acic.anntypes) Hashtbl.t ->
+ Xml.token Stream.t
let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
res,newmetasenv,arguments,newmeta,lastmeta
-let apply_tac ~status:(proof, goal) ~term =
+let apply_tac ~term ~status:(proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano ->
- List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let termty = CicTypeChecker.type_of_aux' metasenv context term in
(* newmeta is the lowest index of the new metas introduced *)
let (consthead,newmetas,arguments,newmeta,_) =
subst_meta_and_metasenv_in_proof
proof metano subst_in newmetasenv''
in
- (newproof,
- (match newmetasenv''' with
- | [] -> None
- | (i,_,_)::_ -> Some i))
+ (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
(* TODO per implementare i tatticali e' necessario che tutte le tattiche
sollevino _solamente_ Fail *)
-let apply_tac ~status ~term =
+let apply_tac ~term ~status =
try
- apply_tac ~status ~term
+ apply_tac ~term ~status
(* TODO cacciare anche altre eccezioni? *)
with CicUnification.UnificationFailed as e ->
raise (Fail (Printexc.to_string e))
-let intros_tac ~status:(proof, goal) ~name =
+let intros_tac ~name ~status:(proof, goal) =
let module C = Cic in
let module R = CicReduction in
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let newmeta = new_meta ~proof in
let (context',ty',bo') = lambda_abstract context newmeta ty name in
let (newproof, _) =
subst_meta_in_proof proof metano bo' [newmeta,context',ty']
in
- let newgoal = Some newmeta in
- (newproof, newgoal)
+ (newproof, [newmeta])
-let cut_tac ~status:(proof, goal) ~term =
+let cut_tac ~term ~status:(proof, goal) =
let module C = Cic in
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let newmeta1 = new_meta ~proof in
let newmeta2 = newmeta1 + 1 in
let context_for_newmeta1 =
subst_meta_in_proof proof metano bo'
[newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
in
- let newgoal = Some newmeta1 in
- (newproof, newgoal)
+ (newproof, [newmeta1 ; newmeta2])
-let letin_tac ~status:(proof, goal) ~term =
+let letin_tac ~term ~status:(proof, goal) =
let module C = Cic in
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let _ = CicTypeChecker.type_of_aux' metasenv context term in
let newmeta = new_meta ~proof in
let context_for_newmeta =
subst_meta_in_proof
proof metano bo'[newmeta,context_for_newmeta,newmetaty]
in
- let newgoal = Some newmeta in
- (newproof, newgoal)
+ (newproof, [newmeta])
(** functional part of the "exact" tactic *)
-let exact_tac ~status:(proof, goal) ~term =
+let exact_tac ~term ~status:(proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
begin
let (newproof, metasenv') =
subst_meta_in_proof proof metano term [] in
- let newgoal =
- (match metasenv' with
- [] -> None
- | (n,_,_)::_ -> Some n)
- in
- (newproof, newgoal)
+ (newproof, [])
end
else
raise (Fail "The type of the provided term is not the one expected.")
(* not really "primite" tactics .... *)
-let elim_intros_simpl_tac ~status:(proof, goal) ~term =
+let elim_intros_simpl_tac ~term ~status:(proof, goal) =
let module T = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let curi,metasenv =
- match proof with
- None -> assert false
- | Some (curi,metasenv,_,_) -> curi,metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano ->
- List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (curi,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let termty = T.type_of_aux' metasenv context term in
let uri,cookingno,typeno,args =
match termty with
proof metano apply_subst' newmetasenv'''
in
(newproof,
- (match newmetasenv'''' with
- | [] -> None
- | (i,_,_)::_ -> Some i))
-
+ List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
val apply_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val exact_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val intros_tac:
- status: ProofEngineTypes.status -> name: string-> ProofEngineTypes.status
+ name: string -> ProofEngineTypes.tactic
val cut_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val letin_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
val elim_intros_simpl_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
+ term: Cic.term -> ProofEngineTypes.tactic
(* proof assistant status *)
-let proof = ref (None : proof)
-let goal = ref (None : goal)
+let proof = ref (None : proof option)
+let goal = ref (None : goal option)
let apply_tactic ~tactic:tactic =
- let (newproof, newgoal) = tactic ~status:(!proof, !goal) in
- proof := newproof;
- goal := newgoal
+ match !proof,!goal with
+ None,_
+ | _,None -> assert false
+ | Some proof', Some goal' ->
+ let (newproof, newgoals) = tactic ~status:(proof', goal') in
+ proof := Some newproof;
+ goal :=
+ (match newgoals, newproof with
+ goal::_, _ -> Some goal
+ | [], (_,(goal,_,_)::_,_,_) ->
+ (* the tactic left no open goal ; let's choose the first open goal *)
+(*CSC: here we could implement and use a proof-tree like notion... *)
+ Some goal
+ | _, _ -> None)
(* metas_in_term term *)
(* Returns the ordered list of the metas that occur in [term]. *)
(* are efficiency reasons. *)
let perforate context term ty =
let module C = Cic in
- let newmeta = new_meta !proof in
- match !proof with
- None -> assert false
- | Some (uri,metasenv,bo,gty) ->
+ match !proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,gty as proof') ->
+ let newmeta = new_meta proof' in
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
exception NotConvertible
(* proof engine status *)
-val proof : ProofEngineTypes.proof ref
-val goal : ProofEngineTypes.goal ref
+val proof : ProofEngineTypes.proof option ref
+val goal : ProofEngineTypes.goal option ref
(* start a new goal undoing part of the proof *)
val perforate : Cic.context -> Cic.term -> Cic.term -> unit
(* other tactics *)
val elim_type : Cic.term -> unit
val ring : unit -> unit
-
(* Returns the first meta whose number is above the *)
(* number of the higher meta. *)
let new_meta ~proof =
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
+ let (_,metasenv,_,_) = proof in
let rec aux =
function
None,[] -> 1
1 + aux (None,metasenv)
let subst_meta_in_proof proof meta term newmetasenv =
- let (uri,metasenv,bo,ty) =
- match proof with
- None -> assert false
- | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
- in
+ let uri,metasenv,bo,ty = proof in
let subst_in = CicUnification.apply_subst [meta,term] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
) metasenv'
in
let bo' = subst_in bo in
- let newproof = Some (uri,metasenv'',bo',ty) in
+ let newproof = uri,metasenv'',bo',ty in
(newproof, metasenv'')
(*CSC: commento vecchio *)
(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
(*CSC: [newmetasenv]. *)
let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,bo,ty) =
- match proof with
- None -> assert false
- | Some (uri,_,bo,ty) -> uri,bo,ty
- in
+ let (uri,_,bo,ty) = proof in
let bo' = subst_in bo in
let metasenv' =
List.fold_right
| _ -> i
) newmetasenv []
in
- let newproof = Some (uri,metasenv',bo',ty) in
+ let newproof = uri,metasenv',bo',ty in
(newproof, metasenv')
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* identity_relocation_list_for_metavariable i canonical_context *)
+(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+(* where n = List.length [canonical_context] *)
val identity_relocation_list_for_metavariable :
'a option list -> Cic.term option list
-val new_meta : proof:('a * (int * 'b * 'c) list * 'd * 'e) option -> int
+
+(* Returns the first meta whose number is above the *)
+(* number of the higher meta. *)
+val new_meta : proof:ProofEngineTypes.proof -> int
+
val subst_meta_in_proof :
ProofEngineTypes.proof ->
int -> Cic.term -> Cic.metasenv ->
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception Impossible of int
+exception ReferenceToDefinition
+exception ReferenceToAxiom
+exception ReferenceToVariable
+exception ReferenceToCurrentProof
+exception ReferenceToInductiveDefinition
+exception WrongUriToInductiveDefinition
+exception RelToHiddenHypothesis
+exception WrongShape
+exception AlreadySimplified
+
+val syntactic_equality : Cic.term -> Cic.term -> bool
+val replace :
+ equality:(Cic.term -> 'a -> bool) ->
+ what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+val reduce :
+ (Cic.name * Cic.context_entry) option list -> Cic.term -> Cic.term
+val simpl : Cic.context -> Cic.term -> Cic.term
open ProofEngineTypes
-let clearbody ~status:(proof, goal) ~hyp =
+let clearbody ~hyp ~status:(proof, goal) =
let module C = Cic in
match hyp with
None -> assert false
| Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
| Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,_,_ =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
let string_of_name =
function
C.Name n -> n
| t -> t
) metasenv
in
- (Some (curi,metasenv',pbo,pty), goal)
+ (curi,metasenv',pbo,pty), [goal]
-let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
+let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
let module C = Cic in
match hyp_to_clear with
None -> assert false
| Some (n_to_clear, _) ->
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
+ let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+ List.find (function (m,_,_) -> m=goal) metasenv
in
let string_of_name =
function
| t -> t
) metasenv
in
- (Some (curi,metasenv',pbo,pty), goal)
+ (curi,metasenv',pbo,pty), [goal]
-val clearbody:
- status: ProofEngineTypes.status ->
- hyp: Cic.hypothesis -> ProofEngineTypes.status
-val clear:
- status: ProofEngineTypes.status ->
- hyp: Cic.hypothesis -> ProofEngineTypes.status
+val clearbody: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
+val clear: hyp: Cic.hypothesis -> ProofEngineTypes.tactic
*)
(**
- current proof (proof uri * metas * (in)complete proof * term to be prooved),
- possibly None
+ current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option
+type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term
(** current goal, integer index *)
-type goal = int option
- (** current status: (proof, goal) pair *)
-type status = proof * goal
+type goal = int
(**
a tactic: make a transition from one status to another one or, usually,
raise a "Fail" (@see Fail) exception in case of failure
*)
-type tactic = status:status -> status
+ (** an unfinished proof with the optional current goal *)
+type tactic = status:(proof * goal) -> proof * goal list
(** tactic failure *)
exception Fail of string
uri_of_string
"cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con"
-(** HELPERS *)
-
- (**
- "Some" constructor's inverse
- @raise Failure "unsome" if None is passed
- *)
-let unsome = function None -> failwith "unsome" | Some item -> item
-
(** CIC PREDICATES *)
(**
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ~status:(proof, goal) =
- match proof with
- | None -> failwith "Ring.metasenv_of_status invoked on None goal"
- | Some (_, m, _, _) -> m
+let metasenv_of_status ~status:((_,m,_,_), _) = m
(**
@param status a proof engine status
@raise Failure when proof or goal are None
@return context corresponding to current goal
*)
-let context_of_status ~status:(proof, goal) =
- let metasenv = metasenv_of_status ~status:(proof, goal) in
- let _, context, _ =
- match goal with
- | None -> failwith "Ring.context_of_status invoked on None goal"
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
- context
+let context_of_status ~status:(proof, goal as status) =
+ let metasenv = metasenv_of_status ~status:status in
+ let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+ context
(** CIC TERM CONSTRUCTORS *)
warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
res
with
- | (Fail _) as e -> begin (* TODO: codice replicato perche' non funge il
- binding multiplo con "as" *)
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- end
- | (CicTypeChecker.NotWellTyped _) as e -> begin (* TODO: si puo' togliere? *)
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- end
- | (CicUnification.UnificationFailed) as e -> begin
+ e ->
+ match e with
+ (Fail _)
+ | (CicTypeChecker.NotWellTyped _)
+ | (CicUnification.UnificationFailed) ->
warn (
"Ring.try_tactics failed with exn: " ^
Printexc.to_string e);
try_tactics ~tactics ~status
- end
- )
+ | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
+ )
| [] -> raise (Fail "try_tactics: no tactics left")
+let thens ~start ~continuations ~status =
+ let (proof,new_goals) = start ~status in
+ try
+ List.fold_left2
+ (fun (proof,goals) goal tactic ->
+ let (proof',new_goals') = tactic ~status:(proof,goal) in
+ (proof',goals@new_goals')
+ ) (proof,[]) new_goals continuations
+ with
+ Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+let id_tac ~status:(proof,goal) =
+ (proof,[goal])
+
+let status_of_single_goal_tactic_result =
+ function
+ proof,[goal] -> proof,goal
+ | _ ->
+ raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
+
(**
auxiliary tactic "elim_type"
@param status current proof engine status
@param term term to cut
*)
-let elim_type_tac ~status ~term =
+let elim_type_tac ~term ~status =
warn "in Ring.elim_type_tac";
- let status' = cut_tac ~term ~status in
- elim_intros_simpl_tac ~term:(Cic.Rel 1) ~status:status'
-
- (**
- move to next goal
- @param status current proof engine status
- *)
-let next_goal ~status =
- warn "in Ring.next_goal";
- (match status with
- | ((Some (_, metasenv, _, _)) as proof, goal) ->
- (match metasenv with
- | _::(n, _, _)::_ -> (proof, Some n)
- | _ -> raise (Fail "No other goal available"))
- | _ -> assert false)
+ thens ~start:(cut_tac ~term)
+ ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
(**
auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
-let elim_type2_tac ~status ~term ~proof =
+let elim_type2_tac ~term ~proof ~status =
warn "in Ring.elim_type2";
- exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status))
+ thens ~start:(elim_type_tac ~term)
+ ~continuations:[id_tac ; exact_tac ~term:proof] ~status
(**
Reflexivity tactic, try to solve current goal using "refl_eqT"
*)
let reflexivity_tac ~status:(proof, goal) =
warn "in Ring.reflexivity_tac";
- let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in
+ let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in
try
apply_tac ~status:(proof, goal) ~term:refl_eqt
with (Fail _) as e ->
@param count number of hypotheses to remove
@param status current proof engine status
*)
-let purge_hyps ~count ~status:(proof, goal) =
+let purge_hyps_tac ~count ~status:(proof, goal as status) =
let module S = ProofEngineStructuralRules in
let rec aux n context status =
assert(n>=0);
match (n, context) with
| (0, _) -> status
- | (n, hd::tl) -> aux (n-1) tl (S.clear ~status ~hyp:hd)
- | (_, []) -> failwith "Ring.purge_hyps: no hypotheses left"
- in
- let metano =
- match goal with
- | None -> failwith "Ring.purge_hyps invoked on None goal"
- | Some n -> n
+ | (n, hd::tl) ->
+ aux (n-1) tl
+ (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
+ | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
- match proof with
- | None -> failwith "Ring.purge_hyps invoked on None proof"
- | Some (_, metasenv, _, _) ->
- let (_, context, _) = conj_of_metano metano metasenv in
- aux count context (proof, goal)
+ let (_, metasenv, _, _) = proof in
+ let (_, context, _) = conj_of_metano goal metasenv in
+ let proof',goal' = aux count context status in
+ assert (goal = goal') ;
+ proof',[goal']
(** THE TACTIC! *)
let ring_tac ~status:(proof, goal) =
warn "in Ring tactic";
let status = (proof, goal) in
- let (proof, goal) = (unsome proof), (unsome goal) in
let eqt = mkMutInd (eqt_uri, 0) proof in
let r = mkConst r_uri proof in
let metasenv = metasenv_of_status ~status in
~status ~proof:t1'_eq_t1''
~term:(Cic.Appl [eqt; r; t1''; t1])
in
- incr new_hyps; (* elim_type add an hyp *)
- newstatus
+ incr new_hyps; (* elim_type add an hyp *)
+ match newstatus with
+ (proof,[goal]) -> proof,goal
+ | _ -> assert false
end else begin
warn "t1'' and t1 are CONVERTIBLE";
status
~term:(Cic.Appl [eqt; r; t2''; t2])
in
incr new_hyps; (* elim_type add an hyp *)
- newstatus
+ match newstatus with
+ (proof,[goal]) -> proof,goal
+ | _ -> assert false
end else begin
warn "t2'' and t2 are CONVERTIBLE";
status
reflexivity_tac ~status:status'
with (Fail _) -> (* leave conclusion to the user *)
warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps ~count:!new_hyps ~status:status')]
+ purge_hyps_tac ~count:!new_hyps ~status:status')]
in
status'')]
- with (Fail _) ->
- raise (Fail "Ring failure")
+ with (Fail s) ->
+ raise (Fail ("Ring failure: " ^ s))
end
| _ -> (* impossible: we are applying ring exacty to 2 terms *)
assert false
(* ring tactics *)
-val ring_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status
+val ring_tac: ProofEngineTypes.tactic
(* auxiliary tactics *)
-val elim_type_tac:
- status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status
-val reflexivity_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status
+val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
+val reflexivity_tac: ProofEngineTypes.tactic
+val id_tac : ProofEngineTypes.tactic
(* pseudo tacticals *)
val try_tactics:
- tactics: (string * ProofEngineTypes.tactic) list ->
- status: ProofEngineTypes.status ->
- ProofEngineTypes.status
-
+ tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+val thens:
+ start: ProofEngineTypes.tactic ->
+ continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
module TextualPp =
struct
(* It also returns the pretty-printing context! *)
"id",hid]
(Cic2Xml.print_term
(UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
+ ~ids_to_inner_sorts acic)
>], (entry::context)
| None ->
[< s ; X.xml_empty "Hidden" [] >], (None::context)
[< final_s ;
Xml.xml_nempty "Goal" []
(Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
+ ~ids_to_inner_sorts acic)
>],
ids_to_terms,ids_to_father_ids,ids_to_hypotheses
;;
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module TextualPp :
+ sig
+ val print_context :
+ (Cic.name * Cic.context_entry) option list ->
+ string * Cic.name option list
+ exception NotImplemented
+ val print_sequent :
+ int * (Cic.name * Cic.context_entry) option list * Cic.term -> string
+ end
+module XmlPp :
+ sig
+ val print_sequent :
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
+ Xml.token Stream.t * (Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t
+ end
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
let document_of_xml (domImplementation : Gdome.domImplementation) strm =
let module G = Gdome in
let module X = Xml in
--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+val document_of_xml :
+ Gdome.domImplementation -> Xml.token Stream.t -> Gdome.document
projects / helm.git / commitdiff