]> matita.cs.unibo.it Git - helm.git/commitdiff
The status has been extended with a "universe", that is a
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:06:57 +0000 (14:06 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:06:57 +0000 (14:06 +0000)
discrimination-tree structure indexing all defined objects.
The universe is functional (hope so).

helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli

index 4539029af26e1b6d276904701c2a414d81693cc7..582ad112d667e559aec395cde9a3c992731656ff 100644 (file)
@@ -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
@@ -304,7 +306,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 +619,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 +654,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 +694,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;
index 7b4bdfb5e5c04f43bfc44ccd11debbb28cf5a04e..9581dc9d6a708bc5522b8d145db045977ae40cf3 100644 (file)
 
 open Printf
 
+let uris_for_inductive_type uri obj =
+  match obj with 
+    | Cic.InductiveDefinition(types,_,_,_) ->
+       let suri = UriManager.string_of_uri uri in
+       let uris,_ =
+         List.fold_left
+           (fun (acc,i) (_,_,_,constructors)->
+              let is = string_of_int i in           
+              let newacc,_ =
+                List.fold_left
+                  (fun (acc,j) _ ->
+                     let js = string_of_int j in
+                       UriManager.uri_of_string
+                         (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1) 
+                  (acc,1) constructors
+              in
+              newacc,i+1)
+           ([],1) types 
+       in uris
+    | _ -> [uri] 
+    
 let add_obj refinement_toolkit uri obj status =
  let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
-  {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
+ let add_to_universe (universe,status) uri =
+   let term = CicUtil.term_of_uri uri in
+   let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+(* prop filtering
+   let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
+   prerr_endline (CicPp.ppterm term);
+   prerr_endline (CicPp.ppterm sort);
+   let tkeys = 
+     if sort = Cic.Sort(Cic.Prop) then Universe.keys [] ty 
+     else [] 
+   in
+*)
+   let tkeys = Universe.keys [] ty in
+   let index_cmd = 
+     List.map 
+       (fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
+       tkeys
+   in
+(* prop filtering 
+   let universe = 
+     if sort = Cic.Sort(Cic.Prop) then 
+       Universe.index_term_and_unfolded_term universe [] term ty
+     else universe  
+*)
+   let universe = Universe.index_term_and_unfolded_term universe [] term ty
+   in
+   let status = GrafiteTypes.add_moo_content index_cmd status in
+   (universe,status)
+ in
+ let universe,status =
+   List.fold_left add_to_universe 
+     (status.GrafiteTypes.universe,status) 
+     ((uris_for_inductive_type uri obj)@lemmas) in
+  {status with 
+     GrafiteTypes.objects = uri::status.GrafiteTypes.objects;
+     GrafiteTypes.universe = universe},
    lemmas
 
 let add_coercion refinement_toolkit ~add_composites status uri arity =
@@ -60,8 +116,8 @@ let time_travel ~present ~past =
   let coercions_to_remove =
    uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions
   in
-   List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
-   List.iter LibrarySync.remove_obj objs_to_remove
+  List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
+  List.iter LibrarySync.remove_obj objs_to_remove
 
 let init () =
   LibrarySync.remove_all_coercions ();
@@ -72,4 +128,5 @@ let init () =
     options = GrafiteTypes.no_options;
     objects = [];
     coercions = [];
+    universe = Universe.empty;
   }
index 0d59e4b469351dc7d39e2b2da2b0c5996780df82..6e1c299e42dbf44dc332ca92b71018395cfec2df 100644 (file)
@@ -57,6 +57,7 @@ type status = {
   options: options;
   objects: UriManager.uri list;
   coercions: UriManager.uri list;
+  universe:Universe.universe;  
 }
 
 let get_current_proof status =
index a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f..b26c0ca21fb6e13bf408dbaf6f06fd54fd6fba0e 100644 (file)
@@ -53,7 +53,8 @@ type status = {
   proof_status: proof_status;                             (** logical status *)
   options: options;
   objects: UriManager.uri list;  (** in-scope objects *)
-  coercions: UriManager.uri list;                      (** defined coercions *)
+  coercions: UriManager.uri list; (** defined coercions *)
+  universe:Universe.universe;  (** universe of terms used by auto *)
 }
 
 val dump_status : status -> unit