max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(init/meta/decl_cmds): avoid blocking

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-27 17:52:45 +01:00
parent e839080834
commit 3804722b91
2 changed files with 17 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/init/meta/decl_cmds.lean
View file

@ -36,17 +36,17 @@ e^.replace (λ e d,
creates the declaration
lemma g_lemma : forall a, g a > 0 := ... -/
meta def copy_decl_updating_type (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
do env ← get_env,
decl ← returnex $ env^.get src_decl_name,
new_type ← return $ apply_replacement replacements decl^.type,
new_value ← return $ expr.const src_decl_name (decl^.univ_params^.for level.param),
add_decl (((decl^.to_definition^.update_type new_type)^.update_name new_decl_name)^.update_value new_value),
return ()
do env ← get_env,
decl ← returnex $ env^.get src_decl_name,
decl ← return $ decl^.update_name $ new_decl_name,
decl ← return $ decl^.update_type $ apply_replacement replacements decl^.type,
decl ← return $ decl^.update_value $ expr.const src_decl_name (decl^.univ_params^.for level.param),
add_decl decl
meta def copy_decl_using (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
do env ← get_env,
decl ← returnex $ env^.get src_decl_name,
new_type ← return $ apply_replacement replacements decl^.type,
new_value ← return $ task.map (apply_replacement replacements) decl^.value_task,
add_decl (((decl^.to_definition^.update_type new_type)^.update_name new_decl_name)^.update_value_task new_value),
return ()
do env ← get_env,
decl ← returnex $ env^.get src_decl_name,
decl ← return $ decl^.update_name $ new_decl_name,
decl ← return $ decl^.update_type $ apply_replacement replacements decl^.type,
decl ← return $ decl^.map_value $ apply_replacement replacements,
add_decl decl

5
library/init/meta/declaration.lean
View file

@ -107,6 +107,11 @@ meta def declaration.update_value_task : declaration → task expr → declarati
| (declaration.thm n ls t v) new_v := declaration.thm n ls t new_v
| d new_v := d
meta def declaration.map_value : declaration → (expr → expr) → declaration
| (declaration.defn n ls t v h tr) f := declaration.defn n ls t (f v) h tr
| (declaration.thm n ls t v) f := declaration.thm n ls t (task.map f v)
| d f := d
meta def declaration.to_definition : declaration → declaration
| (declaration.cnst n ls t tr) := declaration.defn n ls t (default expr) reducibility_hints.abbrev tr
| (declaration.ax n ls t) := declaration.thm n ls t (task.pure (default expr))