little optimization

Author: gares

hb.elpi

@@ -104,8 +104,6 @@ if-MC-compat P :- get-option "mathcomp.axiom" S, !,
   P (some GR).
 if-MC-compat _.
 
-
-
 % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?)
 % Should we make this an HO predicate, eg "located->gref S L is-factory? GR"
 pred located->gref i:string, i:list located, o:gref.
@@ -116,10 +114,6 @@ located->gref S [loc-modpath _|_] _ :- coq.error S "should be a factory, but is
 located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but is a module type".
 located->gref S [] _ :- coq.error "Could not locate name" S.
 
-pred purge-id i:term, o:term.
-purge-id T T1 :-
-  (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1.
-
 % TODO: generalize/rename when we support parameters
 pred argument->gref i:argument, o:gref.
 argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR.
@@ -700,7 +694,7 @@ phant-fun-struct T Name S Params PF Out :- std.do! [
   mk-app (global S) Params SParams,
   mk-app SortProj Params SortProjParams,
   % Msg = {{lib:hb.nomsg}},
-  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SParams)}},
+  Msg = {{lib:hb.some (lib:hb.pair lib:hb.not_a_msg lp:SParams)}},
   (@pi-decl Name SParams s\ phant-fun-unify Msg T {mk-app SortProjParams [s]} (PF s) (UnifSI s)),
   phant-fun-implicit Name SParams UnifSI Out
 ].

structures.v

@@ -7,11 +7,13 @@ Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : option (string * Type)) :=
   phantom T1 t1 -> phantom T2 t2.
 Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition nomsg : option (string * Type) := None.
+Definition is_not_canonically_a : string := "is not canonically a".
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
 Register Coq.Init.Datatypes.None as hb.none.
 Register nomsg as hb.nomsg.
+Register is_not_canonically_a as hb.not_a_msg.
 Register Coq.Init.Datatypes.Some as hb.some.
 Register Coq.Init.Datatypes.pair as hb.pair.
 Register Coq.Init.Datatypes.prod as hb.prod.
@@ -508,6 +510,9 @@ Elpi Typecheck.
 Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None)
   (at level 0, format "`Error_cannot_unify:  t1  'with'  t2", only printing) :
   form_scope.
+  Notation "`Error: t `is_not_canonically_a T" := (unify t _ (Some (is_not_canonically_a, T)))
+  (at level 0, T at level 0, format "`Error:  t  `is_not_canonically_a  T", only printing) :
+  form_scope.
 Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T)))
   (at level 0, msg, T at level 0, format "`Error:  t  msg  T", only printing) :
   form_scope.