X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=520db6aca994a6710ba955362387803e8564d7a7;hb=7ce251730873891f2975bc8c46b122e842d203db;hp=4d8b132269ecd01cfac6abfb0ed8208bca2137a8;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 4d8b13226..520db6aca 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -27,6 +27,12 @@ let cic_name_of_name = function
   | _ -> assert false
 ;;
 
+let rec mk_rels howmany from =
+  match howmany with 
+  | 0 -> []
+  | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
+;;
+
 let refine_term 
  metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
   assert (uri=None);
@@ -36,8 +42,8 @@ let refine_term
     let localise t = 
       try NCicUntrusted.NCicHash.find localization_tbl t
       with Not_found -> 
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-        assert false
+        prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+        (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof
@@ -438,7 +444,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,94 +486,118 @@ 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,[])
-  | CicNotationPt.Record (params,name,ty,fields) ->
-     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 ty' = add_params (interpretate_term context env None false ty) in
-     let fields' =
-      snd (
-       List.fold_left
-        (fun (context,res) (name,ty,_coercion,arity) ->
-          let context' = Cic.Name name :: context in
-           context',(name,interpretate_term context env None false ty)::res
-        ) (context,[]) fields) in
-     let concl =
-      (*here the explicit_named_substituion is assumed to be of length 0 *)
-      let mutind = Cic.MutInd (uri,0,[]) in
-      if params = [] then mutind
-      else
-       Cic.Appl
-        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
-     let con =
+      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 t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
-       concl fields' in
-     let con' = add_params con in
-     let tyl = [name,true,ty',["mk_" ^ name,con']] in
-     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
-      Cic.InductiveDefinition
-       (tyl,[],List.length params,[`Class (`Record field_names)])
-*)
+       (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)
+ | CicNotationPt.Record (params,name,ty,fields) ->
+    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,NCic.Decl t)::context,(name,t)::res
+       ) ([],[]) params
+     in
+      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 ty' =
+     add_params
+      (interpretate_term ~obj_context:[] ~context ~env ~uri:None
+        ~is_path:false ty) in
+    let fields' =
+     snd (
+      List.fold_left
+       (fun (context,res) (name,ty,_coercion,_arity) ->
+         let ty =
+          interpretate_term ~obj_context:[] ~context ~env ~uri:None
+           ~is_path:false ty in
+         let context' = (name,NCic.Decl ty)::context in
+          context',(name,ty)::res
+       ) (context,[]) fields) in
+    let concl =
+     let nref =
+      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
+     let mutind = NCic.Const nref in
+     if params = [] then mutind
+     else
+      NCic.Appl
+       (mutind::mk_rels (List.length params) (List.length fields)) in
+    let con =
+     List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
+    let con' = add_params con in
+    let relevance = [] in
+    let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
+    let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
+     let height = (* XXX calculate *) 0 in
+     let attrs = `Provided, `Record field_names in
+     uri, height, [], [], 
+     NCic.Inductive (true,leftno,tyl,attrs)
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty