From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 2 Mar 2004 17:12:58 +0000 (+0000)
Subject: differentieted empty substitution list from no substitution given
X-Git-Tag: v0_0_4~55
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee02781cec1158f51e98ca73a14b63841e5ba545;p=helm.git

differentieted empty substitution list from no substitution given
---

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 19b6c4b4b..e51e9c0a4 100644
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -70,7 +70,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
   let module Ast = CicAst in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
   let rec aux = function
-    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,subst) ->
         register_uri id (UriManager.string_of_uri uri);
         idref id
@@ -181,7 +181,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -195,11 +195,13 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
 
   and astsubst_of_cicsubst subst =
-    List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
-      subst
+    Some
+      (List.map (fun (uri, annterm) ->
+        (UriManager.name_of_uri uri, aux annterm))
+        subst)
 
   and astcontext_of_ciccontext context =
     List.map
diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 9679501ab..dbbfff8e5 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -76,7 +76,8 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
 	  countterm size1 t
-    | A.Ident(s,l) ->
+    | A.Ident(s,None) -> current_size + (String.length s)
+    | A.Ident(s,Some l) ->
         List.fold_left 
 	  (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -218,8 +219,12 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
 	    | [(s,t)] -> 
 		make_subst start_txt s t "]"
 	    | (s,t)::tl ->
-		(make_subst start_txt s t ";")@(make_substs " " tl) in
-	  make_substs "[" subst in
+		(make_subst start_txt s t ";")@(make_substs " " tl)
+          in
+          match subst with
+          | Some subst -> make_substs "[" subst
+          | None -> []
+        in
 	Box.V([], (* attr here or on Vbox? *)
 	      [Box.Text(map_attributes attr,s);
 	       Box.indent(Box.V([],subst))])
diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 92ab328c1..f7392fa3a 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -44,7 +44,10 @@ type term =
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term
       (* (name, body, decreasing argument) list, where *)
-  | Ident of string * subst list  (* literal, substitutions *)
+  | Ident of string * subst list option
+      (* literal, substitutions.
+      * Some [] -> user has given an empty explicit substitution list 
+      * None -> user has given no explicit substitution list *)
   | Implicit
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)
diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index 02cf5511c..bd9eea601 100644
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -62,8 +62,10 @@ let rec pp_term = function
               sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
-  | CicAst.Ident (name, []) -> name
-  | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some [])
+  | CicAst.Ident (name, None) ->
+      name
+  | CicAst.Ident (name, Some substs) -> sprintf "%s[%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index