From 5f5baa87c244bc700d3c78edac6df7e2825b4dbd Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:46:12 +0000 Subject: [PATCH] ported to latest Ast changes (mainly capture_variable addition) --- .../cic_disambiguation/cicTextualParser2Pp.ml | 33 ++++++++++--------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml index 83da77244..896e1dcc3 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Pp.ml @@ -32,7 +32,11 @@ let pp_binder = function | `Exists -> "exists" | `Forall -> "forall" -let rec pp_term = function +let pp_name = function Cic.Anonymous -> "_" | Cic.Name s -> s +let rec pp_capture_variable = function + | name, None -> pp_name name + | name, Some typ -> "(" ^ pp_name name ^ ": " ^ pp_term typ ^ ")" +and pp_term = function | LocatedTerm ((p_begin, p_end), term) -> (* sprintf "[%d,%d]%s" p_begin p_end (pp_term term) *) pp_term term @@ -40,26 +44,23 @@ let rec pp_term = function | Appl terms -> sprintf "(%s)" (String.concat " " (List.map pp_term terms)) | Appl_symbol (symbol, _, terms) -> sprintf "(%s %s)" symbol (String.concat " " (List.map pp_term terms)) - | Binder (kind, var, typ, body) -> - sprintf "\\%s %s%s.%s" (pp_binder kind) - (match var with Cic.Anonymous -> "_" | Cic.Name s -> s) - (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) + | Binder (kind, var, body) -> + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) (pp_term body) | Case (term, indtype, typ, patterns) -> sprintf "%smatch %s with %s" (match typ with None -> "" | Some t -> sprintf "<%s>" (pp_term t)) (pp_term term) (pp_patterns patterns) - | LetIn (name, t1, t2) -> - sprintf "let %s = %s in %s" name (pp_term t1) (pp_term t2) + | LetIn (var, t1, t2) -> + sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) + (pp_term t2) | LetRec (kind, definitions, term) -> sprintf "let %s %s in %s" (match kind with `Inductive -> "rec" | `CoInductive -> "corec") (String.concat " and " (List.map - (fun (name, body, typ, index) -> - sprintf "%s%s = %s" name - (match typ with None -> "" | Some typ -> ": " ^ pp_term typ) - (pp_term body)) + (fun (var, body, _) -> + sprintf "%s = %s" (pp_capture_variable var) (pp_term body)) definitions)) (pp_term term) | Ident (name, []) -> name @@ -77,11 +78,13 @@ let rec pp_term = function and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) -and pp_pattern (names, term) = +and pp_pattern ((head, vars), term) = sprintf "%s -> %s" - (match names with - | [n] -> n - | names -> "(" ^ String.concat " " names ^ ")") + (match vars with + | [] -> head + | _ -> + sprintf "(%s %s)" head + (String.concat " " (List.map pp_capture_variable vars))) (pp_term term) and pp_patterns patterns = -- 2.39.2