(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns status patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
- | Ast.LetIn ((var,t2), t1, t3) ->
+ | Ast.LetIn ((var,_t2), t1, t3) ->
(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
sprintf "let %s \\def %s in %s" (pp_term var)
(* (pp_term ~pp_parens:true t2) *)
(pp_term ~pp_parens:true t1)
(pp_term ~pp_parens:true t3)
- | Ast.LetRec (kind, definitions, term) ->
- let rec get_guard i = function
- | [] -> (*assert false*) Ast.Implicit `JustOne
- | [term, _] when i = 1 -> term
- | _ :: tl -> get_guard (pred i) tl
- in
- let map (params, (id,typ), body, i) =
- let typ =
- match typ with
- None -> Ast.Implicit `JustOne
- | Some typ -> typ
- in
- sprintf "%s %s on %s: %s \\def %s"
- (pp_term ~pp_parens:false term)
- (String.concat " " (List.map (pp_capture_variable pp_term) params))
- (pp_term ~pp_parens:false (get_guard i params))
- (pp_term typ) (pp_term body)
- in
- sprintf "let %s %s in %s"
- (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
- (String.concat " and " (List.map map definitions))
- (pp_term term)
| Ast.Ident (name, Some []) | Ast.Ident (name, None)
| Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
| Ast.NRef nref -> NReference.string_of_reference nref
| Ast.NumVar s -> "number " ^ s
| Ast.IdentVar s -> "ident " ^ s
| Ast.TermVar (s,Ast.Self _) -> s
- | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l
- | Ast.Ascription (t, n) -> assert false
+ | Ast.TermVar (_s,Ast.Level l) -> "term " ^string_of_int l
+ | Ast.Ascription (_t, _n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
let _pp_term = ref (pp_term ~pp_parens:false)
pp_term ty)
fields)
+let string_of_source = function
+ | `Provided -> ""
+ | `Implied -> "implied "
+ | `Generated -> "generated "
+
let pp_obj pp_term = function
- | Ast.Inductive (params, types) ->
+ | Ast.Inductive (params, types, source) ->
let pp_constructors constructors =
String.concat "\n"
(List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
| [] -> assert false
| (name, inductive, typ, constructors) :: tl ->
let fst_typ_pp =
- sprintf "%sinductive %s%s: %s \\def\n%s"
+ sprintf "%s%sinductive %s%s: %s \\def\n%s"
+ (string_of_source source)
(if inductive then "" else "co") name (pp_params pp_term params)
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (flavour, name, typ, body,_) ->
- sprintf "%s %s:\n %s\n%s"
+ | Ast.Theorem (name, typ, body,(source, flavour, _)) ->
+ sprintf "%s%s %s:\n %s\n%s"
+ (string_of_source source)
(NCicPp.string_of_flavour flavour)
name
(pp_term typ)
(match body with
| None -> ""
| Some body -> "\\def\n " ^ pp_term body)
- | Ast.Record (params,name,ty,fields) ->
+ | Ast.Record (params,name,ty,fields, source) ->
+ string_of_source source ^
"record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^
" \\def {" ^ pp_fields pp_term fields ^ "\n}"
+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
+ let rec get_guard i = function
+ | [] -> assert false (* Ast.Implicit `JustOne *)
+ | [term, _] when i = 1 -> term
+ | _ :: tl -> get_guard (pred i) tl
+ in
+ let map (params, (id,typ), body, i) =
+ let typ =
+ match typ with
+ None -> assert false (* Ast.Implicit `JustOne *)
+ | Some typ -> typ
+ in
+ sprintf "%s %s on %s: %s \\def %s"
+ (pp_term id)
+ (String.concat " " (List.map (pp_capture_variable pp_term) params))
+ (pp_term (get_guard i params))
+ (pp_term typ) (pp_term body)
+ in
+ sprintf "%s%s %s %s"
+ (string_of_source source)
+ (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (NCicPp.string_of_flavour flavour)
+ (String.concat " and " (List.map map definitions))
let rec pp_value (status: #NCic.status) = function
| Env.TermValue t -> sprintf "$%s$" (pp_term status t)