-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
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
-(* 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
"</html>"
;;
+let prooffile = "/home/zack/dati/HELM/currentproof.gTopLevel"
+
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
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 *)
(*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 (
+ "<current_seq>\n" ^
+ (SequentPp.TextualPp.print_sequent seq) ^
+ "\n</current_seq>");
+ print_newline ()
+;;
(* CALLBACKS *)
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
;;
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
;;
(*????
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
xml
>]
in
- Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ;
+ Xml.pp ~quiet:true xml' (Some prooffile) ;
output_html outputhtml
("<h1 color=\"Green\">Current proof saved to " ^
- "/public/sacerdot/currentproof</h1>")
+ prooffile ^ "</h1>")
;;
(* Used to typecheck the loaded proofs *)
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 :=
refresh_sequent proofw ;
output_html outputhtml
("<h1 color=\"Green\">Current proof loaded from " ^
- "/public/sacerdot/currentproof</h1>")
+ prooffile ^ "</h1>")
| _ -> assert false
with
RefreshSequentException e ->
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
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 =
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:"<html><body bgColor=\"white\"></body></html>"
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)) ;
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))
let _ =
CicCooking.init () ;
- MQueryGenerator.init () ;
+ if !usedb then MQueryGenerator.init () ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
+ if !usedb then MQueryGenerator.close ();
MQueryGenerator.close ()
;;
+
+(* 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
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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))
+
--- /dev/null
+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
* 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]. *)
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 *)
(* 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) ->
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
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 =
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 =
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 =
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) *)
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)
-;;
--- /dev/null
+
+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
+
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* 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')
+
--- /dev/null
+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
-(* 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
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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)
+
--- /dev/null
+val clearbody:
+ status: ProofEngineTypes.status ->
+ hyp: Cic.hypothesis -> ProofEngineTypes.status
+val clear:
+ status: ProofEngineTypes.status ->
+ hyp: Cic.hypothesis -> ProofEngineTypes.status
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+ (**
+ 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
+
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+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 <uri, typeno, consno> 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 <uri, typeno> 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 ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
+ warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
+ (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 <aterms, varmap> 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")
+
--- /dev/null
+
+ (* 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
+
projects / helm.git / commitdiff