From 43eef00462911f52ff53360e812b5b937097d05a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 May 2009 21:44:34 +0000 Subject: [PATCH 1/1] - non_punctuational_tacticals ported to NG - experimental generation of elimination principles passing through ASTs --- .../software/components/grafite/grafiteAst.ml | 2 + .../grafite_engine/grafiteEngine.ml | 36 +++++- .../grafite_parser/grafiteParser.ml | 2 + helm/software/components/ng_tactics/.depend | 3 + helm/software/components/ng_tactics/Makefile | 3 +- .../components/ng_tactics/nCicElim.ml | 114 ++++++++++++++++++ .../components/ng_tactics/nCicElim.mli | 14 +++ 7 files changed, 168 insertions(+), 6 deletions(-) create mode 100644 helm/software/components/ng_tactics/nCicElim.ml create mode 100644 helm/software/components/ng_tactics/nCicElim.mli diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 039d5bfa4..6e48074ad 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -216,6 +216,8 @@ type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = * punctuation_tactical | NonPunctuationTactical of loc * non_punctuation_tactical * punctuation_tactical + | NNonPunctuationTactical of loc * non_punctuation_tactical + * punctuation_tactical type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = | Note of loc * string diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index b1cedb077..89f50c8fd 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -583,6 +583,13 @@ let eval_ng_punct (_text, _prefix_len, punct) = | GrafiteAst.Merge _ -> NTactics.merge_tac ;; +let eval_ng_non_punct (_text, _prefix_len, punct) = + match punct with + | GrafiteAst.Focus (_,l) -> NTactics.focus_tac l + | GrafiteAst.Unfocus _ -> NTactics.unfocus_tac + | GrafiteAst.Skip _ -> NTactics.skip_tac +;; + let eval_ng_tac (text, prefix_len, tac) = match tac with | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) @@ -758,14 +765,24 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status else let obj = prerr_endline "CSC: here we should fix the height!!!"; - uri,height,[],[], - NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj + (uri,height,[],[], + NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) + obj) in + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + let objs = NCicElim.mk_elims obj in + let uris = + uri:: + List.map + (fun (uri,_,_,_,_) as obj -> + NCicTypeChecker.typecheck_obj obj; + NCicLibrary.add_obj uri obj; + uri + ) objs in - NCicTypeChecker.typecheck_obj obj; - NCicLibrary.add_obj uri obj; {status with GrafiteTypes.ng_status = - GrafiteTypes.CommandMode lexicon_status },`New [uri] + GrafiteTypes.CommandMode lexicon_status },`New uris | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; @@ -900,6 +917,15 @@ prerr_endline "CSC: here we should fix the height!!!"; in eval_tactical status (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] + | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) -> + (match status.GrafiteTypes.ng_status with + | GrafiteTypes.CommandMode _ -> assert false + | GrafiteTypes.ProofMode nstatus -> + let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) nstatus in + let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in + NTacStatus.pp_tac_status nstatus; + { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus }, + `New []) | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index ecdee9f7b..547e51025 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -834,6 +834,8 @@ EXTEND G.NTactic (loc, G.NId loc, punct) | tac = non_punctuation_tactical; punct = punctuation_tactical -> G.NonPunctuationTactical (loc, tac, punct) + | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical -> + G.NNonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> G.Macro (loc, mac) ] ]; diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index a93613c51..d8765a328 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,6 +1,9 @@ nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi +nCicElim.cmi: nTacStatus.cmo: nTacStatus.cmi nTacStatus.cmx: nTacStatus.cmi nTactics.cmo: nTacStatus.cmi nTactics.cmi nTactics.cmx: nTacStatus.cmx nTactics.cmi +nCicElim.cmo: nCicElim.cmi +nCicElim.cmx: nCicElim.cmi diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index 71183455b..3ee5156f9 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -2,7 +2,8 @@ PACKAGE = ng_tactics INTERFACE_FILES = \ nTacStatus.mli \ - nTactics.mli + nTactics.mli \ + nCicElim.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml new file mode 100644 index 000000000..54d8d5df6 --- /dev/null +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -0,0 +1,114 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +let fresh_name = + let i = ref 0 in + function () -> + incr i; + "x_" ^ string_of_int !i +;; + +let mk_id id = + let id = if id = "_" then fresh_name () else id in + CicNotationPt.Ident (id,None) +;; + +(*CSC: cut&paste from nCicReduction.split_prods, but does not check that + the return type is a sort *) +let rec my_split_prods ~subst context n te = + match (n, NCicReduction.whd ~subst context te) with + | (0, _) -> context,te + | (n, NCic.Prod (name,so,ta)) -> + my_split_prods ~subst ((name,(NCic.Decl so))::context) (n - 1) ta + | (n, _) when n <= 0 -> context,te + | (_, _) -> raise (Failure "my_split_prods") +;; + +let mk_elims (uri,_,_,_,obj) = + match obj with + NCic.Inductive (true,leftno,[it],_) -> + let _,ind_name,ty,cl = it in + let rec_name = ind_name ^ "_rect" in + let rec_name = mk_id rec_name in + let name_of_k id = mk_id ("H_" ^ id) in + let p_name = mk_id "Q_" in + let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + let params = List.rev_map (function name,_ -> mk_id name) params in + let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in + let rec_arg = mk_id (fresh_name ()) in + let args = List.rev_map (function name,_ -> mk_id name) args in + let p_ty = + List.fold_right + (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args + (CicNotationPt.Binder + (`Forall, + (rec_arg,Some (CicNotationPt.Appl (mk_id ind_name :: params @ args))), + CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in + let args = args @ [rec_arg] in + let k_names = List.map (function _,name,_ -> name_of_k name) cl in + let final_params = + List.map (function name -> name, None) params @ + [p_name,Some p_ty] @ + List.map (function name -> name, None) k_names @ + List.map (function name -> name, None) args in + let ty = Some (CicNotationPt.Appl (p_name :: args)) in + let branches = + List.map + (function (_,name,ty) -> + let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in + let cargs_and_recursive_args = + List.rev_map + (function + name,NCic.Def _ -> assert false + | name,NCic.Decl (NCic.Const nref) + | name,NCic.Decl (NCic.Appl (NCic.Const nref::_)) + when + let NReference.Ref (uri',_) = nref in + NUri.eq uri uri' + -> + let name = mk_id name in + name, Some ( + CicNotationPt.Appl + (rec_name :: + params @ + [p_name] @ + k_names @ + List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @ + [name])) + | name,_ -> mk_id name,None + ) cargs in + let cargs,recursive_args = List.split cargs_and_recursive_args in + let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in + CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), + CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args) + ) cl + in + let bo = CicNotationPt.Case (rec_arg,None,None,branches) in + let where = List.length final_params - 1 in + let res = + CicNotationPt.LetRec (`Inductive, + [final_params, (rec_name,ty), bo, where], rec_name) + in + prerr_endline (CicNotationPp.pp_term res); + prerr_endline "#####"; + prerr_endline + (BoxPp.render_to_string + ~map_unicode_to_tex:false + (function x::_ -> x | _ -> assert false) + 80 (CicNotationPres.render (Hashtbl.create 0) + (TermContentPres.pp_ast res))); + + [] + | _ -> [] +;; diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli new file mode 100644 index 000000000..8366f1702 --- /dev/null +++ b/helm/software/components/ng_tactics/nCicElim.mli @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val mk_elims: NCic.obj -> NCic.obj list -- 2.39.2