From 948bb5d710c5d7f3185b6fef76c8e71f247cc664 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2009 16:34:34 +0000 Subject: [PATCH] ncopy partially implemented and fixed (a ?) chain to print elimintaors --- .../components/content_pres/content2pres.ml | 87 +++++++++++++++++-- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 7 ++ .../grafite_engine/grafiteEngine.ml | 32 +++++++ .../grafite_parser/grafiteParser.ml | 4 + .../components/ng_tactics/nCicElim.ml | 32 ++++++- 6 files changed, 154 insertions(+), 9 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 6dee8f040..63eec5e35 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -908,6 +908,7 @@ let recursion_kind2pres params kind = "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)" in B.b_h [] (B.b_kw kind :: params2pres params) +;; let inductive2pres term2pres ind = let constructor2pres decl = @@ -924,10 +925,84 @@ let inductive2pres term2pres ind = term2pres ind.Content.inductive_type ] :: List.map constructor2pres ind.Content.inductive_constructors) -let joint_def2pres term2pres def = +let definition2pres ?recno term2pres d = + let name = match d.Content.def_name with Some x -> x|_->assert false in + let rno = match recno with None -> assert false | Some x -> x in + let ty = d.Content.def_type in + let module P = CicNotationPt in + let rec split_pi i t = + if i <= 1 then + match t with + | P.Binder ((`Pi|`Forall),(var,_ as v),t) -> [v], var, t + | _ -> assert false + else + match t with + | P.Binder ((`Pi|`Forall), var ,ty) -> + let l, r, t = split_pi (i-1) ty in + var :: l, r, t + | _ -> assert false + in + let params, rec_param, ty = split_pi rno ty in + let body = d.Content.def_term in + let params = + List.map + (function + | (name,Some ty) -> + B.b_h [] [B.b_text [] "("; term2pres name; B.b_text [] " : "; + B.b_space; term2pres ty; B.b_text [] ")"; B.b_space] + | (name,None) -> B.b_h [] [term2pres name;B.b_space]) + params + in + B.b_hv [] + [B.b_hv [] + ([ B.b_space; B.b_text [] name ] @ params @ + [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space; + B.b_text [] ":"; B.b_space; term2pres ty]); + B.b_text [] ":="; + B.b_h [] [B.b_space;term2pres body] ] +;; + +let joint_def2pres ?recno term2pres def = match def with | `Inductive ind -> inductive2pres term2pres ind - | _ -> assert false (* ZACK or raise ToDo? *) + | _ -> assert false +;; + +let njoint_def2pres ?recno term2pres def = + match def with + | `Inductive ind -> inductive2pres term2pres ind + | `Definition def -> definition2pres ?recno term2pres def + | _ -> assert false +;; + +let njoint_def2pres term2pres joint_kind defs = + match joint_kind with + | `Recursive recnos -> + B.b_hv [] (B.b_kw "nlet rec " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map2 (fun a b -> njoint_def2pres ~recno:a term2pres b) + recnos defs))) + | `CoRecursive -> + B.b_hv [] (B.b_kw "nlet corec " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) + | `Inductive _ -> + B.b_hv [] (B.b_kw "ninductive " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) + | `CoInductive _ -> + B.b_hv [] (B.b_kw "ncoinductive " :: + List.flatten + (HExtlib.list_mapi (fun x i -> + if i > 0 then [B.b_kw " and ";x] else [x]) + (List.map (njoint_def2pres term2pres) defs))) +;; let content2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres @@ -988,7 +1063,7 @@ let content2pres let ncontent2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres - (id,params,metasenv,obj) + (id,params,metasenv,obj : CicNotationPt.term Content.cobj) = match obj with | `Def (Content.Const, thesis, `Proof p) -> @@ -1025,9 +1100,9 @@ let ncontent2pres0 B.indent (term2pres decl.Content.dec_type)] @ metasenv2pres term2pres metasenv) | `Joint joint -> - B.b_v [] - (recursion_kind2pres params joint.Content.joint_kind - :: List.map (joint_def2pres term2pres) joint.Content.joint_defs) + B.b_v [] + [njoint_def2pres term2pres + joint.Content.joint_kind joint.Content.joint_defs] | _ -> raise ToDo let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 60e3aac4b..813a08071 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -214,6 +214,7 @@ type ncommand = | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | NObj of loc * CicNotationPt.term CicNotationPt.obj | NUnivConstraint of loc * bool * NUri.uri * NUri.uri + | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list | NCoercion of loc * string * CicNotationPt.term * CicNotationPt.term * (string * CicNotationPt.term) * CicNotationPt.term diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 2cd7a4f4f..eddac9746 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -362,6 +362,13 @@ let pp_ncommand = function | NUnivConstraint (_) -> "not supported" | NCoercion (_) -> "not supported" | NQed (_) -> "nqed" + | NCopy (_,name,uri,map) -> + "copy " ^ name ^ " from " ^ NUri.string_of_uri uri ^ " with " ^ + String.concat " and " + (List.map + (fun (a,b) -> NUri.string_of_uri a ^ " ↦ " ^ NUri.string_of_uri b) + map) +;; let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6533e3f86..3a108accc 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -956,6 +956,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = in let obj = uri,height,[],[],obj_kind in let status = NCicLibrary.add_obj status obj in + prerr_endline (NCicPp.ppobj obj); let objs = NCicElim.mk_elims obj in let timestamp,uris_rev = List.fold_left @@ -965,6 +966,37 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = ) (status,[]) objs in let uris = uri::List.rev uris_rev in status#set_ng_mode `CommandMode,`New uris + | GrafiteAst.NCopy (log,tgt,src_uri, map) -> + if status#ng_mode <> `CommandMode then + raise (GrafiteTypes.Command_error "Not in command mode") + else + let tgt_uri_ext, old_ok = + match NCicEnvironment.get_checked_obj src_uri with + | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok + | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok + | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok + | _ -> assert false + in + let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in + let map = (src_uri, tgt_uri) :: map in + let ok = + let rec subst () = function + | NCic.Meta _ -> assert false + | NCic.Const (NReference.Ref (u,spec)) as t -> + (try NCic.Const + (NReference.reference_of_spec (List.assoc u map)spec) + with Not_found -> t) + | t -> NCicUtils.map (fun _ _ -> ()) () subst t + in + NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok + in + let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in + let status = status#set_obj (tgt_uri,0,[],[],ok) in + prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok)); + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + let status = status#set_ng_mode `ProofMode in + eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | GrafiteAst.NObj (loc,obj) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index dfef4d237..5ed293948 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -836,6 +836,10 @@ EXTEND G.NCoercion(loc,name,t,ty,(id,source),target) | IDENT "nrecord" ; (params,name,ty,fields) = record_spec -> G.NObj (loc, N.Record (params,name,ty,fields)) + | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with"; + m = LIST0 [ u1 = URI; SYMBOL <:unicode>; u2 = URI -> u1,u2 ] -> + G.NCopy (loc,s,NUri.uri_of_string u, + List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m) ]]; grafite_command: [ [ diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index fba21753a..08c8b0f56 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -38,8 +38,8 @@ 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 srec_name = ind_name ^ "_rect" in + let rec_name = mk_id srec_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 @@ -61,7 +61,9 @@ let mk_elims (uri,_,_,_,obj) = [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 recno = List.length final_params in + let cty = CicNotationPt.Appl (p_name :: args) in + let ty = Some cty in let branches = List.map (function (_,name,ty) -> @@ -117,6 +119,30 @@ let mk_elims (uri,_,_,_,obj) = (function x::_ -> x | _ -> assert false) 80 (CicNotationPres.render (fun _ -> None) (TermContentPres.pp_ast res))); + prerr_endline "#####"; + let cobj = ("xxx", [], None, `Joint { + Content.joint_id = "yyy"; + joint_kind = `Recursive [recno]; + joint_defs = + [ `Definition { + Content.def_name = Some srec_name; + def_id = "zzz"; + def_aref = "www"; + def_term = bo; + def_type = + List.fold_right + (fun x t -> CicNotationPt.Binder(`Forall,x,t)) + final_params cty + } + ]; + }) + in + let ids_to_nrefs = Hashtbl.create 1 in + let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in + prerr_endline ( + (BoxPp.render_to_string ~map_unicode_to_tex:false + (function x::_ -> x | _ -> assert false) 80 + (CicNotationPres.mpres_of_box boxml))); [] | _ -> [] ;; -- 2.39.2