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