- Procedural: bugfix in pattern generation for elim/rewrite, better debug output, applications are flattened before alpha-conversion to hide a bug of the double type inference :( (it generates folded applications)
- applyTransformation: coercions are shown when rendering a tactic because Procedural is not aware of coercions :(
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
-procedural1.cmo: procedural1.cmi
-procedural1.cmx: procedural1.cmi
+procedural1.cmo: proceduralTypes.cmi procedural1.cmi
+procedural1.cmx: proceduralTypes.cmx procedural1.cmi
procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi
procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
-procedural1.cmo: procedural1.cmi
-procedural1.cmx: procedural1.cmi
+procedural1.cmo: proceduralTypes.cmi procedural1.cmi
+procedural1.cmx: proceduralTypes.cmx procedural1.cmi
procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi
procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
if args = [] then b, hd else b, C.AAppl ("", hd :: args)
let mk_convert st ?name sty ety note =
+ let ppterm t =
+ let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a
+ in
let e = Cn.hole "" in
let csty, cety = H.cic sty, H.cic ety in
- let script =
+ let note =
if !debug then
let sname = match name with None -> "" | Some (id, _) -> id in
- let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
- note sname (Pp.ppterm csty) (Pp.ppterm cety)
- in
- [T.Note note]
- else []
+ Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s"
+ note sname (ppterm csty) (ppterm cety)
+ else ""
in
- assert (Ut.is_sober st.context csty);
- assert (Ut.is_sober st.context cety);
- if Ut.alpha_equivalence csty cety then script else
+ if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else
let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
match name with
- | None -> T.Change (sty, ety, None, e, "") :: script
+ | None -> [T.Change (sty, ety, None, e, note)]
| Some (id, i) ->
begin match get_entry st id with
| C.Def _ -> assert false (* T.ClearBody (id, "") :: script *)
| C.Decl _ ->
- T.Change (ety, sty, Some (id, Some id), e, "") :: script
+ [T.Change (ety, sty, Some (id, Some id), e, note)]
end
let convert st ?name v =
in
ann_term c
-let clear_absts m =
- let rec aux k n = function
- | C.AImplicit (_, None) as t -> t
- | C.ALambda (id, s, v, t) when k > 0 ->
- C.ALambda (id, s, v, aux (pred k) n t)
- | C.ALambda (_, _, _, t) when n > 0 ->
- aux 0 (pred n) (lift 1 (-1) t)
- | t when n > 0 ->
- Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t));
- assert false
- | t -> t
- in
- aux m
+let mk_arel k = C.ARel ("", "", k, "")
+
+let mk_aappl ts = C.AAppl ("", ts)
+
+let rec clear_absts f n k = function
+ | t when n = 0 -> f k t
+ | C.ALambda (_, _, _, t) -> clear_absts f (pred n) (succ k) t
+ | t ->
+ let u = match mk_aappl [lift (succ k) 1 t; mk_arel (succ k)] with
+ | C.AAppl (_, [ C.AAppl (id, ts); t]) -> C.AAppl (id, ts @ [t])
+ | t -> t
+ in
+ clear_absts f (pred n) (succ k) u
let hole id = C.AImplicit (id, Some `Hole)
| C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl)
| C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl)
in
- gen_term 0
+ gen_term
let mk_pattern psno predicate =
- let body = generalize psno predicate in
- clear_absts 0 psno body
+ clear_absts (generalize psno) psno 0 predicate
let get_clears c p xtypes =
let meta = C.Implicit None in
let cic = D.deannotate_term
+let flatten_appls =
+ let rec flatten_xns (uri, t) = uri, flatten_term t
+ and flatten_ms = function
+ | None -> None
+ | Some t -> Some (flatten_term t)
+ and flatten_fix (name, i, ty, bo) =
+ name, i, flatten_term ty, flatten_term bo
+ and flatten_cofix (name, ty, bo) =
+ name, flatten_term ty, flatten_term bo
+ and flatten_term = function
+ | C.Sort _ as t -> t
+ | C.Implicit _ as t -> t
+ | C.Rel _ as t -> t
+ | C.Const (uri, xnss) -> C.Const (uri, List.map flatten_xns xnss)
+ | C.Var (uri, xnss) -> C.Var (uri, List.map flatten_xns xnss)
+ | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, List.map flatten_xns xnss)
+ | C.MutConstruct (uri, tyno, consno, xnss) -> C.MutConstruct (uri, tyno, consno, List.map flatten_xns xnss)
+ | C.Meta (i, mss) -> C.Meta(i, List.map flatten_ms mss)
+(* begin flattening *)
+ | C.Appl [t] -> flatten_term t
+ | C.Appl (C.Appl ts1 :: ts2) -> flatten_term (C.Appl (ts1 @ ts2))
+ | C.Appl [] -> assert false
+(* end flattening *)
+ | C.Appl ts -> C.Appl (List.map flatten_term ts)
+ | C.Cast (te, ty) -> C.Cast (flatten_term te, flatten_term ty)
+ | C.MutCase (sp, i, outty, t, pl) -> C.MutCase (sp, i, flatten_term outty, flatten_term t, List.map flatten_term pl)
+ | C.Prod (n, s, t) -> C.Prod (n, flatten_term s, flatten_term t)
+ | C.Lambda (n, s, t) -> C.Lambda (n, flatten_term s, flatten_term t)
+ | C.LetIn (n, ty, s, t) -> C.LetIn (n, flatten_term ty, flatten_term s, flatten_term t)
+ | C.Fix (i, fl) -> C.Fix (i, List.map flatten_fix fl)
+ | C.CoFix (i, fl) -> C.CoFix (i, List.map flatten_cofix fl)
+ in
+ flatten_term
+
+let sober ?(flatten=false) c t =
+ if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
+
+let alpha_equivalence ?flatten c t1 t2 =
+ let t1 = sober ?flatten c t1 in
+ let t2 = sober ?flatten c t2 in
+ Ut.alpha_equivalence t1 t2
+
let occurs c ~what ~where =
let result = ref false in
let equality c t1 t2 =
- let r = Ut.alpha_equivalence t1 t2 in
+ let r = alpha_equivalence ~flatten:true c t1 t2 in
result := !result || r; r
in
let context, what, with_what = c, [what], [C.Rel 0] in
| [] -> c
| hd :: tl ->
let sname, w = map hd in
- let entry = Some (Cic.Name sname, C.Decl w) in
+ let entry = Some (C.Name sname, C.Decl w) in
add_entries map (entry :: c) tl
let get_sname c i =
try match List.nth c (pred i) with
- | Some (Cic.Name sname, _) -> sname
+ | Some (C.Name sname, _) -> sname
| _ -> assert false
with
| Failure _ -> assert false
| `Prop -> true
| _ -> false
with Not_found -> is_proof context (cic v)
+
val mk_fresh_name:
bool -> Cic.context -> Cic.name -> Cic.name
+
val list_fold_right_cps:
('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c
+
val list_fold_left_cps:
('b -> 'c) -> (('b -> 'c) -> 'b -> 'a -> 'c) -> 'b -> 'a list -> 'c
+
val list_map_cps:
('b list -> 'c) -> (('b -> 'c) -> 'a -> 'c) -> 'a list -> 'c
+
val identity:
'a -> 'a
+
val compose:
('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
val fst3:
'a * 'b * 'c -> 'a
+
val refine:
Cic.context -> Cic.term -> Cic.term
+
val get_type:
string -> Cic.context -> Cic.term -> Cic.term
+
val is_prop:
Cic.context -> Cic.term -> bool
+
val is_proof:
Cic.context -> Cic.term -> bool
+
val is_sort:
Cic.term -> bool
+
val is_unsafe:
int -> Cic.context * Cic.term -> bool
+
val is_not_atomic:
Cic.term -> bool
+
val is_atomic:
Cic.term -> bool
+
val get_ind_type:
UriManager.uri -> int -> int * Cic.inductiveType
+
val get_ind_names:
UriManager.uri -> int -> string list
+
val get_default_eliminator:
Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term
+
val get_ind_parameters:
Cic.context -> Cic.term -> Cic.term list * int
+
val cic:
Cic.annterm -> Cic.term
+
val occurs:
Cic.context -> what:Cic.term -> where:Cic.term -> bool
+
val name_of_uri:
UriManager.uri -> int option -> int option -> string
+
val cic_bc:
Cic.context -> Cic.term -> Cic.term
+
val acic_bc:
Cic.context -> Cic.annterm -> Cic.annterm
+
val is_acic_proof:
(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm ->
bool
+
+val alpha_equivalence:
+ ?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool
| C.LetIn (_, v, ty, t) ->
sober_term c (sober_term c (sober_term c g t) ty) v
| C.Appl []
- | C.Appl [_] -> fun b -> false
+ | C.Appl [_]
+ | C.Appl (C.Appl _ :: _) -> fun b -> false
| C.Appl ts -> sober_terms c g ts
| C.MutCase (_, _, t, v, ts) ->
sober_terms c (sober_term c (sober_term c g t) v) ts
val alpha_equivalence: Cic.term -> Cic.term -> bool
(* FG: Consistency Check
- * detects applications without arguments
+ * detects applications without arguments and folded applications
*)
val is_sober: Cic.context -> Cic.term -> bool
in
let aux = function
| G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm
- ->
+ ->
enable_notations false;
- let str = stm_pp stm in enable_notations true; str
+ let str = stm_pp stm in
+ enable_notations true;
+ str
(* FG: we disable notation for Inductive to avoid recursive notation *)
- | stm -> stm_pp stm
+ | G.Executable (_, G.Tactic _) as stm ->
+ let hc = !Acic2content.hide_coercions in
+ Acic2content.hide_coercions := false;
+ let str = stm_pp stm in
+ Acic2content.hide_coercions := hc;
+ str
+(* FG: we show coercion because the reconstruction is not aware of them *)
+ | stm -> stm_pp stm
in
let script =
Acic2Procedural.procedural_of_acic_object
<key name="theory_file"></key>
<key name="inline">logic/equality/symmetric_eq nodefaults</key>
<key name="inline">logic/equality/transitive_eq nodefaults</key>
+ <key name="inline">logic/equality/eq_elim_r nodefaults</key>
+ <key name="inline">logic/equality/eq_f nodefaults</key>
+ <key name="inline">logic/equality/eq_f' nodefaults</key>
</section>
</helm_registry>
projects / helm.git / commitdiff