From 4720c6af414c4a834a994fdb404fda2d0c04fc03 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 22 Jul 2002 17:50:49 +0000 Subject: [PATCH] Many improvements in tactics (and tactical) representation: 1) tactics are no more functions from state to state, but functions from proof * goal to proof * goal list where the goal list is the list of new goals generated 2) proof and goal are no more optional 3) all the tactics have been slightly changed so that their type is now param1 -> ... -> paramn -> ProofEngineTypes.tactic 4) the tactical thens has been implemented Other changes: 1) more .mli committed 2) comments and copyright notices added where missing --- helm/gTopLevel/.depend | 25 ++-- helm/gTopLevel/Makefile | 13 +- helm/gTopLevel/cic2Xml.ml | 7 +- helm/gTopLevel/cic2Xml.mli | 43 ++++++ helm/gTopLevel/primitiveTactics.ml | 116 ++++----------- helm/gTopLevel/primitiveTactics.mli | 12 +- helm/gTopLevel/proofEngine.ml | 29 ++-- helm/gTopLevel/proofEngine.mli | 29 +++- helm/gTopLevel/proofEngineHelpers.ml | 22 +-- helm/gTopLevel/proofEngineHelpers.mli | 34 ++++- helm/gTopLevel/proofEngineReduction.mli | 43 ++++++ helm/gTopLevel/proofEngineStructuralRules.ml | 30 ++-- helm/gTopLevel/proofEngineStructuralRules.mli | 8 +- helm/gTopLevel/proofEngineTypes.ml | 12 +- helm/gTopLevel/ring.ml | 134 ++++++++---------- helm/gTopLevel/ring.mli | 16 +-- helm/gTopLevel/sequentPp.ml | 29 +++- helm/gTopLevel/sequentPp.mli | 42 ++++++ helm/gTopLevel/xml2Gdome.ml | 25 ++++ helm/gTopLevel/xml2Gdome.mli | 27 ++++ 20 files changed, 430 insertions(+), 266 deletions(-) create mode 100644 helm/gTopLevel/cic2Xml.mli create mode 100644 helm/gTopLevel/proofEngineReduction.mli create mode 100644 helm/gTopLevel/sequentPp.mli create mode 100644 helm/gTopLevel/xml2Gdome.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index ea7ad894e..dea92351a 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,11 +1,15 @@ +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 @@ -16,7 +20,7 @@ ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ 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 \ @@ -26,15 +30,16 @@ doubleTypeInference.cmo: doubleTypeInference.cmi 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 diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 57811ff60..584fc3659 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -14,14 +14,15 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA 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 \ diff --git a/helm/gTopLevel/cic2Xml.ml b/helm/gTopLevel/cic2Xml.ml index e6a03a645..7c674d0ad 100644 --- a/helm/gTopLevel/cic2Xml.ml +++ b/helm/gTopLevel/cic2Xml.ml @@ -1,4 +1,3 @@ - (* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic @@ -31,7 +30,7 @@ exception NotImplemented;; 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 @@ -175,7 +174,7 @@ let print_term curi ids_to_inner_sorts = 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 @@ -234,7 +233,7 @@ let print_object curi ids_to_inner_sorts = 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] diff --git a/helm/gTopLevel/cic2Xml.mli b/helm/gTopLevel/cic2Xml.mli new file mode 100644 index 000000000..62a423f58 --- /dev/null +++ b/helm/gTopLevel/cic2Xml.mli @@ -0,0 +1,43 @@ +(* 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 diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index b52fb7882..75f421ced 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -195,22 +195,13 @@ let new_metasenv_for_apply proof context ty = 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,_) = @@ -240,53 +231,33 @@ let apply_tac ~status:(proof, goal) ~term = 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 = @@ -304,21 +275,12 @@ let cut_tac ~status:(proof, goal) ~term = 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 = @@ -331,34 +293,20 @@ let letin_tac ~status:(proof, goal) ~term = 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.") @@ -366,22 +314,13 @@ let exact_tac ~status:(proof, goal) ~term = (* 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 @@ -537,7 +476,4 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) proof metano apply_subst' newmetasenv''' in (newproof, - (match newmetasenv'''' with - | [] -> None - | (i,_,_)::_ -> Some i)) - + List.map (function (i,_,_) -> i) new_uninstantiatedmetas) diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli index 87142b564..123b3859d 100644 --- a/helm/gTopLevel/primitiveTactics.mli +++ b/helm/gTopLevel/primitiveTactics.mli @@ -1,13 +1,13 @@ 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 diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index ca8c0b54d..47af12f4e 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -28,13 +28,24 @@ open ProofEngineTypes (* 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]. *) @@ -80,10 +91,10 @@ let metas_in_term 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 diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index 1b110a669..66bb4620e 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -1,9 +1,33 @@ +(* 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 @@ -35,4 +59,3 @@ val clear : Cic.hypothesis -> unit (* other tactics *) val elim_type : Cic.term -> unit val ring : unit -> unit - diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml index 7e5f3a4b1..d191340ea 100644 --- a/helm/gTopLevel/proofEngineHelpers.ml +++ b/helm/gTopLevel/proofEngineHelpers.ml @@ -40,11 +40,7 @@ let identity_relocation_list_for_metavariable canonical_context = (* 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 @@ -55,11 +51,7 @@ let new_meta ~proof = 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) @@ -79,7 +71,7 @@ let subst_meta_in_proof proof meta term newmetasenv = ) 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 *) @@ -95,11 +87,7 @@ let subst_meta_in_proof proof meta term newmetasenv = (*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 @@ -118,6 +106,6 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = | _ -> i ) newmetasenv [] in - let newproof = Some (uri,metasenv',bo',ty) in + let newproof = uri,metasenv',bo',ty in (newproof, metasenv') diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli index 89f697750..c5593235c 100644 --- a/helm/gTopLevel/proofEngineHelpers.mli +++ b/helm/gTopLevel/proofEngineHelpers.mli @@ -1,6 +1,38 @@ +(* 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 -> diff --git a/helm/gTopLevel/proofEngineReduction.mli b/helm/gTopLevel/proofEngineReduction.mli new file mode 100644 index 000000000..3dea540d5 --- /dev/null +++ b/helm/gTopLevel/proofEngineReduction.mli @@ -0,0 +1,43 @@ +(* 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 diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml index e3e024f34..e01f95e9f 100644 --- a/helm/gTopLevel/proofEngineStructuralRules.ml +++ b/helm/gTopLevel/proofEngineStructuralRules.ml @@ -25,22 +25,14 @@ 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 @@ -95,22 +87,16 @@ let clearbody ~status:(proof, goal) ~hyp = | 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 @@ -159,5 +145,5 @@ let clear ~status:(proof, goal) ~hyp:hyp_to_clear = | t -> t ) metasenv in - (Some (curi,metasenv',pbo,pty), goal) + (curi,metasenv',pbo,pty), [goal] diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli index a0a423cff..f6ee6a529 100644 --- a/helm/gTopLevel/proofEngineStructuralRules.mli +++ b/helm/gTopLevel/proofEngineStructuralRules.mli @@ -1,6 +1,2 @@ -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 diff --git a/helm/gTopLevel/proofEngineTypes.ml b/helm/gTopLevel/proofEngineTypes.ml index 38492fce9..f5e75fc47 100644 --- a/helm/gTopLevel/proofEngineTypes.ml +++ b/helm/gTopLevel/proofEngineTypes.ml @@ -24,19 +24,17 @@ *) (** - 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 diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index c9e50be29..0b5cfadd2 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -95,14 +95,6 @@ let apolynomial_normalize_ok_uri = 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 *) (** @@ -147,24 +139,17 @@ let conj_of_metano metano = @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 *) @@ -402,50 +387,48 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = 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 @@ -453,9 +436,10 @@ let next_goal ~status = @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" @@ -465,7 +449,7 @@ let elim_type2_tac ~status ~term ~proof = *) 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 -> @@ -483,25 +467,22 @@ let lift ~n (a,b,c,d,e,f,g,h) = @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! *) @@ -512,7 +493,6 @@ let purge_hyps ~count ~status:(proof, goal) = 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 @@ -550,8 +530,10 @@ let ring_tac ~status:(proof, goal) = ~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 @@ -582,7 +564,9 @@ let ring_tac ~status:(proof, goal) = ~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 @@ -593,11 +577,11 @@ let ring_tac ~status:(proof, goal) = 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 diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli index 07c06866d..66ad9b121 100644 --- a/helm/gTopLevel/ring.mli +++ b/helm/gTopLevel/ring.mli @@ -1,15 +1,15 @@ (* 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 diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index c3ab41f88..d0430162e 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -1,3 +1,28 @@ +(* 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! *) @@ -67,7 +92,7 @@ module XmlPp = "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) @@ -79,7 +104,7 @@ module XmlPp = [< 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 ;; diff --git a/helm/gTopLevel/sequentPp.mli b/helm/gTopLevel/sequentPp.mli new file mode 100644 index 000000000..61f843fe8 --- /dev/null +++ b/helm/gTopLevel/sequentPp.mli @@ -0,0 +1,42 @@ +(* 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 diff --git a/helm/gTopLevel/xml2Gdome.ml b/helm/gTopLevel/xml2Gdome.ml index 55041995d..8c6298d09 100644 --- a/helm/gTopLevel/xml2Gdome.ml +++ b/helm/gTopLevel/xml2Gdome.ml @@ -1,3 +1,28 @@ +(* 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 diff --git a/helm/gTopLevel/xml2Gdome.mli b/helm/gTopLevel/xml2Gdome.mli new file mode 100644 index 000000000..45d0e9532 --- /dev/null +++ b/helm/gTopLevel/xml2Gdome.mli @@ -0,0 +1,27 @@ +(* 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 -- 2.39.2