From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 13 Oct 2006 16:53:54 +0000 (+0000)
Subject: New content level representations for LetRec, Inductive and CoInductive.
X-Git-Tag: 0.4.95@7852~892
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=213cc7cf3c9da7c024b44b54e07035b831f7a31f;p=helm.git

New content level representations for LetRec, Inductive and CoInductive.
For LetRec the pretty-printer is now in sync with the parser.
---

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 785c8bd86..47bfe2748 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -114,33 +114,21 @@ let rec pp_term ?(pp_parens = true) t =
         sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1)
           (pp_term ~pp_parens:true t2)
     | Ast.LetRec (kind, definitions, term) ->
-        let strip i t =
-	   let rec aux i l = function
-	      | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body
-	      | body                                 -> List.rev l, body
-	   in 
-	   aux i [] t
-	in
 	let rec get_guard i = function
 	   | []                   -> (*assert false*) Ast.Implicit
 	   | [term, _] when i = 1 -> term
 	   | _ :: tl              -> get_guard (pred i) tl
 	in
-	let map (var, body, i) =
-           let id, vars, typ, body = match var with
-	      | term, Some typ ->
-	         let pvars, pbody = strip i typ in
-		 let _, bbody = strip i body in
-		 term, pvars, pbody, bbody
-	      | term, None ->
-                 let pbody = Ast.Implicit in
-		 let pvars, bbody = strip i body in
-		 term, pvars, pbody, bbody
-	   in
+	let map (params, (id,typ), body, i) =
+         let typ =
+          match typ with
+             None -> Ast.Implicit
+           | Some typ -> typ
+         in
 	   sprintf "%s %s on %s: %s \\def %s" 
 	      (pp_term ~pp_parens:false term)
-	      (String.concat " " (List.map pp_capture_variable vars))
-	      (pp_term ~pp_parens:false (get_guard i vars))
+	      (String.concat " " (List.map pp_capture_variable params))
+	      (pp_term ~pp_parens:false (get_guard i params))
 	      (pp_term typ) (pp_term body)
 	in
 	sprintf "let %s %s in %s"
@@ -271,12 +259,7 @@ let set_pp_term f = _pp_term := f
 
 let pp_params = function
   | [] -> ""
-  | params ->
-      " " ^
-      String.concat " "
-        (List.map
-          (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
-          params)
+  | params -> " " ^ String.concat " " (List.map pp_capture_variable params)
       
 let pp_flavour = function
   | `Definition -> "definition"
diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml
index 6ea1ec917..f6652f63f 100644
--- a/components/acic_content/cicNotationPt.ml
+++ b/components/acic_content/cicNotationPt.ml
@@ -75,8 +75,8 @@ type term =
       (* what to match, inductive type, out type, <pattern,action> list *)
   | Cast of term * 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 *)
+  | LetRec of induction_kind * (capture_variable list * capture_variable * term * int) list * term
+      (* (params, name, body, decreasing arg) list, where *)
   | Ident of string * subst list option
       (* literal, substitutions.
       * Some [] -> user has given an empty explicit substitution list 
@@ -164,7 +164,7 @@ type cic_appl_pattern =
 type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
 type obj =
-  | Inductive of (string * term) list * term inductive_type list
+  | Inductive of capture_variable list * term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
   | Theorem of Cic.object_flavour * string * term * term option
       (** flavour, name, type, body
@@ -174,7 +174,7 @@ type obj =
        *   will be given in proof editing mode using the tactical language,
        *   unless the flavour is an Axiom
        *)
-  | Record of (string * term) list * string * term * (string * term * bool * int) list
+  | Record of capture_variable list * string * term * (string * term * bool * int) list
       (** left parameters, name, type, fields *)
 
 (** {2 Standard precedences} *)
diff --git a/components/acic_content/cicNotationUtil.ml b/components/acic_content/cicNotationUtil.ml
index d9114b180..f331b79ca 100644
--- a/components/acic_content/cicNotationUtil.ml
+++ b/components/acic_content/cicNotationUtil.ml
@@ -40,7 +40,9 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Ast.LetRec (kind, definitions, term) ->
         let definitions =
           List.map
-            (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+            (fun (params, var, ty, decrno) ->
+              List.map aux_capture_variable params, aux_capture_variable var,
+              k ty, decrno)
             definitions
         in
         Ast.LetRec (kind, definitions, k term)
@@ -213,7 +215,8 @@ let meta_names_of_term term =
     aux term
   and aux_pattern (head, _, vars) = 
     List.iter aux_capture_var vars
-  and aux_definition (var, term, i) =
+  and aux_definition (params, var, term, decrno) =
+    List.iter aux_capture_var params ;
     aux_capture_var var ;
     aux term
   and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
@@ -367,6 +370,9 @@ let freshen_obj obj =
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
   let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
+  let freshen_capture_variables =
+   List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t))
+  in
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =
@@ -374,15 +380,15 @@ let freshen_obj obj =
           (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
           indtypes
       in
-      CicNotationPt.Inductive (freshen_name_ty params, indtypes)
+      CicNotationPt.Inductive (freshen_capture_variables params, indtypes)
   | CicNotationPt.Theorem (flav, n, t, ty_opt) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
       CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
   | CicNotationPt.Record (params, n, ty, fields) ->
-      CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
-        freshen_name_ty_b fields)
+      CicNotationPt.Record (freshen_capture_variables params, n,
+        freshen_term ty, freshen_name_ty_b fields)
 
 let freshen_term = freshen_term ?index:None
 
diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index 516d5f542..cda76ce09 100644
--- a/components/acic_content/termAcicContent.ml
+++ b/components/acic_content/termAcicContent.ml
@@ -198,28 +198,72 @@ let ast_of_acic0 term_info acic k =
         let defs = 
           List.map
             (fun (_, n, decr_idx, ty, bo) ->
-              ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
+              let params,bo =
+               let rec aux =
+                function
+                   Cic.ALambda (_,name,so,ta) ->
+                    let params,rest = aux ta in
+                     (CicNotationUtil.name_of_cic_name name,Some (k so))::
+                      params, rest
+                 | t -> [],t
+               in
+                aux bo
+              in
+              let ty =
+               let rec eat_pis =
+                function
+                   0,ty -> ty
+                 | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+                 | n,ty ->
+                    (* I should do a whd here, but I have no context *)
+                    assert false
+               in
+                eat_pis ((List.length params),ty)
+              in
+               (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
             funs
         in
         let name =
           try
             (match List.nth defs no with
-            | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+            | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
+         idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
             (fun (_, n, ty, bo) ->
-              ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
+              let params,bo =
+               let rec aux =
+                function
+                   Cic.ALambda (_,name,so,ta) ->
+                    let params,rest = aux ta in
+                     (CicNotationUtil.name_of_cic_name name,Some (k so))::
+                      params, rest
+                 | t -> [],t
+               in
+                aux bo
+              in
+              let ty =
+               let rec eat_pis =
+                function
+                   0,ty -> ty
+                 | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+                 | n,ty ->
+                    (* I should do a whd here, but I have no context *)
+                    assert false
+               in
+                eat_pis ((List.length params),ty)
+              in
+               (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0))
             funs
         in
         let name =
           try
             (match List.nth defs no with
-            | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+            | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
             | _ -> assert false)
           with Not_found -> assert false
         in
diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index fb4c338a4..243f7c8bf 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -215,7 +215,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
-            (fun acc ((name, _), _, _) ->
+            (fun acc (_, (name, _), _, _) ->
               CicNotationUtil.cic_name_of_name name :: acc)
             context defs
         in
@@ -259,10 +259,16 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         in
         let inductiveFuns =
           List.map
-            (fun ((name, typ), body, decr_idx) ->
-              let cic_body = aux ~localize loc context' body in
+            (fun (params, (name, typ), body, decr_idx) ->
+              let add_binders kind t =
+               List.fold_right
+                (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
+              in
+              let cic_body =
+               aux ~localize loc context' (add_binders `Lambda body) in
               let cic_type =
-               aux_option ~localize loc context (Some `Type) typ in
+               aux_option ~localize loc context (Some `Type)
+                (HExtlib.map_option (add_binders `Pi) typ) in
               let name =
                 match CicNotationUtil.cic_name_of_name name with
                 | Cic.Anonymous ->
@@ -432,14 +438,17 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       let context,res =
        List.fold_left
         (fun (context,res) (name,t) ->
-          Cic.Name name :: context,
-          (name, interpretate_term context env None false t)::res
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
         ) ([],[]) params
       in
        context,List.rev res in
      let add_params =
-      List.fold_right
-       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
+      List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
      let name_to_uris =
       snd (
        List.fold_left
@@ -471,14 +480,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       let context,res =
        List.fold_left
         (fun (context,res) (name,t) ->
-          (Cic.Name name :: context),
-          (name, interpretate_term context env None false t)::res
+          let t =
+           match t with
+              None -> CicNotationPt.Implicit
+            | Some t -> t in
+          let name = CicNotationUtil.cic_name_of_name name in
+           name::context,(name, interpretate_term context env None false t)::res
         ) ([],[]) params
       in
        context,List.rev res in
      let add_params =
       List.fold_right
-       (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
+       (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
      let ty' = add_params (interpretate_term context env None false ty) in
      let fields' =
       snd (
@@ -562,7 +575,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
         | `Exists -> [ loc, Symbol ("exists", 0) ]
         | _ -> []
       in
-      let type_dom = domain_rev_of_term_option loc context typ in
+      let type_dom = domain_rev_of_term_option ~loc context typ in
       let body_dom =
         domain_rev_of_term ~loc
           (CicNotationUtil.cic_name_of_name var :: context) body
@@ -607,19 +620,31 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
       in
       where_dom @ type_dom @ body_dom
   | CicNotationPt.LetRec (kind, defs, where) ->
-      let context' =
+      let add_defs context =
         List.fold_left
-          (fun acc ((var, typ), _, _) ->
-            CicNotationUtil.cic_name_of_name var :: acc)
-          context defs
-      in
-      let where_dom = domain_rev_of_term ~loc context' where in
+          (fun acc (_, (var, _), _, _) ->
+            CicNotationUtil.cic_name_of_name var :: acc
+          ) context defs in
+      let where_dom = domain_rev_of_term ~loc (add_defs context) where in
       let defs_dom =
         List.fold_left
-          (fun dom ((_, typ), body, _) ->
+          (fun dom (params, (_, typ), body, _) ->
+            let context' =
+             add_defs
+              (List.fold_left
+                (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
+                context params)
+            in
             domain_rev_of_term ~loc context' body @
-            domain_rev_of_term_option loc context typ)
-          [] defs
+            domain_rev_of_term_option ~loc context typ @
+            List.rev
+             (snd
+               (List.fold_left
+                (fun (context,res) (var,ty) ->
+                  CicNotationUtil.cic_name_of_name var :: context,
+                  res @ domain_rev_of_term_option ~loc context ty)
+                (add_defs context,[]) params))
+          ) [] defs
       in
       where_dom @ defs_dom
   | CicNotationPt.Ident (name, subst) ->
@@ -654,7 +679,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.Magic _
   | CicNotationPt.Variable _ -> assert false
 
-and domain_rev_of_term_option loc context = function
+and domain_rev_of_term_option ~loc context = function
   | None -> []
   | Some t -> domain_rev_of_term ~loc context t
 
@@ -681,12 +706,17 @@ let domain_of_obj ~context ast =
       let dom = 
        List.fold_left
         (fun dom (_,ty) ->
-          domain_rev_of_term [] ty @ dom
+          match ty with
+             None -> dom
+           | Some ty -> domain_rev_of_term [] ty @ dom
         ) dom params
       in
        List.filter
         (fun (_,name) ->
-          not (  List.exists (fun (name',_) -> name = Id name') params
+          not (  List.exists (fun (name',_) ->
+                  match CicNotationUtil.cic_name_of_name name' with
+                     Cic.Anonymous -> false
+                   | Cic.Name name' -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
         ) dom
    | CicNotationPt.Record (params,_,ty,fields) ->
@@ -696,12 +726,17 @@ let domain_of_obj ~context ast =
       let dom =
        List.fold_left
         (fun dom (_,ty) ->
-          domain_rev_of_term [] ty @ dom
+          match ty with
+             None -> dom
+           | Some ty -> domain_rev_of_term [] ty @ dom
         ) (dom @ domain_rev_of_term [] ty) params
       in
        List.filter
         (fun (_,name) ->
-          not (  List.exists (fun (name',_) -> name = Id name') params
+          not (  List.exists (fun (name',_) ->
+                  match CicNotationUtil.cic_name_of_name name' with
+                     Cic.Anonymous -> false
+                   | Cic.Name name' -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') fields)
         ) dom
  in
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index af185a63e..9b9a5da22 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -61,12 +61,6 @@ type by_continuation =
 
 EXTEND
   GLOBAL: term statement;
-  arg: [
-   [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],Ast.Implicit
-   ]
-  ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
   ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
@@ -360,7 +354,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+    fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";
@@ -382,7 +376,7 @@ EXTEND
   ] ];
   
   record_spec: [ [
-    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+    name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
@@ -551,8 +545,14 @@ EXTEND
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+            | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
+                let ty =
+                 List.fold_right
+                  (fun var ty -> Ast.Binder (`Pi,var,ty)
+                  ) params ty
+                in
+                 name,ty
+            | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
                 name, Ast.Implicit
             | _ -> assert false 
           in
diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index f5ac2b3ec..65000b9ba 100644
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -198,7 +198,7 @@
 	<entry id="grammar.rec_def">&rec_def;</entry>
 	<entry>::=</entry>
 	<entry>
-	  &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
+	  &id; [&id;|<emphasis role="bold">_</emphasis>|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
 	</entry>
 	<entry />
       </row>
@@ -417,6 +417,10 @@
      <command>f</command> must be defined by means of tactics.</para>
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
+  <sect2 id="letrec">
+    <title><emphasis role="bold">letrec</emphasis> &TODO;</title>
+    <titleabbrev>&TODO;</titleabbrev>
+  </sect2>
   <sect2 id="inductive">
     <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
 [<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…