]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_disambiguation/nCicDisambiguate.ml
lambda-delta must be a contrib
[helm.git] / matita / components / ng_disambiguation / nCicDisambiguate.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 open Printf
15
16 open DisambiguateTypes
17
18 module Ast = NotationPt
19 module NRef = NReference 
20
21 let debug_print s = prerr_endline (Lazy.force s);;
22 let debug_print _ = ();;
23
24 let cic_name_of_name = function
25   | Ast.Ident (n, None) ->  n
26   | _ -> assert false
27 ;;
28
29 let rec mk_rels howmany from =
30   match howmany with 
31   | 0 -> []
32   | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) from)
33 ;;
34
35 let refine_term (status: #NCicCoercion.status) metasenv subst context uri ~use_coercions term expty _
36  ~localization_tbl
37 =
38   assert (uri=None);
39   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
40     (status#ppterm ~metasenv ~subst ~context term)));
41   try
42     let localise t = 
43       try NCicUntrusted.NCicHash.find localization_tbl t
44       with Not_found -> 
45         prerr_endline ("NOT LOCALISED" ^ status#ppterm ~metasenv ~subst ~context t);
46         (*assert false*) HExtlib.dummy_floc
47     in
48     let metasenv, subst, term, _ = 
49       NCicRefiner.typeof 
50         (status#set_coerc_db 
51           (if use_coercions then status#coerc_db else NCicCoercion.empty_db))
52         metasenv subst context term expty ~localise 
53     in
54      Disambiguate.Ok (term, metasenv, subst, ())
55   with
56   | NCicRefiner.Uncertain loc_msg ->
57       debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ 
58         status#ppterm ~metasenv ~subst ~context term)) ;
59       Disambiguate.Uncertain loc_msg
60   | NCicRefiner.RefineFailure loc_msg ->
61       debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
62         (status#ppterm ~metasenv ~subst ~context term) (snd(Lazy.force loc_msg))));
63       Disambiguate.Ko loc_msg
64 ;;
65
66 let refine_obj status metasenv subst _context _uri ~use_coercions obj _ _ugraph
67  ~localization_tbl 
68 =
69   assert (metasenv=[]);
70   assert (subst=[]);
71   let localise t = 
72     try NCicUntrusted.NCicHash.find localization_tbl t
73     with Not_found -> 
74       (*assert false*)HExtlib.dummy_floc
75   in
76   try
77     let obj =
78       NCicRefiner.typeof_obj
79         (status#set_coerc_db
80            (if use_coercions then status#coerc_db 
81             else NCicCoercion.empty_db))
82         obj ~localise 
83     in
84       Disambiguate.Ok (obj, [], [], ())
85   with
86   | NCicRefiner.Uncertain loc_msg ->
87       debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^ 
88         status#ppobj obj)) ;
89       Disambiguate.Uncertain loc_msg
90   | NCicRefiner.RefineFailure loc_msg ->
91       debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
92         (status#ppobj obj) (snd(Lazy.force loc_msg))));
93       Disambiguate.Ko loc_msg
94 ;;
95   
96
97   (* TODO move it to Cic *)
98 let find_in_context name context =
99   let rec aux acc = function
100     | [] -> raise Not_found
101     | hd :: _ when hd = name -> acc
102     | _ :: tl ->  aux (acc + 1) tl
103   in
104   aux 1 context
105
106 let interpretate_term_and_interpretate_term_option (status: #NCic.status)
107   ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
108   ~localization_tbl 
109 =
110   (* create_dummy_ids shouldbe used only for interpretating patterns *)
111   assert (uri = None);
112
113   let rec aux ~localize loc context = function
114     | NotationPt.AttributedTerm (`Loc loc, term) ->
115         let res = aux ~localize loc context term in
116         if localize then 
117          NCicUntrusted.NCicHash.add localization_tbl res loc;
118        res
119     | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
120     | NotationPt.Appl 
121         (NotationPt.AttributedTerm (att, inner)::args)->
122         aux ~localize loc context 
123           (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args)))
124     | NotationPt.Appl (NotationPt.Appl inner :: args) ->
125         aux ~localize loc context (NotationPt.Appl (inner @ args))
126     | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
127         let cic_args = List.map (aux ~localize loc context) args in
128         Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
129     | NotationPt.Appl terms ->
130        NCic.Appl (List.map (aux ~localize loc context) terms)
131     | NotationPt.Binder (binder_kind, (var, typ), body) ->
132         let cic_type = aux_option ~localize loc context `Type typ in
133         let cic_name = cic_name_of_name var  in
134         let cic_body = aux ~localize loc (cic_name :: context) body in
135         (match binder_kind with
136         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
137         | `Pi
138         | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
139         | `Exists ->
140             Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0))
141               (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ]))
142     | NotationPt.Case (term, indty_ident, outtype, branches) ->
143         let cic_term = aux ~localize loc context term in
144         let cic_outtype = aux_option ~localize loc context `Term outtype in
145         let do_branch ((_, _, args), term) =
146          let rec do_branch' context = function
147            | [] -> aux ~localize loc context term
148            | (name, typ) :: tl ->
149                let cic_name = cic_name_of_name name in
150                let cic_body = do_branch' (cic_name :: context) tl in
151                let typ =
152                  match typ with
153                  | None -> NCic.Implicit `Type
154                  | Some typ -> aux ~localize loc context typ
155                in
156                NCic.Lambda (cic_name, typ, cic_body)
157          in
158           do_branch' context args
159         in
160         if create_dummy_ids then
161          let branches =
162           List.map
163            (function
164                Ast.Wildcard,term -> ("wildcard",None,[]), term
165              | Ast.Pattern _,_ ->
166                 raise (DisambiguateTypes.Invalid_choice 
167                  (lazy (loc, "Syntax error: the left hand side of a "^
168                    "branch pattern must be \"_\"")))
169            ) branches in
170          let indtype_ref =
171           NReference.reference_of_string "cic:/fake_indty.ind(0,0,0)"
172          in
173           NCic.Match (indtype_ref, cic_outtype, cic_term,
174            (List.map do_branch branches))
175         else
176          let indtype_ref =
177           match indty_ident with
178           | Some (indty_ident, _) ->
179              (match Disambiguate.resolve ~env ~mk_choice 
180                 (Id indty_ident) (`Args []) with
181               | NCic.Const (NReference.Ref (_,NReference.Ind _) as r) -> r
182               | NCic.Implicit _ ->
183                  raise (Disambiguate.Try_again 
184                   (lazy "The type of the term to be matched is still unknown"))
185               | t ->
186                 raise (DisambiguateTypes.Invalid_choice 
187                   (lazy (loc,"The type of the term to be matched "^
188                           "is not (co)inductive: " ^ status#ppterm 
189                           ~metasenv:[] ~subst:[] ~context:[] t))))
190           | None ->
191               let rec fst_constructor =
192                 function
193                    (Ast.Pattern (head, _, _), _) :: _ -> head
194                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
195                  | [] -> raise (Invalid_choice (lazy (loc,"The type "^
196                      "of the term to be matched cannot be determined "^
197                      "because it is an inductive type without constructors "^
198                      "or because all patterns use wildcards")))
199               in
200 (*
201               DisambiguateTypes.Environment.iter
202                   (fun k v ->
203                       prerr_endline
204                         (DisambiguateTypes.string_of_domain_item k ^ " => " ^
205                         description_of_alias v)) env; 
206 *)
207               (match Disambiguate.resolve ~env ~mk_choice
208                 (Id (fst_constructor branches)) (`Args []) with
209               | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> 
210                    let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
211                    NReference.mk_indty b r
212               | NCic.Implicit _ ->
213                  raise (Disambiguate.Try_again 
214                   (lazy "The type of the term to be matched is still unknown"))
215               | t ->
216                 raise (DisambiguateTypes.Invalid_choice 
217                   (lazy (loc, 
218                   "The type of the term to be matched is not (co)inductive: " 
219                   ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
220          in
221          let _,leftsno,itl,_,indtyp_no =
222           NCicEnvironment.get_checked_indtys status indtype_ref in
223          let _,_,_,cl =
224           try
225            List.nth itl indtyp_no
226           with _ -> assert false in
227          let rec count_prod t =
228                  match NCicReduction.whd status ~subst:[] [] t with
229                NCic.Prod (_, _, t) -> 1 + (count_prod t)
230              | _ -> 0 
231          in 
232          let rec sort branches cl =
233           match cl with
234              [] ->
235               let rec analyze unused unrecognized useless =
236                function
237                   [] ->
238                    if unrecognized != [] then
239                     raise (DisambiguateTypes.Invalid_choice
240                      (lazy
241                        (loc,"Unrecognized constructors: " ^
242                         String.concat " " unrecognized)))
243                    else if useless > 0 then
244                     raise (DisambiguateTypes.Invalid_choice
245                      (lazy
246                        (loc,"The last " ^ string_of_int useless ^
247                         "case" ^ if useless > 1 then "s are" else " is" ^
248                         " unused")))
249                    else
250                     []
251                 | (Ast.Wildcard,_)::tl when not unused ->
252                     analyze true unrecognized useless tl
253                 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
254                     analyze unused (head::unrecognized) useless tl
255                 | _::tl -> analyze unused unrecognized (useless + 1) tl
256               in
257                analyze false [] 0 branches
258            | (_,name,ty)::cltl ->
259               let rec find_and_remove =
260                function
261                   [] ->
262                    raise
263                     (DisambiguateTypes.Invalid_choice
264                      (lazy (loc, "Missing case: " ^ name)))
265                 | ((Ast.Wildcard, _) as branch :: _) as branches ->
266                     branch, branches
267                 | (Ast.Pattern (name',_,_),_) as branch :: tl
268                    when name = name' ->
269                     branch,tl
270                 | branch::tl ->
271                    let found,rest = find_and_remove tl in
272                     found, branch::rest
273               in
274                let branch,tl = find_and_remove branches in
275                match branch with
276                   Ast.Pattern (name,y,args),term ->
277                    if List.length args = count_prod ty - leftsno then
278                     ((name,y,args),term)::sort tl cltl
279                    else
280                     raise
281                      (DisambiguateTypes.Invalid_choice
282                       (lazy (loc,"Wrong number of arguments for " ^ name)))
283                 | Ast.Wildcard,term ->
284                    let rec mk_lambdas =
285                     function
286                        0 -> term
287                      | n ->
288                         NotationPt.Binder
289                          (`Lambda, (NotationPt.Ident ("_", None), None),
290                            mk_lambdas (n - 1))
291                    in
292                     (("wildcard",None,[]),
293                      mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
294          in
295           let branches = sort branches cl in
296            NCic.Match (indtype_ref, cic_outtype, cic_term,
297             (List.map do_branch branches))
298     | NotationPt.Cast (t1, t2) ->
299         let cic_t1 = aux ~localize loc context t1 in
300         let cic_t2 = aux ~localize loc context t2 in
301         NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1)
302     | NotationPt.LetIn ((name, typ), def, body) ->
303         let cic_def = aux ~localize loc context def in
304         let cic_name = cic_name_of_name name in
305         let cic_typ =
306           match typ with
307           | None -> NCic.Implicit `Type
308           | Some t -> aux ~localize loc context t
309         in
310         let cic_body = aux ~localize loc (cic_name :: context) body in
311         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
312     | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
313     | NotationPt.Ident _
314     | NotationPt.Uri _
315     | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
316     | NotationPt.Ident (name, subst) ->
317        assert (subst = None);
318        (try
319              NCic.Rel (find_in_context name context)
320        with Not_found -> 
321          try NCic.Const (List.assoc name obj_context)
322          with Not_found ->
323             Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
324     | NotationPt.Uri (uri, subst) ->
325        assert (subst = None);
326        (try
327          NCic.Const (NReference.reference_of_string uri)
328         with NRef.IllFormedReference _ ->
329          NotationPt.fail loc "Ill formed reference")
330     | NotationPt.NRef nref -> NCic.Const nref
331     | NotationPt.NCic t ->  t
332     | NotationPt.Implicit `Vector -> NCic.Implicit `Vector
333     | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
334     | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
335     | NotationPt.UserInput -> NCic.Implicit `Hole
336     | NotationPt.Num (num, i) -> 
337         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
338     | NotationPt.Meta (index, subst) ->
339         let cic_subst =
340          List.map
341           (function None -> assert false| Some t -> aux ~localize loc context t)
342           subst
343         in
344          NCic.Meta (index, (0, NCic.Ctx cic_subst))
345     | NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
346     | NotationPt.Sort `Set -> NCic.Sort (NCic.Type
347        [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
348     | NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
349        [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
350     | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
351        [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
352     | NotationPt.Symbol (symbol, instance) ->
353         Disambiguate.resolve ~env ~mk_choice 
354          (Symbol (symbol, instance)) (`Args [])
355     | NotationPt.Variable _
356     | NotationPt.Magic _
357     | NotationPt.Layout _
358     | NotationPt.Literal _ -> assert false (* god bless Bologna *)
359   and aux_option ~localize loc context annotation = function
360     | None -> NCic.Implicit annotation
361     | Some (NotationPt.AttributedTerm (`Loc loc, term)) ->
362         let res = aux_option ~localize loc context annotation (Some term) in
363         if localize then 
364           NCicUntrusted.NCicHash.add localization_tbl res loc;
365         res
366     | Some (NotationPt.AttributedTerm (_, term)) ->
367         aux_option ~localize loc context annotation (Some term)
368     | Some NotationPt.Implicit `JustOne -> NCic.Implicit annotation
369     | Some NotationPt.Implicit `Vector -> NCic.Implicit `Vector
370     | Some term -> aux ~localize loc context term
371   in
372    (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
373    (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
374 ;;
375
376 let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
377  ~is_path ast ~obj_context ~localization_tbl ~mk_choice
378 =
379   let context = List.map fst context in
380   fst 
381     (interpretate_term_and_interpretate_term_option status
382       ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
383       ~localization_tbl)
384     ~context ast
385 ;;
386
387 let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri
388  ~is_path ~localization_tbl ~mk_choice ~obj_context
389 =
390   let context = List.map fst context in
391   snd 
392     (interpretate_term_and_interpretate_term_option status
393       ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
394       ~localization_tbl)
395     ~context 
396 ;;
397
398 let disambiguate_path status path =
399   let localization_tbl = NCicUntrusted.NCicHash.create 23 in
400   fst
401     (interpretate_term_and_interpretate_term_option status
402     ~obj_context:[] ~mk_choice:(fun _ -> assert false)
403     ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
404     ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
405 ;;
406
407 let ncic_name_of_ident = function
408   | Ast.Ident (name, None) -> name
409   | _ -> assert false
410 ;;
411
412 let interpretate_obj status
413 (*      ?(create_dummy_ids=false)  *)
414      ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice 
415 =
416  assert (context = []);
417  assert (is_path = false);
418  let interpretate_term ~obj_context =
419   interpretate_term ~mk_choice ~localization_tbl ~obj_context in
420  let interpretate_term_option ~obj_context =
421    interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
422  let uri = match uri with | None -> assert false | Some u -> u in
423  match obj with
424  | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
425      let ty' = 
426        interpretate_term status
427          ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
428      in
429      let height = (* XXX calculate *) 0 in
430      uri, height, [], [], 
431      (match bo,flavour with
432       | None,`Axiom -> 
433           let attrs = `Provided, flavour, pragma in
434           NCic.Constant ([],name,None,ty',attrs)
435       | Some _,`Axiom -> assert false
436       | None,_ ->
437           let attrs = `Provided, flavour, pragma in
438           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
439       | Some bo,_ ->
440         (match bo with
441          | NotationPt.LetRec (kind, defs, _) ->
442              let inductive = kind = `Inductive in
443              let _,obj_context =
444                List.fold_left
445                  (fun (i,acc) (_,(name,_),_,k) -> 
446                   (i+1, 
447                     (ncic_name_of_ident name, NReference.reference_of_spec uri 
448                      (if inductive then NReference.Fix (i,k,0)
449                       else NReference.CoFix i)) :: acc))
450                  (0,[]) defs
451              in
452              let inductiveFuns =
453                List.map
454                  (fun (params, (name, typ), body, decr_idx) ->
455                    let add_binders kind t =
456                     List.fold_right
457                      (fun var t -> 
458                         NotationPt.Binder (kind, var, t)) params t
459                    in
460                    let cic_body =
461                      interpretate_term status
462                        ~obj_context ~context ~env ~uri:None ~is_path:false
463                        (add_binders `Lambda body) 
464                    in
465                    let cic_type =
466                      interpretate_term_option status
467                        ~obj_context:[]
468                        ~context ~env ~uri:None ~is_path:false `Type
469                        (HExtlib.map_option (add_binders `Pi) typ)
470                    in
471                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
472                  defs
473              in
474              let attrs = `Provided, flavour, pragma in
475              NCic.Fixpoint (inductive,inductiveFuns,attrs)
476          | bo -> 
477              let bo = 
478                interpretate_term status
479                 ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
480              in
481              let attrs = `Provided, flavour, pragma in
482              NCic.Constant ([],name,Some bo,ty',attrs)))
483  | NotationPt.Inductive (params,tyl) ->
484     let context,params =
485      let context,res =
486       List.fold_left
487        (fun (context,res) (name,t) ->
488          let t =
489           match t with
490              None -> NotationPt.Implicit `JustOne
491            | Some t -> t in
492          let name = cic_name_of_name name in
493          let t =
494           interpretate_term status ~obj_context:[] ~context ~env ~uri:None
495            ~is_path:false t
496          in
497           (name,NCic.Decl t)::context,(name,t)::res
498        ) ([],[]) params
499      in
500       context,List.rev res in
501     let add_params =
502      List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
503     let leftno = List.length params in
504     let _,inductive,_,_ = try List.hd tyl with Failure _ -> assert false in
505     let obj_context =
506      snd (
507       List.fold_left
508        (fun (i,res) (name,_,_,_) ->
509          let nref =
510           NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
511          in
512           i+1,(name,nref)::res)
513        (0,[]) tyl) in
514     let tyl =
515      List.map
516       (fun (name,_,ty,cl) ->
517         let ty' =
518          add_params
519          (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
520            ~is_path:false ty) in
521         let cl' =
522          List.map
523           (fun (name,ty) ->
524             let ty' =
525              add_params
526               (interpretate_term status ~obj_context ~context ~env ~uri:None
527                 ~is_path:false ty) in
528             let relevance = [] in
529              relevance,name,ty'
530           ) cl in
531         let relevance = [] in
532          relevance,name,ty',cl'
533       ) tyl
534     in
535      let height = (* XXX calculate *) 0 in
536      let attrs = `Provided, `Regular in
537      uri, height, [], [], 
538      NCic.Inductive (inductive,leftno,tyl,attrs)
539  | NotationPt.Record (params,name,ty,fields) ->
540     let context,params =
541      let context,res =
542       List.fold_left
543        (fun (context,res) (name,t) ->
544          let t =
545           match t with
546              None -> NotationPt.Implicit `JustOne
547            | Some t -> t in
548          let name = cic_name_of_name name in
549          let t =
550           interpretate_term status ~obj_context:[] ~context ~env ~uri:None
551            ~is_path:false t
552          in
553           (name,NCic.Decl t)::context,(name,t)::res
554        ) ([],[]) params
555      in
556       context,List.rev res in
557     let add_params =
558      List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
559     let leftno = List.length params in
560     let ty' =
561      add_params
562       (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
563         ~is_path:false ty) in
564     let nref =
565      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
566     let obj_context = [name,nref] in
567     let fields' =
568      snd (
569       List.fold_left
570        (fun (context,res) (name,ty,_coercion,_arity) ->
571          let ty =
572           interpretate_term status ~obj_context ~context ~env ~uri:None
573            ~is_path:false ty in
574          let context' = (name,NCic.Decl ty)::context in
575           context',(name,ty)::res
576        ) (context,[]) fields) in
577     let concl =
578      let mutind = NCic.Const nref in
579      if params = [] then mutind
580      else
581       NCic.Appl
582        (mutind::mk_rels (List.length params) (List.length fields)) in
583     let con =
584      List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
585     let con' = add_params con in
586     let relevance = [] in
587     let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
588     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
589      let height = (* XXX calculate *) 0 in
590      let attrs = `Provided, `Record field_names in
591      uri, height, [], [], 
592      NCic.Inductive (true,leftno,tyl,attrs)
593 ;;
594
595 let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
596  ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
597  ~aliases ~universe ~lookup_in_library (text,prefix_len,term) 
598 =
599   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
600    let res,b =
601     MultiPassDisambiguator.disambiguate_thing
602      ~freshen_thing:NotationUtil.freshen_term
603      ~context ~metasenv ~initial_ugraph:() ~aliases
604      ~mk_implicit ~description_of_alias ~fix_instance
605      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
606      ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status)
607      ~passes:(MultiPassDisambiguator.passes ())
608      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
609      ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
610      ~refine_thing:(refine_term status) (text,prefix_len,term)
611      ~mk_localization_tbl ~expty ~subst
612    in
613     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
614 ;;
615
616 let disambiguate_obj (status: #NCicCoercion.status)
617    ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
618    ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) 
619  =
620   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
621    let res,b =
622     MultiPassDisambiguator.disambiguate_thing
623      ~freshen_thing:NotationUtil.freshen_obj
624      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
625      ~mk_implicit ~description_of_alias ~fix_instance
626      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
627      ~universe 
628      ~uri:(Some uri)
629      ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
630      ~passes:(MultiPassDisambiguator.passes ())
631      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
632      ~interpretate_thing:(interpretate_obj status ~mk_choice)
633      ~refine_thing:(refine_obj status) 
634      (text,prefix_len,obj)
635      ~mk_localization_tbl ~expty:None
636    in
637     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
638 ;;
639 (*
640 let _ = 
641 let mk_type n = 
642   if n = 0 then
643      [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
644   else
645      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
646 in
647 let mk_cprop n = 
648   if n = 0 then 
649     [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
650   else
651     [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
652 in
653          NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1);
654          NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1);
655          NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1);
656          NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
657          NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
658          NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
659
660          NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
661          NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
662          NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
663          NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
664          NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
665          NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
666
667          NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
668          NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
669          NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
670          NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
671          NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
672          NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
673
674          NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
675          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
676
677 ;;
678 *)
679