Declarative language ported to new auto (with Universes).

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 4539029af26e1b6d276904701c2a414d81693cc7..a8ee6752ce9cc5a54e45f0add54acee68504422d 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -56,16 +56,18 @@ let namer_of names =
     end else
       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
 
-let tactic_of_ast ast =
+let tactic_of_ast status ast =
   let module PET = ProofEngineTypes in
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.ApplyS (_, term, params) ->
      Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
+       ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
+       ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -158,10 +160,13 @@ let tactic_of_ast ast =
   | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
   | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
-     Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) t ty id t1
+     Declarative.by_term_we_proved ~dbd:(LibraryDb.instance())
+      ~universe:status.GrafiteTypes.universe t ty id t1
   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
      Declarative.we_need_to_prove t id t2
-  | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) t
+  | GrafiteAst.Bydone (_, t) ->
+     Declarative.bydone ~dbd:(LibraryDb.instance())
+      ~universe:status.GrafiteTypes.universe t
   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
      Declarative.we_proceed_by_induction_on t t1
   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
@@ -171,7 +176,8 @@ let tactic_of_ast ast =
   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
   | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
-     Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) termine t1 t2 cont
+     Declarative.rewritingstep ~dbd:(LibraryDb.instance ())
+      ~universe:status.GrafiteTypes.universe termine t1 t2 cont
 
 let classify_tactic tactic = 
   match tactic with
@@ -304,7 +310,7 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
  let proof = GrafiteTypes.get_current_proof status in
  let proof_status = proof, goal in
  let needs_reordering, always_opens_a_goal = classify_tactic tactic in
- let tactic = tactic_of_ast tactic in
+ let tactic = tactic_of_ast status tactic in
  (* apply tactic will change the lexicon_status ... *)
 (* prerr_endline "apply_tactic bassa"; *)
  let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
@@ -617,6 +623,22 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
  let status,uris =
   match cmd with
+  | GrafiteAst.Index (loc,None,uri) -> 
+       assert false (* TODO: for user input *)
+  | GrafiteAst.Index (loc,Some key,uri) -> 
+      let universe = Universe.index 
+       status.GrafiteTypes.universe key (CicUtil.term_of_uri uri) in
+      let status = {status with GrafiteTypes.universe = universe} in
+(* debug
+      let msg =
+       let candidates = Universe.get_candidates status.GrafiteTypes.universe key in
+       ("candidates for " ^ (CicPp.ppterm key) ^ " = " ^ 
+         (String.concat "\n" (List.map CicPp.ppterm candidates))) 
+     in
+     prerr_endline msg;
+*)
+      let status = GrafiteTypes.add_moo_content [cmd] status in
+      status,[] 
   | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
      eval_coercion status ~add_composites uri arity
   | GrafiteAst.Default (loc, what, uris) as cmd ->
@@ -636,6 +658,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      let status = eval_from_moo.efm_go status moopath in
+(* debug
+     let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
+     let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+     let nat = Cic.MutInd(nat_uri,0,[]) in
+     let zero = Cic.MutConstruct(nat_uri,0,1,[]) in
+     let succ = Cic.MutConstruct(nat_uri,0,2,[]) in
+     let fake= Cic.Meta(-1,[]) in
+     let term= Cic.Appl [Cic.Const (lt_uri,[]);zero;Cic.Appl[succ;zero]] in     let msg =
+       let candidates = Universe.get_candidates status.GrafiteTypes.universe term in
+       ("candidates for " ^ (CicPp.ppterm term) ^ " = " ^ 
+         (String.concat "\n" (List.map CicPp.ppterm candidates))) 
+     in
+     prerr_endline msg;
+*)
      status,[]
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,p,_ = GrafiteTypes.get_current_proof status in
@@ -662,7 +698,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
       let status, lemmas = add_obj uri obj status in
-       {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
+       {status with 
+         GrafiteTypes.proof_status = GrafiteTypes.No_proof},
         uri::lemmas
   | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> 
      Setoids.add_relation id a aeq refl sym trans;