| GrafiteAst.Merge _ -> NTactics.merge_tac
;;
+let eval_ng_non_punct (_text, _prefix_len, punct) =
+ match punct with
+ | GrafiteAst.Focus (_,l) -> NTactics.focus_tac l
+ | GrafiteAst.Unfocus _ -> NTactics.unfocus_tac
+ | GrafiteAst.Skip _ -> NTactics.skip_tac
+;;
+
let eval_ng_tac (text, prefix_len, tac) =
match tac with
| GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
else
let obj =
prerr_endline "CSC: here we should fix the height!!!";
- uri,height,[],[],
- NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst) obj
+ (uri,height,[],[],
+ NCicUntrusted.map_obj_kind (NCicUntrusted.apply_subst subst)
+ obj) in
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ let objs = NCicElim.mk_elims obj in
+ let uris =
+ uri::
+ List.map
+ (fun (uri,_,_,_,_) as obj ->
+ NCicTypeChecker.typecheck_obj obj;
+ NCicLibrary.add_obj uri obj;
+ uri
+ ) objs
in
- NCicTypeChecker.typecheck_obj obj;
- NCicLibrary.add_obj uri obj;
{status with
GrafiteTypes.ng_status =
- GrafiteTypes.CommandMode lexicon_status },`New [uri]
+ GrafiteTypes.CommandMode lexicon_status },`New uris
| _ -> raise (GrafiteTypes.Command_error "Not in proof mode"))
| GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) ->
Setoids.add_relation id a aeq refl sym trans;
in
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),`Old []
+ | GrafiteAst.NNonPunctuationTactical (_, non_punct, punct) ->
+ (match status.GrafiteTypes.ng_status with
+ | GrafiteTypes.CommandMode _ -> assert false
+ | GrafiteTypes.ProofMode nstatus ->
+ let nstatus = eval_ng_non_punct (text,prefix_len,non_punct) nstatus in
+ let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
+ NTacStatus.pp_tac_status nstatus;
+ { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
+ `New [])
| GrafiteAst.Command (_, cmd) ->
eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
| GrafiteAst.Macro (loc, macro) ->
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+
+let fresh_name =
+ let i = ref 0 in
+ function () ->
+ incr i;
+ "x_" ^ string_of_int !i
+;;
+
+let mk_id id =
+ let id = if id = "_" then fresh_name () else id in
+ CicNotationPt.Ident (id,None)
+;;
+
+(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
+ the return type is a sort *)
+let rec my_split_prods ~subst context n te =
+ match (n, NCicReduction.whd ~subst context te) with
+ | (0, _) -> context,te
+ | (n, NCic.Prod (name,so,ta)) ->
+ my_split_prods ~subst ((name,(NCic.Decl so))::context) (n - 1) ta
+ | (n, _) when n <= 0 -> context,te
+ | (_, _) -> raise (Failure "my_split_prods")
+;;
+
+let mk_elims (uri,_,_,_,obj) =
+ match obj with
+ NCic.Inductive (true,leftno,[it],_) ->
+ let _,ind_name,ty,cl = it in
+ let rec_name = ind_name ^ "_rect" in
+ let rec_name = mk_id rec_name in
+ let name_of_k id = mk_id ("H_" ^ id) in
+ let p_name = mk_id "Q_" in
+ let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+ let params = List.rev_map (function name,_ -> mk_id name) params in
+ let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
+ let rec_arg = mk_id (fresh_name ()) in
+ let args = List.rev_map (function name,_ -> mk_id name) args in
+ let p_ty =
+ List.fold_right
+ (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
+ (CicNotationPt.Binder
+ (`Forall,
+ (rec_arg,Some (CicNotationPt.Appl (mk_id ind_name :: params @ args))),
+ CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in
+ let args = args @ [rec_arg] in
+ let k_names = List.map (function _,name,_ -> name_of_k name) cl in
+ let final_params =
+ List.map (function name -> name, None) params @
+ [p_name,Some p_ty] @
+ List.map (function name -> name, None) k_names @
+ List.map (function name -> name, None) args in
+ let ty = Some (CicNotationPt.Appl (p_name :: args)) in
+ let branches =
+ List.map
+ (function (_,name,ty) ->
+ let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+ let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
+ let cargs_and_recursive_args =
+ List.rev_map
+ (function
+ name,NCic.Def _ -> assert false
+ | name,NCic.Decl (NCic.Const nref)
+ | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
+ when
+ let NReference.Ref (uri',_) = nref in
+ NUri.eq uri uri'
+ ->
+ let name = mk_id name in
+ name, Some (
+ CicNotationPt.Appl
+ (rec_name ::
+ params @
+ [p_name] @
+ k_names @
+ List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
+ [name]))
+ | name,_ -> mk_id name,None
+ ) cargs in
+ let cargs,recursive_args = List.split cargs_and_recursive_args in
+ let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
+ CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
+ CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
+ ) cl
+ in
+ let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
+ let where = List.length final_params - 1 in
+ let res =
+ CicNotationPt.LetRec (`Inductive,
+ [final_params, (rec_name,ty), bo, where], rec_name)
+ in
+ prerr_endline (CicNotationPp.pp_term res);
+ prerr_endline "#####";
+ prerr_endline
+ (BoxPp.render_to_string
+ ~map_unicode_to_tex:false
+ (function x::_ -> x | _ -> assert false)
+ 80 (CicNotationPres.render (Hashtbl.create 0)
+ (TermContentPres.pp_ast res)));
+
+ []
+ | _ -> []
+;;
projects / helm.git / commitdiff