]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitaEngine.ml
Bugs fixed:
[helm.git] / helm / matita / matitaEngine.ml
1
2 open Printf
3
4 open MatitaTypes
5
6
7 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
8   * names as long as they are available, then it fallbacks to name generation
9   * using FreshNamesGenerator module *)
10 let namer_of names =
11   let len = List.length names in
12   let count = ref 0 in
13   fun metasenv context name ~typ ->
14     if !count < len then begin
15       let name = Cic.Name (List.nth names !count) in
16       incr count;
17       name
18     end else
19       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
20
21 let tactic_of_ast = function
22   | TacticAst.Intros (_, _, names) ->
23       (* TODO Zack implement intros length *)
24       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
25   | TacticAst.Reflexivity _ -> Tactics.reflexivity
26   | TacticAst.Assumption _ -> Tactics.assumption
27   | TacticAst.Contradiction _ -> Tactics.contradiction
28   | TacticAst.Exists _ -> Tactics.exists
29   | TacticAst.Fourier _ -> Tactics.fourier
30   | TacticAst.Goal (_, n) -> Tactics.set_goal n
31   | TacticAst.Left _ -> Tactics.left
32   | TacticAst.Right _ -> Tactics.right
33   | TacticAst.Ring _ -> Tactics.ring
34   | TacticAst.Split _ -> Tactics.split
35   | TacticAst.Symmetry _ -> Tactics.symmetry
36   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
37   | TacticAst.Apply (_, term) -> Tactics.apply term
38   | TacticAst.Absurd (_, term) -> Tactics.absurd term
39   | TacticAst.Exact (_, term) -> Tactics.exact term
40   | TacticAst.Cut (_, term) -> Tactics.cut term
41   | TacticAst.Elim (_, term, _) ->
42       (* TODO Zack implement "using" argument *)
43       (* old: Tactics.elim_intros_simpl term *)
44       Tactics.elim_intros term
45   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
46   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
47   | TacticAst.Auto (_,num) -> 
48       AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
49   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
50 (*
51   (* TODO Zack a lot more of tactics to be implemented here ... *)
52   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
53   | TacticAst.Change of 'term * 'term * 'ident option
54   | TacticAst.Decompose of 'ident * 'ident list
55   | TacticAst.Discriminate of 'ident
56   | TacticAst.Fold of reduction_kind * 'term
57   | TacticAst.Injection of 'ident
58   | TacticAst.LetIn of 'term * 'ident
59   | TacticAst.Replace_pattern of 'term pattern * 'term
60 *)
61   | TacticAst.Reduce (_,reduction_kind,opts) ->
62       let terms, also_in_hypotheses = 
63         match opts with
64         | Some (l,`Goal) -> Some l, false
65         | Some (l,`Everywhere) -> Some l, true
66         | None -> None, false
67       in
68       (match reduction_kind with
69       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
70       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
71       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) 
72   | TacticAst.Rewrite (_,dir,t,ident) ->
73       if dir = `Left then
74         EqualityTactics.rewrite_tac ~term:t 
75       else
76         EqualityTactics.rewrite_back_tac ~term:t
77   | _ -> assert false
78
79 let eval_tactical status tac =
80   let apply_tactic tactic =
81     let (proof, goals) =
82       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
83     in
84     let new_status =
85       match goals with
86       | [] -> 
87           let (_,metasenv,_,_) = proof in
88           (match metasenv with
89           | [] -> Proof proof
90           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
91       | ng::_ -> Incomplete_proof (proof, ng)
92     in
93     { status with proof_status = new_status }
94   in
95   let rec tactical_of_ast = function
96     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
97     | TacticAst.Fail loc -> Tacticals.fail
98     | TacticAst.Do (loc, num, tactical) ->
99         Tacticals.do_tactic num (tactical_of_ast tactical)
100     | TacticAst.IdTac loc -> Tacticals.id_tac
101     | TacticAst.Repeat (loc, tactical) ->
102         Tacticals.repeat_tactic (tactical_of_ast tactical)
103     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
104         Tacticals.seq (List.map tactical_of_ast tacticals)
105     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
106         Tacticals.thens (tactical_of_ast tactical)
107           (List.map tactical_of_ast tacticals)
108     | TacticAst.Tries (loc, tacticals) ->
109         Tacticals.try_tactics
110           (List.map (fun t -> "", tactical_of_ast t) tacticals)
111     | TacticAst.Try (loc, tactical) ->
112         Tacticals.try_tactic (tactical_of_ast tactical)
113   in
114   apply_tactic (tactical_of_ast tac)
115
116 let eval_command status cmd =
117   match cmd with
118   | TacticAst.Set (loc, name, value) -> set_option status name value
119   | TacticAst.Qed loc ->
120       let uri, metasenv, bo, ty = 
121         match status.proof_status with
122         | Proof (Some uri, metasenv, body, ty) ->
123             uri, metasenv, body, ty
124         | Proof (None, metasenv, body, ty) -> 
125             command_error 
126               ("Someone allows to start a thm without giving the "^
127                "name/uri. This should be fixed!")
128         | _-> command_error "You can't qed an uncomplete theorem"
129       in
130       let suri = UriManager.string_of_uri uri in
131       if metasenv <> [] then 
132         command_error "Proof not completed! metasenv is not empty!";
133       let proved_ty,ugraph = 
134         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
135       in
136       let b,ugraph = 
137         CicReduction.are_convertible [] proved_ty ty ugraph 
138       in
139       if not b then 
140         command_error 
141           ("The type of your proof is not convertible with the "^
142           "type you've declared!");
143       MatitaLog.message (sprintf "%s defined" suri);
144       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
145       {status with proof_status = No_proof }
146   | TacticAst.Inductive (loc, dummy_params, types) ->
147       (* dummy_params are not real params, it is a list of nothing, and the only
148        * semantic content is the len, that is leftno (note: leftno and pamaters
149        * have nothing in common).
150        *)
151       let suri =
152         match types with
153         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
154         | _ -> assert false
155       in
156       let uri = UriManager.uri_of_string suri in
157       let leftno = List.length dummy_params in
158       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
159       let ugraph =
160         CicTypeChecker.typecheck_mutual_inductive_defs uri
161           (types, [], leftno) CicUniv.empty_ugraph
162       in
163       let status = 
164         MatitaSync.add_inductive_def
165           ~uri ~types ~params:[] ~leftno ~ugraph status
166       in
167         {status with proof_status = No_proof }
168   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
169       let uri = 
170         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
171       in
172       let goalno = 1 in
173       let metasenv, body = 
174         match status.proof_status with
175         | Intermediate metasenv -> 
176             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
177         | _-> assert false
178       in
179       let initial_proof = (Some uri, metasenv, body, ty) in
180       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
181   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
182       let uri = 
183         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
184       in
185       let metasenv = MatitaMisc.get_proof_metasenv status in
186       let (body_type, ugraph) =
187         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
188       in
189       let (subst, metasenv, ugraph) =
190         CicUnification.fo_unif metasenv [] body_type ty ugraph
191       in
192       if metasenv <> [] then
193         command_error
194           "metasenv not empty while giving a definition with body";
195       let body = CicMetaSubst.apply_subst subst body in
196       let ty = CicMetaSubst.apply_subst subst ty in
197       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
198       {status with proof_status = No_proof}
199   | TacticAst.Theorem (_, _, None, _, _) ->
200       command_error "The grammas should avoid having unnamed theorems!"
201   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
202   | TacticAst.Alias (loc, spec) -> 
203       match spec with
204       | TacticAst.Ident_alias (id,uri) -> 
205           {status with aliases = 
206             DisambiguateTypes.Environment.add 
207               (DisambiguateTypes.Id id) 
208               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) 
209               status.aliases }
210       | TacticAst.Symbol_alias (symb, instance, desc) ->
211           {status with aliases = 
212             DisambiguateTypes.Environment.add 
213               (DisambiguateTypes.Symbol (symb,instance))
214               (DisambiguateChoices.lookup_symbol_by_dsc symb desc) 
215               status.aliases }
216       | TacticAst.Number_alias (instance,desc) ->
217           {status with aliases = 
218             DisambiguateTypes.Environment.add 
219               (DisambiguateTypes.Num instance) 
220               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
221
222 let eval_executable status ex =
223   match ex with
224   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
225   | TacticAst.Command (_, cmd) -> eval_command status cmd
226   | TacticAst.Macro (_, mac) -> 
227       command_error (sprintf "The macro %s can't be in a script" 
228         (TacticAstPp.pp_macro_cic mac))
229
230 let eval_comment status c = status
231             
232 let eval status st =
233   match st with
234   | TacticAst.Executable (_,ex) -> eval_executable status ex
235   | TacticAst.Comment (_,c) -> eval_comment status c
236
237 let disambiguate_term status term =
238   let (aliases, metasenv, cic, _) =
239     match
240       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
241         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
242         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
243     with
244     | [x] -> x
245     | _ -> assert false
246   in
247   let proof_status =
248     match status.proof_status with
249     | No_proof -> Intermediate metasenv
250     | Incomplete_proof ((uri, _, proof, ty), goal) ->
251         Incomplete_proof ((uri, metasenv, proof, ty), goal)
252     | Intermediate _ -> Intermediate metasenv 
253     | Proof _ -> assert false
254   in
255   let status =
256     { status with
257         aliases = aliases;
258         proof_status = proof_status }
259   in
260   status, cic
261   
262 let disambiguate_terms status terms =
263   let term = CicAst.pack terms in
264   let status, term = disambiguate_term status term in
265   status, CicUtil.unpack term
266   
267 let disambiguate_tactic status = function
268   | TacticAst.Transitivity (loc, term) -> 
269       let status, cic = disambiguate_term status term in
270       status, TacticAst.Transitivity (loc, cic)
271   | TacticAst.Apply (loc, term) ->
272       let status, cic = disambiguate_term status term in
273       status, TacticAst.Apply (loc, cic)
274   | TacticAst.Absurd (loc, term) -> 
275       let status, cic = disambiguate_term status term in
276       status, TacticAst.Absurd (loc, cic)
277   | TacticAst.Exact (loc, term) -> 
278       let status, cic = disambiguate_term status term in
279       status, TacticAst.Exact (loc, cic)
280   | TacticAst.Cut (loc, term) -> 
281       let status, cic = disambiguate_term status term in
282       status, TacticAst.Cut (loc, cic)
283   | TacticAst.Elim (loc, term, Some term') ->
284       let status, cic1 = disambiguate_term status term in
285       let status, cic2 = disambiguate_term status term' in
286       status, TacticAst.Elim (loc, cic1, Some cic2)
287   | TacticAst.Elim (loc, term, None) ->
288       let status, cic = disambiguate_term status term in
289       status, TacticAst.Elim (loc, cic, None)
290   | TacticAst.ElimType (loc, term) -> 
291       let status, cic = disambiguate_term status term in
292       status, TacticAst.ElimType (loc, cic)
293   | TacticAst.Replace (loc, what, with_what) -> 
294       let status, cic1 = disambiguate_term status what in
295       let status, cic2 = disambiguate_term status with_what in
296       status, TacticAst.Replace (loc, cic1, cic2)
297   | TacticAst.Change (loc, what, with_what, ident) -> 
298       let status, cic1 = disambiguate_term status what in
299       let status, cic2 = disambiguate_term status with_what in
300       status, TacticAst.Change (loc, cic1, cic2, ident)
301 (*
302   (* TODO Zack a lot more of tactics to be implemented here ... *)
303   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
304   | TacticAst.Change of 'term * 'term * 'ident option
305   | TacticAst.Decompose of 'ident * 'ident list
306   | TacticAst.Discriminate of 'ident
307   | TacticAst.Fold of reduction_kind * 'term
308   | TacticAst.Injection of 'ident
309   | TacticAst.LetIn of 'term * 'ident
310   | TacticAst.Replace_pattern of 'term pattern * 'term
311 *)
312   | TacticAst.Reduce (loc, reduction_kind, opts) ->
313       let status, opts = 
314         match opts with
315         | None -> status, None
316         | Some (l,pat) -> 
317             let status, l = 
318               List.fold_right (fun t (status,acc) ->
319                 let status',t' = disambiguate_term status t in
320                 status', t'::acc) 
321               l (status,[]) 
322             in
323             status, Some (l, pat)
324       in
325       status, TacticAst.Reduce (loc, reduction_kind, opts)
326   | TacticAst.Rewrite (loc,dir,t,ident) ->
327       let status, term = disambiguate_term status t in
328       status, TacticAst.Rewrite (loc,dir,term,ident)
329   | TacticAst.Intros (loc, num, names) ->
330       status, TacticAst.Intros (loc, num, names)
331   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
332   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
333   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
334   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
335   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
336   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
337   | TacticAst.Left loc -> status, TacticAst.Left loc
338   | TacticAst.Right loc -> status, TacticAst.Right loc
339   | TacticAst.Ring loc -> status, TacticAst.Ring loc
340   | TacticAst.Split loc -> status, TacticAst.Split loc
341   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
342   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
343   | x -> 
344       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
345       assert false
346
347 let rec disambiguate_tactical status = function 
348   | TacticAst.Tactic (loc, tactic) -> 
349       let status, tac = disambiguate_tactic status tactic in
350       status, TacticAst.Tactic (loc, tac)
351   | TacticAst.Do (loc, num, tactical) ->
352       let status, tac = disambiguate_tactical status tactical in
353       status, TacticAst.Do (loc, num, tac)
354   | TacticAst.Repeat (loc, tactical) -> 
355       let status, tac = disambiguate_tactical status tactical in
356       status, TacticAst.Repeat (loc, tac)
357   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
358       let status, tacticals = disambiguate_tacticals status tacticals in
359       let tacticals = List.rev tacticals in
360       status, TacticAst.Seq (loc, tacticals)
361   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
362       let status, tactical = disambiguate_tactical status tactical in
363       let status, tacticals = disambiguate_tacticals status tacticals in
364       status, TacticAst.Then (loc, tactical, tacticals)
365   | TacticAst.Tries (loc, tacticals) ->
366       let status, tacticals = disambiguate_tacticals status tacticals in
367       status, TacticAst.Tries (loc, tacticals)
368   | TacticAst.Try (loc, tactical) ->
369       let status, tactical = disambiguate_tactical status tactical in
370       status, TacticAst.Try (loc, tactical)
371   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
372       status, tac
373
374 and disambiguate_tacticals status tacticals =
375   let status, tacticals =
376     List.fold_left
377       (fun (status, tacticals) tactical ->
378         let status, tac = disambiguate_tactical status tactical in
379         status, tac :: tacticals)
380       (status, [])
381       tacticals
382   in
383   let tacticals = List.rev tacticals in
384   status, tacticals
385   
386 let disambiguate_inddef status params indTypes =
387   let add_pi binders t =
388     List.fold_right
389       (fun (name, ast) acc ->
390         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
391       binders t
392   in
393   let ind_binders =
394     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
395   in
396   let binders = ind_binders @ params in
397   let asts = ref [] in
398   let add_ast ast = asts := ast :: !asts in
399   let paramsno = List.length params in
400   let indbindersno = List.length ind_binders in
401   List.iter
402     (fun (name, _, typ, constructors) ->
403       add_ast (add_pi params typ);
404       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
405     indTypes;
406   let status, terms = disambiguate_terms status !asts in
407   let terms = ref (List.rev terms) in
408   let get_term () =
409     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
410   in
411   let uri =
412     match indTypes with
413     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
414     | _ -> assert false
415   in
416   let mutinds =
417     let counter = ref 0 in
418     List.map
419       (fun _ ->
420         incr counter;
421         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
422       indTypes
423   in
424   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
425   let cicIndTypes =
426     List.fold_left
427       (fun acc (name, inductive, typ, constructors) ->
428         let cicTyp = get_term () in
429         let cicConstructors =
430           List.fold_left
431             (fun acc (name, _) ->
432               let typ =
433                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
434               in
435               (name, typ) :: acc)
436             [] constructors
437         in
438         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
439       [] indTypes
440   in
441   let cicIndTypes = List.rev cicIndTypes in
442   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
443
444 let disambiguate_command status = function
445   | TacticAst.Inductive (loc, params, types) ->
446       let (status, (uri, (ind_types, vars, paramsno))) =
447         disambiguate_inddef status params types
448       in
449       let rec mk_list = function
450         | 0 -> []
451         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
452       in  
453       (* once we've built the cic inductive types we no longer need terms
454          corresponding to parameters, but we need the leftno, and we encode
455          it as the length of dummy_params
456       *)
457       let dummy_params = mk_list paramsno in
458       status, TacticAst.Inductive (loc, dummy_params, ind_types)
459   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
460       let status, ty = disambiguate_term status ty in
461       let status, body =
462         match body with
463         | None -> status, None
464         | Some body ->
465             let status, body = disambiguate_term status body in
466             status, Some body
467       in
468       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
469   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
470   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
471       status, cmd
472   | TacticAst.Alias _ as x -> status, x
473
474 let disambiguate_executable status ex =
475   match ex with
476   | TacticAst.Tactical (loc, tac) ->
477       let status, tac = disambiguate_tactical status tac in
478       status, (TacticAst.Tactical (loc, tac))
479   | TacticAst.Command (loc, cmd) ->
480       let status, cmd = disambiguate_command status cmd in
481       status, (TacticAst.Command (loc, cmd))
482   | TacticAst.Macro (_, mac) -> 
483       command_error 
484         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
485                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
486
487 let disambiguate_comment status c = 
488   match c with
489   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
490   | TacticAst.Code (loc,ex) -> 
491         let status, ex = disambiguate_executable status ex in
492         status, TacticAst.Code (loc,ex)
493         
494 let disambiguate_statement status statement =
495   match statement with
496   | TacticAst.Comment (loc,c) -> 
497         let status, c = disambiguate_comment status c in
498         status, TacticAst.Comment (loc,c)
499   | TacticAst.Executable (loc,ex) -> 
500         let status, ex = disambiguate_executable status ex in
501         status, TacticAst.Executable (loc,ex)
502   
503 let eval_ast status ast =
504   let status,st = disambiguate_statement status ast in
505   (* this disambiguation step should be deferred to support tacticals *)
506   eval status st
507
508 let eval_from_stream status str =
509   let st = CicTextualParser2.parse_statement str in
510   eval_ast status st
511   
512 let eval_string status str =
513   eval_from_stream status (Stream.of_string str) 
514
515 let default_options () =
516   let options =
517     StringMap.add "baseuri"
518       (String
519         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
520       no_options
521   in
522   let options =
523     StringMap.add "basedir"
524       (String (Helm_registry.get "matita.basedir" ))
525       options
526   in
527   options
528
529 let initial_status =
530   lazy {
531     aliases = DisambiguateTypes.empty_environment;
532     proof_status = No_proof;
533     options = default_options ();
534     coercions = [];
535     objects = [];
536   }
537