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