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