"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 =
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
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) ->
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 =
| 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
| 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
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
) (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")
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<mapsto>>; 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: [ [
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
[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) ->
(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)));
[]
| _ -> []
;;
projects / helm.git / commitdiff