(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns patterns)
| Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
- | Ast.LetIn (var, t1, t2) ->
- sprintf "let %s \\def %s in %s" (pp_capture_variable pp_term var) (pp_term ~pp_parens:true t1)
- (pp_term ~pp_parens:true t2)
+ | 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
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
| Ast.Sort (`Type _) -> "Type"
- | Ast.Sort `CProp -> "CProp"
+ | Ast.Sort (`CProp _)-> "CProp"
| Ast.Symbol (name, _) -> "'" ^ name
| Ast.UserInput -> ""
and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
and pp_substs substs = String.concat "; " (List.map pp_subst substs)
-and pp_pattern ((head, href, vars), term) =
- let head_pp =
- head ^
- (match debug_printing, href with
- | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
- | _ -> "")
- in
- sprintf "%s \\Rightarrow %s"
- (match vars with
- | [] -> head_pp
- | _ ->
- sprintf "(%s %s)" head_pp
- (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
- (pp_term term)
+and pp_pattern =
+ function
+ Ast.Pattern (head, href, vars), term ->
+ let head_pp =
+ head ^
+ (match debug_printing, href with
+ | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ | _ -> "")
+ in
+ sprintf "%s \\Rightarrow %s"
+ (match vars with
+ | [] -> head_pp
+ | _ ->
+ sprintf "(%s %s)" head_pp
+ (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
+ (pp_term term)
+ | Ast.Wildcard, term ->
+ sprintf "_ \\Rightarrow %s" (pp_term term)
and pp_patterns patterns =
sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))
let pp_flavour = function
| `Definition -> "definition"
+ | `MutualDefinition -> assert false
| `Fact -> "fact"
| `Goal -> "goal"
| `Lemma -> "lemma"
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+ sprintf "<<pretty printing of mutual definitions not implemented yet>>"
| Ast.Theorem (flavour, name, typ, body) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)