From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Apr 2009 23:35:27 +0000 (+0000)
Subject: Inductive definitions are now interpreted (but records are not interpreted yet).
X-Git-Tag: make_still_working~4038
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b3242efcd29ea188ef09b445985abb06c5fad3a;p=helm.git

Inductive definitions are now interpreted (but records are not interpreted yet).
---

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index b9b4fa42b..e3384407c 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -438,7 +438,7 @@ let interpretate_obj
           let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
       | Some bo,_ ->
-         match bo with
+        (match bo with
          | CicNotationPt.LetRec (kind, defs, _) ->
              let inductive = kind = `Inductive in
              let _,obj_context =
@@ -480,51 +480,67 @@ let interpretate_obj
                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
              in
              let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
-             NCic.Constant ([],name,Some bo,ty',attrs))
-  | _ -> raise (MultiPassDisambiguator.DisambiguationError (0, []))
-(*
-  | CicNotationPt.Inductive (params,tyl) ->
-     let uri = match uri with Some uri -> uri | None -> assert false in
-     let context,params =
-      let context,res =
-       List.fold_left
-        (fun (context,res) (name,t) ->
-          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 (name,ty,t)) params in
-     let obj_context =
-      snd (
-       List.fold_left
-        (*here the explicit_named_substituion is assumed to be of length 0 *)
-        (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
-        (0,[]) tyl) in
-     let tyl =
-      List.map
-       (fun (name,b,ty,cl) ->
-         let ty' = add_params (interpretate_term context env None false ty) in
-         let cl' =
-          List.map
-           (fun (name,ty) ->
-             let ty' =
-              add_params
-               (interpretate_term ~obj_context ~context ~env ~uri:None
-                 ~is_path:false ty)
-             in
-              name,ty'
-           ) cl
+             NCic.Constant ([],name,Some bo,ty',attrs)))
+ | CicNotationPt.Inductive (params,tyl) ->
+    let context,params =
+     let context,res =
+      List.fold_left
+       (fun (context,res) (name,t) ->
+         let t =
+          match t with
+             None -> CicNotationPt.Implicit
+           | Some t -> t in
+         let name = cic_name_of_name name in
+         let t =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false t
          in
-          name,b,ty',cl'
-       ) tyl
+          (name,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
      in
-      Cic.InductiveDefinition (tyl,[],List.length params,[])
+      context,List.rev res in
+    let add_params =
+     List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
+    let leftno = List.length params in
+    let obj_context =
+     snd (
+      List.fold_left
+       (fun (i,res) (name,_,_,_) ->
+         let _,inductive,_,_ =
+          (* ??? *)
+          try List.hd tyl with Failure _ -> assert false in
+         let nref =
+          NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
+         in
+          i+1,(name,nref)::res)
+       (0,[]) tyl) in
+    let tyl =
+     List.map
+      (fun (name,_,ty,cl) ->
+        let ty' =
+         add_params
+         (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false ty) in
+        let cl' =
+         List.map
+          (fun (name,ty) ->
+            let ty' =
+             add_params
+              (interpretate_term ~obj_context ~context ~env ~uri:None
+                ~is_path:false ty) in
+            let relevance = [] in
+             relevance,name,ty'
+          ) cl in
+        let relevance = [] in
+         relevance,name,ty',cl'
+      ) tyl
+    in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Regular in
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
+ | _ -> assert false
+(*
   | CicNotationPt.Record (params,name,ty,fields) ->
      let uri = match uri with Some uri -> uri | None -> assert false in
      let context,params =
@@ -535,7 +551,7 @@ let interpretate_obj
            match t with
               None -> CicNotationPt.Implicit
             | Some t -> t in
-          let name = CicNotationUtil.cic_name_of_name name in
+          let name = cic_name_of_name name in
            name::context,(name, interpretate_term context env None false t)::res
         ) ([],[]) params
       in