(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+ | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
sprintf "<<pretty printing of mutual definitions not implemented yet>>"
- | Ast.Theorem (flavour, name, typ, body) ->
+ | Ast.Theorem (flavour, name, typ, body,_) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)
name
type 'term obj =
| Inductive of 'term capture_variable list * 'term inductive_type list
(** parameters, list of loc * mutual inductive types *)
- | Theorem of Cic.object_flavour * string * 'term * 'term option
+ | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma
(** flavour, name, type, body
* - name is absent when an unnamed theorem is being proved, tipically in
* interactive usage
indtypes
in
CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
- | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
+ | CicNotationPt.Theorem (flav, n, t, ty_opt,p) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
- CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
+ CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
| CicNotationPt.Record (params, n, ty, fields) ->
CicNotationPt.Record (freshen_capture_variables params, n,
freshen_term ty, freshen_name_ty_b fields)
let mk_statement flavour name t v =
let name = match name with Some name -> name | None -> assert false in
- let obj = N.Theorem (flavour, name, t, v) in
+ let obj = N.Theorem (flavour, name, t, v, `Regular) in
G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
let mk_qed =
let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
(match bo,flavour with
let domain_of_obj ~context ast =
assert (context = []);
match ast with
- | Ast.Theorem (_,_,ty,bo) ->
+ | Ast.Theorem (_,_,ty,bo,_) ->
domain_of_term [] ty
@ (match bo with
None -> []
let obj = uri,height,[],[],obj_kind in
let old_status = status in
let status = NCicLibrary.add_obj status obj in
+(* prerr_endline (NCicPp.ppobj obj); *)
HLog.message ("New object: " ^ NUri.string_of_uri uri);
(try
(*prerr_endline (NCicPp.ppobj obj);*)
match obj with
| CicNotationPt.Inductive (_,(name,_,_,_)::_)
| CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
| CicNotationPt.Inductive _ -> assert false
in
UriManager.uri_of_string (baseuri ^ "/" ^ name)
match obj with
| CicNotationPt.Inductive (_,(name,_,_,_)::_)
| CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
| CicNotationPt.Inductive _ -> assert false
in
UriManager.uri_of_string (baseuri ^ "/" ^ name)
else
`MutualDefinition
in
- (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body))))
+ (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
let nmk_rec_corec ind_kind defs loc =
let loc,t = mk_rec_corec ind_kind defs loc in
IDENT "nqed" -> G.NQed loc
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- G.NObj (loc, N.Theorem (nflavour, name, typ, body))
+ G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
body = term ->
- G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
+ G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
| IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
- G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
+ G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
| IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
paramspec = OPT inverter_param_list ;
outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
G.Obj (loc,
N.Theorem
- (`Variant,name,typ,Some (N.Ident (newname, None))))
+ (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
| flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- G.Obj (loc, N.Theorem (flavour, name, typ, body))
+ G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
| flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
body = term ->
G.Obj (loc,
- N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
+ N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
| IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
- G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
+ G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
| LETCOREC ; defs = let_defs ->
mk_rec_corec `CoInductive defs loc
| LETREC ; defs = let_defs ->
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
let uri = match uri with | None -> assert false | Some u -> u in
match obj with
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) ->
let ty' =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
uri, height, [], [],
(match bo,flavour with
| None,`Axiom ->
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,None,ty',attrs)
| Some _,`Axiom -> assert false
| None,_ ->
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
(match bo with
([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
interpretate_term
~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ let attrs = `Provided, new_flavour_of_flavour flavour, pragma in
NCic.Constant ([],name,Some bo,ty',attrs)))
| CicNotationPt.Inductive (params,tyl) ->
let context,params =
ppsubst ~formatter ~metasenv ~subst subst
;;
+let string_of_generated = function
+ | `Generated -> "Generated"
+ | `Provided -> "Provided"
+;;
+
+let string_of_flavour = function
+ | `Definition -> "Definition"
+ | `Fact -> "Fact"
+ | `Lemma -> "Lemma"
+ | `Theorem -> "Theorem"
+ | `Corollary -> "Corollary"
+ | `Example -> "Example"
+;;
+
+let string_of_pragma = function
+ | `Coercion _arity -> "Coercion _"
+ | `Elim _sort -> "Elim _"
+ | `Projection -> "Projection"
+ | `InversionPrinciple -> "InversionPrinciple"
+ | `Variant -> "Variant"
+ | `Local -> "Local"
+ | `Regular -> "Regular"
+;;
+
+let string_of_fattrs (g,f,p) =
+ String.concat ","
+ [ string_of_generated g; string_of_flavour f; string_of_pragma p ]
+;;
+
let ppobj ~formatter (u,_,metasenv, subst, o) =
F.fprintf formatter "metasenv:\n";
ppmetasenv ~formatter ~subst metasenv;
(*ppsubst subst ~formatter ~metasenv;*) F.fprintf formatter "...";
F.fprintf formatter "\n";
match o with
- | NCic.Fixpoint (b, fl, _) ->
+ | NCic.Fixpoint (b, fl, attrs) ->
F.fprintf formatter "{%s}@\n@[<hov 0>" (NUri.string_of_uri u);
F.fprintf formatter "@[<hov 2>%s"(if b then "let rec " else "let corec ");
HExtlib.list_iter_sep
F.fprintf formatter "@]@;@[<hov 2>:=@;";
ppterm ~formatter ~metasenv ~subst ~context:[] ~inside_fix:true bo;
F.fprintf formatter "@]") fl;
- F.fprintf formatter "@]"
+ F.fprintf formatter "@; %s" (string_of_fattrs attrs);
+ F.fprintf formatter "@]"
| NCic.Inductive (b, leftno,tyl, _) ->
F.fprintf formatter "{%s} with %d fixed params@\n@[<hov 0>@[<hov 2>%s"
(NUri.string_of_uri u) leftno
val ppsubst: metasenv:NCic.metasenv -> NCic.substitution -> string
val ppobj: NCic.obj -> string
+
+(* variants that use a formatter
+module Format : sig
+ val ppterm:
+ formatter:Format.formatter ->
+ context:NCic.context ->
+ subst:NCic.substitution ->
+ metasenv:NCic.metasenv ->
+ ?margin:int ->
+ ?inside_fix:bool ->
+ NCic.term -> unit
+
+ val ppcontext:
+ ?sep:string ->
+ formatter:Format.formatter ->
+ subst:NCic.substitution ->
+ metasenv:NCic.metasenv ->
+ NCic.context -> unit
+
+ val ppmetasenv:
+ formatter:Format.formatter ->
+ subst:NCic.substitution -> NCic.metasenv -> unit
+
+ val ppsubst:
+ formatter:Format.formatter ->
+ metasenv:NCic.metasenv -> NCic.substitution -> unit
+
+ val ppobj:
+ formatter:Format.formatter -> NCic.obj -> unit
+end
+*)
aux (List.map fst ctx) t
;;
-let rec fire_projection_redex () = function
+let rec fire_projection_redex on_args = function
| C.Meta _ as t -> t
| C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
- let l = List.map (fire_projection_redex ()) ol in
+ let l= if on_args then List.map (fire_projection_redex true) ol else ol in
let t = if l == ol then ot else C.Appl l in
let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
let conclude () =
- let l' = HExtlib.sharing_map (fire_projection_redex ()) l in
- if l == l' then t else C.Appl l'
+ if on_args then
+ let l' = HExtlib.sharing_map (fire_projection_redex true) l in
+ if l == l' then t else C.Appl l'
+ else
+ t (* ot is the same *)
in
- if (*pragma <> `Projection ||*) List.length args <= rno then conclude ()
+ if pragma <> `Projection || List.length args <= rno then conclude ()
else
(match List.nth args rno with
| C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
(match NCicReduction.head_beta_reduce ~delta:max_int t with
| C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
let _,kargs = HExtlib.split_nth leftno kargs in
- NCicReduction.head_beta_reduce
- ~delta:max_int (C.Appl (pat :: kargs))
+ fire_projection_redex false
+ (NCicReduction.head_beta_reduce
+ ~delta:max_int (C.Appl (pat :: kargs)))
| C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
let _,kargs = HExtlib.split_nth leftno kargs in
- NCicReduction.head_beta_reduce
- ~delta:max_int (C.Appl (pat :: kargs @ args))
+ fire_projection_redex false
+ (NCicReduction.head_beta_reduce
+ ~delta:max_int (C.Appl (pat :: kargs @ args)))
| _ -> conclude ())
| _ -> conclude ())
- | t -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t
+ | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
+ | t -> t
;;
let apply_subst ?(fix_projections=false) subst context t =
apply_subst subst () (NCicSubstitution.lift n t)) l))))
| t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
in
- (if fix_projections then fire_projection_redex () else fun x -> x)
+ (if fix_projections then fire_projection_redex true else fun x -> x)
(clean_or_fix_dependent_abstrations context (apply_subst subst () t))
;;
| l -> CicNotationPt.Appl l
;;
-let mk_elim uri leftno it (outsort,suffix) =
+let mk_elim uri leftno it (outsort,suffix) pragma =
let _,ind_name,ty,cl = it in
let srec_name = ind_name ^ "_" ^ suffix in
let rec_name = mk_id srec_name in
(CicNotationPres.mpres_of_box boxml)));
*)
CicNotationPt.Theorem
- (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res)
+ (`Definition,srec_name,
+ CicNotationPt.Implicit `JustOne,Some res,pragma)
;;
let ast_of_sort s =
let mk_elims (uri,_,_,_,obj) =
match obj with
NCic.Inductive (true,leftno,[itl],_) ->
- List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s))
+ List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
| _ -> []
80 (CicNotationPres.render (fun _ -> None)
(TermContentPres.pp_ast res)));*)
CicNotationPt.Theorem
- (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res)
+ (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection)
;;
let mk_projections (_,_,_,_,obj) =
let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",
- 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in
+ 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
+ (CicNotationPt.Implicit (`Tagged "inv")),`Regular)) in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
(mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))),
convert_formula fv false context f)
in
- let o = PT.Theorem (`Theorem,name,f,None) in
+ let o = PT.Theorem (`Theorem,name,f,None,`Regular) in
(statements @
[ GA.Executable(floc,GA.Command(floc,
(*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
projects / helm.git / commitdiff