]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_unification/cicRefine.ml
The getter maps are now dumped also if matitac exits abruptly.
[helm.git] / helm / ocaml / cic_unification / cicRefine.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 open Printf
27
28 exception RefineFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
31
32 let debug_print = fun _ -> ()
33
34 let fo_unif_subst subst context metasenv t1 t2 ugraph =
35   try
36     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
37   with
38       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
39     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
40 ;;
41
42 let rec split l n =
43  match (l,n) with
44     (l,0) -> ([], l)
45   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
46   | (_,_) -> raise (AssertFailure "split: list too short")
47 ;;
48
49 let rec type_of_constant uri ugraph =
50   let module C = Cic in
51   let module R = CicReduction in
52   let module U = UriManager in
53     (*
54       let obj =
55       try
56       CicEnvironment.get_cooked_obj uri
57       with Not_found -> assert false
58       in
59     *)
60   let obj,u= CicEnvironment.get_obj ugraph uri in
61     match obj with
62         C.Constant (_,_,ty,_,_) -> ty,u
63       | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
64       | _ ->
65           raise
66             (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
67
68 and type_of_variable uri ugraph =
69   let module C = Cic in
70   let module R = CicReduction in
71   let module U = UriManager in
72     (*
73       let obj =
74       try
75       CicEnvironment.get_cooked_obj uri
76       with Not_found -> assert false
77       in
78     *)
79   let obj,u = CicEnvironment.get_obj ugraph uri in
80     match obj with
81         C.Variable (_,_,ty,_,_) -> ty,u
82       |  _ ->
83            raise
84             (RefineFailure
85                ("Unknown variable definition " ^ UriManager.string_of_uri uri))
86
87 and type_of_mutual_inductive_defs uri i ugraph =
88   let module C = Cic in
89   let module R = CicReduction in
90   let module U = UriManager in
91     (*
92       let obj =
93       try
94       CicEnvironment.get_cooked_obj uri
95       with Not_found -> assert false
96       in
97     *)
98   let obj,u = CicEnvironment.get_obj ugraph uri in
99     match obj with
100         C.InductiveDefinition (dl,_,_,_) ->
101           let (_,_,arity,_) = List.nth dl i in
102             arity,u
103       | _ ->
104           raise
105             (RefineFailure
106                ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
107
108 and type_of_mutual_inductive_constr uri i j ugraph =
109   let module C = Cic in
110   let module R = CicReduction in
111   let module U = UriManager in
112     (*
113       let obj =
114       try
115       CicEnvironment.get_cooked_obj uri
116       with Not_found -> assert false
117       in
118     *)
119   let obj,u = CicEnvironment.get_obj ugraph uri in
120     match obj with
121         C.InductiveDefinition (dl,_,_,_) ->
122           let (_,_,_,cl) = List.nth dl i in
123           let (_,ty) = List.nth cl (j-1) in
124             ty,u
125       | _ ->
126           raise
127             (RefineFailure
128                ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
129
130
131 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
132
133 (* the check_branch function checks if a branch of a case is refinable. 
134    It returns a pair (outype_instance,args), a subst and a metasenv.
135    outype_instance is the expected result of applying the case outtype 
136    to args. 
137    The problem is that outype is in general unknown, and we should
138    try to synthesize it from the above information, that is in general
139    a second order unification problem. *)
140  
141 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
142   let module C = Cic in
143     (* let module R = CicMetaSubst in *)
144   let module R = CicReduction in
145     match R.whd ~subst context expectedtype with
146         C.MutInd (_,_,_) ->
147           (n,context,actualtype, [term]), subst, metasenv, ugraph
148       | C.Appl (C.MutInd (_,_,_)::tl) ->
149           let (_,arguments) = split tl left_args_no in
150             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
151       | C.Prod (name,so,de) ->
152           (* we expect that the actual type of the branch has the due 
153              number of Prod *)
154           (match R.whd ~subst context actualtype with
155                C.Prod (name',so',de') ->
156                  let subst, metasenv, ugraph1 = 
157                    fo_unif_subst subst context metasenv so so' ugraph in
158                  let term' =
159                    (match CicSubstitution.lift 1 term with
160                         C.Appl l -> C.Appl (l@[C.Rel 1])
161                       | t -> C.Appl [t ; C.Rel 1]) in
162                    (* we should also check that the name variable is anonymous in
163                       the actual type de' ?? *)
164                    check_branch (n+1) 
165                      ((Some (name,(C.Decl so)))::context) 
166                        metasenv subst left_args_no de' term' de ugraph1
167              | _ -> raise (AssertFailure "Wrong number of arguments"))
168       | _ -> raise (AssertFailure "Prod or MutInd expected")
169
170 and type_of_aux' metasenv context t ugraph =
171   let rec type_of_aux subst metasenv context t ugraph =
172     let module C = Cic in
173     let module S = CicSubstitution in
174     let module U = UriManager in
175       match t with
176           (*    function *)
177           C.Rel n ->
178             (try
179                match List.nth context (n - 1) with
180                    Some (_,C.Decl ty) -> 
181                      t,S.lift n ty,subst,metasenv, ugraph
182                  | Some (_,C.Def (_,Some ty)) -> 
183                      t,S.lift n ty,subst,metasenv, ugraph
184                  | Some (_,C.Def (bo,None)) ->
185                      type_of_aux subst metasenv context (S.lift n bo) ugraph 
186                  | None -> raise (RefineFailure "Rel to hidden hypothesis")
187              with
188                  _ -> raise (RefineFailure "Not a close term")
189             )
190         | C.Var (uri,exp_named_subst) ->
191             let exp_named_subst',subst',metasenv',ugraph1 =
192               check_exp_named_subst 
193                 subst metasenv context exp_named_subst ugraph 
194             in
195             let ty_uri,ugraph1 = type_of_variable uri ugraph in
196             let ty =
197               CicSubstitution.subst_vars exp_named_subst' ty_uri
198             in
199               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
200         | C.Meta (n,l) -> 
201             (try
202                let (canonical_context, term,ty) = 
203                  CicUtil.lookup_subst n subst 
204                in
205                let l',subst',metasenv',ugraph1 =
206                  check_metasenv_consistency n subst metasenv context
207                    canonical_context l ugraph 
208                in
209                  (* trust or check ??? *)
210                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
211                    subst', metasenv', ugraph1
212                    (* type_of_aux subst metasenv 
213                       context (CicSubstitution.subst_meta l term) *)
214              with CicUtil.Subst_not_found _ ->
215                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
216                let l',subst',metasenv', ugraph1 =
217                  check_metasenv_consistency n subst metasenv context
218                    canonical_context l ugraph
219                in
220                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty, 
221                    subst', metasenv',ugraph1)
222         | C.Sort (C.Type tno) -> 
223             let tno' = CicUniv.fresh() in 
224             let ugraph1 = CicUniv.add_gt tno' tno ugraph in
225               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
226         | C.Sort _ -> 
227             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
228         | C.Implicit _ -> raise (AssertFailure "21")
229         | C.Cast (te,ty) ->
230             let ty',_,subst',metasenv',ugraph1 =
231               type_of_aux subst metasenv context ty ugraph 
232             in
233             let te',inferredty,subst'',metasenv'',ugraph2 =
234               type_of_aux subst' metasenv' context te ugraph1
235             in
236               (try
237                  let subst''',metasenv''',ugraph3 =
238                    fo_unif_subst subst'' context metasenv'' 
239                      inferredty ty ugraph2
240                  in
241                    C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
242                with
243                    _ -> raise (RefineFailure "Cast"))
244         | C.Prod (name,s,t) ->
245             let s',sort1,subst',metasenv',ugraph1 = 
246               type_of_aux subst metasenv context s ugraph 
247             in
248             let t',sort2,subst'',metasenv'',ugraph2 =
249               type_of_aux subst' metasenv' 
250                 ((Some (name,(C.Decl s')))::context) t ugraph1
251             in
252             let sop,subst''',metasenv''',ugraph3 =
253               sort_of_prod subst'' metasenv'' 
254                 context (name,s') (sort1,sort2) ugraph2
255             in
256               C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
257         | C.Lambda (n,s,t) ->
258             let s',sort1,subst',metasenv',ugraph1 = 
259               type_of_aux subst metasenv context s ugraph
260             in
261               (match CicReduction.whd ~subst:subst' context sort1 with
262                    C.Meta _
263                  | C.Sort _ -> ()
264                  | _ ->
265                      raise (RefineFailure (sprintf
266                                              "Not well-typed lambda-abstraction: the source %s should be a type;
267              instead it is a term of type %s" (CicPp.ppterm s)
268                                              (CicPp.ppterm sort1)))
269               ) ;
270               let t',type2,subst'',metasenv'',ugraph2 =
271                 type_of_aux subst' metasenv' 
272                   ((Some (n,(C.Decl s')))::context) t ugraph1
273               in
274                 C.Lambda (n,s',t'),C.Prod (n,s',type2),
275                   subst'',metasenv'',ugraph2
276         | C.LetIn (n,s,t) ->
277             (* only to check if s is well-typed *)
278             let s',ty,subst',metasenv',ugraph1 = 
279               type_of_aux subst metasenv context s ugraph
280             in
281             let t',inferredty,subst'',metasenv'',ugraph2 =
282               type_of_aux subst' metasenv' 
283                 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
284             in
285               (* One-step LetIn reduction. 
286                * Even faster than the previous solution.
287                * Moreover the inferred type is closer to the expected one. 
288                *)
289               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
290                 subst',metasenv',ugraph2
291         | C.Appl (he::((_::_) as tl)) ->
292             let he',hetype,subst',metasenv',ugraph1 = 
293               type_of_aux subst metasenv context he ugraph 
294             in
295             let tlbody_and_type,subst'',metasenv'',ugraph2 =
296               List.fold_right
297                 (fun x (res,subst,metasenv,ugraph) ->
298                    let x',ty,subst',metasenv',ugraph1 =
299                      type_of_aux subst metasenv context x ugraph
300                    in
301                      (x', ty)::res,subst',metasenv',ugraph1
302                 ) tl ([],subst',metasenv',ugraph1)
303             in
304             let tl',applty,subst''',metasenv''',ugraph3 =
305               eat_prods subst'' metasenv'' context 
306                 hetype tlbody_and_type ugraph2
307             in
308               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
309         | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
310         | C.Const (uri,exp_named_subst) ->
311             let exp_named_subst',subst',metasenv',ugraph1 =
312               check_exp_named_subst subst metasenv context 
313                 exp_named_subst ugraph in
314             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
315             let cty =
316               CicSubstitution.subst_vars exp_named_subst' ty_uri
317             in
318               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
319         | C.MutInd (uri,i,exp_named_subst) ->
320             let exp_named_subst',subst',metasenv',ugraph1 =
321               check_exp_named_subst subst metasenv context 
322                 exp_named_subst ugraph 
323             in
324             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
325             let cty =
326               CicSubstitution.subst_vars exp_named_subst' ty_uri in
327               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
328         | C.MutConstruct (uri,i,j,exp_named_subst) ->
329             let exp_named_subst',subst',metasenv',ugraph1 =
330               check_exp_named_subst subst metasenv context 
331                 exp_named_subst ugraph 
332             in
333             let ty_uri,ugraph2 = 
334               type_of_mutual_inductive_constr uri i j ugraph1 
335             in
336             let cty =
337               CicSubstitution.subst_vars exp_named_subst' ty_uri 
338             in
339               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
340                 metasenv',ugraph2
341         | C.MutCase (uri, i, outtype, term, pl) ->
342             (* first, get the inductive type (and noparams) 
343              * in the environment  *)
344             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
345               let obj,u = CicEnvironment.get_obj ugraph uri in
346               match obj with
347                   C.InductiveDefinition (l,expl_params,parsno,_) -> 
348                     List.nth l i , expl_params, parsno, u
349                 | _ ->
350                     raise
351                       (RefineFailure
352                          ("Unkown mutual inductive definition " ^ 
353                          U.string_of_uri uri)) 
354            in
355            let rec count_prod t =
356              match CicReduction.whd ~subst context t with
357                  C.Prod (_, _, t) -> 1 + (count_prod t)
358                | _ -> 0 
359            in 
360            let no_args = count_prod arity in
361              (* now, create a "generic" MutInd *)
362            let metasenv,left_args = 
363              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
364            in
365            let metasenv,right_args = 
366              let no_right_params = no_args - no_left_params in
367                if no_right_params < 0 then assert false
368                else CicMkImplicit.n_fresh_metas 
369                       metasenv subst context no_right_params 
370            in
371            let metasenv,exp_named_subst = 
372              CicMkImplicit.fresh_subst metasenv subst context expl_params in
373            let expected_type = 
374              if no_args = 0 then 
375                C.MutInd (uri,i,exp_named_subst)
376              else
377                C.Appl 
378                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
379            in
380              (* check consistency with the actual type of term *)
381            let term',actual_type,subst,metasenv,ugraph1 = 
382              type_of_aux subst metasenv context term ugraph in
383            let expected_type',_, subst, metasenv,ugraph2 =
384              type_of_aux subst metasenv context expected_type ugraph1
385            in
386            let actual_type = CicReduction.whd ~subst context actual_type in
387            let subst,metasenv,ugraph3 =
388              fo_unif_subst subst context metasenv 
389                expected_type' actual_type ugraph2
390            in
391            let rec instantiate_prod t =
392             function
393                [] -> t
394              | he::tl ->
395                 match CicReduction.whd ~subst context t with
396                    C.Prod (_,_,t') ->
397                     instantiate_prod (CicSubstitution.subst he t') tl
398                  | _ -> assert false
399            in
400            let arity_instantiated_with_left_args =
401             instantiate_prod arity left_args in
402              (* TODO: check if the sort elimination 
403               * is allowed: [(I q1 ... qr)|B] *)
404            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
405              List.fold_left
406                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
407                   let constructor =
408                     if left_args = [] then
409                       (C.MutConstruct (uri,i,j,exp_named_subst))
410                     else
411                       (C.Appl 
412                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
413                   in
414                   let p',actual_type,subst,metasenv,ugraph1 = 
415                     type_of_aux subst metasenv context p ugraph 
416                   in
417                   let constructor',expected_type, subst, metasenv,ugraph2 = 
418                     type_of_aux subst metasenv context constructor ugraph1 
419                   in
420                   let outtypeinstance,subst,metasenv,ugraph3 =
421                     check_branch 0 context metasenv subst no_left_params 
422                       actual_type constructor' expected_type ugraph2 
423                   in
424                     (pl @ [p'],j+1,
425                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
426                ([],1,[],subst,metasenv,ugraph3) pl 
427            in
428            
429              (* we are left to check that the outype matches his instances.
430                 The easy case is when the outype is specified, that amount
431                 to a trivial check. Otherwise, we should guess a type from
432                 its instances 
433              *)
434              
435            (match outtype with
436            | C.Meta (n,l) ->
437                (let candidate,ugraph5,metasenv = 
438                  let exp_name_subst, metasenv = 
439                     let o,_ = 
440                       CicEnvironment.get_obj CicUniv.empty_ugraph uri 
441                     in
442                     let uris = CicUtil.params_of_obj o in
443                     List.fold_right (
444                       fun uri (acc,metasenv) -> 
445                         let metasenv',new_meta = 
446                            CicMkImplicit.mk_implicit metasenv subst context
447                         in
448                         let irl =
449                           CicMkImplicit.identity_relocation_list_for_metavariable 
450                             context
451                         in
452                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
453                     ) uris ([],metasenv)
454                  in
455                  let ty =
456                   match left_args,right_args with
457                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
458                    | _,_ ->
459                       let rec mk_right_args =
460                        function
461                           0 -> []
462                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
463                       in
464                       let right_args_no = List.length right_args in
465                       let lifted_left_args =
466                        List.map (CicSubstitution.lift right_args_no) left_args
467                       in
468                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
469                         (lifted_left_args @ mk_right_args right_args_no))
470                  in
471                  let fresh_name = 
472                    FreshNamesGenerator.mk_fresh_name ~subst metasenv 
473                      context Cic.Anonymous ~typ:ty
474                  in
475                  match outtypeinstances with
476                  | [] -> 
477                      let extended_context = 
478                       let rec add_right_args =
479                        function
480                           Cic.Prod (name,ty,t) ->
481                            Some (name,Cic.Decl ty)::(add_right_args t)
482                         | _ -> []
483                       in
484                        (Some (fresh_name,Cic.Decl ty))::
485                        (List.rev
486                         (add_right_args arity_instantiated_with_left_args))@
487                        context
488                      in
489                      let metasenv,new_meta = 
490                        CicMkImplicit.mk_implicit metasenv subst extended_context
491                      in
492                      let irl =
493                        CicMkImplicit.identity_relocation_list_for_metavariable 
494                          extended_context
495                      in
496                      let rec add_lambdas b =
497                       function
498                          Cic.Prod (name,ty,t) ->
499                           Cic.Lambda (name,ty,(add_lambdas b t))
500                        | _ -> Cic.Lambda (fresh_name, ty, b)
501                      in
502                      let candidate = 
503                       add_lambdas (Cic.Meta (new_meta,irl))
504                        arity_instantiated_with_left_args
505                      in
506                      (Some candidate),ugraph4,metasenv
507                  | (constructor_args_no,_,instance,_)::tl -> 
508                      try
509                        let instance' = 
510                          CicSubstitution.delift constructor_args_no
511                            (CicMetaSubst.apply_subst subst instance)
512                        in
513                        let candidate,ugraph,metasenv =
514                          List.fold_left (
515                            fun (candidate_oty,ugraph,metasenv) 
516                              (constructor_args_no,_,instance,_) ->
517                                match candidate_oty with
518                                | None -> None,ugraph,metasenv
519                                | Some ty ->
520                                  try 
521                                    let instance' = 
522                                      CicSubstitution.delift
523                                       constructor_args_no
524                                        (CicMetaSubst.apply_subst subst instance)
525                                    in
526                                    let b,ugraph1 =
527                                       CicReduction.are_convertible context 
528                                         instance' ty ugraph
529                                    in
530                                    if b then 
531                                      candidate_oty,ugraph1,metasenv 
532                                    else 
533                                      None,ugraph,metasenv
534                                  with Failure s -> None,ugraph,metasenv
535                          ) (Some instance',ugraph4,metasenv) tl
536                        in
537                        match candidate with
538                        | None -> None, ugraph,metasenv
539                        | Some t -> 
540                           let rec add_lambdas n b =
541                            function
542                               Cic.Prod (name,ty,t) ->
543                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
544                             | _ ->
545                               Cic.Lambda (fresh_name, ty,
546                                CicSubstitution.lift (n + 1) t)
547                           in
548                            Some
549                             (add_lambdas 0 t arity_instantiated_with_left_args),
550                            ugraph,metasenv 
551                      with Failure s -> 
552                        None,ugraph4,metasenv
553                in
554                match candidate with
555                | None -> raise (Uncertain "can't solve an higher order unification problem") 
556                | Some candidate ->
557                    let s,m,u = 
558                      fo_unif_subst subst context metasenv 
559                        candidate outtype ugraph5
560                    in
561                      C.MutCase (uri, i, outtype, term', pl'),
562                        (Cic.Appl (outtype::right_args@[term'])),s,m,u)
563            | _ ->    (* easy case *)
564              let _,_, subst, metasenv,ugraph5 =
565                type_of_aux subst metasenv context
566                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
567              in
568              let (subst,metasenv,ugraph6) = 
569                List.fold_left
570                  (fun (subst,metasenv,ugraph) 
571                         (constructor_args_no,context,instance,args) ->
572                     let instance' = 
573                       let appl =
574                         let outtype' =
575                           CicSubstitution.lift constructor_args_no outtype
576                         in
577                           C.Appl (outtype'::args)
578                       in
579                         CicReduction.whd ~subst context appl
580                     in
581                     fo_unif_subst subst context metasenv 
582                         instance instance' ugraph)
583                  (subst,metasenv,ugraph5) outtypeinstances 
584              in
585                C.MutCase (uri, i, outtype, term', pl'),
586                  CicReduction.whd ~subst        context 
587                    (C.Appl(outtype::right_args@[term])),
588                  subst,metasenv,ugraph6)
589         | C.Fix (i,fl) ->
590             let fl_ty',subst,metasenv,types,ugraph1 =
591               List.fold_left
592                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
593                    let ty',_,subst',metasenv',ugraph1 = 
594                       type_of_aux subst metasenv context ty ugraph 
595                    in
596                      fl @ [ty'],subst',metasenv', 
597                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
598                 ) ([],subst,metasenv,[],ugraph) fl
599             in
600             let len = List.length types in
601             let context' = types@context in
602             let fl_bo',subst,metasenv,ugraph2 =
603               List.fold_left
604                 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
605                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
606                      type_of_aux subst metasenv context' bo ugraph
607                    in
608                    let subst',metasenv',ugraph' =
609                      fo_unif_subst subst context' metasenv
610                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
611                    in 
612                      fl @ [bo'] , subst',metasenv',ugraph'
613                 ) ([],subst,metasenv,ugraph1) fl 
614             in
615             let (_,_,ty,_) = List.nth fl i in
616             (* now we have the new ty in fl_ty', the new bo in fl_bo',
617              * and we want the new fl with bo' and ty' injected in the right
618              * place.
619              *) 
620             let rec map3 f l1 l2 l3 =
621               match l1,l2,l3 with
622               | [],[],[] -> []
623               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
624               | _ -> assert false 
625             in
626             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') ) 
627               fl_ty' fl_bo' fl 
628             in
629               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
630         | C.CoFix (i,fl) ->
631             let fl_ty',subst,metasenv,types,ugraph1 =
632               List.fold_left
633                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
634                    let ty',_,subst',metasenv',ugraph1 = 
635                      type_of_aux subst metasenv context ty ugraph 
636                    in
637                      fl @ [ty'],subst',metasenv', 
638                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
639                 ) ([],subst,metasenv,[],ugraph) fl
640             in
641             let len = List.length types in
642             let context' = types@context in
643             let fl_bo',subst,metasenv,ugraph2 =
644               List.fold_left
645                 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
646                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
647                      type_of_aux subst metasenv context' bo ugraph
648                    in
649                    let subst',metasenv',ugraph' = 
650                      fo_unif_subst subst context' metasenv
651                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
652                    in
653                      fl @ [bo'],subst',metasenv',ugraph'
654                 ) ([],subst,metasenv,ugraph1) fl 
655             in
656             let (_,ty,_) = List.nth fl i in
657             (* now we have the new ty in fl_ty', the new bo in fl_bo',
658              * and we want the new fl with bo' and ty' injected in the right
659              * place.
660              *) 
661             let rec map3 f l1 l2 l3 =
662               match l1,l2,l3 with
663               | [],[],[] -> []
664               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
665               | _ -> assert false
666             in
667             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') ) 
668               fl_ty' fl_bo' fl 
669             in
670               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
671
672   (* check_metasenv_consistency checks that the "canonical" context of a
673      metavariable is consitent - up to relocation via the relocation list l -
674      with the actual context *)
675   and check_metasenv_consistency
676     metano subst metasenv context canonical_context l ugraph
677     =
678     let module C = Cic in
679     let module R = CicReduction in
680     let module S = CicSubstitution in
681     let lifted_canonical_context = 
682       let rec aux i =
683         function
684             [] -> []
685           | (Some (n,C.Decl t))::tl ->
686               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
687           | (Some (n,C.Def (t,None)))::tl ->
688               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
689           | None::tl -> None::(aux (i+1) tl)
690           | (Some (n,C.Def (t,Some ty)))::tl ->
691               (Some (n,
692                      C.Def ((S.subst_meta l (S.lift i t)),
693                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
694       in
695         aux 1 canonical_context 
696     in
697       try
698         List.fold_left2 
699           (fun (l,subst,metasenv,ugraph) t ct -> 
700              match (t,ct) with
701                  _,None ->
702                    l @ [None],subst,metasenv,ugraph
703                | Some t,Some (_,C.Def (ct,_)) ->
704                    let subst',metasenv',ugraph' = 
705                    (try
706                       fo_unif_subst subst context metasenv t ct ugraph
707                     with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
708                    in
709                      l @ [Some t],subst',metasenv',ugraph'
710                | Some t,Some (_,C.Decl ct) ->
711                    let t',inferredty,subst',metasenv',ugraph1 =
712                      type_of_aux subst metasenv context t ugraph
713                    in
714                    let subst'',metasenv'',ugraph2 = 
715                      (try
716                         fo_unif_subst
717                           subst' context metasenv' inferredty ct ugraph1
718                       with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
719                    in
720                      l @ [Some t'], subst'',metasenv'',ugraph2
721                | None, Some _  ->
722                    raise (RefineFailure (sprintf
723                                            "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
724                                            (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
725                                            (CicMetaSubst.ppcontext subst canonical_context)))
726           ) ([],subst,metasenv,ugraph) l lifted_canonical_context 
727       with
728           Invalid_argument _ ->
729             raise
730             (RefineFailure
731                (sprintf
732                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
733                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
734                   (CicMetaSubst.ppcontext subst canonical_context)))
735
736   and check_exp_named_subst metasubst metasenv context tl ugraph =
737     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
738       match tl with
739           [] -> [],metasubst,metasenv,ugraph
740         | ((uri,t) as subst)::tl ->
741             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
742             let typeofvar =
743               CicSubstitution.subst_vars substs ty_uri in
744               (* CSC: why was this code here? it is wrong
745                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
746                  Cic.Variable (_,Some bo,_,_) ->
747                  raise
748                  (RefineFailure
749                  "A variable with a body can not be explicit substituted")
750                  | Cic.Variable (_,None,_,_) -> ()
751                  | _ ->
752                  raise
753                  (RefineFailure
754                  ("Unkown variable definition " ^ UriManager.string_of_uri uri))
755                  ) ;
756               *)
757             let t',typeoft,metasubst',metasenv',ugraph2 =
758               type_of_aux metasubst metasenv context t ugraph1
759             in
760             let metasubst'',metasenv'',ugraph3 =
761               try
762                 fo_unif_subst 
763                   metasubst' context metasenv' typeoft typeofvar ugraph2
764               with _ ->
765                 raise (RefineFailure
766                          ("Wrong Explicit Named Substitution: " ^ 
767                            CicMetaSubst.ppterm metasubst' typeoft ^
768                           " not unifiable with " ^ 
769                           CicMetaSubst.ppterm metasubst' typeofvar))
770             in
771             (* FIXME: no mere tail recursive! *)
772             let exp_name_subst, metasubst''', metasenv''', ugraph4 = 
773               check_exp_named_subst_aux 
774                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
775             in
776               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
777     in
778       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
779
780
781   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
782     let module C = Cic in
783     let context_for_t2 = (Some (name,C.Decl s))::context in
784     let t1'' = CicReduction.whd ~subst context t1 in
785     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
786       match (t1'', t2'') with
787           (C.Sort s1, C.Sort s2)
788             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
789               C.Sort s2,subst,metasenv,ugraph
790         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
791             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
792             let t' = CicUniv.fresh() in 
793             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
794             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
795               C.Sort (C.Type t'),subst,metasenv,ugraph2
796         | (C.Sort _,C.Sort (C.Type t1)) -> 
797             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
798             C.Sort (C.Type t1),subst,metasenv,ugraph
799         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
800         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
801             (* TODO how can we force the meta to become a sort? If we don't we
802              * brake the invariant that refine produce only well typed terms *)
803             (* TODO if we check the non meta term and if it is a sort then we are
804              * likely to know the exact value of the result e.g. if the rhs is a
805              * Sort (Prop | Set | CProp) then the result is the rhs *)
806             let (metasenv,idx) =
807               CicMkImplicit.mk_implicit_sort metasenv subst in
808             let (subst, metasenv,ugraph1) =
809               fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
810             in
811               t2'',subst,metasenv,ugraph1
812         | (_,_) ->
813             raise (RefineFailure (sprintf
814                                     "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
815                                     (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
816                                     (CicPp.ppterm t2'')))
817
818   and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
819     let rec mk_prod metasenv context =
820       function
821           [] ->
822             let (metasenv, idx) = 
823               CicMkImplicit.mk_implicit_type metasenv subst context 
824             in
825             let irl =
826               CicMkImplicit.identity_relocation_list_for_metavariable context
827             in
828               metasenv,Cic.Meta (idx, irl)
829         | (_,argty)::tl ->
830             let (metasenv, idx) = 
831               CicMkImplicit.mk_implicit_type metasenv subst context 
832             in
833             let irl =
834               CicMkImplicit.identity_relocation_list_for_metavariable context
835             in
836             let meta = Cic.Meta (idx,irl) in
837             let name =
838               (* The name must be fresh for context.                 *)
839               (* Nevertheless, argty is well-typed only in context.  *)
840               (* Thus I generate a name (name_hint) in context and   *)
841               (* then I generate a name --- using the hint name_hint *)
842               (* --- that is fresh in (context'@context).            *)
843               let name_hint = 
844                 (* Cic.Name "pippo" *)
845                 FreshNamesGenerator.mk_fresh_name ~subst metasenv 
846                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
847                   (CicMetaSubst.apply_subst_context subst context)
848                   Cic.Anonymous
849                   ~typ:(CicMetaSubst.apply_subst subst argty) 
850               in
851                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
852                 FreshNamesGenerator.mk_fresh_name ~subst
853                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
854             in
855             let metasenv,target =
856               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
857             in
858               metasenv,Cic.Prod (name,meta,target)
859     in
860     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
861     let (subst, metasenv,ugraph1) =
862       try
863         fo_unif_subst subst context metasenv hetype hetype' ugraph
864       with exn ->
865         debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
866                          (CicPp.ppterm hetype)
867                          (CicPp.ppterm hetype')
868                          (CicMetaSubst.ppmetasenv metasenv [])
869                          (CicMetaSubst.ppsubst subst));
870         raise exn
871
872     in
873     let rec eat_prods metasenv subst context hetype ugraph =
874       function
875         | [] -> [],metasenv,subst,hetype,ugraph
876         | (hete, hety)::tl ->
877             (match hetype with
878                  Cic.Prod (n,s,t) ->
879                    let arg,subst,metasenv,ugraph1 =
880                      try
881                        let subst,metasenv,ugraph1 = 
882                          fo_unif_subst subst context metasenv hety s ugraph
883                        in
884                          hete,subst,metasenv,ugraph1
885                      with exn ->
886                        (* we search a coercion from hety to s *)
887                        let coer = CoercGraph.look_for_coercion 
888                          (CicMetaSubst.apply_subst subst hety) 
889                          (CicMetaSubst.apply_subst subst s) 
890                        in
891                        match coer with
892                        | None -> raise exn
893                        | Some c -> 
894                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
895                    in
896                    let coerced_args,metasenv',subst',t',ugraph2 =
897                      eat_prods metasenv subst context
898                        (* (CicMetaSubst.subst subst hete t) tl *)
899                        (CicSubstitution.subst hete t) ugraph1 tl
900                    in
901                      arg::coerced_args,metasenv',subst',t',ugraph2
902                | _ -> assert false
903             )
904     in
905     let coerced_args,metasenv,subst,t,ugraph2 =
906       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type 
907     in
908       coerced_args,t,subst,metasenv,ugraph2
909   in
910   
911   (* eat prods ends here! *)
912   
913   let t',ty,subst',metasenv',ugraph1 =
914    type_of_aux [] metasenv context t ugraph
915   in
916   let substituted_t = CicMetaSubst.apply_subst subst' t' in
917   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
918     (* Andrea: ho rimesso qui l'applicazione della subst al
919        metasenv dopo che ho droppato l'invariante che il metsaenv
920        e' sempre istanziato *)
921   let substituted_metasenv = 
922     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
923     (* metasenv' *)
924     (*  substituted_t,substituted_ty,substituted_metasenv *)
925     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
926   let cleaned_t =
927     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
928   let cleaned_ty =
929     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
930   let cleaned_metasenv =
931     List.map
932       (function (n,context,ty) ->
933          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
934          let context' =
935            List.map
936              (function
937                   None -> None
938                 | Some (n, Cic.Decl t) ->
939                     Some (n,
940                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
941                 | Some (n, Cic.Def (bo,ty)) ->
942                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
943                     let ty' =
944                       match ty with
945                           None -> None
946                         | Some ty ->
947                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
948                     in
949                       Some (n, Cic.Def (bo',ty'))
950              ) context
951          in
952            (n,context',ty')
953       ) substituted_metasenv
954   in
955     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
956 ;;
957
958 let type_of_aux' metasenv context term ugraph =
959   try 
960     type_of_aux' metasenv context term ugraph
961   with 
962     CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
963     
964
965 (* DEBUGGING ONLY 
966 let type_of_aux' metasenv context term =
967  try
968   let (t,ty,m) = 
969       type_of_aux' metasenv context term in
970     debug_print
971      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
972    debug_print
973     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
974    (t,ty,m)
975  with
976  | RefineFailure msg as e ->
977      debug_print ("@@@ REFINE FAILED: " ^ msg);
978      raise e
979  | Uncertain msg as e ->
980      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
981      raise e
982 ;; *)