From 426cad2769fcf6c6f1fdee965e6f0414aaf240db Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jun 2005 16:52:07 +0000 Subject: [PATCH] added records pp, ast and fixed a bug in match with only one branch --- helm/ocaml/cic_transformations/ast2pres.ml | 3 +- helm/ocaml/cic_transformations/tacticAst.ml | 2 ++ helm/ocaml/cic_transformations/tacticAstPp.ml | 29 ++++++++++++------- 3 files changed, 23 insertions(+), 11 deletions(-) diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index c82f0fb8a..f0f9d934f 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -230,7 +230,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) append_tail ~tail (Box.Object([],rhs))]) in let plbox = match pl with - [] -> append_tail ~tail (Box.Text([],"[]")) + | [] -> append_tail ~tail (Box.Text([],"[]")) + | [r] -> (make_rule ~tail:("]" :: tail) "[" r) | r::tl -> Box.V([], (make_rule ~tail:[] "[" r) :: diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 7fabafda3..9023b4869 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -133,6 +133,8 @@ type 'term command = *) | Coercion of loc * 'term | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Record of loc * (string * 'term) list * string * 'term * (string * 'term) list type ('term, 'ident) tactical = | Tactic of loc * ('term, 'ident) tactic diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 822618eb4..a5c0478ac 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -42,7 +42,7 @@ let pp_reduction_kind = function | `Simpl -> "simplify" | `Whd -> "whd" | `Normalize -> "normalize" - + let rec pp_tactic = function | Absurd (_, term) -> "absurd" ^ pp_term_ast term | Apply (_, term) -> "apply " ^ pp_term_ast term @@ -149,19 +149,24 @@ let pp_alias = function | Number_alias (instance,desc) -> sprintf "alias num (instance %d) = \"%s\"" instance desc +let pp_params = function + | [] -> "" + | params -> + " " ^ + String.concat " " + (List.map + (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) + params) + +let pp_fields fields = + (if fields <> [] then "\n" else "") ^ + String.concat ";\n" + (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields) + let pp_command = function | Qed _ -> "qed" | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value | Inductive (_, params, types) -> - let pp_params = function - | [] -> "" - | params -> - " " ^ - String.concat " " - (List.map - (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ)) - params) - in let pp_constructors constructors = String.concat "\n" (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) @@ -190,6 +195,10 @@ let pp_command = function | Some body -> "\\def " ^ pp_term_ast body) | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" | Alias (_,s) -> pp_alias s + | Record (_,params,name,ty,fields) -> + "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ + pp_fields fields ^ "}" + let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac -- 2.39.2