]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_disambiguation/nCicDisambiguate.ml
missing notation file
[helm.git] / matitaB / 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,_) ->  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 ~universe ~uri ~is_path
108   ~localization_tbl 
109 =
110   let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term
111   DisambiguateTypes.codomain_item) in
112   (* create_dummy_ids shouldbe used only for interpretating patterns *)
113   assert (uri = None);
114
115   let rec aux ~localize loc context = function
116     | NotationPt.AttributedTerm (`Loc loc, term) ->
117         let res = aux ~localize loc context term in
118         if localize then 
119          NCicUntrusted.NCicHash.add localization_tbl res loc;
120        res
121     | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
122     | NotationPt.Appl (NotationPt.Appl inner :: args) ->
123         aux ~localize loc context (NotationPt.Appl (inner @ args))
124     | NotationPt.Appl 
125         (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
126         aux ~localize loc context 
127           (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
128     | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) 
129     | NotationPt.Appl
130       (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) ->
131         NCic.Implicit `Term
132     | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args) 
133     | NotationPt.Appl (NotationPt.AttributedTerm 
134       (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) ->
135         let cic_args = List.map (aux ~localize loc context) args in
136         (try
137         prerr_endline ("interpr Appl/Sym: " ^ symb);
138         let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in
139         Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*))
140           interpr (`Args cic_args)
141         with Failure err -> 
142           prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err); 
143           assert false)
144     | NotationPt.Appl terms ->
145        NCic.Appl (List.map (aux ~localize loc context) terms)
146     | NotationPt.Binder (binder_kind, (var, typ), body) ->
147         let cic_type = aux_option ~localize loc context `Type typ in
148         let cic_name = cic_name_of_name var  in
149         let cic_body = aux ~localize loc (cic_name :: context) body in
150         (match binder_kind with
151         | `Lambda -> NCic.Lambda (cic_name, cic_type, cic_body)
152         | `Pi
153         | `Forall -> NCic.Prod (cic_name, cic_type, cic_body)
154         | `Exists -> assert false)
155             (*Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", None))
156               (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])*)
157     | NotationPt.Case (term, indty_ident, outtype, branches) ->
158         let cic_term = aux ~localize loc context term in
159         let cic_outtype = aux_option ~localize loc context `Term outtype in
160         let do_branch ((_, _, args), term) =
161          let rec do_branch' context = function
162            | [] -> aux ~localize loc context term
163            | (name, typ) :: tl ->
164                let cic_name = cic_name_of_name name in
165                let cic_body = do_branch' (cic_name :: context) tl in
166                let typ =
167                  match typ with
168                  | None -> NCic.Implicit `Type
169                  | Some typ -> aux ~localize loc context typ
170                in
171                NCic.Lambda (cic_name, typ, cic_body)
172          in
173           do_branch' context args
174         in
175         if create_dummy_ids then
176          let branches =
177           List.map
178            (function
179                Ast.Wildcard,term -> ("wildcard",None,[]), term
180              | Ast.Pattern _,_ ->
181                 raise (DisambiguateTypes.Invalid_choice 
182                  (lazy (loc, "Syntax error: the left hand side of a "^
183                    "branch pattern must be \"_\"")))
184            ) branches
185          in
186          (*
187           NCic.MutCase (ref, cic_outtype, cic_term,
188             (List.map do_branch branches))
189           *) ignore branches; assert false (* patterns not implemented yet *)
190         else
191          let indtype_ref =
192           match indty_ident with
193           | Some (_,Some r) -> r
194           | Some (_, None) ->
195               raise (Disambiguate.Try_again 
196                 (lazy "The type of the term to be matched is still unknown"))
197           | None ->
198               let rec fst_constructor concrete_pat_found =
199                 function
200                  | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl
201                  | (Ast.Pattern (head, Some href, _), _) :: _ -> 
202                      head, href 
203                  | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl
204                  | [] when concrete_pat_found -> raise (Disambiguate.Try_again 
205                    (lazy "The type of the term to be matched is still unknown"))
206                  | [] -> raise (Invalid_choice (lazy (loc,"The type "^
207                      "of the term to be matched cannot be determined "^
208                      "because it is an inductive type without constructors "^
209                      "or because all patterns use wildcards")))
210               in
211 (*
212               DisambiguateTypes.Environment.iter
213                   (fun k v ->
214                       prerr_endline
215                         (DisambiguateTypes.string_of_domain_item k ^ " => " ^
216                         description_of_alias v)) env; 
217 *)
218               let kname,href = fst_constructor false branches in
219               let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href
220               in
221               NReference.mk_indty b href
222          in
223          let _,leftsno,itl,_,indtyp_no =
224           NCicEnvironment.get_checked_indtys status indtype_ref in
225          let _,_,_,cl =
226           try
227            List.nth itl indtyp_no
228           with _ -> assert false in
229          let rec count_prod t =
230                  match NCicReduction.whd status ~subst:[] [] t with
231                NCic.Prod (_, _, t) -> 1 + (count_prod t)
232              | _ -> 0 
233          in 
234          let rec sort cno branches cl =
235           match cl with
236              [] ->
237               let rec analyze unused unrecognized useless =
238                function
239                   [] ->
240                    if unrecognized != [] then
241                     raise (DisambiguateTypes.Invalid_choice
242                      (lazy
243                        (loc,"Unrecognized constructors: " ^
244                         String.concat " " unrecognized)))
245                    else if useless > 0 then
246                     raise (DisambiguateTypes.Invalid_choice
247                      (lazy
248                        (loc,"The last " ^ string_of_int useless ^
249                         "case" ^ if useless > 1 then "s are" else " is" ^
250                         " unused")))
251                    else
252                     []
253                 | (Ast.Wildcard,_)::tl when not unused ->
254                     analyze true unrecognized useless tl
255                 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
256                     analyze unused (head::unrecognized) useless tl
257                 | _::tl -> analyze unused unrecognized (useless + 1) tl
258               in
259                analyze false [] 0 branches
260            | (_,name,ty)::cltl ->
261               let rec find_and_remove =
262                function
263                   [] ->
264                    raise
265                     (DisambiguateTypes.Invalid_choice
266                      (lazy (loc, "Missing case: " ^ name)))
267                 | ((Ast.Wildcard, _) as branch :: _) as branches ->
268                     branch, branches
269                 | (Ast.Pattern (name',Some href,_),_) as branch :: tl ->
270                   prerr_endline 
271                    (Printf.sprintf "analysis of %s and %s" name name');
272                   (match href with
273                    | NReference.Ref (curi, (NReference.Con (n,cno',_))) ->
274                      (* check che la curi corrisponda alla uri del tipo induttivo *)
275                       let this_indty = NReference.mk_indty true href in
276                       if indtype_ref <> this_indty then
277                         (prerr_endline "fail1";
278                         raise (DisambiguateTypes.Invalid_choice
279                           (lazy (loc, Printf.sprintf 
280                             "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s."
281                             (NReference.string_of_reference indtype_ref)
282                             (NReference.string_of_reference href)
283                             (NReference.string_of_reference this_indty)))))
284                       else
285                               if cno = cno' then (prerr_endline "ok";branch, tl)
286                         else
287                               (prerr_endline (Printf.sprintf "skip %d %d" cno cno');
288                               let found,rest = find_and_remove tl in
289                           found, branch::rest)
290                    | _ ->
291                      (prerr_endline "fail2";
292                      raise
293                       (DisambiguateTypes.Invalid_choice
294                        (lazy (loc,"Malformed pattern: found " ^ 
295                                   (NReference.string_of_reference href) ^
296                                   " which is not a type constructor.")))))
297                 | (Ast.Pattern (name',_,_),_) as branch :: tl
298                    when name = name' ->
299                     branch,tl
300                 | branch::tl ->
301                    let found,rest = find_and_remove tl in
302                     found, branch::rest
303               in
304                let branch,tl = find_and_remove branches in
305                match branch with
306                   Ast.Pattern (name,y,args),term ->
307                    if List.length args = count_prod ty - leftsno then
308                     ((name,y,args),term)::sort (cno+1) tl cltl
309                    else
310                     raise
311                      (DisambiguateTypes.Invalid_choice
312                       (lazy (loc,"Wrong number of arguments for " ^ name)))
313                 | Ast.Wildcard,term ->
314                    let rec mk_lambdas =
315                     function
316                        0 -> term
317                      | n ->
318                         NotationPt.Binder
319                          (`Lambda, (NotationPt.Ident ("_", `Ambiguous), None),
320                            mk_lambdas (n - 1))
321                    in
322                     (("wildcard",None,[]),
323                      mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl
324          in
325           let branches = sort 1 branches cl in
326            NCic.Match (indtype_ref, cic_outtype, cic_term,
327             (List.map do_branch branches))
328     | NotationPt.Cast (t1, t2) ->
329         let cic_t1 = aux ~localize loc context t1 in
330         let cic_t2 = aux ~localize loc context t2 in
331         NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1)
332     | NotationPt.LetIn ((name, typ), def, body) ->
333         let cic_def = aux ~localize loc context def in
334         let cic_name = cic_name_of_name name in
335         let cic_typ =
336           match typ with
337           | None -> NCic.Implicit `Type
338           | Some t -> aux ~localize loc context t
339         in
340         let cic_body = aux ~localize loc (cic_name :: context) body in
341         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
342     | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
343     | NotationPt.Ident _
344     | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
345     | NotationPt.Ident (name, `Rel) ->
346         (try NCic.Rel (find_in_context name context)
347         with Not_found -> 
348          (try NCic.Const (List.assoc name obj_context)
349           with Not_found -> assert false)) (* bug in initialize_ast *)
350     | NotationPt.Ident (name, `Ambiguous) ->
351          (try NCic.Const (List.assoc name obj_context)
352          with Not_found -> NCic.Implicit `Closed)
353             (* Disambiguate.resolve ~env ~mk_choice (Id (name,None)) (`Args [])) *)
354     | NotationPt.Ident (name, `Uri uri) ->
355        (try
356          NCic.Const (NReference.reference_of_string uri)
357         with NRef.IllFormedReference _ ->
358          NotationPt.fail loc "Ill formed reference")
359     | NotationPt.NRef nref -> NCic.Const nref
360     | NotationPt.NCic t ->  t
361     | NotationPt.Implicit `Vector -> NCic.Implicit `Vector
362     | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
363     | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
364     | NotationPt.UserInput -> NCic.Implicit `Hole
365     | NotationPt.Num (num, i) ->
366         let i = HExtlib.map_option 
367           (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in
368         Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num)
369     | NotationPt.Meta (index, subst) ->
370         let cic_subst =
371          List.map
372           (function None -> assert false| Some t -> aux ~localize loc context t)
373           subst
374         in
375          NCic.Meta (index, (0, NCic.Ctx cic_subst))
376     | NotationPt.Sort `Prop -> NCic.Sort NCic.Prop
377     | NotationPt.Sort `Set -> NCic.Sort (NCic.Type
378        [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
379     | NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
380        [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
381     | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
382        [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
383     | NotationPt.Symbol (symbol, instance) ->
384         let instance = HExtlib.map_option 
385            (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc))
386            instance
387         in
388         Disambiguate.resolve ~env ~universe ~mk_choice 
389          (loc (*,Symbol symbol*)) instance (`Args [])
390     | NotationPt.Variable _
391     | NotationPt.Magic _
392     | NotationPt.Layout _
393     | NotationPt.Literal _ -> assert false (* god bless Bologna *)
394   and aux_option ~localize loc context annotation = function
395     | None -> NCic.Implicit annotation
396     | Some (NotationPt.AttributedTerm (`Loc loc, term)) ->
397         let res = aux_option ~localize loc context annotation (Some term) in
398         if localize then 
399           NCicUntrusted.NCicHash.add localization_tbl res loc;
400         res
401     | Some (NotationPt.AttributedTerm (_, term)) ->
402         aux_option ~localize loc context annotation (Some term)
403     | Some NotationPt.Implicit `JustOne -> NCic.Implicit annotation
404     | Some NotationPt.Implicit `Vector -> NCic.Implicit `Vector
405     | Some term -> aux ~localize loc context term
406   in
407    (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
408    (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
409 ;;
410
411 let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri
412  ~is_path ast ~obj_context ~localization_tbl ~mk_choice
413 =
414   let context = List.map fst context in
415   fst 
416     (interpretate_term_and_interpretate_term_option status
417       ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
418       ~localization_tbl)
419     ~context ast
420 ;;
421
422 let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env
423   ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context
424 =
425   let context = List.map fst context in
426   snd 
427     (interpretate_term_and_interpretate_term_option status
428       ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
429       ~localization_tbl)
430     ~context 
431 ;;
432
433 let disambiguate_path status path =
434   let localization_tbl = NCicUntrusted.NCicHash.create 23 in
435   fst
436     (interpretate_term_and_interpretate_term_option status
437     ~obj_context:[] ~mk_choice:(fun _ -> assert false)
438     ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty
439     ~universe:DisambiguateTypes.Environment.empty
440     ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
441 ;;
442
443 let ncic_name_of_ident = function
444   | Ast.Ident (name,_) -> name
445   | _ -> assert false
446 ;;
447
448 let interpretate_obj status
449 (*      ?(create_dummy_ids=false)  *)
450      ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice 
451 =
452  assert (context = []);
453  assert (is_path = false);
454  let interpretate_term ~obj_context =
455   interpretate_term ~mk_choice ~localization_tbl ~obj_context in
456  let interpretate_term_option ~obj_context =
457    interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
458  let uri = match uri with | None -> assert false | Some u -> u in
459  match obj with
460  | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
461      let ty' = 
462        interpretate_term status
463          ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty 
464      in
465      let height = (* XXX calculate *) 0 in
466      uri, height, [], [], 
467      (match bo,flavour with
468       | None,`Axiom -> 
469           let attrs = `Provided, flavour, pragma in
470           NCic.Constant ([],name,None,ty',attrs)
471       | Some _,`Axiom -> assert false
472       | None,_ ->
473           let attrs = `Provided, flavour, pragma in
474           NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
475       | Some bo,_ ->
476         (match bo with
477          | NotationPt.LetRec (kind, defs, _) ->
478              let inductive = kind = `Inductive in
479              let _,obj_context =
480                List.fold_left
481                  (fun (i,acc) (_,(name,_),_,k) -> 
482                   (i+1, 
483                     (ncic_name_of_ident name, NReference.reference_of_spec uri 
484                      (if inductive then NReference.Fix (i,k,0)
485                       else NReference.CoFix i)) :: acc))
486                  (0,[]) defs
487              in
488              let inductiveFuns =
489                List.map
490                  (fun (params, (name, typ), body, decr_idx) ->
491                    let add_binders kind t =
492                     List.fold_right
493                      (fun var t -> 
494                         NotationPt.Binder (kind, var, t)) params t
495                    in
496                    let cic_body =
497                      interpretate_term status
498                        ~obj_context ~context ~env ~universe ~uri:None ~is_path:false
499                        (add_binders `Lambda body) 
500                    in
501                    let cic_type =
502                      interpretate_term_option status
503                        ~obj_context:[]
504                        ~context ~env ~universe ~uri:None ~is_path:false `Type
505                        (HExtlib.map_option (add_binders `Pi) typ)
506                    in
507                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
508                  defs
509              in
510              let attrs = `Provided, flavour, pragma in
511              NCic.Fixpoint (inductive,inductiveFuns,attrs)
512          | bo -> 
513              let bo = 
514                interpretate_term status
515                 ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo
516              in
517              let attrs = `Provided, flavour, pragma in
518              NCic.Constant ([],name,Some bo,ty',attrs)))
519  | NotationPt.Inductive (params,tyl) ->
520     let context,params =
521      let context,res =
522       List.fold_left
523        (fun (context,res) (name,t) ->
524          let t =
525           match t with
526              None -> NotationPt.Implicit `JustOne
527            | Some t -> t in
528          let name = cic_name_of_name name in
529          let t =
530           interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
531            ~is_path:false t
532          in
533           (name,NCic.Decl t)::context,(name,t)::res
534        ) ([],[]) params
535      in
536       context,List.rev res in
537     let add_params =
538      List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
539     let leftno = List.length params in
540     let _,inductive,_,_ = try List.hd tyl with Failure _ -> assert false in
541     let obj_context =
542      snd (
543       List.fold_left
544        (fun (i,res) (name,_,_,_) ->
545          let nref =
546           NReference.reference_of_spec uri (NReference.Ind (inductive,i,leftno))
547          in
548           i+1,(name,nref)::res)
549        (0,[]) tyl) in
550     let tyl =
551      List.map
552       (fun (name,_,ty,cl) ->
553         let ty' =
554          add_params
555          (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
556            ~is_path:false ty) in
557         let cl' =
558          List.map
559           (fun (name,ty) ->
560             let ty' =
561              add_params
562               (interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
563                 ~is_path:false ty) in
564             let relevance = [] in
565              relevance,name,ty'
566           ) cl in
567         let relevance = [] in
568          relevance,name,ty',cl'
569       ) tyl
570     in
571      let height = (* XXX calculate *) 0 in
572      let attrs = `Provided, `Regular in
573      uri, height, [], [], 
574      NCic.Inductive (inductive,leftno,tyl,attrs)
575  | NotationPt.Record (params,name,ty,fields) ->
576     let context,params =
577      let context,res =
578       List.fold_left
579        (fun (context,res) (name,t) ->
580          let t =
581           match t with
582              None -> NotationPt.Implicit `JustOne
583            | Some t -> t in
584          let name = cic_name_of_name name in
585          let t =
586           interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
587            ~is_path:false t
588          in
589           (name,NCic.Decl t)::context,(name,t)::res
590        ) ([],[]) params
591      in
592       context,List.rev res in
593     let add_params =
594      List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in
595     let leftno = List.length params in
596     let ty' =
597      add_params
598       (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
599         ~is_path:false ty) in
600     let nref =
601      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
602     let obj_context = [name,nref] in
603     let fields' =
604      snd (
605       List.fold_left
606        (fun (context,res) (name,ty,_coercion,_arity) ->
607          let ty =
608           interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
609            ~is_path:false ty in
610          let context' = (name,NCic.Decl ty)::context in
611           context',(name,ty)::res
612        ) (context,[]) fields) in
613     let concl =
614      let mutind = NCic.Const nref in
615      if params = [] then mutind
616      else
617       NCic.Appl
618        (mutind::mk_rels (List.length params) (List.length fields)) in
619     let con =
620      List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in
621     let con' = add_params con in
622     let relevance = [] in
623     let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
624     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
625      let height = (* XXX calculate *) 0 in
626      let attrs = `Provided, `Record field_names in
627      uri, height, [], [], 
628      NCic.Inductive (true,leftno,tyl,attrs)
629 ;;
630
631 let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names t =
632   (* ast_of_alias_spec is duplicate in Disambiguate *)
633   let ast_of_alias_spec t alias = match (t,alias) with
634     | _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri) 
635     | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
636     | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
637     | _ -> assert false
638   in
639   let lookup_choices =
640      fun item ->
641       (*match universe with
642       | None -> 
643           lookup_in_library 
644             interactive_user_uri_choice 
645             input_or_locate_uri item
646       | Some e ->
647           (try Environment.find item e
648           with Not_found -> [])
649 *)
650           (try 
651              let res = Environment.find item universe in
652              let id = match item with
653                | DisambiguateTypes.Id id -> id
654                | DisambiguateTypes.Symbol _ -> "SYM"
655                | DisambiguateTypes.Num _ -> "NUM"
656              in
657              debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
658                (List.length res)));
659              res
660           with Not_found -> [])
661    in
662   let init = initialize_ast ~universe ~lookup_in_library in
663   let init_var ~local_names (n,ty) = 
664           (n,HExtlib.map_option (init ~local_names) ty)
665   in
666   let init_vars ~local_names vars =
667   (* 
668     List.fold_right (fun (n,ty) (nacc,tyacc) ->
669       (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
670     ) vars (local_names,[])
671   *)
672     let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
673       (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
674       ) (local_names,[]) vars
675     in a, List.rev b
676   in
677   let init_pattern ~local_names = function
678     | Ast.Wildcard as t -> local_names,t
679     | Ast.Pattern (c,uri,vars) -> 
680         let ln',vars' = init_vars ~local_names vars in
681         let uri' = match uri with
682           | Some _ -> uri
683           | None -> 
684              let choices = lookup_choices (DisambiguateTypes.Id c) in
685              if List.length choices <> 1 then None
686              else (match (List.hd choices) with
687              | GrafiteAst.Ident_alias (_,u) -> 
688                  Some (NReference.reference_of_string u)
689              | _ -> assert false)
690         in
691         ln',Ast.Pattern (c,uri',vars')
692   in
693   let mk_alias = function
694     | Ast.Ident (id,_) -> DisambiguateTypes.Id id
695     | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
696     | Ast.Num _ -> DisambiguateTypes.Num
697     | _ -> assert false
698   in
699    match t with
700    | Ast.Ident (id,(`Ambiguous|`Rel))
701        when List.mem id local_names -> Ast.Ident (id,`Rel)
702    | Ast.Ident (id,`Rel) -> init ~local_names (Ast.Ident (id,`Ambiguous))
703    | Ast.Ident (_,`Ambiguous)
704    | Ast.Num (_,None) 
705    | Ast.Symbol (_,None) -> 
706        let choices = lookup_choices (mk_alias t) in
707        if List.length choices <> 1 then t
708        else ast_of_alias_spec t (List.hd choices)
709    | Ast.AttributedTerm (a,u) -> Ast.AttributedTerm (a, init ~local_names u)
710    | Ast.Appl tl -> Ast.Appl (List.map (init ~local_names) tl)
711    | Ast.Binder (k,(n,ty),body) ->
712        let n' = cic_name_of_name n in
713        let ty' = HExtlib.map_option (init ~local_names) ty in
714        let body' = init ~local_names:(n'::local_names) body in
715        Ast.Binder (k,(n,ty'),body')
716    | Ast.Case (t,ity,oty,pl) -> 
717        let t' = init ~local_names t in
718        let oty' = HExtlib.map_option (init ~local_names) oty in
719        let pl' = 
720          List.map (fun (p,u) ->
721            let ns,p' = init_pattern ~local_names p in
722            p',init ~local_names:ns u) pl in
723        let ity' = HExtlib.map_option 
724          (fun (ity_id,href) -> 
725             let href' = match href with
726             | None -> 
727                let choices = lookup_choices (DisambiguateTypes.Id ity_id) in
728                if List.length choices <> 1 then None
729                else (match (List.hd choices) with
730                  | GrafiteAst.Ident_alias (_,u) ->
731                     Some (NReference.reference_of_string u)
732                  | _ -> assert false)
733             | Some _ -> href
734             in (ity_id,href')) ity
735        in Ast.Case (t',ity',oty',pl')
736    | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
737    | Ast.LetIn ((n,ty),u,v) -> 
738        let n' = cic_name_of_name n in
739        let ty' = HExtlib.map_option (init ~local_names) ty in
740        let u' = init ~local_names u in
741        let v' = init ~local_names:(n'::local_names) v in
742        Ast.LetIn ((n,ty'),u',v')
743    | Ast.LetRec (ik,l,t) ->
744        let recfuns = 
745          List.fold_right (fun (_,(n,_),_,_) acc ->
746            cic_name_of_name n::acc) l [] in
747        let l' = List.map (fun (vl,(n,ty),u,m) -> 
748          let ln',vl' = init_vars ~local_names vl in
749          let ty' = HExtlib.map_option (init ~local_names:ln') ty in
750          let ln'' = recfuns@ln' in
751          let u' = init ~local_names:ln'' u in
752          vl',(n,ty'),u',m) l in
753        let t' = init ~local_names:(recfuns@local_names) t in
754        Ast.LetRec (ik,l',t') (* XXX: t??? *)
755    | t -> t
756 ;;
757
758 let initialize_obj ~universe ~lookup_in_library o =
759   let init = initialize_ast ~universe ~lookup_in_library in
760   let init_var ~local_names (n,ty) = 
761           (n,HExtlib.map_option (init ~local_names) ty)
762   in
763   let init_vars ~local_names vars = 
764     let a,b = List.fold_left (fun (nacc,tyacc) (n,ty) ->
765       (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
766       ) (local_names,[]) vars
767     in a, List.rev b
768     (*List.fold_right (fun (n,ty) (nacc,tyacc) ->
769       (cic_name_of_name n::nacc,(init_var ~local_names:nacc (n,ty)::tyacc))
770     ) vars (local_names,[])*)
771   in
772
773   match o with
774   | Ast.Inductive (ls,itl) ->
775       let ln,ls' = init_vars ~local_names:[] ls in
776       let indtys = 
777          List.fold_right 
778            (fun (name,_,_,_) acc -> name::acc) itl [] in
779       let itl' = List.map
780         (fun (name,isind,ty,cl) ->
781            let ty' = init ~local_names:ln ty in
782            let cl' = 
783              List.map (fun (cname,cty) -> 
784                cname, init ~local_names:(indtys@ln) cty) cl
785            in
786            name,isind,ty',cl') itl
787       in
788       Ast.Inductive (ls',itl')
789   | Ast.Theorem (flav,n,ty,bo,p) ->
790       let ty' = init ~local_names:[] ty in
791       let bo' = HExtlib.map_option (init ~local_names:[]) bo in 
792       Ast.Theorem (flav,n,ty',bo',p)
793   | Ast.Record (ls,n,ty,fl) ->
794       let ln,ls' = init_vars ~local_names:[] ls in
795       let ty' = init ~local_names:ln ty in
796       let _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) -> 
797         (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl 
798       in
799       let fl' = List.rev fl' in
800       Ast.Record (ls',n,ty',fl')
801 ;;
802
803 let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
804  ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
805  ~aliases ~universe ~lookup_in_library (text,prefix_len,term) 
806 =
807   let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
808   let local_names = List.map (fun (n,_) -> n) context in
809   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
810     Disambiguate.disambiguate_thing
811      ~context ~metasenv ~subst ~use_coercions:true 
812      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
813      ~initial_ugraph:() ~expty
814      ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
815      ~universe ~lookup_in_library 
816      ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
817      ~domain_of_thing:Disambiguate.domain_of_term
818      ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
819      ~refine_thing:(refine_term status) 
820      (text,prefix_len,
821       (initialize_ast ~universe ~lookup_in_library ~local_names term))
822      ~visit:Disambiguate.bfvisit
823      ~mk_localization_tbl
824 ;;
825
826 let disambiguate_obj (status: #NCicCoercion.status)
827    ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
828    ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) 
829  =
830   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
831   let obj' = initialize_obj ~universe ~lookup_in_library obj in
832     Disambiguate.disambiguate_thing
833      ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true 
834      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
835      ~initial_ugraph:() ~expty:None
836      ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
837      ~universe ~lookup_in_library 
838      ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
839      ~pp_term:(NotationPp.pp_term status)
840      ~domain_of_thing:Disambiguate.domain_of_obj
841      ~interpretate_thing:(interpretate_obj status ~mk_choice)
842      ~refine_thing:(refine_obj status) 
843      (text,prefix_len,obj')
844      ~visit:Disambiguate.bfvisit_obj
845      ~mk_localization_tbl
846 ;;
847 (*
848 let _ = 
849 let mk_type n = 
850   if n = 0 then
851      [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
852   else
853      [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
854 in
855 let mk_cprop n = 
856   if n = 0 then 
857     [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
858   else
859     [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
860 in
861          NCicEnvironment.add_constraint true (mk_type 0) (mk_type 1);
862          NCicEnvironment.add_constraint true (mk_cprop 0) (mk_cprop 1);
863          NCicEnvironment.add_constraint true (mk_cprop 0) (mk_type 1);
864          NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1);
865          NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0);
866          NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0);
867
868          NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2);
869          NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2);
870          NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2);
871          NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2);
872          NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1);
873          NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1);
874
875          NCicEnvironment.add_constraint true (mk_type 2) (mk_type 3);
876          NCicEnvironment.add_constraint true (mk_cprop 2) (mk_cprop 3);
877          NCicEnvironment.add_constraint true (mk_cprop 2) (mk_type 3);
878          NCicEnvironment.add_constraint true (mk_type 2) (mk_cprop 3);
879          NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2);
880          NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2);
881
882          NCicEnvironment.add_constraint false (mk_cprop 3) (mk_type 3);
883          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
884
885 ;;
886 *)
887