From cbe0302d6b0d2bca6657fa7479a62d0004665612 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 11 Nov 2004 13:30:45 +0000 Subject: [PATCH] added dummy entry in CicAst: UserInput --- helm/ocaml/cic_disambiguation/disambiguate.ml | 2 ++ helm/ocaml/cic_transformations/ast2pres.ml | 5 +++++ helm/ocaml/cic_transformations/cicAst.ml | 3 +++ helm/ocaml/cic_transformations/cicAstPp.ml | 2 ++ 4 files changed, 12 insertions(+) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 0c57754f6..055630971 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -280,6 +280,7 @@ let interpretate ~context ~env ast = | CicAst.Sort `CProp -> Cic.Sort Cic.CProp | CicAst.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () + | CicAst.UserInput -> assert false and aux_option loc context = function | None -> Cic.Implicit (Some `Type) | Some term -> aux loc context term @@ -368,6 +369,7 @@ let domain_of_term ~context ast = local_context | CicAst.Sort _ -> [] | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicAst.UserInput -> assert false and aux_option loc context = function | None -> [] diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml index cafd80c4a..87944aa34 100644 --- a/helm/ocaml/cic_transformations/ast2pres.ml +++ b/helm/ocaml/cic_transformations/ast2pres.ml @@ -93,6 +93,8 @@ and countterm current_size t = | A.Num (s, _) -> current_size + String.length s | A.Sort _ -> current_size + 4 (* sort name *) | A.Symbol (s,_) -> current_size + String.length s + + | A.UserInput -> current_size ;; let is_big t = @@ -328,6 +330,8 @@ let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = []) | A.Symbol (s, _) -> Box.Text([],s) + | A.UserInput -> Box.Text([],"") + and aux_option ~tail = function None -> Box.Text([],"_") | Some ast -> ast2box ~tail ast @@ -463,6 +467,7 @@ let ast2mpres ?(priority = 0) ?(assoc = false) (ast, ids_to_uris) = | A.Sort `Type -> P.Mtext ([], "Type") | A.Sort `CProp -> P.Mtext ([], "CProp") | A.Implicit -> P.Mtext([], "?") + | A.UserInput -> P.Mtext([], "") | A.Appl [] -> assert false | A.Appl ((hd::tl) as l) -> let rec find_symbol idref = function diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml index fcc803697..cb65c2497 100644 --- a/helm/ocaml/cic_transformations/cicAst.ml +++ b/helm/ocaml/cic_transformations/cicAst.ml @@ -75,6 +75,9 @@ type term = | Sort of sort_kind | Symbol of string * int (* canonical name, instance *) + | UserInput (* place holder for user input, used by MatitaConsole, not to be + used elsewhere *) + and capture_variable = Cic.name * term option (* name, type *) and meta_subst = term option and subst = string * term diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index dda70793f..4c0412949 100644 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -78,6 +78,8 @@ let rec pp_term = function | CicAst.Sort `CProp -> "CProp" | CicAst.Symbol (name, _) -> name + | CicAst.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) -- 2.39.2