]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteEngine.ml
Added initial support for inversion principles in Matita NG.
[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml
index b1cc9d671f5acd17f0fcbf64931c4b220c3e7fd2..0806057ec14ab1d67189dba4832028c6509576db 100644 (file)
@@ -33,6 +33,7 @@ exception IncludedFileNotCompiled of string * string
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * (Cic.term,Cic.lazy_term) GrafiteAst.macro)
+exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a
 
@@ -40,6 +41,11 @@ type options = {
   do_heavy_checks: bool ; 
 }
 
+let concat_nuris uris nuris =
+   match uris,nuris with
+   | `New uris, `New nuris -> `New (nuris@uris)
+   | _ -> assert false
+;;
 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   * names as long as they are available, then it fallbacks to name generation
   * using FreshNamesGenerator module *)
@@ -475,24 +481,46 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+ let basic_eval_unification_hint (t,n) 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
   NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
 ;;
 
 let eval_unification_hint status t n = 
- let estatus = GrafiteTypes.get_estatus status in
- let metasenv,subst,estatus,t =
-  GrafiteDisambiguate.disambiguate_nterm None estatus [] [] [] ("",0,t) in
+ let metasenv,subst,status,t =
+  GrafiteDisambiguate.disambiguate_nterm None status [] [] [] ("",0,t) in
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
- let status = GrafiteTypes.set_estatus estatus status in
- let estatus =
-  basic_eval_unification_hint (t,n) (GrafiteTypes.get_estatus status) in
- let dump = inject_unification_hint (t,n)::estatus#dump in
- let estatus = estatus#set_dump dump in
- let status = GrafiteTypes.set_estatus estatus status in
+ let status = basic_eval_unification_hint (t,n) status in
+ let dump = inject_unification_hint (t,n)::status#dump in
+ let status = status#set_dump dump in
+  status,`New []
+;;
+
+let basic_eval_add_constraint (u1,u2) status =
+ NCicLibrary.add_constraint status u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (u1,u2) 
+       ~refresh_uri_in_universe 
+       ~refresh_uri_in_term
+ =
+  let u1 = refresh_uri_in_universe u1 in 
+  let u2 = refresh_uri_in_universe u2 in 
+  basic_eval_add_constraint (u1,u2)
+ in
+  NRstatus.Serializer.register "constraints" basic_eval_add_constraint
+;;
+
+let eval_add_constraint status u1 u2 = 
+ let status = basic_eval_add_constraint (u1,u2) status in
+ let dump = inject_constraint (u1,u2)::status#dump in
+ let status = status#set_dump dump in
   status,`Old []
 ;;
 
@@ -520,7 +548,7 @@ let eval_coercion status ~add_composites uri arity saturations =
  let status, lemmas =
   GrafiteSync.add_coercion ~add_composites 
     ~pack_coercion_obj:CicRefine.pack_coercion_obj
-   status uri arity saturations (GrafiteTypes.get_baseuri status) in
+   status uri arity saturations status#baseuri in
  let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in
  let status = GrafiteTypes.add_moo_content [moo_content] status in 
   add_coercions_of_lemmas lemmas status
@@ -603,7 +631,8 @@ let eval_ng_punct (_text, _prefix_len, punct) =
   | GrafiteAst.Merge _ -> NTactics.merge_tac 
 ;;
 
-let rec eval_ng_tac (text, prefix_len, tac) =
+let eval_ng_tac tac =
+ let rec aux f (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
   | GrafiteAst.NAssert (_loc, seqs) ->
@@ -629,6 +658,10 @@ let rec eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
+  | GrafiteAst.NConstructor (_loc,num,args) -> 
+     NTactics.constructor_tac 
+       ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
+  | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -639,6 +672,7 @@ let rec eval_ng_tac (text, prefix_len, tac) =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
   | GrafiteAst.NLetIn (_loc,where,what,name) ->
       NTactics.letin_tac ~where:(text,prefix_len,where) 
         ~what:(text,prefix_len,what) name
@@ -655,91 +689,201 @@ let rec eval_ng_tac (text, prefix_len, tac) =
   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
-      (eval_ng_tac (text, prefix_len, tac))
+      (aux f (text, prefix_len, tac))
   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
+  | GrafiteAst.NBlock (_,l) -> 
+      NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
+  |GrafiteAst.NRepeat (_,tac) ->
+      NTactics.repeat_tac (f f (text, prefix_len, tac))
+ in
+  aux aux tac (* trick for non uniform recursion call *)
 ;;
       
-let subst_metasenv_and_fix_names s =
-  let u,h,metasenv, subst,o = s#obj in
+let subst_metasenv_and_fix_names status =
+  let u,h,metasenv, subst,o = status#obj in
   let o = 
     NCicUntrusted.map_obj_kind ~skip_body:true 
      (NCicUntrusted.apply_subst subst []) o
   in
-   s#set_obj (u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
+   status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
 ;;
 
 let rec eval_ncommand opts status (text,prefix_len,cmd) =
   match cmd with
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
+  | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->
+      NCicCoercDeclaration.eval_ncoercion status name t ty source target
   | GrafiteAst.NQed loc ->
-      (match status#ng_status with
-       | GrafiteTypes.ProofMode estatus ->
-          let uri,height,menv,subst,obj_kind = estatus#obj in
-           if menv <> [] then
-            raise
-             (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
-           else
-            let obj_kind =
-             NCicUntrusted.map_obj_kind 
-              (NCicUntrusted.apply_subst subst []) obj_kind in
-            let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
-            (* fix the height inside the object *)
-            let rec fix () = function 
-              | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
-                 NCic.Const (NReference.reference_of_spec u
-                  (match spec with
-                  | NReference.Def _ -> NReference.Def height
-                  | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
-                  | NReference.CoFix _ -> NReference.CoFix height
-                  | NReference.Ind _ | NReference.Con _
-                  | NReference.Decl as s -> s))
-              | t -> NCicUtils.map (fun _ () -> ()) () fix t
-            in
-            let obj_kind = 
-              match obj_kind with
-              | NCic.Fixpoint _ -> 
-                  NCicUntrusted.map_obj_kind (fix ()) obj_kind 
-              | _ -> obj_kind
-            in
-            let obj = uri,height,[],[],obj_kind in
-             NCicTypeChecker.typecheck_obj obj;
-             let estatus = NCicLibrary.add_obj estatus uri obj in
-             let objs = NCicElim.mk_elims obj in
-             let timestamp,uris_rev =
-               List.fold_left
-                (fun (estatus,uris_rev) (uri,_,_,_,_) as obj ->
-                  NCicTypeChecker.typecheck_obj obj;
-                  let estatus = NCicLibrary.add_obj estatus uri obj in
-                   estatus,uri::uris_rev
-                ) (estatus,[]) objs in
-             let uris = uri::List.rev uris_rev in
-              status#set_ng_status
-               (GrafiteTypes.CommandMode (estatus :> NEstatus.status)),`New uris
-       | _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
+     if status#ng_mode <> `ProofMode then
+      raise (GrafiteTypes.Command_error "Not in proof mode")
+     else
+      let uri,height,menv,subst,obj_kind = status#obj in
+       if menv <> [] then
+        raise
+         (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
+       else
+        let obj_kind =
+         NCicUntrusted.map_obj_kind 
+          (NCicUntrusted.apply_subst subst []) obj_kind in
+        let height = NCicTypeChecker.height_of_obj_kind uri [] obj_kind in
+        (* fix the height inside the object *)
+        let rec fix () = function 
+          | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
+             NCic.Const (NReference.reference_of_spec u
+              (match spec with
+              | NReference.Def _ -> NReference.Def height
+              | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+              | NReference.CoFix _ -> NReference.CoFix height
+              | NReference.Ind _ | NReference.Con _
+              | NReference.Decl as s -> s))
+          | t -> NCicUtils.map (fun _ () -> ()) () fix t
+        in
+        let obj_kind = 
+          match obj_kind with
+          | NCic.Fixpoint _ -> 
+              NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+          | _ -> obj_kind
+        in
+        let obj = uri,height,[],[],obj_kind in
+        let old_status = status in
+        let status = NCicLibrary.add_obj status obj in
+        HLog.message ("New object: " ^ NUri.string_of_uri uri);
+         (try
+       (*prerr_endline (NCicPp.ppobj obj);*)
+           let boxml = NCicElim.mk_elims obj in
+           let boxml = boxml @ NCicElim.mk_projections obj in
+(*
+           let objs = [] in
+           let timestamp,uris_rev =
+             List.fold_left
+              (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
+                let status = NCicLibrary.add_obj status obj in
+                 status,uri::uris_rev
+              ) (status,[]) objs in
+           let uris = uri::List.rev uris_rev in
+*)
+           let status = status#set_ng_mode `CommandMode in
+           let status = LexiconSync.add_aliases_for_objs status (`New [uri]) in
+           let status,uris =
+            List.fold_left
+             (fun (status,uris) boxml ->
+               try
+                let status,nuris =
+                 eval_ncommand opts status
+                  ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
+                in
+                status, concat_nuris uris nuris
+               with
+               | MultiPassDisambiguator.DisambiguationError _ 
+               | NCicTypeChecker.TypeCheckerFailure _ ->
+                  HLog.warn "error in generating projection/eliminator";
+                  status,uris
+             ) (status,`New [] (* uris *)) boxml in
+           let coercions =
+            match obj with
+              _,_,_,_,NCic.Inductive
+               (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
+               ->
+                HExtlib.filter_map
+                 (fun (name,is_coercion,arity) ->
+                   if is_coercion then Some(name,leftno,arity) else None) fields
+            | _ -> [] in
+           let status,uris =
+            List.fold_left
+             (fun (status,uris) (name,cpos,arity) ->
+               try
+                 let metasenv,subst,status,t =
+                  GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                   ("",0,CicNotationPt.Ident (name,None)) in
+                 assert (metasenv = [] && subst = []);
+                 let status, nuris = 
+                   NCicCoercDeclaration.
+                     basic_eval_and_record_ncoercion_from_t_cpos_arity 
+                      status (name,t,cpos,arity)
+                 in
+                 let uris = concat_nuris nuris uris in
+                 status, uris
+               with MultiPassDisambiguator.DisambiguationError _-> 
+                 HLog.warn ("error in generating coercion: "^name);
+                 status, uris) 
+             (status,uris) coercions
+           in
+            status,uris
+          with
+           exn ->
+            NCicLibrary.time_travel old_status;
+            raise exn)
+  | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+       let tgt_uri_ext, old_ok = 
+         match NCicEnvironment.get_checked_obj src_uri with
+         | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
+         | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
+         | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
+         | _ -> assert false
+       in
+       let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
+       let map = (src_uri, tgt_uri) :: map in
+       let ok = 
+         let rec subst () = function
+           | NCic.Meta _ -> assert false
+           | NCic.Const (NReference.Ref (u,spec)) as t ->
+               (try NCic.Const 
+                 (NReference.reference_of_spec (List.assoc u map)spec)
+               with Not_found -> t)
+           | t -> NCicUtils.map (fun _ _ -> ()) () subst t
+         in
+         NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
+       in
+       let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
+       let status = status#set_obj (tgt_uri,0,[],[],ok) in
+       (*prerr_endline (NCicPp.ppobj (tgt_uri,0,[],[],ok));*)
+       let status = status#set_stack ninitial_stack in
+       let status = subst_metasenv_and_fix_names status in
+       let status = status#set_ng_mode `ProofMode in
+       eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
   | GrafiteAst.NObj (loc,obj) ->
-     let estatus =
-       match status#ng_status with
-       | GrafiteTypes.ProofMode _ -> assert false
-       | GrafiteTypes.CommandMode es -> es 
-     in
-     let estatus,obj =
-      GrafiteDisambiguate.disambiguate_nobj estatus
-       ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in
-     let uri,height,nmenv,nsubst,nobj = obj in
-     let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
-     let status =
-      status#set_ng_status
-       (GrafiteTypes.ProofMode
-         (subst_metasenv_and_fix_names
-           ((new NTacStatus.status obj ninitial_stack)#set_estatus estatus)))
-     in
-     (match nmenv with
-         [] ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let status,obj =
+       GrafiteDisambiguate.disambiguate_nobj status
+        ~baseuri:status#baseuri (text,prefix_len,obj) in
+      let uri,height,nmenv,nsubst,nobj = obj in
+      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
+      let status = status#set_obj obj in
+      let status = status#set_stack ninitial_stack in
+      let status = subst_metasenv_and_fix_names status in
+      let status = status#set_ng_mode `ProofMode in
+      (match nmenv with
+          [] ->
+           eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+        | _ -> status,`New [])
+  | GrafiteAst.NInverter (loc, name, indty) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let status = status#set_ng_mode `ProofMode in
+      let metasenv,subst,status,indty =
+       GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+      let _,leftno,tys,_,_ = match indty with
+          NCic.Const r -> NCicEnvironment.get_checked_indtys r
+        | _ -> assert false in
+      let it = match tys with
+          hd::tl -> hd
+        | _ -> assert false
+      in
+     let status,obj =
+      NInversion.mk_inverter name it leftno status status#baseuri in
+     let _,_,menv,_,_ = obj in
+     (match menv with
+        [] ->
           eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
-       | _ -> status,`New [])
-  | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
-      status, `New [u1;u2]
+      | _ -> assert false)
+  | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
+      eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
@@ -792,7 +936,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      in
       res,`Old uris
   | GrafiteAst.Inverter (loc, name, indty, params) ->
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
      let indty_uri = 
        try CicUtil.uri_of_term indty
@@ -806,39 +950,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, _, baseuri) ->
-     let moopath_rw, moopath_r = 
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true,
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:false
-     in
-     let moopath = 
-       if Sys.file_exists moopath_r then moopath_r else
-         if Sys.file_exists moopath_rw then moopath_rw else
-           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
+  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
+     (* Old Include command is not recursive; new one is *)
+     let status =
+      if new_or_old = `OldAndNew then
+       let moopath_rw, moopath_r = 
+        LibraryMisc.obj_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:true,
+        LibraryMisc.obj_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:false in
+       let moopath = 
+        if Sys.file_exists moopath_r then moopath_r else
+          if Sys.file_exists moopath_rw then moopath_rw else
+            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
+       in
+        eval_from_moo.efm_go status moopath
+      else
+       status
      in
-     let status = eval_from_moo.efm_go status moopath in
-     let estatus = GrafiteTypes.get_estatus status in
-     let estatus =
+      let status =
        NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        estatus in
-     let status = GrafiteTypes.set_estatus estatus status 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,`Old []
+        status in
+      let status =
+       GrafiteTypes.add_moo_content
+        [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+      in
+       status,`Old []
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
       prerr_endline (Auto.pp_proofterm (Lazy.force p));
@@ -881,7 +1018,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
           ".ind",
           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
        | _ -> assert false in
-     let buri = GrafiteTypes.get_baseuri status in 
+     let buri = status#baseuri in 
      let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in
      let obj = CicRefine.pack_coercion_obj obj in
      let metasenv = GrafiteTypes.get_proof_metasenv status in
@@ -961,18 +1098,17 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       eval_tactical status
        (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
   | GrafiteAst.NTactic (_(*loc*), tacl) ->
-      (match status#ng_status with
-      | GrafiteTypes.CommandMode _ -> assert false
-      | GrafiteTypes.ProofMode nstatus ->
-         let nstatus =
-          List.fold_left 
-            (fun nstatus tac ->
-              let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
-              subst_metasenv_and_fix_names nstatus)
-            nstatus tacl
-         in
-          status#set_ng_status (GrafiteTypes.ProofMode nstatus),
-         `New [])
+      if status#ng_mode <> `ProofMode then
+       raise (GrafiteTypes.Command_error "Not in proof mode")
+      else
+       let status =
+        List.fold_left 
+          (fun status tac ->
+            let status = eval_ng_tac (text,prefix_len,tac) status in
+            subst_metasenv_and_fix_names status)
+          status tacl
+       in
+        status,`New []
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
       eval_tactical status
@@ -986,6 +1122,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       eval_ncommand opts status (text,prefix_len,cmd)
   | GrafiteAst.Macro (loc, macro) ->
      raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
+  | GrafiteAst.NMacro (loc, macro) ->
+     raise (NMacro (loc,macro))
 
 } and eval_from_moo = {efm_go = fun status fname ->
   let ast_of_cmd cmd =