From 76cb30ecd0159512548aee0ba7085ab17c6fd5bd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 1 Jul 2002 20:22:39 +0000 Subject: [PATCH] - added Ring tactic on reals - module splitting - proofEngine is now almost functional --- helm/gTopLevel/.depend | 32 +- helm/gTopLevel/Makefile | 12 +- helm/gTopLevel/gTopLevel.ml | 65 +- helm/gTopLevel/logicalOperations.ml | 25 + helm/gTopLevel/primitiveTactics.ml | 543 ++++++++++++ helm/gTopLevel/primitiveTactics.mli | 13 + helm/gTopLevel/proofEngine.ml | 791 +----------------- helm/gTopLevel/proofEngine.mli | 38 + helm/gTopLevel/proofEngineHelpers.ml | 123 +++ helm/gTopLevel/proofEngineHelpers.mli | 11 + helm/gTopLevel/proofEngineReduction.ml | 2 +- helm/gTopLevel/proofEngineStructuralRules.ml | 163 ++++ helm/gTopLevel/proofEngineStructuralRules.mli | 6 + helm/gTopLevel/proofEngineTypes.ml | 43 + helm/gTopLevel/ring.ml | 607 ++++++++++++++ helm/gTopLevel/ring.mli | 15 + 16 files changed, 1723 insertions(+), 766 deletions(-) create mode 100644 helm/gTopLevel/primitiveTactics.ml create mode 100644 helm/gTopLevel/primitiveTactics.mli create mode 100644 helm/gTopLevel/proofEngine.mli create mode 100644 helm/gTopLevel/proofEngineHelpers.ml create mode 100644 helm/gTopLevel/proofEngineHelpers.mli create mode 100644 helm/gTopLevel/proofEngineStructuralRules.ml create mode 100644 helm/gTopLevel/proofEngineStructuralRules.mli create mode 100644 helm/gTopLevel/proofEngineTypes.ml create mode 100644 helm/gTopLevel/ring.ml create mode 100644 helm/gTopLevel/ring.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 13d6f74d5..ea7ad894e 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -1,18 +1,40 @@ -proofEngine.cmo: proofEngineReduction.cmo -proofEngine.cmx: proofEngineReduction.cmx +proofEngineHelpers.cmo: proofEngineHelpers.cmi +proofEngineHelpers.cmx: proofEngineHelpers.cmi +proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ + proofEngineStructuralRules.cmi +proofEngineStructuralRules.cmi: proofEngineTypes.cmo +primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmo \ + proofEngineTypes.cmo primitiveTactics.cmi +primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ + proofEngineTypes.cmx primitiveTactics.cmi +primitiveTactics.cmi: proofEngineTypes.cmo +ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ + proofEngineTypes.cmo ring.cmi +ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ + proofEngineTypes.cmx ring.cmi +ring.cmi: proofEngineTypes.cmo +proofEngine.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmo proofEngineStructuralRules.cmi \ + proofEngineTypes.cmo ring.cmi proofEngine.cmi +proofEngine.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmx proofEngineStructuralRules.cmx \ + proofEngineTypes.cmx ring.cmx proofEngine.cmi +proofEngine.cmi: proofEngineTypes.cmo 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.cmo +logicalOperations.cmo: proofEngine.cmi logicalOperations.cmx: proofEngine.cmx -sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo +sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmi sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx mQueryGenerator.cmo: mQueryGenerator.cmi mQueryGenerator.cmx: mQueryGenerator.cmi gTopLevel.cmo: cic2Xml.cmo cic2acic.cmi logicalOperations.cmo \ - mQueryGenerator.cmi proofEngine.cmo sequentPp.cmo xml2Gdome.cmo + mQueryGenerator.cmi proofEngine.cmi sequentPp.cmo xml2Gdome.cmo 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 121d94f50..57811ff60 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -14,15 +14,21 @@ LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICA all: gTopLevel opt: gTopLevel.opt -DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml \ +DEPOBJS = xml2Gdome.ml proofEngineTypes.ml proofEngineHelpers.ml \ + proofEngineReduction.ml proofEngineStructuralRules.ml \ + proofEngineStructuralRules.mli \ + primitiveTactics.ml primitiveTactics.mli ring.ml ring.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 -TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ +TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ + proofEngineReduction.cmo proofEngineStructuralRules.cmo \ + primitiveTactics.cmo ring.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ - gTopLevel.cmo + gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 85e9b5ebc..15cfdcd10 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2000-2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -47,6 +47,8 @@ let htmlfooter = "" ;; +let prooffile = "/home/zack/dati/HELM/currentproof.gTopLevel" + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let htmlheader_and_content = ref htmlheader;; @@ -55,6 +57,16 @@ let current_cic_infos = ref None;; let current_goal_infos = ref None;; let current_scratch_infos = ref None;; +(* COMMAND LINE OPTIONS *) + +let usedb = ref true + +let argspec = + [ + "-nodb", Arg.Clear usedb, "disable use of MathQL DB" + ] +in +Arg.parse argspec ignore "" (* MISC FUNCTIONS *) @@ -151,11 +163,29 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = (*CSC: We save the innertypes to disk so that we can retrieve them in the *) (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) (*CSC: local. *) - Xml.pp xmlinnertypes (Some "/home/fguidi/innertypes") ; + Xml.pp xmlinnertypes (Some "/tmp/innertypes") ; let output = applyStylesheets input mml_styles mml_args in output ;; + (* pretty print on standard output the current sequent *) +let dumpsequent () = + let metasenv = + match !ProofEngine.proof with + | None -> assert false + | Some (_, metasenv, _, _) -> metasenv + in + let seq = + match !ProofEngine.goal with + | None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + print_string ( + "\n" ^ + (SequentPp.TextualPp.print_sequent seq) ^ + "\n"); + print_newline () +;; (* CALLBACKS *) @@ -632,6 +662,9 @@ let apply rendering_window = let elimintrossimpl rendering_window = call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window ;; +let elimtype rendering_window = + call_tactic_with_input ProofEngine.elim_type rendering_window +;; let whd rendering_window = call_tactic_with_goal_input ProofEngine.whd rendering_window ;; @@ -653,6 +686,7 @@ let change rendering_window = let letin rendering_window = call_tactic_with_input ProofEngine.letin rendering_window ;; +let ring rendering_window = call_tactic ProofEngine.ring rendering_window;; let clearbody rendering_window = call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window ;; @@ -717,7 +751,8 @@ let qed rendering_window () = (*???? let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; *) -let dtdname = "/projects/helm/V7/dtd/cic.dtd";; +(* let dtdname = "/home/zack/dati/HELM/V7/dtd/cic.dtd";; *) +let dtdname = "/public/helm-cvs/helm/dtd/cic.dtd";; let save rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -738,10 +773,10 @@ let save rendering_window () = xml >] in - Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ; + Xml.pp ~quiet:true xml' (Some prooffile) ; output_html outputhtml ("

Current proof saved to " ^ - "/public/sacerdot/currentproof

") + prooffile ^ "") ;; (* Used to typecheck the loaded proofs *) @@ -758,7 +793,7 @@ let load rendering_window () = let proofw = (rendering_window#proofw : GMathView.math_view) in try let uri = UriManager.uri_of_string "cic:/dummy.con" in - match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with + match CicParser.obj_of_xml prooffile uri with Cic.CurrentProof (_,metasenv,bo,ty) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.proof := @@ -772,7 +807,7 @@ let load rendering_window () = refresh_sequent proofw ; output_html outputhtml ("

Current proof loaded from " ^ - "/public/sacerdot/currentproof

") + prooffile ^ "") | _ -> assert false with RefreshSequentException e -> @@ -1370,6 +1405,9 @@ class rendering_window output proofw (label : GMisc.label) = let elimintrossimplb = GButton.button ~label:"ElimIntrosSimpl" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimtypeb = + GButton.button ~label:"ElimType" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let whdb = GButton.button ~label:"Whd" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in @@ -1391,6 +1429,9 @@ class rendering_window output proofw (label : GMisc.label) = let letinb = GButton.button ~label:"Let ... In" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let ringb = + GButton.button ~label:"Ring" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let hbox4 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let clearbodyb = @@ -1399,6 +1440,9 @@ class rendering_window output proofw (label : GMisc.label) = let clearb = GButton.button ~label:"Clear" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let dumpb = + GButton.button ~label:"Dump" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -1441,6 +1485,7 @@ object(self) ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; + ignore(elimtypeb#connect#clicked (elimtype self)) ; ignore(whdb#connect#clicked (whd self)) ; ignore(reduceb#connect#clicked (reduce self)) ; ignore(simplb#connect#clicked (simpl self)) ; @@ -1448,8 +1493,10 @@ object(self) ignore(cutb#connect#clicked (cut self)) ; ignore(changeb#connect#clicked (change self)) ; ignore(letinb#connect#clicked (letin self)) ; + ignore(ringb#connect#clicked (ring self)) ; ignore(clearbodyb#connect#clicked (clearbody self)) ; ignore(clearb#connect#clicked (clear self)) ; + ignore(dumpb#connect#clicked dumpsequent); ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -1471,8 +1518,10 @@ let initialize_everything () = let _ = CicCooking.init () ; - MQueryGenerator.init () ; + if !usedb then MQueryGenerator.init () ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; + if !usedb then MQueryGenerator.close (); MQueryGenerator.close () ;; + diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 074e66c80..9144f4740 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -1,3 +1,28 @@ +(* 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/. + *) + let get_parent id ids_to_terms ids_to_father_ids = match Hashtbl.find ids_to_father_ids id with None -> None diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml new file mode 100644 index 000000000..b52fb7882 --- /dev/null +++ b/helm/gTopLevel/primitiveTactics.ml @@ -0,0 +1,543 @@ +(* 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/. + *) + +open ProofEngineHelpers +open ProofEngineTypes + +exception NotAnInductiveTypeToEliminate +exception NotTheRightEliminatorShape +exception NoHypothesesFound + +(* TODO problemone del fresh_name, aggiungerlo allo status? *) +let fresh_name () = "FOO" + +(* lambda_abstract newmeta ty *) +(* returns a triple [bo],[context],[ty'] where *) +(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) +(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) +(* So, lambda_abstract is the core of the implementation of *) +(* the Intros tactic. *) +let lambda_abstract context newmeta ty name = + let module C = Cic in + let rec collect_context context = + function + C.Cast (te,_) -> collect_context context te + | C.Prod (n,s,t) -> + let n' = + match n with + C.Name _ -> n +(*CSC: generatore di nomi? Chiedere il nome? *) + | C.Anonimous -> C.Name name + in + let (context',ty,bo) = + collect_context ((Some (n',(C.Decl s)))::context) t + in + (context',ty,C.Lambda(n',s,bo)) + | C.LetIn (n,s,t) -> + let (context',ty,bo) = + collect_context ((Some (n,(C.Def s)))::context) t + in + (context',ty,C.LetIn(n,s,bo)) + | _ as t -> + let irl = identity_relocation_list_for_metavariable context in + context, t, (C.Meta (newmeta,irl)) + in + collect_context context ty + +let eta_expand metasenv context t arg = + let module T = CicTypeChecker in + let module S = CicSubstitution in + let module C = Cic in + let rec aux n = + function + t' when t' = S.lift n arg -> C.Rel (1 + n) + | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1) + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) + | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) + | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) + | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) + | C.Appl l -> C.Appl (List.map (aux n) l) + | C.Const _ as t -> t + | C.MutInd _ + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux n outt, aux n t, + List.map (aux n) pl) + | C.Fix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + let argty = + T.type_of_aux' metasenv context arg + in + (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) + +(*CSC: The call to the Intros tactic is embedded inside the code of the *) +(*CSC: Elim tactic. Do we already need tacticals? *) +(* Auxiliary function for apply: given a type (a backbone), it returns its *) +(* head, a META environment in which there is new a META for each hypothesis,*) +(* a list of arguments for the new applications and the indexes of the first *) +(* and last new METAs introduced. The nth argument in the list of arguments *) +(* is the nth new META lambda-abstracted as much as possible. Hence, this *) +(* functions already provides the behaviour of Intros on the new goals. *) +let new_metasenv_for_apply_intros proof context ty = + let module C = Cic in + let module S = CicSubstitution in + let rec aux newmeta = + function + C.Cast (he,_) -> aux newmeta he + | C.Prod (name,s,t) -> + let newcontext,ty',newargument = + lambda_abstract context newmeta s (fresh_name ()) + in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta + | t -> t,[],[],newmeta + in + let newmeta = new_meta ~proof in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in + res,newmetasenv,arguments,newmeta,lastmeta + +(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) +let classify_metas newmeta in_subst_domain subst_in metasenv = + List.fold_right + (fun (i,canonical_context,ty) (old_uninst,new_uninst) -> + if in_subst_domain i then + old_uninst,new_uninst + else + let ty' = subst_in canonical_context ty in + let canonical_context' = + List.fold_right + (fun entry canonical_context' -> + let entry' = + match entry with + Some (n,Cic.Decl s) -> + Some (n,Cic.Decl (subst_in canonical_context' s)) + | Some (n,Cic.Def s) -> + Some (n,Cic.Def (subst_in canonical_context' s)) + | None -> None + in + entry'::canonical_context' + ) canonical_context [] + in + if i < newmeta then + ((i,canonical_context',ty')::old_uninst),new_uninst + else + old_uninst,((i,canonical_context',ty')::new_uninst) + ) metasenv ([],[]) + +(* Auxiliary function for apply: given a type (a backbone), it returns its *) +(* head, a META environment in which there is new a META for each hypothesis,*) +(* a list of arguments for the new applications and the indexes of the first *) +(* and last new METAs introduced. The nth argument in the list of arguments *) +(* is just the nth new META. *) +let new_metasenv_for_apply proof context ty = + let module C = Cic in + let module S = CicSubstitution in + let rec aux newmeta = + function + C.Cast (he,_) -> aux newmeta he + | C.Prod (name,s,t) -> + let irl = identity_relocation_list_for_metavariable context in + let newargument = C.Meta (newmeta,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 1) (S.subst newargument t) + in + res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta + | t -> t,[],[],newmeta + in + let newmeta = new_meta ~proof in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in + res,newmetasenv,arguments,newmeta,lastmeta + +let apply_tac ~status:(proof, goal) ~term = + (* 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 termty = CicTypeChecker.type_of_aux' metasenv context term in + (* newmeta is the lowest index of the new metas introduced *) + let (consthead,newmetas,arguments,newmeta,_) = + new_metasenv_for_apply proof context termty + in + let newmetasenv = newmetas@metasenv in + let subst,newmetasenv' = + CicUnification.fo_unif newmetasenv context consthead ty + in + let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in + let apply_subst = CicUnification.apply_subst subst in + let old_uninstantiatedmetas,new_uninstantiatedmetas = + (* subst_in doesn't need the context. Hence the underscore. *) + let subst_in _ = CicUnification.apply_subst subst in + classify_metas newmeta in_subst_domain subst_in newmetasenv' + in + let bo' = + if List.length newmetas = 0 then + term + else + let arguments' = List.map apply_subst arguments in + Cic.Appl (term::arguments') + in + let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in + let (newproof, newmetasenv''') = + let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in + subst_meta_and_metasenv_in_proof + proof metano subst_in newmetasenv'' + in + (newproof, + (match newmetasenv''' with + | [] -> None + | (i,_,_)::_ -> Some i)) + + (* TODO per implementare i tatticali e' necessario che tutte le tattiche + sollevino _solamente_ Fail *) +let apply_tac ~status ~term = + try + apply_tac ~status ~term + (* TODO cacciare anche altre eccezioni? *) + with CicUnification.UnificationFailed as e -> + raise (Fail (Printexc.to_string e)) + +let intros_tac ~status:(proof, goal) ~name = + 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 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) + +let cut_tac ~status:(proof, goal) ~term = + 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 newmeta1 = new_meta ~proof in + let newmeta2 = newmeta1 + 1 in + let context_for_newmeta1 = + (Some (C.Name "dummy_for_cut",C.Decl term))::context in + let irl1 = + identity_relocation_list_for_metavariable context_for_newmeta1 in + let irl2 = identity_relocation_list_for_metavariable context in + let newmeta1ty = CicSubstitution.lift 1 ty in + let bo' = + C.Appl + [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; + C.Meta (newmeta2,irl2)] + in + let (newproof, _) = + subst_meta_in_proof proof metano bo' + [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; + in + let newgoal = Some newmeta1 in + (newproof, newgoal) + +let letin_tac ~status:(proof, goal) ~term = + 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 _ = CicTypeChecker.type_of_aux' metasenv context term in + let newmeta = new_meta ~proof in + let context_for_newmeta = + (Some (C.Name "dummy_for_letin",C.Def term))::context in + let irl = + identity_relocation_list_for_metavariable context_for_newmeta in + let newmetaty = CicSubstitution.lift 1 ty in + let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in + let (newproof, _) = + subst_meta_in_proof + proof metano bo'[newmeta,context_for_newmeta,newmetaty] + in + let newgoal = Some newmeta in + (newproof, newgoal) + + (** functional part of the "exact" tactic *) +let exact_tac ~status:(proof, goal) ~term = + (* 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 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) + 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 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 termty = T.type_of_aux' metasenv context term in + let uri,cookingno,typeno,args = + match termty with + C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[]) + | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) -> + (uri,cookingno,typeno,args) + | _ -> + prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty)); + flush stderr; + raise NotAnInductiveTypeToEliminate + in + let eliminator_uri = + let buri = U.buri_of_uri uri in + let name = + match CicEnvironment.get_cooked_obj uri cookingno with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv context ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.Type -> "_rect" + | _ -> assert false + in + U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + in + let eliminator_cookingno = + UriManager.relative_depth curi eliminator_uri 0 + in + let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in + let ety = + T.type_of_aux' [] [] eliminator_ref + in + let (econclusion,newmetas,arguments,newmeta,lastmeta) = +(* + new_metasenv_for_apply context ety +*) + new_metasenv_for_apply_intros proof context ety + in + (* Here we assume that we have only one inductive hypothesis to *) + (* eliminate and that it is the last hypothesis of the theorem. *) + (* A better approach would be fingering the hypotheses in some *) + (* way. *) + let meta_of_corpse = + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas + in + let irl = + identity_relocation_list_for_metavariable canonical_context + in + Cic.Meta (lastmeta - 1, irl) + in + let newmetasenv = newmetas @ metasenv in + let subst1,newmetasenv' = + CicUnification.fo_unif newmetasenv context term meta_of_corpse + in + let ueconclusion = CicUnification.apply_subst subst1 econclusion in + (* The conclusion of our elimination principle is *) + (* (?i farg1 ... fargn) *) + (* The conclusion of our goal is ty. So, we can *) + (* eta-expand ty w.r.t. farg1 .... fargn to get *) + (* a new ty equal to (P farg1 ... fargn). Now *) + (* ?i can be instantiated with P and we are ready *) + (* to refine the term. *) + let emeta, fargs = + match ueconclusion with +(*CSC: Code to be used for Apply + C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs + | C.Meta (emeta,_) -> emeta,[] +*) +(*CSC: Code to be used for ApplyIntros *) + C.Appl (he::fargs) -> + let rec find_head = + function + C.Meta (emeta,_) -> emeta + | C.Lambda (_,_,t) -> find_head t + | C.LetIn (_,_,t) -> find_head t + | _ ->raise NotTheRightEliminatorShape + in + find_head he,fargs + | C.Meta (emeta,_) -> emeta,[] +(* *) + | _ -> raise NotTheRightEliminatorShape + in + let ty' = CicUnification.apply_subst subst1 ty in + let eta_expanded_ty = +(*CSC: newmetasenv' era metasenv ??????????? *) + List.fold_left (eta_expand newmetasenv' context) ty' fargs + in + let subst2,newmetasenv'' = +(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite +da subst1!!!! Dovrei rimuoverle o sono innocue?*) + CicUnification.fo_unif + newmetasenv' context ueconclusion eta_expanded_ty + in + let in_subst_domain i = + let eq_to_i = function (j,_) -> i=j in + List.exists eq_to_i subst1 || + List.exists eq_to_i subst2 + in +(*CSC: codice per l'elim + (* When unwinding the META that corresponds to the elimination *) + (* predicate (which is emeta), we must also perform one-step *) + (* beta-reduction. apply_subst doesn't need the context. Hence *) + (* the underscore. *) + let apply_subst _ t = + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + subst2 (Some (emeta,List.length fargs)) t' + in +*) +(*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *) + let apply_subst context t = + let t' = CicUnification.apply_subst (subst1@subst2) t in + ProofEngineReduction.simpl context t' + in +(* *) + let old_uninstantiatedmetas,new_uninstantiatedmetas = + classify_metas newmeta in_subst_domain apply_subst + newmetasenv'' + in + let arguments' = List.map (apply_subst context) arguments in + let bo' = Cic.Appl (eliminator_ref::arguments') in + let newmetasenv''' = + new_uninstantiatedmetas@old_uninstantiatedmetas + in + let (newproof, newmetasenv'''') = + (* When unwinding the META that corresponds to the *) + (* elimination predicate (which is emeta), we must *) + (* also perform one-step beta-reduction. *) + (* The only difference w.r.t. apply_subst is that *) + (* we also substitute metano with bo'. *) + (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) + (*CSC: no? *) +(*CSC: codice per l'elim + let apply_subst' t = + let t' = CicUnification.apply_subst subst1 t in + CicUnification.apply_subst_reducing + ((metano,bo')::subst2) + (Some (emeta,List.length fargs)) t' + in +*) +(*CSC: codice per l'elim_intros_simpl *) + let apply_subst' t = + CicUnification.apply_subst + ((metano,bo')::(subst1@subst2)) t + in +(* *) + subst_meta_and_metasenv_in_proof + proof metano apply_subst' newmetasenv''' + in + (newproof, + (match newmetasenv'''' with + | [] -> None + | (i,_,_)::_ -> Some i)) + diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli new file mode 100644 index 000000000..87142b564 --- /dev/null +++ b/helm/gTopLevel/primitiveTactics.mli @@ -0,0 +1,13 @@ +val apply_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status +val exact_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status +val intros_tac: + status: ProofEngineTypes.status -> name: string-> ProofEngineTypes.status +val cut_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status +val letin_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status + +val elim_intros_simpl_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index c605d41a9..ca8c0b54d 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -23,97 +23,18 @@ * http://cs.unibo.it/helm/. *) -let proof = - ref (None : (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option) -;; -let goal = ref (None : int option);; +open ProofEngineHelpers +open ProofEngineTypes -(*CSC: commento vecchio *) -(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *) -(* This (heavy) function must be called when a tactic can instantiate old *) -(* metavariables (i.e. existential variables). It substitues the metasenv *) -(* of the proof with the result of removing [meta] from the domain of *) -(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) -(* in the current proof. Finally it applies [apply_subst_replacing] to *) -(* current proof. *) -(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) -(*CSC: ci ripasso sopra apply_subst!!! *) -(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *) -(*CSC: [newmetasenv]. *) -let subst_meta_and_metasenv_in_current_proof meta subst_in newmetasenv = - let (uri,bo,ty) = - match !proof with - None -> assert false - | Some (uri,_,bo,ty) -> uri,bo,ty - in - let bo' = subst_in bo in - let metasenv' = - List.fold_right - (fun metasenv_entry i -> - match metasenv_entry with - (m,canonical_context,ty) when m <> meta -> - let canonical_context' = - List.map - (function - None -> None - | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) - | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) - ) canonical_context - in - (m,canonical_context',subst_in ty)::i - | _ -> i - ) newmetasenv [] - in - proof := Some (uri,metasenv',bo',ty) ; - metasenv' -;; + (* proof assistant status *) -let subst_meta_in_current_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 subst_in = CicUnification.apply_subst [meta,term] in - let metasenv' = - newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) - in - let metasenv'' = - List.map - (function i,canonical_context,ty -> - let canonical_context' = - List.map - (function - Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) - | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s)) - | None -> None - ) canonical_context - in - i,canonical_context',(subst_in ty) - ) metasenv' - in - let bo' = subst_in bo in - proof := Some (uri,metasenv'',bo',ty) ; - metasenv'' -;; +let proof = ref (None : proof) +let goal = ref (None : goal) -(* Returns the first meta whose number is above the *) -(* number of the higher meta. *) -let new_meta () = - let metasenv = - match !proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let rec aux = - function - None,[] -> 1 - | Some n,[] -> n - | None,(n,_,_)::tl -> aux (Some n,tl) - | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) - in - 1 + aux (None,metasenv) -;; +let apply_tactic ~tactic:tactic = + let (newproof, newgoal) = tactic ~status:(!proof, !goal) in + proof := newproof; + goal := newgoal (* metas_in_term term *) (* Returns the ordered list of the metas that occur in [term]. *) @@ -151,22 +72,6 @@ let metas_in_term term = he::(elim_duplicates (List.filter (function el -> he <> el) tl)) in elim_duplicates metas -;; - -(* 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] *) -(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) -let identity_relocation_list_for_metavariable canonical_context = - let canonical_context_length = List.length canonical_context in - let rec aux = - function - (_,[]) -> [] - | (n,None::tl) -> None::(aux ((n+1),tl)) - | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) - in - aux (1,canonical_context) -;; (* perforate context term ty *) (* replaces the term [term] in the proof with a new metavariable whose type *) @@ -175,7 +80,7 @@ let identity_relocation_list_for_metavariable canonical_context = (* are efficiency reasons. *) let perforate context term ty = let module C = Cic in - let newmeta = new_meta () in + let newmeta = new_meta !proof in match !proof with None -> assert false | Some (uri,metasenv,bo,gty) -> @@ -199,14 +104,12 @@ let perforate context term ty = in proof := Some (uri,metasenv'',bo',gty) ; goal := Some newmeta -;; + (************************************************************) (* Some easy tactics. *) (************************************************************) -exception Fail of string;; - (*CSC: generatore di nomi? Chiedere il nome? *) let fresh_name = let next_fresh_index = ref 0 @@ -214,444 +117,6 @@ in function () -> incr next_fresh_index ; "fresh_name" ^ string_of_int !next_fresh_index -;; - -(* lambda_abstract newmeta ty *) -(* returns a triple [bo],[context],[ty'] where *) -(* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) -(* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *) -(* So, lambda_abstract is the core of the implementation of *) -(* the Intros tactic. *) -let lambda_abstract context newmeta ty = - let module C = Cic in - let rec collect_context context = - function - C.Cast (te,_) -> collect_context context te - | C.Prod (n,s,t) -> - let n' = - match n with - C.Name _ -> n -(*CSC: generatore di nomi? Chiedere il nome? *) - | C.Anonimous -> C.Name (fresh_name ()) - in - let (context',ty,bo) = - collect_context ((Some (n',(C.Decl s)))::context) t - in - (context',ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> - let (context',ty,bo) = - collect_context ((Some (n,(C.Def s)))::context) t - in - (context',ty,C.LetIn(n,s,bo)) - | _ as t -> - let irl = identity_relocation_list_for_metavariable context in - context, t, (C.Meta (newmeta,irl)) - in - collect_context context ty -;; - -let intros () = - 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 newmeta = new_meta () in - let (context',ty',bo') = lambda_abstract context newmeta ty in - let _ = subst_meta_in_current_proof metano bo' [newmeta,context',ty'] in - goal := Some newmeta -;; - -(* The term bo must be closed in the current context *) -let exact bo = - let module T = CicTypeChecker 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 - if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then - begin - let metasenv' = subst_meta_in_current_proof metano bo [] in - goal := - match metasenv' with - [] -> None - | (n,_,_)::_ -> Some n - end - else - raise (Fail "The type of the provided term is not the one expected.") -;; - -(*CSC: The call to the Intros tactic is embedded inside the code of the *) -(*CSC: Elim tactic. Do we already need tacticals? *) -(* Auxiliary function for apply: given a type (a backbone), it returns its *) -(* head, a META environment in which there is new a META for each hypothesis,*) -(* a list of arguments for the new applications and the indexes of the first *) -(* and last new METAs introduced. The nth argument in the list of arguments *) -(* is the nth new META lambda-abstracted as much as possible. Hence, this *) -(* functions already provides the behaviour of Intros on the new goals. *) -let new_metasenv_for_apply_intros context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let newcontext,ty',newargument = lambda_abstract context newmeta s in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta - | t -> t,[],[],newmeta - in - let newmeta = new_meta () in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in - res,newmetasenv,arguments,newmeta,lastmeta -;; - -(* Auxiliary function for apply: given a type (a backbone), it returns its *) -(* head, a META environment in which there is new a META for each hypothesis,*) -(* a list of arguments for the new applications and the indexes of the first *) -(* and last new METAs introduced. The nth argument in the list of arguments *) -(* is just the nth new META. *) -let new_metasenv_for_apply context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let irl = identity_relocation_list_for_metavariable context in - let newargument = C.Meta (newmeta,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta - | t -> t,[],[],newmeta - in - let newmeta = new_meta () in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in - res,newmetasenv,arguments,newmeta,lastmeta -;; - - -(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) -let classify_metas newmeta in_subst_domain subst_in metasenv = - List.fold_right - (fun (i,canonical_context,ty) (old_uninst,new_uninst) -> - if in_subst_domain i then - old_uninst,new_uninst - else - let ty' = subst_in canonical_context ty in - let canonical_context' = - List.fold_right - (fun entry canonical_context' -> - let entry' = - match entry with - Some (n,Cic.Decl s) -> - Some (n,Cic.Decl (subst_in canonical_context' s)) - | Some (n,Cic.Def s) -> - Some (n,Cic.Def (subst_in canonical_context' s)) - | None -> None - in - entry'::canonical_context' - ) canonical_context [] - in - if i < newmeta then - ((i,canonical_context',ty')::old_uninst),new_uninst - else - old_uninst,((i,canonical_context',ty')::new_uninst) - ) metasenv ([],[]) -;; - -(* The term bo must be closed in the current context *) -let apply term = - 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 termty = CicTypeChecker.type_of_aux' metasenv context term in - (* newmeta is the lowest index of the new metas introduced *) - let (consthead,newmetas,arguments,newmeta,_) = - new_metasenv_for_apply context termty - in - let newmetasenv = newmetas@metasenv in - let subst,newmetasenv' = - CicUnification.fo_unif newmetasenv context consthead ty - in - let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in - let apply_subst = CicUnification.apply_subst subst in - let old_uninstantiatedmetas,new_uninstantiatedmetas = - (* subst_in doesn't need the context. Hence the underscore. *) - let subst_in _ = CicUnification.apply_subst subst in - classify_metas newmeta in_subst_domain subst_in newmetasenv' - in - let bo' = - if List.length newmetas = 0 then - term - else - let arguments' = List.map apply_subst arguments in - Cic.Appl (term::arguments') - in - let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in - let newmetasenv''' = - let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in - subst_meta_and_metasenv_in_current_proof metano subst_in - newmetasenv'' - in - match newmetasenv''' with - [] -> goal := None - | (i,_,_)::_ -> goal := Some i -;; - -let eta_expand metasenv context t arg = - let module T = CicTypeChecker in - let module S = CicSubstitution in - let module C = Cic in - let rec aux n = - function - t' when t' = S.lift n arg -> C.Rel (1 + n) - | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1) - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) - | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) - | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) - | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) - | C.Appl l -> C.Appl (List.map (aux n) l) - | C.Const _ as t -> t - | C.MutInd _ - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,aux n outt, aux n t, - List.map (aux n) pl) - | C.Fix (i,fl) -> - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) - fl - in - C.CoFix (i, substitutedfl) - in - let argty = - T.type_of_aux' metasenv context arg - in - (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) -;; - -exception NotAnInductiveTypeToEliminate;; -exception NotTheRightEliminatorShape;; -exception NoHypothesesFound;; - -let elim_intros_simpl term = - 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 termty = T.type_of_aux' metasenv context term in - let uri,cookingno,typeno,args = - match termty with - C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[]) - | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) -> - (uri,cookingno,typeno,args) - | _ -> raise NotAnInductiveTypeToEliminate - in - let eliminator_uri = - let buri = U.buri_of_uri uri in - let name = - match CicEnvironment.get_cooked_obj uri cookingno with - C.InductiveDefinition (tys,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - | _ -> assert false - in - let ext = - match T.type_of_aux' metasenv context ty with - C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.Type -> "_rect" - | _ -> assert false - in - U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") - in - let eliminator_cookingno = - UriManager.relative_depth curi eliminator_uri 0 - in - let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in - let ety = - T.type_of_aux' [] [] eliminator_ref - in - let (econclusion,newmetas,arguments,newmeta,lastmeta) = -(* - new_metasenv_for_apply context ety -*) - new_metasenv_for_apply_intros context ety - in - (* Here we assume that we have only one inductive hypothesis to *) - (* eliminate and that it is the last hypothesis of the theorem. *) - (* A better approach would be fingering the hypotheses in some *) - (* way. *) - let meta_of_corpse = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas - in - let irl = - identity_relocation_list_for_metavariable canonical_context - in - Cic.Meta (lastmeta - 1, irl) - in - let newmetasenv = newmetas @ metasenv in - let subst1,newmetasenv' = - CicUnification.fo_unif newmetasenv context term meta_of_corpse - in - let ueconclusion = CicUnification.apply_subst subst1 econclusion in - (* The conclusion of our elimination principle is *) - (* (?i farg1 ... fargn) *) - (* The conclusion of our goal is ty. So, we can *) - (* eta-expand ty w.r.t. farg1 .... fargn to get *) - (* a new ty equal to (P farg1 ... fargn). Now *) - (* ?i can be instantiated with P and we are ready *) - (* to refine the term. *) - let emeta, fargs = - match ueconclusion with -(*CSC: Code to be used for Apply - C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs - | C.Meta (emeta,_) -> emeta,[] -*) -(*CSC: Code to be used for ApplyIntros *) - C.Appl (he::fargs) -> - let rec find_head = - function - C.Meta (emeta,_) -> emeta - | C.Lambda (_,_,t) -> find_head t - | C.LetIn (_,_,t) -> find_head t - | _ ->raise NotTheRightEliminatorShape - in - find_head he,fargs - | C.Meta (emeta,_) -> emeta,[] -(* *) - | _ -> raise NotTheRightEliminatorShape - in - let ty' = CicUnification.apply_subst subst1 ty in - let eta_expanded_ty = -(*CSC: newmetasenv' era metasenv ??????????? *) - List.fold_left (eta_expand newmetasenv' context) ty' fargs - in - let subst2,newmetasenv'' = -(*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite -da subst1!!!! Dovrei rimuoverle o sono innocue?*) - CicUnification.fo_unif - newmetasenv' context ueconclusion eta_expanded_ty - in - let in_subst_domain i = - let eq_to_i = function (j,_) -> i=j in - List.exists eq_to_i subst1 || - List.exists eq_to_i subst2 - in -(*CSC: codice per l'elim - (* When unwinding the META that corresponds to the elimination *) - (* predicate (which is emeta), we must also perform one-step *) - (* beta-reduction. apply_subst doesn't need the context. Hence *) - (* the underscore. *) - let apply_subst _ t = - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - subst2 (Some (emeta,List.length fargs)) t' - in -*) -(*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *) - let apply_subst context t = - let t' = CicUnification.apply_subst (subst1@subst2) t in - ProofEngineReduction.simpl context t' - in -(* *) - let old_uninstantiatedmetas,new_uninstantiatedmetas = - classify_metas newmeta in_subst_domain apply_subst - newmetasenv'' - in - let arguments' = List.map (apply_subst context) arguments in - let bo' = Cic.Appl (eliminator_ref::arguments') in - let newmetasenv''' = - new_uninstantiatedmetas@old_uninstantiatedmetas - in - let newmetasenv'''' = - (* When unwinding the META that corresponds to the *) - (* elimination predicate (which is emeta), we must *) - (* also perform one-step beta-reduction. *) - (* The only difference w.r.t. apply_subst is that *) - (* we also substitute metano with bo'. *) - (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) - (*CSC: no? *) -(*CSC: codice per l'elim - let apply_subst' t = - let t' = CicUnification.apply_subst subst1 t in - CicUnification.apply_subst_reducing - ((metano,bo')::subst2) - (Some (emeta,List.length fargs)) t' - in -*) -(*CSC: codice per l'elim_intros_simpl *) - let apply_subst' t = - CicUnification.apply_subst - ((metano,bo')::(subst1@subst2)) t - in -(* *) - subst_meta_and_metasenv_in_current_proof metano - apply_subst' newmetasenv''' - in - match newmetasenv'''' with - [] -> goal := None - | (i,_,_)::_ -> goal := Some i -;; let reduction_tactic reduction_function term = let curi,metasenv,pbo,pty = @@ -702,7 +167,6 @@ let reduction_tactic reduction_function term = in proof := Some (curi,metasenv',pbo,pty) ; goal := Some metano -;; (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) let reduction_tactic_in_scratch reduction_function term ty = @@ -719,17 +183,16 @@ let reduction_tactic_in_scratch reduction_function term ty = let term' = reduction_function context term in ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' ~where:ty -;; -let whd = reduction_tactic CicReduction.whd;; -let reduce = reduction_tactic ProofEngineReduction.reduce;; -let simpl = reduction_tactic ProofEngineReduction.simpl;; +let whd = reduction_tactic CicReduction.whd +let reduce = reduction_tactic ProofEngineReduction.reduce +let simpl = reduction_tactic ProofEngineReduction.simpl -let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;; +let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd let reduce_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.reduce;; + reduction_tactic_in_scratch ProofEngineReduction.reduce let simpl_in_scratch = - reduction_tactic_in_scratch ProofEngineReduction.simpl;; + reduction_tactic_in_scratch ProofEngineReduction.simpl (* It is just the opposite of whd. The code should probably be merged. *) let fold term = @@ -771,65 +234,8 @@ let fold term = in proof := Some (curi,metasenv',pbo,pty) ; goal := Some metano -;; - -let cut term = - 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 newmeta1 = new_meta () in - let newmeta2 = newmeta1 + 1 in - let context_for_newmeta1 = - (Some (C.Name "dummy_for_cut",C.Decl term))::context in - let irl1 = - identity_relocation_list_for_metavariable context_for_newmeta1 in - let irl2 = identity_relocation_list_for_metavariable context in - let newmeta1ty = CicSubstitution.lift 1 ty in - let bo' = - C.Appl - [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in - let _ = - subst_meta_in_current_proof metano bo' - [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; - in - goal := Some newmeta1 -;; -let letin term = - 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 _ = CicTypeChecker.type_of_aux' metasenv context term in - let newmeta = new_meta () in - let context_for_newmeta = - (Some (C.Name "dummy_for_letin",C.Def term))::context in - let irl = - identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in - let _ = subst_meta_in_current_proof metano bo' [newmeta,context_for_newmeta,newmetaty] in - goal := Some newmeta -;; - -exception NotConvertible;; +exception NotConvertible (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *) (*CSC: while [goal_input] can have a richer context (because of binders) *) @@ -875,142 +281,29 @@ let change ~goal_input ~input = end else raise NotConvertible -;; -let clearbody = - let module C = Cic in - function - 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 string_of_name = - function - C.Name n -> n - | C.Anonimous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear_body -> - let cleared_entry = - let ty = - CicTypeChecker.type_of_aux' metasenv context term - in - Some (n_to_clear_body, Cic.Decl ty) - in - cleared_entry::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def t) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("The correctness of hypothesis " ^ - string_of_name n ^ - " relies on the body of " ^ - string_of_name n_to_clear_body) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("The correctness of the goal relies on the body of " ^ - string_of_name n_to_clear_body)) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) -;; +(************************************************************) +(* Tactics defined elsewhere *) +(************************************************************) + + (* primitive tactics *) + +let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) +let intros () = + apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ())) +let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) +let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) +let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) +let elim_intros_simpl term = + apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) + + (* structural tactics *) + +let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp) +let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) + + (* other tactics *) + +let elim_type term = apply_tactic (Ring.elim_type_tac ~term) +let ring () = apply_tactic Ring.ring_tac -let clear hyp_to_clear = - 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 metano,context,ty = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonimous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear -> None::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def t) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("Hypothesis " ^ - string_of_name n ^ - " uses hypothesis " ^ - string_of_name n_to_clear) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("Hypothesis " ^ string_of_name n_to_clear ^ - " occurs in the goal")) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) -;; diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli new file mode 100644 index 000000000..1b110a669 --- /dev/null +++ b/helm/gTopLevel/proofEngine.mli @@ -0,0 +1,38 @@ + +exception NotConvertible + + (* proof engine status *) +val proof : ProofEngineTypes.proof ref +val goal : ProofEngineTypes.goal ref + + (* start a new goal undoing part of the proof *) +val perforate : Cic.context -> Cic.term -> Cic.term -> unit + + (* reduction tactics *) +val whd : Cic.term -> unit +val reduce : Cic.term -> unit +val simpl : Cic.term -> unit +val fold : Cic.term -> unit +val change : goal_input:Cic.term -> input:Cic.term -> unit + + (* scratch area reduction tactics *) +val whd_in_scratch : Cic.term -> Cic.term -> Cic.term +val reduce_in_scratch : Cic.term -> Cic.term -> Cic.term +val simpl_in_scratch : Cic.term -> Cic.term -> Cic.term + + (* "primitive" tactics *) +val apply : Cic.term -> unit +val intros : unit -> unit +val cut : Cic.term -> unit +val letin : Cic.term -> unit +val exact : Cic.term -> unit +val elim_intros_simpl : Cic.term -> unit + + (* structural tactics *) +val clearbody : Cic.hypothesis -> unit +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 new file mode 100644 index 000000000..7e5f3a4b1 --- /dev/null +++ b/helm/gTopLevel/proofEngineHelpers.ml @@ -0,0 +1,123 @@ +(* 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/. + *) + +(* 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] *) +(*CSC: ma mi basta la lunghezza del contesto canonico!!!*) +let identity_relocation_list_for_metavariable canonical_context = + let canonical_context_length = List.length canonical_context in + let rec aux = + function + (_,[]) -> [] + | (n,None::tl) -> None::(aux ((n+1),tl)) + | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl)) + in + aux (1,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 rec aux = + function + None,[] -> 1 + | Some n,[] -> n + | None,(n,_,_)::tl -> aux (Some n,tl) + | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl) + in + 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 subst_in = CicUnification.apply_subst [meta,term] in + let metasenv' = + newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv) + in + let metasenv'' = + List.map + (function i,canonical_context,ty -> + let canonical_context' = + List.map + (function + Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s)) + | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s)) + | None -> None + ) canonical_context + in + i,canonical_context',(subst_in ty) + ) metasenv' + in + let bo' = subst_in bo in + let newproof = Some (uri,metasenv'',bo',ty) in + (newproof, metasenv'') + +(*CSC: commento vecchio *) +(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *) +(* This (heavy) function must be called when a tactic can instantiate old *) +(* metavariables (i.e. existential variables). It substitues the metasenv *) +(* of the proof with the result of removing [meta] from the domain of *) +(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *) +(* in the current proof. Finally it applies [apply_subst_replacing] to *) +(* current proof. *) +(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *) +(*CSC: ci ripasso sopra apply_subst!!! *) +(*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 bo' = subst_in bo in + let metasenv' = + List.fold_right + (fun metasenv_entry i -> + match metasenv_entry with + (m,canonical_context,ty) when m <> meta -> + let canonical_context' = + List.map + (function + None -> None + | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t)) + | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t)) + ) canonical_context + in + (m,canonical_context',subst_in ty)::i + | _ -> i + ) newmetasenv [] + in + let newproof = Some (uri,metasenv',bo',ty) in + (newproof, metasenv') + diff --git a/helm/gTopLevel/proofEngineHelpers.mli b/helm/gTopLevel/proofEngineHelpers.mli new file mode 100644 index 000000000..89f697750 --- /dev/null +++ b/helm/gTopLevel/proofEngineHelpers.mli @@ -0,0 +1,11 @@ +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 +val subst_meta_in_proof : + ProofEngineTypes.proof -> + int -> Cic.term -> Cic.metasenv -> + ProofEngineTypes.proof * Cic.metasenv +val subst_meta_and_metasenv_in_proof : + ProofEngineTypes.proof -> + int -> (Cic.term -> Cic.term) -> Cic.metasenv -> + ProofEngineTypes.proof * Cic.metasenv diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 8589a6442..87cf24c21 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml new file mode 100644 index 000000000..e3e024f34 --- /dev/null +++ b/helm/gTopLevel/proofEngineStructuralRules.ml @@ -0,0 +1,163 @@ +(* 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/. + *) + +open ProofEngineTypes + +let clearbody ~status:(proof, goal) ~hyp = + 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 string_of_name = + function + C.Name n -> n + | C.Anonimous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear_body -> + let cleared_entry = + let ty = + CicTypeChecker.type_of_aux' metasenv context term + in + Some (n_to_clear_body, Cic.Decl ty) + in + cleared_entry::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def t) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ + string_of_name n_to_clear_body) + ) + in + entry::context + ) canonical_context [] + in + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("The correctness of the goal relies on the body of " ^ + string_of_name n_to_clear_body)) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (Some (curi,metasenv',pbo,pty), goal) + +let clear ~status:(proof, goal) ~hyp:hyp_to_clear = + 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 metano,context,ty = + match goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + let string_of_name = + function + C.Name n -> n + | C.Anonimous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (fun entry context -> + match entry with + t when t == hyp_to_clear -> None::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def t) -> + let _ = + try + CicTypeChecker.type_of_aux' metasenv context t + with + _ -> + raise + (Fail + ("Hypothesis " ^ + string_of_name n ^ + " uses hypothesis " ^ + string_of_name n_to_clear) + ) + in + entry::context + ) canonical_context [] + in + let _ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + with + _ -> + raise + (Fail + ("Hypothesis " ^ string_of_name n_to_clear ^ + " occurs in the goal")) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (Some (curi,metasenv',pbo,pty), goal) + diff --git a/helm/gTopLevel/proofEngineStructuralRules.mli b/helm/gTopLevel/proofEngineStructuralRules.mli new file mode 100644 index 000000000..a0a423cff --- /dev/null +++ b/helm/gTopLevel/proofEngineStructuralRules.mli @@ -0,0 +1,6 @@ +val clearbody: + status: ProofEngineTypes.status -> + hyp: Cic.hypothesis -> ProofEngineTypes.status +val clear: + status: ProofEngineTypes.status -> + hyp: Cic.hypothesis -> ProofEngineTypes.status diff --git a/helm/gTopLevel/proofEngineTypes.ml b/helm/gTopLevel/proofEngineTypes.ml new file mode 100644 index 000000000..38492fce9 --- /dev/null +++ b/helm/gTopLevel/proofEngineTypes.ml @@ -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/. + *) + + (** + current proof (proof uri * metas * (in)complete proof * term to be prooved), + possibly None + *) +type proof = (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option + (** current goal, integer index *) +type goal = int option + (** current status: (proof, goal) pair *) +type status = proof * goal + (** + 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 + + (** tactic failure *) +exception Fail of string + diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml new file mode 100644 index 000000000..080e280b5 --- /dev/null +++ b/helm/gTopLevel/ring.ml @@ -0,0 +1,607 @@ +(* 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/. + *) + +open CicReduction +open PrimitiveTactics +open ProofEngineTypes +open UriManager + +(** DEBUGGING *) + + (** perform debugging output? *) +let debug = false + + (** debugging print *) +let warn s = + if debug then + prerr_endline ("RING WARNING: " ^ s) + +(** CIC URIS *) + +(** + Note: For constructors URIs aren't really URIs but rather triples of + the form (uri, typeno, consno). This discrepancy is to preserver an + uniformity of invocation of "mkXXX" functions. +*) + +let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" +let refl_eqt_uri = (eqt_uri, 0, 1) +let sym_eqt_uri = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con" +let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" +let true_uri = (bool_uri, 0, 1) +let false_uri = (bool_uri, 0, 2) + +let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con" +let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" +let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con" +let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con" +let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" +let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" +let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" + +let apolynomial_uri = + uri_of_string + "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind" +let apvar_uri = (apolynomial_uri, 0, 1) +let ap0_uri = (apolynomial_uri, 0, 2) +let ap1_uri = (apolynomial_uri, 0, 3) +let applus_uri = (apolynomial_uri, 0, 4) +let apmult_uri = (apolynomial_uri, 0, 5) +let apopp_uri = (apolynomial_uri, 0, 6) + +let varmap_uri = + uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap.ind" +let empty_vm_uri = (varmap_uri, 0, 1) +let node_vm_uri = (varmap_uri, 0, 2) +let varmap_find_uri = + uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap_find.con" +let index_uri = + uri_of_string "cic:/Coq/ring/Quote/variables_map/index.ind" +let left_idx_uri = (index_uri, 0, 1) +let right_idx_uri = (index_uri, 0, 2) +let end_idx_uri = (index_uri, 0, 3) + +let interp_ap_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con" +let interp_sacs_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con" +let apolynomial_normalize_uri = + uri_of_string + "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con" +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 *) + + (** + check whether a term is a constant or not, if argument "uri" is given and is + not "None" also check if the constant correspond to the given one or not + *) +let cic_is_const ?(uri: uri option = None) term = + match uri with + | None -> + (match term with + | Cic.Const _ -> true + | _ -> false) + | Some realuri -> + (match term with + | Cic.Const (u, _) when (eq u realuri) -> true + | _ -> false) + +(** PROOF AND GOAL ACCESSORS *) + + (** + @param proof a proof + @return the uri of a given proof + *) +let uri_of_proof ~proof:(uri, _, _, _) = uri + + (** + @param metano meta list index + @param metasenv meta list (environment) + @raise Failure if metano is not found in metasenv + @return conjecture corresponding to metano in metasenv + *) +let conj_of_metano metano = + try + List.find (function (m, _, _) -> m = metano) + with Not_found -> + failwith ( + "Ring.conj_of_metano: " ^ + (string_of_int metano) ^ " no such meta") + + (** + @param status current proof engine status + @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 + + (** + @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 + +(** CIC TERM CONSTRUCTORS *) + + (** + Create a Cic term consisting of a constant + @param uri URI of the constant + @proof current proof + *) +let mkConst ~uri ~proof = + let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in + Cic.Const (uri, cookingsno) + + (** + Create a Cic term consisting of a constructor + @param uri triple where uri is the uri of an inductive + type, typeno is the type number in a mutind structure (0 based), consno is + the constructor number (1 based) + @param proof current proof + *) +let mkCtor ~uri:(uri, typeno, consno) ~proof = + let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in + Cic.MutConstruct (uri, cookingsno, typeno, consno) + + (** + Create a Cic term consisting of a type member of a mutual induction + @param uri pair where uri is the uri of a mutual inductive + type and typeno is the type number (0 based) in the mutual induction + *) +let mkMutInd ~uri:(uri, typeno) ~proof = + let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in + Cic.MutInd (uri, cookingsno, typeno) + +(** EXCEPTIONS *) + + (** + raised when the current goal is not ringable; a goal is ringable when is an + equality on reals (@see r_uri) + *) +exception GoalUnringable + +(** RING's FUNCTIONS LIBRARY *) + + (** + Check whether the ring tactic can be applied on a given term (i.e. that is + an equality on reals) + @param term term to be tested + @return true if the term is ringable, false otherwise + *) +let ringable = + let is_equality = function + | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true + | _ -> false + in + let is_real = function + | Cic.Const (uri, _) when (eq uri r_uri) -> true + | _ -> false + in + function + | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) -> + warn "Goal Ringable!"; + true + | _ -> + warn "Goal Not Ringable :-(("; + false + + (** + split an equality goal of the form "t1 = t2" in its two subterms t1 and t2 + after checking that the goal is ringable + @param goal the current goal + @return a pair (t1,t2) that are two sides of the equality goal + @raise GoalUnringable if the goal isn't ringable + *) +let split_eq = function + | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term -> + warn ("" ^ (CicPp.ppterm t1) ^ ""); + warn ("" ^ (CicPp.ppterm t2) ^ ""); + (t1, t2) + | _ -> raise GoalUnringable + + (** + @param i an integer index representing a 1 based number of node in a binary + search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left + child of the root (if any), 3 is the right child of the root (if any), 4 is + the left child of the left child of the root (if any), ....) + @param proof the current proof + @return an index representing the same node in a varmap (@see varmap_uri), + the returned index is as defined in index (@see index_uri) + *) +let path_of_int n proof = + let rec digits_of_int n = + if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + in + List.fold_right + (fun digit path -> + Cic.Appl [ + mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof; + path]) + (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) + (mkCtor end_idx_uri proof) + + (** + Build a variable map (@see varmap_uri) from a variables array. + A variable map is almost a binary tree so this function receiving a var list + like [v;w;x;y;z] will build a varmap of shape: v + / \ + w x + / \ + y z + @param vars variables array + @param proof current proof + @return a cic term representing the variable map containing vars variables + *) +let btree_of_array ~vars ~proof = + let r = mkConst r_uri proof in (* cic objects *) + let empty_vm = mkCtor empty_vm_uri proof in + let empty_vm_r = Cic.Appl [empty_vm; r] in + let node_vm = mkCtor node_vm_uri proof in + let node_vm_r = Cic.Appl [node_vm; r] in + let size = Array.length vars in + let halfsize = size lsr 1 in + let rec aux n = (* build the btree starting from position n *) + (* + n is the position in the vars array _1_based_ in order to access + left and right child using (n*2, n*2+1) trick + *) + if n > size then + empty_vm_r + else if n > halfsize then (* no more children *) + Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r] + else (* still children *) + Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)] + in + aux 1 + + (** + abstraction function: + concrete polynoms -----> (abstract polynoms, varmap) + @param terms list of conrete polynoms + @param proof current proof + @return a pair where aterms is a list of abstract polynoms + and varmap is the variable map needed to interpret them + *) +let abstract_poly ~terms ~proof = + let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) + let varlist = ref [] in (* vars list in reverse order *) + let counter = ref 1 in (* index of next new variable *) + let rec aux = function (* TODO not tail recursive *) + (* "bop" -> binary operator | "uop" -> unary operator *) + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *) + Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2] + | Cic.Appl (bop::t1::t2::[]) + when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) + Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2] + | Cic.Appl (uop::t::[]) + when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) + Cic.Appl [mkCtor apopp_uri proof; aux t] + | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) + mkCtor ap0_uri proof + | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) + mkCtor ap1_uri proof + | t -> (* variable *) + try + Hashtbl.find varhash t (* use an old var *) + with Not_found -> begin (* create a new var *) + let newvar = + Cic.Appl [mkCtor apvar_uri proof; path_of_int !counter proof] + in + incr counter; + varlist := t :: !varlist; + Hashtbl.add varhash t newvar; + newvar + end + in + (List.map aux terms, + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof) + + (** + given a list of abstract terms (i.e. apolynomials) build the ring "segments" + that is triples like (t', t'', t''') where + t' = interp_ap(varmap, at) + t'' = interp_sacs(varmap, (apolynomial_normalize at)) + t''' = apolynomial_normalize_ok(varmap, at) + at is the abstract term built from t, t is a single member of aterms + *) +let build_segments ~terms ~proof = + let r = mkConst r_uri proof in (* cic objects *) + let rplus = mkConst rplus_uri proof in + let rmult = mkConst rmult_uri proof in + let ropp = mkConst ropp_uri proof in + let r0 = mkConst r0_uri proof in + let r1 = mkConst r1_uri proof in + let interp_ap = mkConst interp_ap_uri proof in + let interp_sacs = mkConst interp_sacs_uri proof in + let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in + let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in + let rtheory = mkConst rtheory_uri proof in + let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) + Cic.Lambda (Cic.Anonimous, r, + Cic.Lambda (Cic.Anonimous, r, + mkCtor false_uri proof)) + in + let theory_args = [r; rplus; rmult; r1; r0; ropp] in + let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *) + List.map (* build ring segments *) + (fun t -> + Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]), + Cic.Appl ( + interp_sacs :: + (theory_args @ + [varmap; Cic.Appl [apolynomial_normalize; t]])), + Cic.Appl ( + (apolynomial_normalize_ok :: theory_args) @ + [lxy_false; varmap; rtheory; t])) + aterms + +(** AUX TACTIC{,AL}S *) + + (** + naive implementation of ORELSE tactical, try a sequence of tactics in turn: + if one fails pass to the next one and so on, eventually raises (failure "no + tactics left") + TODO warning: not tail recursive due to "try .. with" boxing + *) +let rec try_tactics ~(tactics: (string * tactic) list) ~status = + warn "in Ring.try_tactics"; + match tactics with + | (descr, tac)::tactics -> + warn ("Ring.try_tactics IS TRYING " ^ descr); + (try + let res = tac ~status in + 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 + warn ( + "Ring.try_tactics failed with exn: " ^ + Printexc.to_string e); + try_tactics ~tactics ~status + end + ) + | [] -> raise (Fail "try_tactics: no tactics left") + + (** + auxiliary tactic "elim_type" + @param status current proof engine status + @param term term to cut + *) +let elim_type_tac ~status ~term = + 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) + + (** + auxiliary tactic, use elim_type and try to close 2nd subgoal using proof + @param status current proof engine 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 = + exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status)) + + (** + Reflexivity tactic, try to solve current goal using "refl_eqT" + Warning: this isn't equale to the coq's Reflexivity because this one tries + only refl_eqT, coq's one also try "refl_equal" + @param status current proof engine status + *) +let reflexivity_tac ~status:(proof, goal) = + warn "in Ring.reflexivity_tac"; + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in + try + apply_tac ~status:(proof, goal) ~term:refl_eqt + with (Fail _) as e -> + let e_str = Printexc.to_string e in + raise (Fail ("Reflexivity failed with exception: " ^ e_str)) + + (** lift an 8-uple of debrujins indexes of n *) +let lift ~n (a,b,c,d,e,f,g,h) = + match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with + | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h) + | _ -> assert false + + (** + remove hypothesis from a given status starting from the last one + @param count number of hypotheses to remove + @param status current proof engine status + *) +let purge_hyps ~count ~status:(proof, goal) = + 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 + 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) + +(** THE TACTIC! *) + + (** + Ring tactic, does associative and commutative rewritings in Reals ring + @param status current proof engine status + *) +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 + let (metano, context, ty) = conj_of_metano goal metasenv in + let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) + match (build_segments ~terms:[t1; t2] ~proof) with + | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin + List.iter (* debugging, feel free to remove *) + (fun (descr, term) -> + warn (descr ^ " " ^ (CicPp.ppterm term))) + (List.combine + ["t1"; "t1'"; "t1''"; "t1'_eq_t1''"; + "t2"; "t2'"; "t2''"; "t2'_eq_t2''"] + [t1; t1'; t1''; t1'_eq_t1''; + t2; t2'; t2''; t2'_eq_t2'']); + try + let new_hyps = ref 0 in (* number of new hypotheses created *) + try_tactics + ~status + ~tactics:[ + "reflexivity", reflexivity_tac; + "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1''; + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; + "exact sym_eqt su t1 ...", exact_tac ~term:( + Cic.Appl [ + mkConst sym_eqt_uri proof; mkConst r_uri proof; + t1''; t1; t1'_eq_t1'']); + "elim_type eqt su t1 ...", (fun ~status -> + let status' = (* status after 1st elim_type use *) + let context = context_of_status ~status in + if not (are_convertible context t1'' t1) then begin + warn "t1'' and t1 are NOT CONVERTIBLE"; + let newstatus = + elim_type2_tac (* 1st elim_type use *) + ~status ~proof:t1'_eq_t1'' + ~term:(Cic.Appl [eqt; r; t1''; t1]) + in + incr new_hyps; (* elim_type add an hyp *) + newstatus + end else begin + warn "t1'' and t1 are CONVERTIBLE"; + status + end + in + let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') = + lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') + in + let status'' = + try_tactics (* try to solve 1st subgoal *) + ~status:status' + ~tactics:[ + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; + "exact sym_eqt su t2 ...", + exact_tac ~term:( + Cic.Appl [ + mkConst sym_eqt_uri proof; + mkConst r_uri proof; + t2''; t2; t2'_eq_t2'']); + "elim_type eqt su t2 ...", (fun ~status -> + let status' = + let context = context_of_status ~status in + if not (are_convertible context t2'' t2) then begin + warn "t2'' and t2 are NOT CONVERTIBLE"; + let newstatus = + elim_type2_tac (* 2nd elim_type use *) + ~status ~proof:t2'_eq_t2'' + ~term:(Cic.Appl [eqt; r; t2''; t2]) + in + incr new_hyps; (* elim_type add an hyp *) + newstatus + end else begin + warn "t2'' and t2 are CONVERTIBLE"; + status + end + in + try (* try to solve main goal *) + warn "trying reflexivity ...."; + 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')] + in + status'')] + with (Fail _) -> + raise (Fail "Ring failure") + end + | _ -> (* impossible: we are applying ring exacty to 2 terms *) + assert false + + (* wrap ring_tac catching GoalUnringable and raising Fail *) +let ring_tac ~status = + try + ring_tac ~status + with GoalUnringable -> + raise (Fail "goal unringable") + diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli new file mode 100644 index 000000000..07c06866d --- /dev/null +++ b/helm/gTopLevel/ring.mli @@ -0,0 +1,15 @@ + + (* ring tactics *) +val ring_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status + + (* auxiliary tactics *) +val elim_type_tac: + status: ProofEngineTypes.status -> term: Cic.term -> ProofEngineTypes.status +val reflexivity_tac: status: ProofEngineTypes.status -> ProofEngineTypes.status + + (* pseudo tacticals *) +val try_tactics: + tactics: (string * ProofEngineTypes.tactic) list -> + status: ProofEngineTypes.status -> + ProofEngineTypes.status + -- 2.39.2