]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/proofEngine.ml
* Bug fixed: Elim did not work for principles whose conclusion was just
[helm.git] / helm / gTopLevel / proofEngine.ml
1 type binder_type =
2    Declaration of Cic.name * Cic.term
3  | Definition of Cic.name * Cic.term
4 ;;
5
6 type metasenv = (int * Cic.term) list;;
7
8 type named_context = binder_type list;;
9
10 type sequent = named_context * Cic.term;;
11
12 let proof =
13  ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
14 ;;
15 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
16 (* Note: the sequent is redundant: it can be computed from the type of the   *)
17 (* metavariable and its context in the proof. We keep it just for efficiency *)
18 (* because computing the context of a term may be quite expensive.           *)
19 let goal = ref (None : (int * sequent) option);;
20
21 exception NotImplemented
22
23 let cic_context_of_named_context =
24  List.map
25   (function
26       Declaration (_,t) -> Cic.Decl t
27     | Definition (_,t) -> Cic.Def t
28   )
29 ;;
30
31 (* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing    *)
32 (*   newmetasenv                                                          *)
33 (* This (heavy) function must be called when a tactic can instantiate old *)
34 (* metavariables (i.e. existential variables). It substitues the metasenv *)
35 (* of the proof with the result of removing [meta] from the domain of     *)
36 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
37 (* in the current proof. Finally it applies [apply_subst_replacing] to    *)
38 (*  current proof.                                                        *)
39 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
40 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
41 (*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
42 (*CSC: newmetasenv!!!                                                      *)
43 let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
44  newmetasenv
45 =
46  let (uri,bo,ty) =
47   match !proof with
48      None -> assert false
49    | Some (uri,_,bo,ty) -> uri,bo,ty
50  in
51   let subst_in t =
52    ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
53   in
54    let bo' = apply_subst_replacing (subst_in bo) in
55    let metasenv' = List.remove_assoc meta newmetasenv in
56     proof := Some (uri,metasenv',bo',ty)
57 ;;
58
59 let refine_meta meta term newmetasenv =
60  let (uri,metasenv,bo,ty) =
61   match !proof with
62      None -> assert false
63    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
64  in
65   let subst_in t =
66    ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
67   in
68    let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
69     let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
70     let bo' = subst_in bo in
71      proof := Some (uri,metasenv'',bo',ty)
72 ;;
73
74 (* Returns the first meta whose number is above the *)
75 (* number of the higher meta.                       *)
76 let new_meta () =
77  let metasenv =
78   match !proof with
79      None -> assert false
80    | Some (_,metasenv,_,_) -> metasenv
81  in
82   let rec aux =
83    function
84       None,[] -> 1
85     | Some n,[] -> n
86     | None,(n,_)::tl -> aux (Some n,tl)
87     | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
88   in
89    1 + aux (None,metasenv)
90 ;;
91
92 (* metas_in_term term                                                *)
93 (* Returns the ordered list of the metas that occur in [term].       *)
94 (* Duplicates are removed. The implementation is not very efficient. *)
95 let metas_in_term term =
96  let module C = Cic in
97   let rec aux =
98    function
99       C.Rel _
100     | C.Var _ -> []
101     | C.Meta n -> [n]
102     | C.Sort _
103     | C.Implicit -> []
104     | C.Cast (te,ty) -> (aux te) @ (aux ty)
105     | C.Prod (_,s,t) -> (aux s) @ (aux t)
106     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
107     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
108     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
109     | C.Const _
110     | C.Abst _
111     | C.MutInd _
112     | C.MutConstruct _ -> []
113     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
114        (aux outt) @ (aux t) @
115         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
116     | C.Fix (i,fl) ->
117         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
118     | C.CoFix (i,fl) ->
119         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
120   in
121    let metas = aux term in
122     let rec elim_duplicates =
123      function
124         [] -> []
125       | he::tl ->
126          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
127     in
128      elim_duplicates metas
129 ;;
130
131 (* perforate context term ty                                                 *)
132 (* replaces the term [term] in the proof with a new metavariable whose type  *)
133 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
134 (* could be easily computed; so the only reasons to have it as an argument   *)
135 (* are efficiency reasons.                                                   *)
136 let perforate context term ty =
137  let module C = Cic in
138   let newmeta = new_meta () in
139    match !proof with
140       None -> assert false
141     | Some (uri,metasenv,bo,gty) ->
142        (* We push the new meta at the end of the list for pretty-printing *)
143        (* purposes: in this way metas are ordered.                        *)
144        let metasenv' = metasenv@[newmeta,ty] in
145         let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
146         (* It may be possible that some metavariables occurred only in *)
147         (* the term we are perforating and they now occurs no more. We *)
148         (* get rid of them, collecting the really useful metavariables *)
149         (* in metasenv''.                                              *)
150          let newmetas = metas_in_term bo' in
151           let metasenv'' =
152            List.filter (function (n,_) -> List.mem n newmetas) metasenv'
153           in
154            proof := Some (uri,metasenv'',bo',gty) ;
155            goal := Some (newmeta,(context,ty)) ;
156            newmeta
157 ;;
158
159 (************************************************************)
160 (*                  Some easy tactics.                      *)
161 (************************************************************)
162
163 exception Fail of string;;
164
165 (* lambda_abstract newmeta ty *)
166 (* returns a triple [bo],[context],[ty'] where              *)
167 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
168 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
169 (* So, lambda_abstract is the core of the implementation of *)
170 (* the Intros tactic.                                       *)
171 let lambda_abstract newmeta ty =
172  let module C = Cic in
173   let rec collect_context =
174    function
175       C.Cast (te,_)   -> collect_context te
176     | C.Prod (n,s,t)  ->
177        let (ctx,ty,bo) = collect_context t in
178         let n' =
179          match n with
180             C.Name _ -> n
181 (*CSC: generatore di nomi? Chiedere il nome? *)
182           | C.Anonimous -> C.Name "fresh_name"
183         in
184          ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
185     | C.LetIn (n,s,t) ->
186        let (ctx,ty,bo) = collect_context t in
187         ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
188     | _ as t -> [], t, (C.Meta newmeta)
189   in
190    let revcontext,ty',bo = collect_context ty in
191     bo,(List.rev revcontext),ty'
192 ;;
193
194 let intros () =
195  let module C = Cic in
196  let module R = CicReduction in
197   let metasenv =
198    match !proof with
199       None -> assert false
200     | Some (_,metasenv,_,_) -> metasenv
201   in
202   let (metano,context,ty) =
203    match !goal with
204       None -> assert false
205     | Some (metano,(context,ty)) -> metano,context,ty
206   in
207    let newmeta = new_meta () in
208     let (bo',newcontext,ty') = lambda_abstract newmeta ty in
209       let context'' = newcontext @ context in
210        refine_meta metano bo' [newmeta,ty'] ;
211        goal := Some (newmeta,(context'',ty'))
212 ;;
213
214 (* The term bo must be closed in the current context *)
215 let exact bo =
216  let module T = CicTypeChecker in
217  let module R = CicReduction in
218   let metasenv =
219    match !proof with
220       None -> assert false
221     | Some (_,metasenv,_,_) -> metasenv
222   in
223   let (metano,context,ty) =
224    match !goal with
225       None -> assert false
226     | Some (metano,(context,ty)) ->
227        assert (ty = List.assoc metano metasenv) ;
228        (* Invariant: context is the actual context of the meta in the proof *)
229        metano,context,ty
230   in
231    let context = cic_context_of_named_context context in
232     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
233      begin
234       refine_meta metano bo [] ;
235       goal := None
236      end
237     else
238      raise (Fail "The type of the provided term is not the one expected.")
239 ;;
240
241 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
242 (*CSC: Elim tactic. Do we already need tacticals?                       *)
243 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
244 (* head, a META environment in which there is new a META for each hypothesis,*)
245 (* a list of arguments for the new applications and the indexes of the first *)
246 (* and last new METAs introduced. The nth argument in the list of arguments  *)
247 (* is the nth new META lambda-abstracted as much as possible. Hence, this    *)
248 (* functions already provides the behaviour of Intros on the new goals.      *)
249 let new_metasenv_for_apply_intros ty =
250  let module C = Cic in
251  let module S = CicSubstitution in
252   let rec aux newmeta =
253    function
254       C.Cast (he,_) -> aux newmeta he
255     | C.Prod (_,s,t) ->
256        let newargument,newcontext,ty' = lambda_abstract newmeta s in
257         let (res,newmetasenv,arguments,lastmeta) =
258          aux (newmeta + 1) (S.subst newargument t)
259         in
260          res,(newmeta,ty')::newmetasenv,newargument::arguments,lastmeta
261     | t -> t,[],[],newmeta
262   in
263    let newmeta = new_meta () in
264     (* WARNING: here we are using the invariant that above the most *)
265     (* recente new_meta() there are no used metas.                  *)
266     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
267      res,newmetasenv,arguments,newmeta,lastmeta
268 ;;
269
270 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
271 (* head, a META environment in which there is new a META for each hypothesis,*)
272 (* a list of arguments for the new applications and the indexes of the first *)
273 (* and last new METAs introduced. The nth argument in the list of arguments  *)
274 (* is just the nth new META.                                                 *)
275 let new_metasenv_for_apply ty =
276  let module C = Cic in
277  let module S = CicSubstitution in
278   let rec aux newmeta =
279    function
280       C.Cast (he,_) -> aux newmeta he
281     | C.Prod (_,s,t) ->
282        let newargument = C.Meta newmeta in
283         let (res,newmetasenv,arguments,lastmeta) =
284          aux (newmeta + 1) (S.subst newargument t)
285         in
286          res,(newmeta,s)::newmetasenv,newargument::arguments,lastmeta
287     | t -> t,[],[],newmeta
288   in
289    let newmeta = new_meta () in
290     (* WARNING: here we are using the invariant that above the most *)
291     (* recente new_meta() there are no used metas.                  *)
292     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
293      res,newmetasenv,arguments,newmeta,lastmeta
294 ;;
295
296
297 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
298 let classify_metas newmeta in_subst_domain apply_subst metasenv =
299  List.fold_right
300   (fun (i,ty) (old_uninst,new_uninst) ->
301     if in_subst_domain i then
302      old_uninst,new_uninst
303     else
304      let ty' = apply_subst ty in
305       if i < newmeta then
306        ((i,ty')::old_uninst),new_uninst
307       else
308        old_uninst,((i,ty')::new_uninst)
309   ) metasenv ([],[])
310 ;;
311
312 (* The term bo must be closed in the current context *)
313 let apply term =
314  let module T = CicTypeChecker in
315  let module R = CicReduction in
316  let module C = Cic in
317   let metasenv =
318    match !proof with
319       None -> assert false
320     | Some (_,metasenv,_,_) -> metasenv
321   in
322   let (metano,context,ty) =
323    match !goal with
324       None -> assert false
325     | Some (metano,(context,ty)) ->
326        assert (ty = List.assoc metano metasenv) ;
327        (* Invariant: context is the actual context of the meta in the proof *)
328        metano,context,ty
329   in
330    let ciccontext = cic_context_of_named_context context in
331     let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
332      (* newmeta is the lowest index of the new metas introduced *)
333      let (consthead,newmetas,arguments,newmeta,_) =
334       new_metasenv_for_apply termty
335      in
336       let newmetasenv = newmetas@metasenv in
337        let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
338         let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
339         let apply_subst = CicUnification.apply_subst subst in
340 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
341         let apply_subst_replacing t =
342          List.fold_left
343           (fun t (i,bo) ->
344             ProofEngineReduction.replace
345              ~what:(Cic.Meta i) ~with_what:bo ~where:t)
346           t subst
347         in
348          let old_uninstantiatedmetas,new_uninstantiatedmetas =
349           classify_metas newmeta in_subst_domain apply_subst newmetasenv
350          in
351           let bo' =
352            if List.length newmetas = 0 then
353             term
354            else
355             let arguments' = List.map apply_subst arguments in
356              Cic.Appl (term::arguments')
357           in
358            refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
359             (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
360            match new_uninstantiatedmetas with
361               [] -> goal := None
362             | (i,ty)::_ -> goal := Some (i,(context,ty))
363 ;;
364
365 let eta_expand metasenv ciccontext t arg =
366  let module T = CicTypeChecker in
367  let module S = CicSubstitution in
368  let module C = Cic in
369   let rec aux n =
370    function
371       t' when t' = S.lift n arg -> C.Rel (1 + n)
372     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
373     | C.Var _
374     | C.Meta _
375     | C.Sort _
376     | C.Implicit as t -> t
377     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
378     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
379     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
380     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
381     | C.Appl l -> C.Appl (List.map (aux n) l)
382     | C.Const _ as t -> t
383     | C.Abst _ -> assert false
384     | C.MutInd _
385     | C.MutConstruct _ as t -> t
386     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
387        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
388         List.map (aux n) pl)
389     | C.Fix (i,fl) ->
390        let tylen = List.length fl in
391         let substitutedfl =
392          List.map
393           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
394            fl
395         in
396          C.Fix (i, substitutedfl)
397     | C.CoFix (i,fl) ->
398        let tylen = List.length fl in
399         let substitutedfl =
400          List.map
401           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
402            fl
403         in
404          C.CoFix (i, substitutedfl)
405   in
406    let argty =
407     T.type_of_aux' metasenv ciccontext arg
408    in
409     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
410 ;;
411
412 exception NotAnInductiveTypeToEliminate;;
413 exception NotTheRightEliminatorShape;;
414 exception NoHypothesesFound;;
415
416 let elim_intros term =
417  let module T = CicTypeChecker in
418  let module U = UriManager in
419  let module R = CicReduction in
420  let module C = Cic in
421   let curi,metasenv =
422    match !proof with
423       None -> assert false
424     | Some (curi,metasenv,_,_) -> curi,metasenv
425   in
426   let (metano,context,ty) =
427    match !goal with
428       None -> assert false
429     | Some (metano,(context,ty)) ->
430        assert (ty = List.assoc metano metasenv) ;
431        (* Invariant: context is the actual context of the meta in the proof *)
432        metano,context,ty
433   in
434    let ciccontext = cic_context_of_named_context context in
435     let termty = T.type_of_aux' metasenv ciccontext term in
436     let uri,cookingno,typeno,args =
437      match termty with
438         C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
439       | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
440           (uri,cookingno,typeno,args)
441       | _ -> raise NotAnInductiveTypeToEliminate
442     in
443      let eliminator_uri =
444       let buri = U.buri_of_uri uri in
445       let name = 
446        match CicEnvironment.get_cooked_obj uri cookingno with
447           C.InductiveDefinition (tys,_,_) ->
448            let (name,_,_,_) = List.nth tys typeno in
449             name
450         | _ -> assert false
451       in
452       let ext =
453        match T.type_of_aux' metasenv ciccontext ty with
454           C.Sort C.Prop -> "_ind"
455         | C.Sort C.Set  -> "_rec"
456         | C.Sort C.Type -> "_rect"
457         | _ -> assert false
458       in
459        U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
460      in
461       let eliminator_cookingno =
462        UriManager.relative_depth curi eliminator_uri 0
463       in
464       let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
465        let ety =
466         T.type_of_aux' [] [] eliminator_ref
467        in
468         let (econclusion,newmetas,arguments,newmeta,lastmeta) =
469          new_metasenv_for_apply ety
470         in
471          (* Here we assume that we have only one inductive hypothesis to *)
472          (* eliminate and that it is the last hypothesis of the theorem. *)
473          (* A better approach would be fingering the hypotheses in some  *)
474          (* way.                                                         *)
475          let meta_of_corpse = Cic.Meta (lastmeta - 1) in
476          let newmetasenv = newmetas @ metasenv in
477 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
478 flush stderr ;
479          let subst1 =
480           CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
481          in
482           let ueconclusion = CicUnification.apply_subst subst1 econclusion in
483 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
484 flush stderr ;
485            (* The conclusion of our elimination principle is *)
486            (*  (?i farg1 ... fargn)                         *)
487            (* The conclusion of our goal is ty. So, we can   *)
488            (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
489            (* a new ty equal to (P farg1 ... fargn). Now     *)
490            (* ?i can be instantiated with P and we are ready *)
491            (* to refine the term.                            *)
492            let emeta, fargs =
493             match ueconclusion with
494 (*CSC: Code to be used for Apply *)
495                C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
496              | C.Meta emeta -> emeta,[]
497 (*CSC: Code to be used for ApplyIntros
498                C.Appl (he::fargs) ->
499                 let rec find_head =
500                  function
501                     C.Meta emeta -> emeta
502                   | C.Lambda (_,_,t) -> find_head t
503                   | C.LetIn (_,_,t) -> find_head t
504                   | _ ->raise NotTheRightEliminatorShape
505                 in
506                  find_head he,fargs
507 *)
508              | _ -> raise NotTheRightEliminatorShape
509            in
510             let ty' = CicUnification.apply_subst subst1 ty in
511             let eta_expanded_ty =
512              List.fold_left (eta_expand metasenv ciccontext) ty' fargs
513             in
514 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
515              let subst2 =
516 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
517 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
518               CicUnification.fo_unif
519                newmetasenv ciccontext ueconclusion eta_expanded_ty
520              in
521 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
522 prerr_endline "unwind"; flush stderr;
523               let in_subst_domain i =
524                let eq_to_i = function (j,_) -> i=j in
525                 List.exists eq_to_i subst1 ||
526                 List.exists eq_to_i subst2
527               in
528                (* When unwinding the META that corresponds to the elimination *)
529                (* predicate (which is emeta), we must also perform one-step   *)
530                (* beta-reduction.                                             *)
531                let apply_subst t =
532                 let t' = CicUnification.apply_subst subst1 t in
533                  CicUnification.apply_subst_reducing
534                   subst2 (Some (emeta,List.length fargs)) t'
535                in
536 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
537                let apply_subst_replacing t =
538                 let t' =
539                  List.fold_left
540                   (fun t (i,bo) ->
541                     ProofEngineReduction.replace
542                      ~what:(Cic.Meta i) ~with_what:bo ~where:t)
543                   t subst1
544                 in
545                  List.fold_left
546                   (fun t (i,bo) ->
547                     ProofEngineReduction.replace
548                      ~what:(Cic.Meta i) ~with_what:bo ~where:t)
549                   t' subst2
550                in
551                 let newmetasenv' =
552                  List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
553                 in
554                  let old_uninstantiatedmetas,new_uninstantiatedmetas =
555                   classify_metas newmeta in_subst_domain apply_subst newmetasenv
556                  in
557                   let arguments' = List.map apply_subst arguments in
558                    let bo' = Cic.Appl (eliminator_ref::arguments') in
559 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
560 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
561                     refine_meta_with_brand_new_metasenv metano bo'
562                      apply_subst_replacing
563                      (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
564                     match new_uninstantiatedmetas with
565                        [] -> goal := None
566                      | (i,ty)::_ -> goal := Some (i,(context,ty))
567 ;;
568
569 let reduction_tactic reduction_function term =
570  let curi,metasenv,pbo,pty =
571   match !proof with
572      None -> assert false
573    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
574  in
575  let (metano,context,ty) =
576   match !goal with
577      None -> assert false
578    | Some (metano,(context,ty)) -> metano,context,ty
579  in
580   let term' = reduction_function term in
581    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
582    (* the type of one metavariable. So we replace it everywhere.   *)
583    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
584    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
585    let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
586     let ty' = replace ty in
587     let context' =
588      List.map
589       (function
590           Definition  (n,t) -> Definition  (n,replace t)
591         | Declaration (n,t) -> Declaration (n,replace t)
592       ) context
593     in
594      let metasenv' = 
595       List.map
596        (function
597            (n,_) when n = metano -> (metano,ty')
598          | _ as t -> t
599        ) metasenv
600      in
601       proof := Some (curi,metasenv',pbo,pty) ;
602       goal := Some (metano,(context',ty'))
603 ;;
604
605 let reduction_tactic_in_scratch reduction_function ty term =
606  let metasenv =
607   match !proof with
608      None -> []
609    | Some (_,metasenv,_,_) -> metasenv
610  in
611  let context =
612   match !goal with
613      None -> []
614    | Some (_,(context,_)) -> context
615  in
616   let term' = reduction_function term in
617    ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
618 ;;
619
620 let whd    = reduction_tactic CicReduction.whd;;
621 let reduce = reduction_tactic ProofEngineReduction.reduce;;
622 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
623
624 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
625 let reduce_in_scratch =
626  reduction_tactic_in_scratch ProofEngineReduction.reduce;;
627 let simpl_in_scratch  =
628  reduction_tactic_in_scratch ProofEngineReduction.simpl;;
629
630 (* It is just the opposite of whd. The code should probably be merged. *)
631 let fold term =
632  let curi,metasenv,pbo,pty =
633   match !proof with
634      None -> assert false
635    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
636  in
637  let (metano,context,ty) =
638   match !goal with
639      None -> assert false
640    | Some (metano,(context,ty)) -> metano,context,ty
641  in
642   let term' = CicReduction.whd term in
643    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
644    (* the type of one metavariable. So we replace it everywhere.   *)
645    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
646    (*CSC: che si guadagni nulla in fatto di efficienza.    *) 
647    let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
648     let ty' = replace ty in
649     let context' =
650      List.map
651       (function
652           Declaration (n,t) -> Declaration (n,replace t)
653         | Definition  (n,t) -> Definition (n,replace t)
654       ) context
655     in
656      let metasenv' = 
657       List.map
658        (function
659            (n,_) when n = metano -> (metano,ty')
660          | _ as t -> t
661        ) metasenv
662      in
663       proof := Some (curi,metasenv',pbo,pty) ;
664       goal := Some (metano,(context',ty'))
665 ;;
666
667 let cut term =
668  let module C = Cic in
669   let curi,metasenv,pbo,pty =
670    match !proof with
671       None -> assert false
672     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
673   in
674   let (metano,context,ty) =
675    match !goal with
676       None -> assert false
677     | Some (metano,(context,ty)) -> metano,context,ty
678   in
679    let newmeta1 = new_meta () in
680    let newmeta2 = newmeta1 + 1 in
681     let newmeta1ty = CicSubstitution.lift 1 ty in
682     let bo' =
683      C.Appl
684       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
685        C.Meta newmeta2]
686     in
687 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
688      refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
689      goal :=
690       Some
691        (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
692         newmeta1ty))
693 ;;
694
695 let letin term =
696  let module C = Cic in
697   let curi,metasenv,pbo,pty =
698    match !proof with
699       None -> assert false
700     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
701   in
702   let (metano,context,ty) =
703    match !goal with
704       None -> assert false
705     | Some (metano,(context,ty)) -> metano,context,ty
706   in
707    let ciccontext = cic_context_of_named_context context in
708    let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
709     let newmeta = new_meta () in
710      let newmetaty = CicSubstitution.lift 1 ty in
711      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
712       refine_meta metano bo' [newmeta,newmetaty];
713       goal :=
714        Some
715         (newmeta,
716          ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
717 ;;
718
719 exception NotConvertible;;
720
721 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
722 (*CSC: while [goal_input] can have a richer context (because of binders) *)
723 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
724 (*CSC: Is that evident? Is that right? Or should it be changed?          *)
725 let change ~goal_input ~input =
726  let curi,metasenv,pbo,pty =
727   match !proof with
728      None -> assert false
729    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
730  in
731  let (metano,context,ty) =
732   match !goal with
733      None -> assert false
734    | Some (metano,(context,ty)) -> metano,context,ty
735  in
736   let ciccontext = cic_context_of_named_context context in
737    (* are_convertible works only on well-typed terms *)
738    ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
739    if CicReduction.are_convertible goal_input input then
740     begin
741      let ty' = ProofEngineReduction.replace goal_input input ty in
742       let metasenv' = 
743        List.map
744         (function
745             (n,_) when n = metano -> (metano,ty')
746           | _ as t -> t
747         ) metasenv
748       in
749        proof := Some (curi,metasenv',pbo,pty) ;
750        goal := Some (metano,(context,ty'))
751     end
752   else
753    raise NotConvertible
754 ;;