From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 11 Nov 2004 13:30:45 +0000 (+0000)
Subject: added dummy entry in CicAst: UserInput
X-Git-Tag: PRE_UNIVERSES~31
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbe0302d6b0d2bca6657fa7479a62d0004665612;p=helm.git

added dummy entry in CicAst: UserInput
---

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)