From da6e5b3fcfc9ae2fb4655b755cc3b0db600a966d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 Jul 2003 08:14:43 +0000 Subject: [PATCH] 1. folded maction are now selectable 2. metavariable occurrences are now displayed together with their substitution (to be improved) 3. the hypothesis in the metasenv are now displayed in the right order --- helm/ocaml/cic_transformations/cexpr2pres.ml | 42 +++++++++++++++---- .../ocaml/cic_transformations/content2pres.ml | 7 +++- .../content_expressions.ml | 14 ++++++- .../content_expressions.mli | 4 +- 4 files changed, 53 insertions(+), 14 deletions(-) diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml index 40f185dcd..f6a3b490d 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -49,7 +49,13 @@ let countterm current_size t = let c1 = current_size + (String.length name) in countsubst subst c1 | CE.LocalVar (_,name) -> current_size + (String.length name) - | CE.Meta (_,name) -> current_size + (String.length name) + | CE.Meta (_,name,l) -> + List.fold_left + (fun i t -> + match t with + None -> i + | Some t' -> aux i t' + ) (current_size + String.length name) l | CE.Num (_,value) -> current_size + (String.length value) | CE.Appl (_,l) -> List.fold_left aux current_size l @@ -134,11 +140,20 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = if tail = [] then P.Mi (attr,name) else P.Mrow([],P.Mi (attr,name)::tail) - | CE.Meta (xref,name) -> + | CE.Meta (xref,name,l) -> let attr = make_attributes [Some "helm","xref"] [xref] in - if tail = [] then - P.Mi (attr,name) - else P.Mrow([],P.Mi (attr,name)::tail) + let l' = + List.map + (function + None -> P.Mo [] "_" + | Some t -> cexpr2pres t + ) l + in + if tail = [] then + P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")]) + else + P.Mrow + ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail) | CE.Num (xref,value) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then @@ -293,11 +308,20 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = if tail = [] then P.Mi (attr,name) else P.Mrow ([],P.Mi (attr,name)::tail) - | CE.Meta (xref,name) -> + | CE.Meta (xref,name,l) -> let attr = make_attributes [Some "helm","xref"] [xref] in - if tail = [] then - P.Mi (attr,name) - else P.Mrow ([],P.Mi (attr,name)::tail) + let l' = + List.map + (function + None -> P.Mo [] "_" + | Some t -> cexpr2pres t + ) l + in + if tail = [] then + P.Mrow ([],P.Mi (attr,name) :: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")]) + else + P.Mrow + ([],P.Mi (attr,name):: P.Mo ([],"[") :: l' @ [P.Mo ([],"]")] @ tail) | CE.Num (xref,value) -> let attr = make_attributes [Some "helm","xref"] [xref] in if tail = [] then diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index cfa061bfb..69b0966f1 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -612,7 +612,10 @@ and proof2pres term2pres p = let body = conclude2pres p.Con.proof_conclude true false in let presacontext = P.Maction([None,"actiontype","toggle" ; None,"selection","1"], - [P.indented (P.Mtext([None,"mathcolor","Red"],"Proof")); + [P.indented + (P.Mtext + ([None,"mathcolor","Red" ; + Some "helm", "xref", p.Con.proof_id],"Proof")) ; acontext2pres p.Con.proof_apply_context body true]) in P.Mtable ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"], @@ -849,7 +852,7 @@ let content2pres term2pres (id,params,metasenv,obj) = | Some n -> n) ; P.Mo [] ":=" ; proof2pres term2pres p] - ) context @ + ) (List.rev context) @ [ P.Mo [] "|-" ] @ [ P.Mi [] (string_of_int n) ; P.Mo [] ":" ; diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index b78d1380a..f1c648e9b 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -42,7 +42,7 @@ type cexpr = Symbol of string option * string * subst option * string option (* h:xref, name, subst, definitionURL *) | LocalVar of (string option) * string (* h:xref, name *) - | Meta of string option * string (* h:xref, name *) + | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) | Num of string option * string (* h:xref, value *) | Appl of string option * cexpr list (* h:xref, args *) | Binder of string option * string * decl * cexpr @@ -58,6 +58,8 @@ and def = string * cexpr (* name, body *) and subst = (UriManager.uri * cexpr) list +and + meta_subst = cexpr option list ;; (* NOTATION *) @@ -275,7 +277,15 @@ let acic2cexpr ids_to_inner_sorts t = | C.AVar (id,uri,subst) -> Symbol (Some id, UriManager.name_of_uri uri, make_subst subst, Some (UriManager.string_of_uri uri)) - | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n))) + | C.AMeta (id,n,l) -> + let l' = + List.rev_map + (function + None -> None + | Some t -> Some (acic2cexpr t) + ) l + in + Meta (Some id,("?" ^ (string_of_int n)),l') | C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None) | C.AImplicit _ -> raise NotImplemented | C.AProd (id,n,s,t) -> diff --git a/helm/ocaml/cic_transformations/content_expressions.mli b/helm/ocaml/cic_transformations/content_expressions.mli index 5eb2e503c..e945d96d2 100644 --- a/helm/ocaml/cic_transformations/content_expressions.mli +++ b/helm/ocaml/cic_transformations/content_expressions.mli @@ -37,7 +37,7 @@ type Symbol of string option * string * (subst option) * string option (* h:xref, name, subst, definitionURL *) | LocalVar of string option * string (* h:xref, name *) - | Meta of string option * string (* h:xref, name *) + | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *) | Num of string option * string (* h:xref, value *) | Appl of string option * cexpr list (* h:xref, args *) | Binder of string option *string * decl * cexpr @@ -53,6 +53,8 @@ and def = string * cexpr (* name, body *) and subst = (UriManager.uri * cexpr) list +and + meta_subst = cexpr option list ;; -- 2.39.2