From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 31 Jan 2007 18:36:04 +0000 (+0000)
Subject: Several bugs fixed:
X-Git-Tag: 0.4.95@7852~637
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e134b6f156268364d3027e73910c19e9c7e09838;p=helm.git

Several bugs fixed:
 1. mutual definitions were not generated correctly
    (e.g. let rec even ... and odd in even actually resulted in a
     definition of odd!)
 2. a top-level mutual definition now generates two constants (as it
    should have always been)
---

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 6d70c22c9..2873912c0 100644
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -263,6 +263,7 @@ let pp_params pp_term = function
       
 let pp_flavour = function
   | `Definition -> "definition"
+  | `MutualDefinition -> assert false
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -301,6 +302,8 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body) ->
     sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)
diff --git a/components/cic/cic.ml b/components/cic/cic.ml
index c5a5c1e40..1b02df3f1 100644
--- a/components/cic/cic.ml
+++ b/components/cic/cic.ml
@@ -57,6 +57,7 @@ type name =
 
 type object_flavour =
   [ `Definition
+  | `MutualDefinition
   | `Fact
   | `Lemma
   | `Remark
diff --git a/components/cic/cicParser.ml b/components/cic/cicParser.ml
index 3122affd4..49a5a1ab7 100644
--- a/components/cic/cicParser.ml
+++ b/components/cic/cicParser.ml
@@ -667,6 +667,7 @@ let end_element ctxt tag =
       push ctxt 
         (match pop_tag_attrs ctxt with
         | [ "value", "definition"] -> Obj_flavour `Definition
+        | [ "value", "mutual_definition"] -> Obj_flavour `MutualDefinition
         | [ "value", "fact"] -> Obj_flavour `Fact
         | [ "value", "lemma"] -> Obj_flavour `Lemma
         | [ "value", "remark"] -> Obj_flavour `Remark
diff --git a/components/cic_acic/cic2Xml.ml b/components/cic_acic/cic2Xml.ml
index afe22d374..c90bc348c 100644
--- a/components/cic_acic/cic2Xml.ml
+++ b/components/cic_acic/cic2Xml.ml
@@ -294,6 +294,8 @@ let xml_of_attrs attributes =
   in
   let flavour_of = function
     | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+    | `MutualDefinition ->
+        Xml.xml_empty "flavour" [None, "value", "mutual_definition"]
     | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
     | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
     | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 1d4a6a61e..5c198cb59 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -86,7 +86,7 @@ let uniq_domain dom =
  in
   snd (aux [] dom)
 
-let debug = false
+let debug = true
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
@@ -267,14 +267,14 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         let cic_body =
          let unlocalized_body = aux ~localize:false loc context' body in
          match unlocalized_body with
-            Cic.Rel 1 -> `AvoidLetInNoAppl
-          | Cic.Appl (Cic.Rel 1::l) ->
+            Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
+          | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
              (try
                let l' =
                 List.map
                  (function t ->
                    let t',subst,metasenv =
-                    CicMetaSubst.delift_rels [] [] 1 t
+                    CicMetaSubst.delift_rels [] [] (List.length defs) t
                    in
                     assert (subst=[]);
                     assert (metasenv=[]);
@@ -286,10 +286,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                      let l' = List.map (aux ~localize loc context) l in
-                      `AvoidLetIn l'
+                      `AvoidLetIn (n,l')
                   | _ -> assert false
                 else
-                 `AvoidLetIn l'
+                 `AvoidLetIn (n,l')
               with
                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                 if localize then
@@ -324,42 +324,32 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
               (name, decr_idx, cic_type, cic_body))
             defs
         in
-        let counter = ref ~-1 in
-        let build_term funs =
-          (* this is the body of the fold_right function below. Rationale: Fix
-           * and CoFix cases differs only in an additional index in the
-           * inductiveFun list, see Cic.term *)
-          match kind with
-          | `Inductive ->
-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let fix = Cic.Fix (!counter,funs) in
-                 match cic with
-                    `Recipe (`AddLetIn cic) ->
-                      `Term (Cic.LetIn (Cic.Name var, fix, cic))
-                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l))
-                  | `Recipe `AvoidLetInNoAppl -> `Term fix
-                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t)))
+        let fix_or_cofix n =
+         match kind with
+            `Inductive -> Cic.Fix (n,inductiveFuns)
           | `CoInductive ->
-              let funs =
-                List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
+              let coinductiveFuns =
+                List.map
+                 (fun (name, _, typ, body) -> name, typ, body)
+                 inductiveFuns
               in
-              (fun (var, _, _, _) cic ->
-                incr counter;
-                let cofix = Cic.CoFix (!counter,funs) in
-                 match cic with
-                    `Recipe (`AddLetIn cic) ->
-                      `Term (Cic.LetIn (Cic.Name var, cofix, cic))
-                  | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l))
-                  | `Recipe `AvoidLetInNoAppl -> `Term cofix
-                  | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t)))
+               Cic.CoFix (n,coinductiveFuns)
         in
-         (match
-           List.fold_right (build_term inductiveFuns) inductiveFuns
-            (`Recipe cic_body)
-          with
-             `Recipe _ -> assert false
-           | `Term t -> t)
+         let counter = ref ~-1 in
+         let build_term funs (var,_,_,_) t =
+          incr counter;
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+         in
+          (match cic_body with
+              `AvoidLetInNoAppl n ->
+                let n' = List.length inductiveFuns - n in
+                 fix_or_cofix n'
+            | `AvoidLetIn (n,l) ->
+                let n' = List.length inductiveFuns - n in
+                 Cic.Appl (fix_or_cofix n'::l)
+            | `AddLetIn cic_body ->         
+                List.fold_right (build_term inductiveFuns) inductiveFuns
+                 cic_body)
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
     | CicNotationPt.Ident (name, subst)
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 2d3789221..9a0cc9f43 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -574,6 +574,11 @@ EXTEND
         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
+         (* In case of mutual definitions here we produce just
+            the syntax tree for the first one. The others will be
+            generated from the completely specified term just before
+            insertion in the environment. We use the flavour
+            `MutualDefinition to rememer this. *)
           let name,ty = 
             match defs with
             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
@@ -588,8 +593,14 @@ EXTEND
             | _ -> assert false 
           in
           let body = Ast.Ident (name,None) in
-          GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty,
-            Some (Ast.LetRec (ind_kind, defs, body))))
+          let flavour =
+           if List.length defs = 1 then
+            `Definition
+           else
+            `MutualDefinition
+          in
+           GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
+             Some (Ast.LetRec (ind_kind, defs, body))))
     | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a4908ce7c..086893a97 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -405,12 +405,54 @@ let generate_inversion refinement_toolkit uri obj =
        add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
     (!build_inversion_principle uri obj)
 
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+    Cic.Fix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,idx,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.Fix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | Cic.CoFix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (n+1,uris)
+         else
+          let uri =
+           UriManager.uri_of_string
+            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
+          let bo = Cic.CoFix (n,funs) in 
+          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | _ -> assert false
+
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;
  let uris = ref [] in
  try
   begin
    match obj with
+    | Cic.Constant (name,Some bo,_,_,attrs) when
+       List.mem (`Flavour `MutualDefinition) attrs ->
+        uris :=
+         !uris @
+           generate_sibling_mutual_definitions refinement_toolkit uri attrs
+            name bo
     | Cic.Constant _ -> ()
     | Cic.InductiveDefinition (_,_,_,attrs) ->
         uris := !uris @